A common conditional cell kernel for exchangeable arrays

Fix two sequences of hidden row and column indices, e and f. A visible cell (i,j) is observed together with the hidden block, its row against the hidden columns, and its column against the hidden rows. cellContext e f i j packages these three observations in the same measurable space for every visible cell.

For a separately exchangeable array law, the joint law of this context and the cell is independent of the choice of i and j, as long as they lie outside the two hidden index ranges. In particular, Mathlib's canonical condDistrib yields one and the same kernel for every visible cell. This is the kernel that a cell-noise randomization can use after the hidden block and the row and column strips have been generated. The statement is about the one-cell conditional law; conditional independence of different visible cells is a separate input to their simultaneous coding.

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.

def TauCeti.Probability.cellContext {α : Type u_1} (e f : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) : ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)

The hidden block and the two hidden strips adjacent to cell (i,j). The first component contains the block and the row strip, and the second contains the column strip.

Equations

• TauCeti.Probability.cellContext e f i j x = ((fun (p : ℕ × ℕ) => x (e p.1, f p.2), fun (b : ℕ) => x (i, f b)), fun (a : ℕ) => x (e a, j))

@[simp]

theorem TauCeti.Probability.cellContext_block_apply {α : Type u_1} (e f : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) (p : ℕ × ℕ) : (cellContext e f i j x).1.1 p = x (e p.1, f p.2)

@[simp]

theorem TauCeti.Probability.cellContext_rowStrip_apply {α : Type u_1} (e f : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) (b : ℕ) : (cellContext e f i j x).1.2 b = x (i, f b)

@[simp]

theorem TauCeti.Probability.cellContext_colStrip_apply {α : Type u_1} (e f : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) (a : ℕ) : (cellContext e f i j x).2 a = x (e a, j)

theorem TauCeti.Probability.measurable_cellContext {α : Type u_1} [MeasurableSpace α] (e f : ℕ → ℕ) (i j : ℕ) : Measurable (cellContext e f i j)

Reading a cell context from an array is measurable.

theorem TauCeti.Probability.cellContext_pairReindex {α : Type u_1} (e f : ℕ → ℕ) (i j : ℕ) (rowPerm colPerm : Equiv.Perm ℕ) (he : ∀ (a : ℕ), rowPerm (e a) = e a) (hf : ∀ (b : ℕ), colPerm (f b) = f b) (x : ℕ × ℕ → α) : cellContext e f i j (pairReindex rowPerm colPerm x) = cellContext e f (rowPerm i) (colPerm j) x

Reindexing while fixing the hidden indices transports the visible cell context to the context at the reindexed cell.

theorem TauCeti.Probability.SeparatelyExchangeable.map_cellContext_cell_eq_of_fixed {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (e f : ℕ → ℕ) (i j : ℕ) (rowPerm colPerm : Equiv.Perm ℕ) (he : ∀ (a : ℕ), rowPerm (e a) = e a) (hf : ∀ (b : ℕ), colPerm (f b) = f b) : MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (cellContext e f (rowPerm i) (colPerm j) x, x (rowPerm i, colPerm j))) ρ = MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (cellContext e f i j x, x (i, j))) ρ

The joint law of a cell and its hidden context is invariant under reindexing that fixes the hidden rows and columns pointwise.

theorem TauCeti.Probability.SeparatelyExchangeable.map_cellContext_cell_eq {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (e f : ℕ → ℕ) {i i' j j' : ℕ} (hi : i ∉ Set.range e) (hi' : i' ∉ Set.range e) (hj : j ∉ Set.range f) (hj' : j' ∉ Set.range f) : MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (cellContext e f i' j' x, x (i', j'))) ρ = MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (cellContext e f i j x, x (i, j))) ρ

All visible cells have the same joint law with their hidden block and adjacent hidden strips. Neither hidden enumeration must be injective; the only requirement is that neither visible index occurs in its corresponding hidden range.

theorem TauCeti.Probability.SeparatelyExchangeable.condDistrib_cellContext_eq {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (e f : ℕ → ℕ) {i i' j j' : ℕ} (hi : i ∉ Set.range e) (hi' : i' ∉ Set.range e) (hj : j ∉ Set.range f) (hj' : j' ∉ Set.range f) : ProbabilityTheory.condDistrib (fun (x : ℕ × ℕ → α) => x (i', j')) (cellContext e f i' j') ρ = ProbabilityTheory.condDistrib (fun (x : ℕ × ℕ → α) => x (i, j)) (cellContext e f i j) ρ

The regular conditional law of a visible cell given its hidden block and adjacent strips is the same kernel at every visible position. The equality is of Mathlib's canonical kernel versions, so it holds everywhere on the context space.

theorem TauCeti.Probability.SeparatelyExchangeable.exists_common_cell_coding {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (e f : ℕ → ℕ) {i₀ j₀ : ℕ} (hi₀ : i₀ ∉ Set.range e) (hj₀ : j₀ ∉ Set.range f) : ∃ (g : ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α) → ↑unitInterval → α), Measurable (Function.uncurry g) ∧ ∀ (i j : ℕ), i ∉ Set.range e → j ∉ Set.range f → ∀ (z : ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)), MeasureTheory.Measure.map (g z) MeasureTheory.volume = (ProbabilityTheory.condDistrib (fun (x : ℕ × ℕ → α) => x (i, j)) (cellContext e f i j) ρ) z

A single measurable cell coding realizes every visible cell's conditional law. Given a reference visible cell, the canonical conditional kernel of that cell can be randomized by a uniform variable. The common-kernel theorem makes the same coding work at every other visible position, with its own hidden block and adjacent strips as input. This statement concerns each cell's conditional law separately; it does not assert independence of the randomizations.