Approximation Infrastructure for Bounded Measurable Extension

This file provides the L¹ convergence lemmas and simple function approximation infrastructure needed for extending conditional independence results from simple functions to bounded measurable functions.

Main results

• tendsto_condexp_L1 - L¹ convergence of conditional expectations (continuity)
• approx_bounded_measurable - Approximate bounded measurable by simple functions

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Section 6.1

Helper lemmas for bounded measurable extension

theorem tendsto_condexp_L1 {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (_hm : m ≤ mΩ) {fn : ℕ → Ω → ℝ} {f : Ω → ℝ} (h_int : ∀ (n : ℕ), MeasureTheory.Integrable (fn n) μ) (hf : MeasureTheory.Integrable f μ) (hL1 : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |fn n ω - f ω| ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |μ[fn n|m] ω - μ[f|m] ω| ∂μ) Filter.atTop (nhds 0)

CE is continuous from L¹ to L¹ (wrapper around mathlib's lemma).

Note: This lemma uses pointwise/product topology on Ω → ℝ for the output convergence. For proper L¹ convergence of conditional expectations, the mathlib approach is to use condExpL1CLM (conditional expectation as a continuous linear map on L¹ spaces).

The proof strategy is:

1. L¹ contraction: condExp is an L¹ contraction, i.e., eLpNorm (μ[g|m]) 1 μ ≤ eLpNorm g 1 μ
   • In mathlib: eLpNorm_one_condExp_le_eLpNorm (in Real.lean)
2. Linearity: μ[fn n - f | m] =ᵐ[μ] μ[fn n | m] - μ[f | m] (by condExp_sub)
3. Apply contraction: eLpNorm (μ[fn n | m] - μ[f | m]) 1 μ ≤ eLpNorm (fn n - f) 1 μ → 0
4. Convert norms: The hypothesis uses lintegral of nnnorm, which equals eLpNorm with exponent 1

The conclusion as stated uses pointwise topology, but the natural convergence mode is L¹. For applications, L¹ convergence of condExp is typically what's needed.

theorem approx_bounded_measurable {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {f : α → ℝ} (M : ℝ) (hf_meas : Measurable f) (hf_bdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ M) : ∃ (fn : ℕ → MeasureTheory.SimpleFunc α ℝ), (∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, |(fn n) x| ≤ M) ∧ (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => (fn n) x) Filter.atTop (nhds (f x))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), ↑‖(fn n) x - f x‖₊ ∂μ) Filter.atTop (nhds 0)

Helper: approximate bounded measurable function by simple functions.

Eapprox-based approximation for real-valued functions

The following lemma provides a simple function approximation sequence for measurable functions f : α → ℝ via the eapprox construction on positive/negative parts.

This is used in the conditional independence extension proofs where we need:

1. Pointwise bound: |sf n x| ≤ |f x| (not just ae, but everywhere)
2. Pointwise convergence: sf n x → f x for all x

Unlike approx_bounded_measurable which uses StronglyMeasurable.approxBounded, this construction works via the ENNReal eapprox machinery and provides deterministic (not almost-everywhere) bounds.

theorem eapprox_real_approx {α : Type u_5} [MeasurableSpace α] (f : α → ℝ) (hf : Measurable f) : ∃ (sf : ℕ → MeasureTheory.SimpleFunc α ℝ), (∀ (n : ℕ) (x : α), |(sf n) x| ≤ |f x|) ∧ ∀ (x : α), Filter.Tendsto (fun (n : ℕ) => (sf n) x) Filter.atTop (nhds (f x))

Eapprox-based simple function approximation for real-valued functions.

Given a measurable f : α → ℝ, this constructs a sequence of simple functions that approximate f pointwise with the key property that |sf n x| ≤ |f x| holds everywhere (not just almost everywhere).

The construction uses SimpleFunc.eapprox on the positive and negative parts:

• Split f = f⁺ - f⁻ where f⁺ = max(f, 0), f⁻ = max(-f, 0)
• Apply eapprox to ofReal ∘ f⁺ and ofReal ∘ f⁻
• Convert back to ℝ via toReal
• Take the difference

Key properties:

1. |sf n x| ≤ |f x| for all n, x (deterministic bound)
2. sf n x → f x as n → ∞ for all x (pointwise convergence)

L¹ convergence helper lemmas

These lemmas capture common patterns in the bounded measurable extension proofs:

1. Product L¹ convergence: bounded × L¹-convergent → L¹-convergent
2. Set integral convergence: L¹ convergence implies set integral convergence

theorem tendsto_integral_mul_of_bounded_L1 {Ω : Type u_5} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} {gn : ℕ → Ω → ℝ} {g : Ω → ℝ} (M : ℝ) (_hM_nn : 0 ≤ M) (hf_asm : MeasureTheory.AEStronglyMeasurable f μ) (hf_bdd : ∀ᵐ (ω : Ω) ∂μ, |f ω| ≤ M) (hgn_int : ∀ (n : ℕ), MeasureTheory.Integrable (gn n) μ) (hg_int : MeasureTheory.Integrable g μ) (hL1 : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |gn n ω - g ω| ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |f ω * (gn n ω - g ω)| ∂μ) Filter.atTop (nhds 0)

