Conditional independence and the indicator conditional-expectation projection

The two directions relating Mathlib's ProbabilityTheory.CondIndep to the "drop-information" identity μ[𝟙_H | mF ⊔ mG] =ᵐ μ[𝟙_H | mG] on conditional expectations of indicators, together with the generic contraction-independence identity that feeds them:

• condIndep_of_indicator_condExp_eq — builds CondIndep mG mF mH from that criterion (for all mH-measurable H).
• condExp_indicator_sup_eq_of_condIndep — the converse projection: from CondIndep mG mF mH, conditioning an mH-measurable indicator on the join mF ⊔ mG collapses to conditioning on mG.
• condIndep_of_condIndep_of_le_of_le — weak union: conditional independence persists when the conditioning σ-algebra is enlarged by information from one side.
• condExp_indicator_eq_of_law_eq_of_comap_le — Kallenberg's contraction-independence identity (Lemma 1.3): if the pair laws agree, (X, W) =ᵈ (X, W'), and σ(W) ≤ σ(W'), then conditioning the indicator of X ⁻¹' A on the finer σ(W') equals conditioning on the coarser σ(W). Its pair-law/L² machinery is generic conditional-expectation infrastructure, kept private here.
• iCondIndep_of_condIndep_compl — a family is conditionally independent if each member is conditionally independent of all the others together. It turns local deletion arguments into simultaneous conditional independence.

The first four results feed the de Finetti block-product factorisation / prefix-deletion drop-info step — the standard conditional-independence characterisation of the de Finetti route; see Kallenberg, Probabilistic Symmetries and Invariance Principles (Springer, 2005). Adapted from cameronfreer/exchangeability (Probability/CondExp.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22).

The complement criterion turns one-cell deletion arguments into conditional independence of all visible array cells given the crossing strips.

For a random path x : ι → α over a countable index type, two further results specialize these criteria to the coordinate restrictions s.domRestrict x:

• condIndepFun_domRestrict_of_subset — weak union for coordinate restrictions: conditioning on more coordinates from the second side preserves conditional independence.
• condIndepFun_domRestrict_of_reindexing — if a law-preserving reindexing of the coordinates fixes those in C and reads the coordinates in D off those in R ⊆ D, then the coordinates in C are conditionally independent of those in D given those in R; condIndepFun_domRestrict_of_finite_reindexing extends this to an infinite set of coordinates from its finite subsets. These are the local conditional-independence principles behind the Aldous--Hoover representation of exchangeable arrays, where the reindexings come from the symmetry of the array law.

theorem TauCeti.Probability.condIndep_of_indicator_condExp_eq {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mF mG mH : MeasurableSpace Ω} (hmF : mF ≤ mΩ) (hmG : mG ≤ mΩ) (hmH : mH ≤ mΩ) (h : ∀ (H : Set Ω), MeasurableSet H → μ[H.indicator fun (x : Ω) => 1 | mF ⊔ mG] =ᵐ[μ] μ[H.indicator fun (x : Ω) => 1 | mG]) : ProbabilityTheory.CondIndep mG mF mH hmG μ

Conditional independence from the drop-information criterion. If conditioning 𝟙_H on mF ⊔ mG is a.e. the same as conditioning on mG (for every mH-measurable H), then mF and mH are conditionally independent given mG.

theorem TauCeti.Probability.condExp_indicator_sup_eq_of_condIndep {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mF mG mH : MeasurableSpace Ω} (hmF : mF ≤ mΩ) (hmG : mG ≤ mΩ) (hmH : mH ≤ mΩ) (hCI : ProbabilityTheory.CondIndep mG mF mH hmG μ) {H : Set Ω} (hH : MeasurableSet H) : μ[H.indicator fun (x : Ω) => 1 | mF ⊔ mG] =ᵐ[μ] μ[H.indicator fun (x : Ω) => 1 | mG]

Projection from conditional independence. If mF and mH are conditionally independent given mG (in the sense of Mathlib's ProbabilityTheory.CondIndep), then conditioning the indicator of an mH-measurable set H on the join mF ⊔ mG collapses to conditioning on mG. This is the converse of condIndep_of_indicator_condExp_eq.

theorem TauCeti.Probability.condIndep_of_condIndep_of_le_of_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mF mG mG' mH : MeasurableSpace Ω} (hmF : mF ≤ mΩ) (hmG : mG ≤ mΩ) (hmH : mH ≤ mΩ) (h : ProbabilityTheory.CondIndep mG mF mH hmG μ) (hGG' : mG ≤ mG') (hG'H : mG' ≤ mH) : ProbabilityTheory.CondIndep mG' mF mH ⋯ μ

Conditional independence persists when the conditioning information is enlarged inside one side. If mF and mH are conditionally independent given mG, and mG ≤ mG' ≤ mH, then they are conditionally independent given mG'.

This is the weak-union property of conditional independence, in the nested form most useful for random fields: one may reveal additional information from the mH side without creating a dependence on mF.

Kallenberg Lemma 1.3 (contraction-independence)

The pair-law/L² machinery below is generic conditional-expectation infrastructure: its hypotheses mention only measurable maps, equality of pair laws, and the σ-algebra ordering σ(W) ≤ σ(W') — never contractability. The support lemmas stay private; the contraction-independence conclusion is public so the de Finetti prefix-deletion file can reuse it across the module boundary.

theorem TauCeti.Probability.condExp_indicator_eq_of_law_eq_of_comap_le {Ω : Type u_1} {α : Type u_2} {γ : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace γ] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (X : Ω → α) (W W' : Ω → γ) (hX : Measurable X) (hW : Measurable W) (hW' : Measurable W') (h_law : MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W' ω)) μ) (h_le : MeasurableSpace.comap W inferInstance ≤ MeasurableSpace.comap W' inferInstance) {A : Set α} (hA : MeasurableSet A) : μ[(X ⁻¹' A).indicator fun (x : Ω) => 1 | MeasurableSpace.comap W' inferInstance] =ᵐ[μ] μ[(X ⁻¹' A).indicator fun (x : Ω) => 1 | MeasurableSpace.comap W inferInstance]

