Integration Helper Lemmas

Convenience wrappers around mathlib's integration theory, providing specialized lemmas for common patterns in the de Finetti proofs.

Main Results

• abs_integral_mul_le_L2: Cauchy-Schwarz inequality for L² functions
• eLpNorm_one_eq_integral_abs: Connection between L¹ integral and eLpNorm
• L2_tendsto_implies_L1_tendsto_of_bounded: L² → L¹ convergence for bounded functions
• integral_pushforward_id: Integral of identity under pushforward measure
• integral_pushforward_sq_diff: Integral of squared difference under pushforward

These lemmas eliminate boilerplate by wrapping mathlib's general theorems.

Implementation Notes

The file has no project dependencies - imports only mathlib.

Cauchy-Schwarz Inequality

theorem Exchangeability.Probability.IntegrationHelpers.abs_integral_mul_le_L2 {Ω : Type u_1} {inst✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f g : Ω → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : |∫ (ω : Ω), f ω * g ω ∂μ| ≤ (∫ (ω : Ω), f ω ^ 2 ∂μ) ^ (1 / 2) * (∫ (ω : Ω), g ω ^ 2 ∂μ) ^ (1 / 2)

Cauchy-Schwarz inequality for L² real-valued functions.

For integrable functions f, g in L²(μ): |∫ f·g dμ| ≤ (∫ f² dμ)^(1/2) · (∫ g² dμ)^(1/2)

This is Hölder's inequality specialized to p = q = 2. We derive it from the nonnegative version by observing that |∫ f·g| ≤ ∫ |f|·|g| and |f|² = f².

Lp Norm Connections and Convergence

theorem Exchangeability.Probability.IntegrationHelpers.eLpNorm_one_eq_integral_abs {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.eLpNorm f 1 μ = ENNReal.ofReal (∫ (ω : Ω), |f ω| ∂μ)

Connection between L¹ Bochner integral and eLpNorm.

For integrable real-valued functions, the L¹ norm (eLpNorm with p=1) equals the ENNReal coercion of the integral of absolute value.

This bridges the gap between Real-valued integrals (∫ |f| ∂μ : ℝ) and ENNReal-valued Lp norms (eLpNorm f 1 μ : ℝ≥0∞), which is essential for applying mathlib's convergence in measure machinery.

theorem Exchangeability.Probability.IntegrationHelpers.L2_tendsto_implies_L1_tendsto_of_bounded {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (f : ℕ → Ω → ℝ) (g : Ω → ℝ) (hf_meas : ∀ (n : ℕ), Measurable (f n)) (hf_bdd : ∃ (M : ℝ), ∀ (n : ℕ) (ω : Ω), |f n ω| ≤ M) (hg_memLp : MeasureTheory.MemLp g 2 μ) (hL2 : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), (f n ω - g ω) ^ 2 ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |f n ω - g ω| ∂μ) Filter.atTop (nhds 0)

L² convergence implies L¹ convergence for uniformly bounded functions.

On a probability space, if fₙ → g in L² and the functions are uniformly bounded, then fₙ → g in L¹.

This follows from Cauchy-Schwarz: ∫|f - g| ≤ (∫(f-g)²)^(1/2) · (∫ 1)^(1/2) = (∫(f-g)²)^(1/2)

This lemma provides the key bridge between the Mean Ergodic Theorem (which gives L² convergence) and applications requiring L¹ convergence (such as ViaL2's Cesàro average convergence).

Pushforward Measure Integrals

theorem Exchangeability.Probability.IntegrationHelpers.integral_pushforward_id {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} (hf : Measurable f) : ∫ (x : ℝ), x ∂MeasureTheory.Measure.map f μ = ∫ (ω : Ω), f ω ∂μ

Integral of identity function under pushforward measure.

For measurable f: ∫ x, x d(f₊μ) = ∫ ω, f ω dμ

Eliminates boilerplate of proving AEStronglyMeasurable id.

theorem Exchangeability.Probability.IntegrationHelpers.integral_pushforward_sq_diff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} (hf : Measurable f) (c : ℝ) : ∫ (x : ℝ), (x - c) ^ 2 ∂MeasureTheory.Measure.map f μ = ∫ (ω : Ω), (f ω - c) ^ 2 ∂μ

Integral of squared difference under pushforward measure.

For measurable f and constant c: ∫ x, (x - c)² d(f₊μ) = ∫ ω, (f ω - c)² dμ

theorem Exchangeability.Probability.IntegrationHelpers.integral_pushforward_continuous {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} {g : ℝ → ℝ} (hf : Measurable f) (hg : Continuous g) : ∫ (x : ℝ), g x ∂MeasureTheory.Measure.map f μ = ∫ (ω : Ω), g (f ω) ∂μ

Integral of continuous function under pushforward.

For measurable f and continuous g: ∫ x, g x d(f₊μ) = ∫ ω, g (f ω) dμ