Product L¹ convergence: bounded factor × L¹-convergent → L¹-convergent.

If f is bounded a.e. by M and ∫|gn - g| → 0, then ∫|f * (gn - g)| → 0. This pattern appears repeatedly in monotone class arguments.

theorem tendsto_setIntegral_of_L1 {Ω : Type u_5} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {fn : ℕ → Ω → ℝ} {f : Ω → ℝ} (hfn_int : ∀ (n : ℕ), MeasureTheory.Integrable (fn n) μ) (hf_int : MeasureTheory.Integrable f μ) (hL1 : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |fn n ω - f ω| ∂μ) Filter.atTop (nhds 0)) (C : Set Ω) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω) in C, fn n ω ∂μ) Filter.atTop (nhds (∫ (ω : Ω) in C, f ω ∂μ))

Set integral convergence from L¹ convergence.

If ∫|fn - f| → 0 and both fn, f are integrable, then for any measurable set C, ∫_C fn → ∫_C f.

theorem tendsto_L1_of_pointwise_dominated {Ω : Type u_5} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {fn : ℕ → Ω → ℝ} {f : Ω → ℝ} (M : ℝ) (_hM_nn : 0 ≤ M) (hfn_int : ∀ (n : ℕ), MeasureTheory.Integrable (fn n) μ) (hf_int : MeasureTheory.Integrable f μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (ω : Ω) ∂μ, |fn n ω - f ω| ≤ 2 * M) (h_tendsto : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => fn n ω) Filter.atTop (nhds (f ω))) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |fn n ω - f ω| ∂μ) Filter.atTop (nhds 0)

L¹ convergence from pointwise dominated convergence.

If fn → f pointwise ae, |fn - f| ≤ 2M ae, and M is finite, then ∫|fn - f| → 0. This wraps tendsto_integral_of_dominated_convergence for the common L¹ case.

theorem integrable_condExp_mul_of_bounded {Ω : Type u_5} {m m₀ : MeasurableSpace Ω} (_hm : m ≤ m₀) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f g : Ω → ℝ} (M : ℝ) (hM_nn : 0 ≤ M) (hf_bdd : ∀ᵐ (ω : Ω) ∂μ, |f ω| ≤ M) (_hg_int : MeasureTheory.Integrable g μ) : MeasureTheory.Integrable (μ[f|m] * μ[g|m]) μ

Integrability of conditional expectation product with bounded factor.

If f is bounded ae by M, then μ[f|m] * μ[g|m] is integrable for any integrable g.

theorem tendsto_condExp_L1_of_dominated {Ω : Type u_5} {m m₀ : MeasurableSpace Ω} (hm : m ≤ m₀) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {fn : ℕ → Ω → ℝ} {f : Ω → ℝ} (M : ℝ) (hM_nn : 0 ≤ M) (hfn_asm : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fn n) μ) (hfn_bdd : ∀ (n : ℕ), ∀ᵐ (ω : Ω) ∂μ, |fn n ω| ≤ M) (hf_bdd : ∀ᵐ (ω : Ω) ∂μ, |f ω| ≤ M) (h_tendsto : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => fn n ω) Filter.atTop (nhds (f ω))) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |μ[fn n|m] ω - μ[f|m] ω| ∂μ) Filter.atTop (nhds 0)

L¹ convergence of conditional expectations from dominated convergence.

If fn → f pointwise ae, uniformly bounded by M, then ∫|μ[fn|m] - μ[f|m]| → 0.