Conditional independence of visible array cells #
For a separately exchangeable array, all cells whose row and column are outside two infinite hidden index sets are conditionally independent given the crossing strips. This is the simultaneous form of the local finite-block independence theorem and supplies the cell-noise factorization in the Aldous--Hoover representation.
The statement uses Mathlib's conditional independence of an indexed family, so it controls every finite collection of distinct visible cells at once.
References #
- D. Aldous, "Representations for partially exchangeable arrays of random variables", Journal of Multivariate Analysis 11 (1981), 581--598.
- O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 7.
theorem
TauCeti.Probability.SeparatelyExchangeable.iCondIndepFun_visibleCells
{α : Type u_1}
[MeasurableSpace α]
[StandardBorelSpace α]
{ρ : MeasureTheory.Measure (ℕ × ℕ → α)}
[MeasureTheory.IsFiniteMeasure ρ]
(hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p)
{S T : Set ℕ}
(hS : S.Infinite)
(hT : T.Infinite)
:
have H := Set.univ ×ˢ T ∪ S ×ˢ Set.univ;
have V := Sᶜ ×ˢ Tᶜ;
ProbabilityTheory.iCondIndepFun (MeasurableSpace.comap H.domRestrict inferInstance) ⋯
(fun (p : ↑V) (x : ℕ × ℕ → α) => x ↑p) ρ
The visible cells are conditionally independent given all entries on the crossing hidden strips. In particular this controls any finite set of distinct visible cells, not only rectangular blocks.