Integrability and σ-algebra Factorization for Conditional Expectation

This file provides integrability lemmas, uniqueness arguments, and σ-algebra factorization lemmas for conditional expectations.

Main results

• integrable_mul_of_bound_one: Product with bounded factor is integrable
• abs_condExp_le_condExp_abs: Jensen's inequality for conditional expectation
• condExp_indicator_ae_bound_one: CE of indicator is a.e. in [0,1]
• sigma_factor_le: Pullback σ-algebra inequality for factorizations

Integrability of products with bounded factors

theorem integrable_mul_of_bound_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f g : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) (hg_meas : MeasureTheory.AEStronglyMeasurable g μ) (hbound : ∀ᵐ (ω : Ω) ∂μ, ‖g ω‖ ≤ 1) : MeasureTheory.Integrable (fun (ω : Ω) => g ω * f ω) μ

If f ∈ L¹(μ) and g is a.e. bounded by 1, then g⋅f ∈ L¹(μ).

theorem abs_condExp_le_condExp_abs {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (hm : m ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] {f : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) : ∀ᵐ (ω : Ω) ∂μ, |μ[f|m] ω| ≤ μ[fun (ω : Ω) => |f ω| |m] ω

Jensen's inequality for conditional expectation: the absolute value of a conditional expectation is a.e. bounded by the conditional expectation of the absolute value.

For integrable f: |μ[f|m]| ≤ μ[|f||m] almost everywhere.

theorem condExp_indicator_ae_bound_one {Ω : Type u_1} {β : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mW : MeasurableSpace Ω} (hm : mW ≤ m0) {Z : Ω → β} [MeasurableSpace β] {B : Set β} (hZ : Measurable Z) (hB : MeasurableSet B) : ∀ᵐ (ω : Ω) ∂μ, 0 ≤ μ[fun (ω : Ω) => (Z ⁻¹' B).indicator (fun (x : Ω) => 1) ω|mW] ω ∧ μ[fun (ω : Ω) => (Z ⁻¹' B).indicator (fun (x : Ω) => 1) ω|mW] ω ≤ 1

The conditional expectation of an indicator (ℝ-valued) is a.e. in [0,1].

σ-algebra factorization

theorem sigma_factor_le {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {η : Ω → α} {ζ : Ω → β} {g : β → α} (hη : η = g ∘ ζ) (hg : Measurable g) : MeasurableSpace.comap η inferInstance ≤ MeasurableSpace.comap ζ inferInstance

Pullback σ-algebra inequality for factorizations.

If η = g ∘ ζ with g measurable, then the σ-algebra generated by η is contained in the σ-algebra generated by ζ.

This is the fundamental fact about σ-algebra factorization: knowing ζ gives you at least as much information as knowing η = g(ζ).

Mathematical statement: σ(η) ≤ σ(ζ) when η = g ∘ ζ.

Wrappers for dominated convergence and L¹ continuity

theorem MeasureTheory.tendsto_set_integral_of_L1 {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} {fn : ℕ → α → ℝ} {f : α → ℝ} (hf_int : Integrable f μ) (hfn_int : ∀ (n : ℕ), Integrable (fn n) μ) (hL1 : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (ω : α), ↑‖fn n ω - f ω‖₊ ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : α) in s, fn n ω ∂μ) Filter.atTop (nhds (∫ (ω : α) in s, f ω ∂μ))

Restricted dominated convergence: L¹ convergence implies set integral convergence.

If fn → f in L¹(μ), then ∫_s fn → ∫_s f for any measurable set s.

This requires integrability hypotheses to ensure the integrals are well-defined.

theorem MeasureTheory.tendsto_set_integral_mul_of_L1 {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} {fn : ℕ → α → ℝ} {f H : α → ℝ} {C : ℝ} (hf_int : Integrable f μ) (hfn_int : ∀ (n : ℕ), Integrable (fn n) μ) (hH_int : Integrable H μ) (hL1 : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (ω : α), ↑‖fn n ω - f ω‖₊ ∂μ) Filter.atTop (nhds 0)) (hC : 0 ≤ C) (hH_bdd : ∀ᵐ (ω : α) ∂μ, ‖H ω‖ ≤ C) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : α) in s, fn n ω * H ω ∂μ) Filter.atTop (nhds (∫ (ω : α) in s, f ω * H ω ∂μ))

L¹ convergence of product with bounded factor.

If fn → f in L¹ and H is bounded a.e., then ∫_s (fn * H) → ∫_s (f * H).