Kallenberg Lemma 1.3 (contraction-independence). If (X, W) =ᵈ (X, W') and σ(W) ≤ σ(W') (so W is a contraction of W'), then conditioning the indicator of X on the finer σ(W') equals conditioning on the coarser σ(W), almost everywhere.

theorem TauCeti.Probability.iCondIndep_of_condIndep_compl {Ω : Type u_4} {ι : Type u_5} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m' : MeasurableSpace Ω} (hm' : m' ≤ mΩ) {m : ι → MeasurableSpace Ω} (hm : ∀ (i : ι), m i ≤ mΩ) (h : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) (⨆ (j : { j : ι // j ≠ i }), m ↑j) hm' μ) : ProbabilityTheory.iCondIndep m' hm' m μ

A family is conditionally independent when each member is conditionally independent of all the others together, given the same conditioning sigma-algebra. This criterion applies when local independence is proved by removing one coordinate from a process.

Conditional independence of coordinate restrictions

theorem TauCeti.Probability.condIndepFun_domRestrict_of_subset {ι : Type u_1} {α : Type u_2} [Countable ι] [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ι → α)} [MeasureTheory.IsFiniteMeasure ρ] {β : Type u_3} [MeasurableSpace β] {f : (ι → α) → β} (hf : Measurable f) {R H D : Set ι} (h : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap R.domRestrict inferInstance) ⋯ f D.domRestrict ρ) (hRH : R ⊆ H) (hHD : H ⊆ D) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap H.domRestrict inferInstance) ⋯ f D.domRestrict ρ

Weak union for coordinate restrictions. If f is conditionally independent of the coordinates in D given those in R, then it stays so given the coordinates in any H with R ⊆ H ⊆ D.

theorem TauCeti.Probability.condIndepFun_domRestrict_of_reindexing {ι : Type u_1} {α : Type u_2} [Countable ι] [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ι → α)} [MeasureTheory.IsFiniteMeasure ρ] {C R D : Set ι} (hRD : R ⊆ D) (r : ι → ι) (hr : MeasureTheory.Measure.map (fun (x : ι → α) (i : ι) => x (r i)) ρ = ρ) (hfix : ∀ i ∈ C, r i = i) (hinto : Set.MapsTo r D R) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap R.domRestrict inferInstance) ⋯ C.domRestrict D.domRestrict ρ

Conditional independence from a law-preserving reindexing. Let r reindex the coordinates of a random path x : ι → α without changing its law. If r fixes every coordinate in C and maps the coordinates in D into R ⊆ D, then the coordinates in C are conditionally independent of those in D given those in R.

theorem TauCeti.Probability.condIndepFun_domRestrict_of_finite_reindexing {ι : Type u_1} {α : Type u_2} [Countable ι] [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ι → α)} [MeasureTheory.IsFiniteMeasure ρ] {R D U : Set ι} (hRD : R ⊆ D) (hreindex : ∀ (C : Set ι), C.Finite → C ⊆ U → ∃ (r : ι → ι), MeasureTheory.Measure.map (fun (x : ι → α) (i : ι) => x (r i)) ρ = ρ ∧ (∀ i ∈ C, r i = i) ∧ Set.MapsTo r D R) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap R.domRestrict inferInstance) ⋯ U.domRestrict D.domRestrict ρ

Conditional independence from law-preserving reindexings of finite coordinate sets. The coordinates in U are conditionally independent of those in D given those in R ⊆ D as soon as every finite subset of U is fixed by some law-preserving reindexing that maps D into R. The reindexing may depend on the finite subset.