Local conditional independence of finite array blocks

For a separately exchangeable array, any finite block of entries inside an infinite rectangle is conditionally independent of the entries outside the block given the other entries of the rectangle. This is the finite-block form of the local conditional-independence principle used to factor the visible-cell laws in the Aldous--Hoover representation.

The block whose law is controlled may be a sub-block of the hidden block: if C is a finite set of cells in the rectangle and B ⊆ C, then B is conditionally independent of the complement of the hidden block C given the reservoir, the rectangle with C removed. Nothing forces B to be all of C, and C need not be minimal, so the reservoir -- the rest of the rectangle -- may be chosen coarsely as long as it still avoids B.

A jointly exchangeable array is only invariant under relabelling both axes at once, so for it the infinite rectangle becomes an infinite square S ×ˢ S. The finite block may then contain diagonal entries and both orientations (i, j) and (j, i) of an off-diagonal cell, as the cell noise of the jointly exchangeable Aldous--Hoover representation requires.

Both statements come from the reindexing criterion condIndepFun_domRestrict_of_reindexing: a self-injection of the index set fixing the block moves everything outside it into the reservoir, without changing the array law (SeparatelyExchangeable.map_arrayBlock_eq, JointlyExchangeable.map_arrayBlock_diag_eq).

Main results

• SeparatelyExchangeable.condIndepFun_domRestrict_subblock_compl_of_finite_block_of_subset — local conditional independence inside an infinite rectangle;
• JointlyExchangeable.condIndepFun_domRestrict_subblock_compl_of_finite_block_of_subset — local conditional independence inside an infinite square, for jointly exchangeable arrays.

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.condIndepFun_domRestrict_of_finite_reindexing {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (R D U : Set (ℕ × ℕ)) (hRD : R ⊆ D) (hreindex : ∀ (C : Set (ℕ × ℕ)), C.Finite → C ⊆ U → ∃ (a : ℕ → ℕ) (b : ℕ → ℕ), Function.Injective a ∧ Function.Injective b ∧ (∀ p ∈ C, (a p.1, b p.2) = p) ∧ ∀ p ∈ D, (a p.1, b p.2) ∈ R) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap R.domRestrict inferInstance) ⋯ U.domRestrict D.domRestrict ρ

Conditional independence of all entries in U follows when every finite subset can be fixed by a reindexing of the two axes that moves D into the intermediate conditioning set R.

theorem TauCeti.Probability.SeparatelyExchangeable.condIndepFun_domRestrict_subblock_compl_of_finite_block_of_subset {α : 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) {B C : Set (ℕ × ℕ)} (hC : C.Finite) (hBsub : B ⊆ C) (hCsub : C ⊆ S ×ˢ T) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (S ×ˢ T \ C).domRestrict inferInstance) ⋯ B.domRestrict Cᶜ.domRestrict ρ

A finite block of array entries in an infinite rectangle is conditionally independent of everything outside a finite block containing it, given the rest of the rectangle.

The entries that are read off are the sub-block B ⊆ C, while the conditioning set is the rectangle with the whole hidden block C removed, and the events compared are those of the complement of C. Taking B = C recovers the statement that one finite block is conditionally independent of the rest of the array given the other entries of the rectangle; taking B to be a proper sub-block of C says the same for a part of the hidden block, with a reservoir that is allowed to hide more of the hidden block than that part needs.

C is the only set that has to be finite: B needs no finiteness hypothesis of its own, since B ⊆ C.

theorem TauCeti.Probability.JointlyExchangeable.condIndepFun_domRestrict_subblock_compl_of_finite_block_of_subset {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {S : Set ℕ} (hS : S.Infinite) {B C : Set (ℕ × ℕ)} (hC : C.Finite) (hBsub : B ⊆ C) (hCsub : C ⊆ S ×ˢ S) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (S ×ˢ S \ C).domRestrict inferInstance) ⋯ B.domRestrict Cᶜ.domRestrict ρ

A finite block of entries of a jointly exchangeable array inside an infinite square is conditionally independent of everything outside a finite block containing it, given the rest of the square.

This is the jointly exchangeable form of SeparatelyExchangeable.condIndepFun_domRestrict_subblock_compl_of_finite_block_of_subset: the rectangle S ×ˢ T becomes the square S ×ˢ S, since only a simultaneous relabelling of both axes preserves the array law. The blocks may contain diagonal entries, and both orientations of an off-diagonal cell.