Clip01: Clamping to [0,1]

This file defines clip01, which clamps real values to the interval [0,1], and proves basic properties used in L¹ convergence arguments.

Main definitions

• clip01 x: Clamps x to the interval [0,1] via max 0 (min 1 x)

Main results

• clip01_range: 0 ≤ clip01 x ≤ 1
• clip01_1Lipschitz: clip01 is 1-Lipschitz
• abs_clip01_sub_le: |clip01 x - clip01 y| ≤ |x - y|
• continuous_clip01: clip01 is continuous
• l1_convergence_under_clip01: L¹ convergence is preserved under clip01

def Exchangeability.DeFinetti.ViaL2.Helpers.clip01 (x : ℝ) : ℝ

Clip a real to the interval [0,1].

Equations

• Exchangeability.DeFinetti.ViaL2.Helpers.clip01 x = max 0 (min 1 x)

theorem Exchangeability.DeFinetti.ViaL2.Helpers.clip01_range (x : ℝ) : 0 ≤ clip01 x ∧ clip01 x ≤ 1

theorem Exchangeability.DeFinetti.ViaL2.Helpers.clip01_1Lipschitz : LipschitzWith 1 clip01

clip01 is 1-Lipschitz.

theorem Exchangeability.DeFinetti.ViaL2.Helpers.abs_clip01_sub_le (x y : ℝ) : |clip01 x - clip01 y| ≤ |x - y|

Pointwise contraction from the 1-Lipschitzness.

theorem Exchangeability.DeFinetti.ViaL2.Helpers.continuous_clip01 : Continuous clip01

clip01 is continuous.

theorem Exchangeability.DeFinetti.ViaL2.Helpers.l1_convergence_under_clip01 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {fn : ℕ → Ω → ℝ} {f : Ω → ℝ} (h_meas : ∀ (n : ℕ), AEMeasurable (fn n) μ) (hf : AEMeasurable f μ) (h_integrable : ∀ (n : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => fn n ω - f ω) μ) (h : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |fn n ω - f ω| ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |clip01 (fn n ω) - clip01 (f ω)| ∂μ) Filter.atTop (nhds 0)

L¹-stability under 1-Lipschitz post-composition. If ∫ |fₙ - f| → 0, then ∫ |clip01 ∘ fₙ - clip01 ∘ f| → 0.

This follows from mathlib's LipschitzWith.norm_compLp_sub_le: Since clip01 is 1-Lipschitz and maps 0 to 0, we have ‖clip01 ∘ f - clip01 ∘ g‖₁ ≤ 1 * ‖f - g‖₁.