Refining the conditioning algebra of mutual conditional independence

A family of σ-algebras that is mutually conditionally independent given m' remains mutually conditionally independent given any larger algebra m₂ ≥ m' that is itself conditionally independent of the family's join given m'.

This is the "useless extra information" principle: enlarging the conditioning from m' to m₂ cannot destroy independence when everything m₂ adds is itself conditionally independent of the family.

The engine, kept private

The proof rests on a projection identity: if m₁ and m₂ are conditionally independent given m' ≤ m₂, then for every m₁-set E,

μ⟦E | m₂⟧ =ᵐ[μ] μ⟦E | m'⟧.

The candidate μ⟦E | m'⟧ is m'-strongly measurable, hence m₂-strongly measurable because the containment m' ≤ m₂ is raw; and its set integral over an m₂-set F is computed by the pull-out property of conditional expectation together with the product identity of conditional independence: both ∫ x in F, μ⟦E | m'⟧ x and ∫ x in F, 1_E x equal ∫ x, (μ⟦E | m'⟧ * μ⟦F | m'⟧) x. Uniqueness of the conditional expectation at m₂ finishes.

The identity is deliberately private: its natural generality — integrable functions rather than indicators, one-sided measurability hypotheses — is not yet pinned down by a second consumer, and the σ-algebra-level refinement theorem is the only interface currently consumed.

Contents

• ProbabilityTheory.iCondIndep_of_condIndep_iSup — the refinement theorem.

The StandardBorelSpace hypothesis is inherited from Mathlib's definition of CondIndep and iCondIndep through condExpKernel; the underlying argument does not use it.

theorem ProbabilityTheory.iCondIndep_of_condIndep_iSup {Ω : Type u_1} {m₂ m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_2} {m : ι → MeasurableSpace Ω} (hm' : m' ≤ mΩ) (hm₂ : m₂ ≤ mΩ) (hm'₂ : m' ≤ m₂) (hm : ∀ (i : ι), m i ≤ mΩ) (h : iCondIndep m' hm' m μ) (hci : CondIndep m' (⨆ (i : ι), m i) m₂ hm' μ) : iCondIndep m₂ hm₂ m μ

Refining the conditioning of mutual conditional independence. If the family m is mutually conditionally independent given m', and the larger algebra m₂ ≥ m' is conditionally independent of the join ⨆ i, m i given m', then the family is mutually conditionally independent given m₂.

The single hypothesis hci covers both uses of the projection identity — the accumulated finite intersection and each individual factor are all events of the join.