Generic conditional-expectation facts

• condExp_comp_ae_eq_of_pair_law_eq: if (Y, Z) and (Y', Z) have the same law, then for a measurable real observable f the conditional expectations of f ∘ Y and f ∘ Y' given σ(Z) agree a.e.
• condExp_ae_eq_of_forall_condExp_ae_eq_of_tendsto_eLpNorm: L¹-continuity of conditional expectation — if Xn → Xlim in L¹ (in eLpNorm) and each μ[Xn n | F] agrees a.e. with a fixed Y, then μ[Xlim | F] agrees a.e. with Y.
• condExp_ae_eq_integral_of_forall_zero_or_one: conditioning on a μ-trivial σ-algebra — one all of whose sets have measure 0 or 1 — is integrating: μ[f | m'] is a.e. the constant ∫ f ∂μ.
• ae_eq_condExp_of_forall_setIntegral_fiber_eq: conditional-expectation uniqueness can be checked on the fibers of a countable-valued observation.
• condExp_ae_eq_of_le_of_le: if conditioning on a σ-algebra agrees a.e. with conditioning on a coarser one, then so does conditioning on every σ-algebra between them.
• condExp_ae_eq_of_forall_exists_ae_eq: conditioning on two nested σ-algebras gives a.e. the same result when every set of the finer one agrees a.e. with a set of the coarser one.

All are generic conditional-expectation facts (no exchangeability/tail/directing-measure hypotheses), each the bridge for a downstream construction.

The first two are adapted from cameronfreer/exchangeability (Probability/CondExp.lean and Probability/Martingale/Convergence.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22); the third from Graphon/LevyDownward.lean in cameronfreer/graphon (Apache 2.0) at commit 175911f9d2e053f2a33d966658dfce0e4ae2811d.

theorem TauCeti.MeasureTheory.condExp_comp_ae_eq_of_pair_law_eq {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace α] [mβ : MeasurableSpace β] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (Y Y' : Ω → α) (Z : Ω → β) (hY : Measurable Y) (hY' : Measurable Y') (hZ : Measurable Z) (hpair : MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, Z ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Y' ω, Z ω)) μ) {f : α → ℝ} (hf : Measurable f) : μ[fun (ω : Ω) => f (Y ω) | MeasurableSpace.comap Z mβ] =ᵐ[μ] μ[fun (ω : Ω) => f (Y' ω) | MeasurableSpace.comap Z mβ]

If the pairs (Y, Z) and (Y', Z) have the same law, then for a measurable real observable f the conditional expectations of f ∘ Y and f ∘ Y' given σ(Z) agree almost everywhere.

Both conditional expectations are pinned down by their integrals over the sets Z ⁻¹' E, and each such integral is an integral of fun p => f p.1 over the slab univ ×ˢ E against the joint law, which is where the hypothesis applies. Equal laws make f ∘ Y integrable exactly when f ∘ Y' is, so no integrability hypothesis is needed: when it fails both sides are 0.

theorem TauCeti.MeasureTheory.condExp_ae_eq_of_forall_condExp_ae_eq_of_tendsto_eLpNorm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {F : MeasurableSpace Ω} {Xlim Y : Ω → ℝ} {Xn : ℕ → Ω → ℝ} (hXlimint : MeasureTheory.Integrable Xlim μ) (hXn_int : ∀ (n : ℕ), MeasureTheory.Integrable (Xn n) μ) (h_condExp : ∀ (n : ℕ), μ[Xn n | F] =ᵐ[μ] Y) (hL1 : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Xlim - Xn n) 1 μ) Filter.atTop (nhds 0)) : μ[Xlim | F] =ᵐ[μ] Y

L¹-continuity of conditional expectation. If Xn → Xlim in L¹ (in eLpNorm) and each μ[Xn n | F] agrees a.e. with a fixed Y, then μ[Xlim | F] agrees a.e. with Y.

theorem TauCeti.MeasureTheory.condExp_ae_eq_integral_of_forall_zero_or_one {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {m' : MeasurableSpace Ω} (hm' : m' ≤ m0) (htriv : ∀ (s : Set Ω), MeasurableSet s → μ s = 0 ∨ μ s = 1) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} (hf : MeasureTheory.Integrable f μ) : μ[f | m'] =ᵐ[μ] fun (x : Ω) => ∫ (x : Ω), f x ∂μ

Conditioning on a μ-trivial σ-algebra is integrating: if every m'-measurable set has measure 0 or 1, then μ[f | m'] is a.e. the constant ∫ f ∂μ.

theorem TauCeti.MeasureTheory.ae_eq_condExp_of_forall_setIntegral_fiber_eq {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [MeasurableSpace ι] [Countable ι] [MeasurableSingletonClass ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure Ω} {X : Ω → ι} (hX : Measurable X) [MeasureTheory.SigmaFinite (μ.trim ⋯)] {f g : Ω → E} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hfg : ∀ (i : ι), ∫ (x : Ω) in X ⁻¹' {i}, g x ∂μ = ∫ (x : Ω) in X ⁻¹' {i}, f x ∂μ) : g =ᵐ[μ] μ[f | MeasurableSpace.comap X inst✝]

To identify a conditional expectation given a countable-valued observation, it suffices to compare integrals on its fibers. The candidate must be integrable and measurable with respect to the observation's σ-algebra.

theorem TauCeti.MeasureTheory.condExp_ae_eq_of_le_of_le {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m₁ m₂ m₃ m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → E} (h₁₂ : m₁ ≤ m₂) (h₂₃ : m₂ ≤ m₃) (h₃ : m₃ ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim h₃)] [MeasureTheory.SigmaFinite (μ.trim ⋯)] (h : μ[f | m₃] =ᵐ[μ] μ[f | m₁]) : μ[f | m₂] =ᵐ[μ] μ[f | m₁]

Conditioning on an intermediate σ-algebra. If conditioning f on m₃ gives a.e. the same result as conditioning on the coarser m₁ ≤ m₃, then so does conditioning on any m₂ between them.

theorem TauCeti.MeasureTheory.condExp_ae_eq_of_forall_exists_ae_eq {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m₁ m₂ m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → E} (h₁₂ : m₁ ≤ m₂) (h₂ : m₂ ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim ⋯)] (h : ∀ (s : Set Ω), MeasurableSet s → ∃ (t : Set Ω), MeasurableSet t ∧ s =ᵐ[μ] t) : μ[f | m₂] =ᵐ[μ] μ[f | m₁]

Conditioning on σ-algebras that agree up to null sets. If m₁ ≤ m₂ and every m₂-measurable set agrees μ-almost everywhere with an m₁-measurable set, then conditioning on m₂ gives a.e. the same result as conditioning on m₁: σ-algebras that differ only by μ-null sets cannot be told apart by conditional expectations.