Documentation

TauCeti.Probability.Exchangeability.Arrays.Strip.Independence

Conditional independence of crossing array strips #

For a separately exchangeable array, the row strips along T and the column strips along S are conditionally independent given their intersection S ×ˢ T whenever either index set is infinite. Thus the two families of strips used in the hidden/visible array decomposition are independent given the entire hidden block, not merely given a directing measure.

When S and T are both infinite, a finite visible rectangle outside those hidden axes is conditionally independent of every entry outside it given the union of the row and column strips. This is the block form of the conditional cell-noise factorization: after the crossing strips have been revealed, the rest of the array carries no further information about that visible block.

The same factorization holds for a jointly exchangeable array, with one infinite set S of hidden indices serving both axes: a finite visible square I ×ˢ I, diagonal included, is conditionally independent of every entry outside it given all entries in a hidden row or a hidden column.

References #

Main results #

source
theorem TauCeti.Probability.SeparatelyExchangeable.condIndepFun_rowStrip_colStrip {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (S : Set ℕ) {T : Set ℕ} (hST : S.Infinite ∨ T.Infinite) :
ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (S ×ˢ T).domRestrict inferInstance) ⋯ (Set.univ ×ˢ T).domRestrict (S ×ˢ Set.univ).domRestrict ρ

The row strips along T and the column strips along S are conditionally independent given the entire intersection block whenever at least one of S and T is infinite.

source
theorem TauCeti.Probability.SeparatelyExchangeable.condIndepFun_rowStrip_colStrip_of_enum {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e f : ℕ → ℕ} (hef : (Set.range e).Infinite ∨ (Set.range f).Infinite) (g g' : ℕ → ℕ) :
ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (fun (x : ℕ × ℕ → α) (q : ℕ × ℕ) => x (e q.1, f q.2)) inferInstance) ⋯ (fun (x : ℕ × ℕ → α) (i b : ℕ) => x (g i, f b)) (fun (x : ℕ × ℕ → α) (j a : ℕ) => x (e a, g' j)) ρ

Enumerated crossing strips are conditionally independent given the hidden block. Let e and f enumerate hidden rows and hidden columns, at least one of them with infinite range. Then the row strips (x (g i, f ·))ᵢ and the column strips (x (e ·, g' j))ⱼ are conditionally independent given the ℕ × ℕ-indexed hidden block (x (e a, f b))_{a,b}, for arbitrary g and g'. This is condIndepFun_rowStrip_colStrip for range e and range f, restated with ℕ-indexed strips and block.

source
theorem TauCeti.Probability.SeparatelyExchangeable.condIndepFun_visibleBlock_compl {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {S T I J : Set ℕ} (hS : S.Infinite) (hT : T.Infinite) (hI : I.Finite) (hJ : J.Finite) (hIS : Disjoint I S) (hJT : Disjoint J T) :
have C := I ×ˢ J; have H := Set.univ ×ˢ T ∪ S ×ˢ Set.univ; ProbabilityTheory.CondIndepFun (MeasurableSpace.comap H.domRestrict inferInstance) ⋯ C.domRestrict Cᶜ.domRestrict ρ

A finite visible rectangle is conditionally independent of its complement given the crossing hidden strips. Let S and T be infinite sets of hidden row and column indices, and let the finite sets I and J be disjoint from them. Once all entries in hidden rows or hidden columns are known, the block I ×ˢ J is conditionally independent of every entry outside that block.

The conditioning set is the full cross (univ ×ˢ T) ∪ (S ×ˢ univ), rather than only the finite part of the cross adjacent to I ×ˢ J. This form can therefore be iterated over disjoint visible blocks when constructing the cell-noise layer of an array representation.

source
theorem TauCeti.Probability.JointlyExchangeable.condIndepFun_visibleBlock_compl {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {S I : Set ℕ} (hS : S.Infinite) (hI : I.Finite) (hIS : Disjoint I S) :
have C := I ×ˢ I; have H := Set.univ ×ˢ S ∪ S ×ˢ Set.univ; ProbabilityTheory.CondIndepFun (MeasurableSpace.comap H.domRestrict inferInstance) ⋯ C.domRestrict Cᶜ.domRestrict ρ

A finite visible square of a jointly exchangeable array is conditionally independent of its complement given the crossing hidden strips. Let S be an infinite set of hidden indices and let the finite set I be disjoint from it. Once all entries in a hidden row or a hidden column are known, the block I ×ˢ I is conditionally independent of every entry outside that block.

This is the jointly exchangeable form of SeparatelyExchangeable.condIndepFun_visibleBlock_compl, with one set of hidden indices serving both axes. The block contains the diagonal entries (i, i) and both orientations (i, j) and (j, i) of each visible off-diagonal cell, which is the cell layer of the jointly exchangeable Aldous--Hoover representation.