Basic Helper Lemmas for Conditional Expectation

This file provides basic helper lemmas for working with conditional expectations, σ-finiteness, and indicator functions.

These are foundational utilities extracted from the main CondExp.lean file to improve compilation speed.

Main components

σ-Finiteness

• sigmaFinite_trim_of_le: Trimmed measure inherits σ-finiteness from finite measures

Indicators

• indicator_iUnion_tsum_of_pairwise_disjoint: Union of disjoint indicators equals their sum

Helper lemmas for σ-finiteness and indicators

Note: Some lemmas in this section explicitly include {m m₀ : MeasurableSpace Ω} as parameters to work with multiple measurable space structures (e.g., for trimmed measures). This makes the section variable [MeasurableSpace Ω] unused for those lemmas, requiring set_option linter.unusedSectionVars false.

theorem Exchangeability.Probability.sigmaFinite_trim_of_le {Ω : Type u_1} [MeasurableSpace Ω] {m m₀ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ m₀) : MeasureTheory.SigmaFinite (μ.trim hm)

If μ is finite, then any trim of μ is σ-finite.

theorem Exchangeability.Probability.indicator_iUnion_tsum_of_pairwise_disjoint {Ω : Type u_1} [MeasurableSpace Ω] (f : ℕ → Set Ω) (hdisj : Pairwise (Function.onFun Disjoint f)) : (fun (ω : Ω) => (⋃ (i : ℕ), f i).indicator (fun (x : Ω) => 1) ω) = fun (ω : Ω) => ∑' (i : ℕ), (f i).indicator (fun (x : Ω) => 1) ω

For pairwise disjoint sets, the indicator of the union equals the pointwise tsum of indicators (for ℝ-valued constants).

theorem Exchangeability.Probability.indicator_tsum_le_one_of_pairwise_disjoint {Ω : Type u_1} [MeasurableSpace Ω] (f : ℕ → Set Ω) (hdisj : Pairwise (Function.onFun Disjoint f)) (x : Ω) : ∑' (i : ℕ), (f i).indicator (fun (x : Ω) => 1) x ≤ 1

For pairwise disjoint sets, the tsum of indicators is bounded by 1 at each point. This follows from the fact that at most one indicator is 1 at any point.

theorem Exchangeability.Probability.measure_tsum_eq_measure_iUnion {α : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : ℕ → Set α) (hf_meas : ∀ (i : ℕ), MeasurableSet (f i)) (hdisj : Pairwise (Function.onFun Disjoint f)) : ∑' (i : ℕ), μ (f i) = μ (⋃ (i : ℕ), f i)

For pairwise disjoint measurable sets, the tsum of measures equals the measure of the union.

theorem Exchangeability.Probability.measure_tsum_le_one_of_pairwise_disjoint {α : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (f : ℕ → Set α) (hf_meas : ∀ (i : ℕ), MeasurableSet (f i)) (hdisj : Pairwise (Function.onFun Disjoint f)) : ∑' (i : ℕ), μ (f i) ≤ 1

For pairwise disjoint measurable sets under a probability measure, the tsum of measures is at most 1.