One cell kernel codes every visible cell of an exchangeable array

Split the rows and the columns of a separately exchangeable array into the hidden indices enumerated by e and f and their visible complements. The crossing strips are all array positions lying in a hidden row or in a hidden column; a visible cell (i, j) meets them in its own cellContext e f i j, the hidden block together with the hidden part of row i and the hidden part of column j.

Given that context, the cell is conditionally independent of all the remaining crossing strips: the strips of the other visible rows and columns say nothing more about it. Together with the conditional independence of distinct visible cells and with the common conditional cell kernel, this turns the cell layer into a genuine coding: a single measurable function of a context and a uniform variable generates every visible cell at once, each from its own context and its own fresh uniform variable, jointly with the crossing strips. That is the strengthening a representation needs over a family of codings chosen separately at each position, which is all that conditional independence given the strips gives by itself.

This is the cell noise of the Aldous–Hoover representation of a separately exchangeable array, with the position-independent coding function the representation asks for; the global noise and the row and column noises are supplied by the block and vertex strip codings.

Main results

• TauCeti.Probability.SeparatelyExchangeable.condIndepFun_cell_crossingStrips — a visible cell is conditionally independent of the crossing strips given its own context.
• TauCeti.Probability.SeparatelyExchangeable.exists_common_visibleCells_coding — one common coding function generates every finite family of visible cells from their contexts and independent uniform variables.
• TauCeti.Probability.SeparatelyExchangeable.exists_common_visibleArray_coding — the same coding function generates all the visible cells at once, from i.i.d. uniform variables indexed by the visible positions.

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_cell_crossingStrips {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e f : ℕ → ℕ} (he : (Set.range e).Infinite) (hf : (Set.range f).Infinite) {i j : ℕ} (hi : i ∉ Set.range e) (hj : j ∉ Set.range f) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (cellContext e f i j) inferInstance) ⋯ (fun (x : ℕ × ℕ → α) => x (i, j)) (Set.univ ×ˢ Set.range f ∪ Set.range e ×ˢ Set.univ).domRestrict ρ

A visible cell sees the crossing strips only through its own context. Let e and f enumerate infinitely many hidden rows and hidden columns of a separately exchangeable array, and let (i, j) be a cell outside both hidden ranges. Given the hidden block together with the hidden part of row i and the hidden part of column j, the entry at (i, j) is conditionally independent of all entries in hidden rows or hidden columns: the strips of the other visible rows and columns carry no further information about it.

theorem TauCeti.Probability.SeparatelyExchangeable.exists_common_visibleCells_coding {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e f : ℕ → ℕ} (he : (Set.range e).Infinite) (hf : (Set.range f).Infinite) : have H := Set.univ ×ˢ Set.range f ∪ Set.range e ×ˢ Set.univ; have V := (Set.range e)ᶜ ×ˢ (Set.range f)ᶜ; ∃ (g : ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α) → ↑unitInterval → α), Measurable (Function.uncurry g) ∧ ∀ (F : Finset ↑V), MeasureTheory.Measure.map (fun (q : (ℕ × ℕ → α) × (↥F → ↑unitInterval)) => (H.domRestrict q.1, fun (p : ↥F) => g (cellContext e f (↑↑p).1 (↑↑p).2 q.1) (q.2 p))) (ρ.prod (MeasureTheory.Measure.pi fun (x : ↥F) => MeasureTheory.volume)) = MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (H.domRestrict x, fun (p : ↥F) => x ↑↑p)) ρ

Every visible cell of a separately exchangeable array is generated from its own hidden context by one common coding function and one fresh uniform variable. Let e and f enumerate infinitely many hidden rows and hidden columns. There is a single measurable g such that, for every finite family of visible cells, feeding each cell's cellContext and its own independent uniform variable to g reproduces the joint law of the crossing strips and that whole family of cells.

The coding function does not depend on the position of the cell, which is what lets it serve as the cell noise U i j of an Aldous–Hoover representation.

theorem TauCeti.Probability.SeparatelyExchangeable.exists_common_visibleArray_coding {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e f : ℕ → ℕ} (he : (Set.range e).Infinite) (hf : (Set.range f).Infinite) : have H := Set.univ ×ˢ Set.range f ∪ Set.range e ×ˢ Set.univ; have V := (Set.range e)ᶜ ×ˢ (Set.range f)ᶜ; ∃ (g : ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α) → ↑unitInterval → α), Measurable (Function.uncurry g) ∧ MeasureTheory.Measure.map (fun (q : (ℕ × ℕ → α) × (↑V → ↑unitInterval)) => (H.domRestrict q.1, fun (p : ↑V) => g (cellContext e f (↑p).1 (↑p).2 q.1) (q.2 p))) (ρ.prod (MeasureTheory.Measure.infinitePi fun (x : ↑V) => MeasureTheory.volume)) = MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (H.domRestrict x, V.domRestrict x)) ρ

One common cell coding generates the whole visible array. Let e and f enumerate infinitely many hidden rows and hidden columns. There is a single measurable g such that feeding every visible cell's cellContext and its own fresh uniform variable to g, the uniform variables being i.i.d. over all visible cells, reproduces the joint law of the crossing strips and of the entire visible part of the array.

This is SeparatelyExchangeable.exists_common_visibleCells_coding for the infinite family of all visible cells at once: the crossing strips and the coded visible cells together recover the whole array law.