Three closure properties of conditional independence

All three are glue Mathlib does not currently provide.

• Joining the conditioning algebra to one side is free: from m₁ ⊥⊥ m₂ ∣ m' conclude m₁ ⊥⊥ (m' ⊔ m₂) ∣ m'. Whatever the conditioning algebra already knows cannot carry new dependence. Proved through the π-system {e ∩ f | e ∈ m', f ∈ m₂} generating the join: on such a set the m'-measurable part pulls out of the conditional expectation as an indicator (condExp_indicator), and the base product identity finishes pointwise.

• CondIndepFun respects almost-everywhere equality of the functions — the conditional analogue of IndepFun.congr. Conditional independence of functions is characterized by conditional expectations of indicator preimages, and every term depends on the functions only through their a.e. pointwise values. This is what lets a variable that is only a.e. equal to a conditioning-measurable one be absorbed into a side of a conditional independence.

Neither statement mentions this repository's signatures. The [StandardBorelSpace Ω] hypotheses come with Mathlib's definition of CondIndep/CondIndepFun through condExpKernel.

• The conditioning σ-algebra may be replaced by an equal one (CondIndepFun.congr_cond): the dependent ≤ proof moves by proof irrelevance once the σ-algebra equality is substituted. Needed wherever a conditioning map is reindexed — the rank-one coupling and screening arguments and the pooled screening transport all consume it.

theorem ProbabilityTheory.CondIndep.sup_right {Ω : Type u_1} {m' m₁ m₂ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {hm' : m' ≤ mΩ} (h : CondIndep m' m₁ m₂ hm' μ) (h1 : m₁ ≤ mΩ) (h2 : m₂ ≤ mΩ) : CondIndep m' m₁ (m' ⊔ m₂) hm' μ

Joining the conditioning algebra to one side of a conditional independence is free: if m₁ ⊥⊥ m₂ ∣ m', then m₁ ⊥⊥ (m' ⊔ m₂) ∣ m'.

theorem ProbabilityTheory.CondIndepFun.congr {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {hm' : m' ≤ mΩ} {β : Type u_2} {β' : Type u_3} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f f' : Ω → β} {g g' : Ω → β'} (h : CondIndepFun m' hm' f g μ) (hfm : Measurable f) (hgm : Measurable g) (hfm' : Measurable f') (hgm' : Measurable g') (hff' : f =ᵐ[μ] f') (hgg' : g =ᵐ[μ] g') : CondIndepFun m' hm' f' g' μ

CondIndepFun respects a.e. equality of the functions — the conditional analogue of IndepFun.congr.

theorem ProbabilityTheory.CondIndepFun.congr_cond {Ω : Type u_2} {β : Type u_3} {γ : Type u_4} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ} {m₁ m₂ : MeasurableSpace Ω} {h1 : m₁ ≤ mΩ} (h : CondIndepFun m₁ h1 f g μ) (h12 : m₁ = m₂) (h2 : m₂ ≤ mΩ) : CondIndepFun m₂ h2 f g μ

The conditioning σ-algebra may be replaced by an equal one. The dependent ≤ proof is handled by proof irrelevance once the σ-algebra equality is substituted. Shared glue: the rank-one coupling and screening arguments both need it, and so does any transport of a conditional independence statement whose conditioning map has been reindexed.