Conditional Expectation and Lp Helper Lemmas

This file contains utility lemmas for conditional expectation and Lp norm manipulation.

Main Definitions

None - this file only contains helper lemmas.

Main Results

• condExp_const_mul: Scalar linearity of conditional expectation
• condExp_sum_finset: Finite sum linearity of conditional expectation
• integrable_of_bounded_measurable: Bounded measurable functions are integrable on finite measure spaces
• eLpNorm_one_le_eLpNorm_two_toReal: L¹ norm bounded by L² norm on probability spaces
• ennreal_tendsto_toReal_zero: ENNReal convergence to zero implies Real convergence

Lp norm placeholder

Lp seminorm: use mathlib's eLpNorm

Conditional expectation linearity helpers

theorem condExp_const_mul {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace Ω} (_hm : m ≤ mΩ) (c : ℝ) (f : Ω → ℝ) : μ[fun (ω : Ω) => c * f ω|m] =ᵐ[μ] fun (ω : Ω) => c * μ[f|m] ω

Scalar linearity of conditional expectation. Mathematical content: CE[c·f| mSI] = c·CE[f| mSI] Mathlib source: MeasureTheory.condexp_smul for scalar multiplication.

theorem condExp_sum_finset {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace Ω} (_hm : m ≤ mΩ) {ι : Type u_2} (s : Finset ι) (f : ι → Ω → ℝ) (hint : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ) : μ[fun (ω : Ω) => ∑ i ∈ s, f i ω|m] =ᵐ[μ] fun (ω : Ω) => ∑ i ∈ s, μ[f i|m] ω

Finite sum linearity of conditional expectation. Mathematical content: CE[Σᵢfᵢ| mSI] = ΣᵢCE[fᵢ| mSI] Mathlib source: Direct application of MeasureTheory.condExp_finset_sum. NOTE: Uses η-expansion to work around notation elaboration issues with ∑ i ∈ s, f i vs fun ω => ∑ i ∈ s, f i ω.

theorem integrable_of_bounded_measurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ℝ} (hf_meas : Measurable f) (C : ℝ) (hf_bd : ∀ (ω : Ω), |f ω| ≤ C) : MeasureTheory.Integrable f μ

On a finite measure space, a bounded measurable real function is integrable.

theorem eLpNorm_one_le_eLpNorm_two_toReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (f : Ω → ℝ) (hL1 : MeasureTheory.Integrable f μ) (hL2 : MeasureTheory.MemLp f 2 μ) : ∫ (ω : Ω), |f ω| ∂μ ≤ (MeasureTheory.eLpNorm f 2 μ).toReal

On a probability space, ‖f‖₁ ≤ ‖f‖₂. Version with real integral on the left. We assume MemLp f 2 μ so the right-hand side is finite; this matches all uses below where the function is bounded (hence in L²).

Proof strategy (from user's specification):

• Use snorm_mono_exponent or memℒp_one_of_memℒp_two to get MemLp f 1 μ from MemLp f 2 μ
• Show both eLpNorm f 1 μ and eLpNorm f 2 μ are finite
• Apply exponent monotonicity: eLpNorm f 1 μ ≤ eLpNorm f 2 μ on probability spaces
• Convert ∫|f| to (eLpNorm f 1 μ).toReal and apply ENNReal.toReal_le_toReal

theorem ennreal_tendsto_toReal_zero {ι : Type u_1} (f : ι → ENNReal) {a : Filter ι} (hf : Filter.Tendsto f a (nhds 0)) : Filter.Tendsto (fun (x : ι) => (f x).toReal) a (nhds 0)

If f → 0 in ENNReal, then (toReal ∘ f) → 0 in ℝ.