Conditioning on σ-algebras that represent each other modulo the measure

If m₂ ≤ m₁ and every m₁-measurable set is almost everywhere equal to an m₂-measurable one, then conditioning on m₁ and on m₂ give the same answer:

μ[f | m₁] =ᵐ[μ] μ[f | m₂]

and consequently mutual conditional independence given m₁ is the same statement as mutual conditional independence given m₂.

This is the recurring situation in which a σ-algebra has a concrete realization — a factor map — that generates it only eventwise modulo the measure. The raw σ-algebras are then genuinely different objects, and no equality between them is available or claimed; what is available is this transfer of everything conditional expectation can see.

The proof does not lift the hypothesis to functions

The tempting route is to show that μ[f | m₁], being m₁-strongly measurable, is a.e. equal to an m₂-measurable function, and then conclude. That route is blocked: eventual measurability is strictly weaker than being a.e. equal to a measurable function — Mathlib's MeasureTheory.EventuallyMeasurable says so explicitly and leaves the equivalence as a TODO — so the lift would mean redoing simple-function approximation.

It is unnecessary. Run the uniqueness argument in the other direction: take μ[f | m₂] as the candidate for m₁. It is m₂-strongly measurable, hence m₁-strongly measurable because the containment m₂ ≤ m₁ is raw; and its set integrals over m₁-sets are computed by moving to an m₂ representative, where setIntegral_condExp applies. Uniqueness of the conditional expectation at m₁ then finishes. The hypothesis is used only on sets, which is the form it naturally arrives in.

Contents

• MeasureTheory.condExp_eq_condExp_of_ae_representable;
• ProbabilityTheory.iCondIndepFun_congr_of_ae_representable — the conditioning transfer;
• MeasureTheory.eventuallyMeasurableSet_sup — representability passes to a join: if every m₁-set has an m₂-representative modulo the filter, so does every m₁ ⊔ m₂-set. This is how the hypothesis hrep above is discharged for a conditioning algebra of the form m₁ ⊔ m₂ when only the m₁ half needs representing. The proof is sup_le into Mathlib's eventuallyMeasurableSpace, which is exactly the σ-algebra of representable sets.

theorem MeasureTheory.condExp_eq_condExp_of_ae_representable {α : Type u_1} {E : Type u_2} {m₁ m₂ m₀ : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [IsFiniteMeasure μ] (hm₂₁ : m₂ ≤ m₁) (hm₁ : m₁ ≤ m₀) (hrep : ∀ (s : Set α), MeasurableSet s → ∃ (t : Set α), MeasurableSet t ∧ s =ᵐ[μ] t) {f : α → E} (hf : Integrable f μ) : μ[f | m₁] =ᵐ[μ] μ[f | m₂]

Conditioning is insensitive to replacing a σ-algebra by one that represents it modulo the measure. No equality of σ-algebras is assumed or asserted: only that m₂ ≤ m₁ and that every m₁-set has an m₂-representative almost everywhere.

theorem MeasureTheory.eventuallyMeasurableSet_sup {α : Type u_1} {m₁ m₂ : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] (h : ∀ (s : Set α), MeasurableSet s → ∃ (t : Set α), MeasurableSet t ∧ s =ᶠ[l] t) {s : Set α} (hs : MeasurableSet s) : ∃ (t : Set α), MeasurableSet t ∧ s =ᶠ[l] t

Representability passes to a join. If every m₁-set has an m₂-representative modulo the σ-filter l, then so does every m₁ ⊔ m₂-set: the representable sets form the σ-algebra eventuallyMeasurableSpace m₂ l, which contains m₁ by hypothesis and m₂ outright.

theorem ProbabilityTheory.iCondIndepFun_congr_of_ae_representable {α : Type u_1} {m₁ m₂ : MeasurableSpace α} [m₀ : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (hm₂₁ : m₂ ≤ m₁) (hm₁ : m₁ ≤ m₀) (hrep : ∀ (s : Set α), MeasurableSet s → ∃ (t : Set α), MeasurableSet t ∧ s =ᵐ[μ] t) {ι : Type u_2} {β : ι → Type u_3} [mβ : (i : ι) → MeasurableSpace (β i)] {X : (i : ι) → α → β i} (hX : ∀ (i : ι), Measurable (X i)) : iCondIndepFun m₁ hm₁ X μ ↔ iCondIndepFun m₂ ⋯ X μ

Mutual conditional independence transfers between σ-algebras that represent each other modulo the measure. The conditioning factor may be replaced by any eventwise realization of it without changing the statement — which is what lets a concrete factor map stand in for an abstractly defined conditioning σ-algebra.

The standard Borel hypothesis is not needed for the underlying conditional-expectation statement MeasureTheory.condExp_eq_condExp_of_ae_representable, which is stated for an arbitrary finite measure. It appears here only because ProbabilityTheory.iCondIndepFun is itself defined through condExpKernel, which Mathlib provides only over a standard Borel space.