One cell kernel codes every off-diagonal pair of a jointly exchangeable array

Fix an infinite set of hidden vertices of a jointly exchangeable array, enumerated by e; the other vertices are visible. The Aldous–Hoover coding of such an array draws one cell variable per unordered pair of vertices, so the two entries x (i, j) and x (j, i) at a visible off-diagonal pair have to be generated together, from that one variable and the information carried by the vertices i and j.

The information a pair sees is its square context: the hidden block, the strips of i and of j against the hidden vertices, and the two diagonal entries x (i, i) and x (j, j). These are exactly the entries of the square spanned by the hidden vertices together with i and j, other than the pair itself, so by local conditional independence the pair is conditionally independent of everything else given its square context. The diagonal entries cannot be left out: no relabelling of the vertices separates the pair (i, j), (j, i) from the diagonal entries at i and j, since all four cells live on the same two vertices. In the representation the diagonal is therefore produced at the vertex level, together with the strips, and the cell variables are indexed by the off-diagonal unordered pairs, coded here.

Every visible ordered pair has the same joint law with its square context, so Mathlib's canonical conditional distribution gives one kernel for all of them (JointlyExchangeable.condDistrib_offDiagonalPairSquareContext_eq in Cell/JointPair.lean, where the square context offDiagonalPairSquareContext is defined). Combined with the conditional independence of distinct pairs given the crossing strips and the diagonal, the pair layer becomes a genuine coding: a single measurable function of a square context and a uniform variable generates every off-diagonal pair at once, each from its own context and its own fresh uniform variable, jointly with the crossing strips and the diagonal. This is the jointly exchangeable counterpart of SeparatelyExchangeable.exists_common_visibleArray_coding.

A joint Aldous–Hoover coding f(U, U_vert i, U_vert j, U_cell {i, j}) sees the two vertices of a pair through their noise, but not which of them comes first, while the pair coding above is indexed by increasing representatives. The coding is therefore produced in an oriented form: for any measurable set O of square contexts, it may be chosen so that whenever exactly one of a context and its reversal lies in O, the coding of the reversed context is the reversed coding. Off O the pair is coded as the reversal of the reversed pair; both codings have the same joint law with the crossing strips and the diagonal, so switching between them along an event of the strips and the diagonal changes nothing in law (TauCeti.MeasureTheory.Measure.map_ite_mem_eq).

Main results

• TauCeti.Probability.JointlyExchangeable.condIndepFun_offDiagonalPair_crossingStripsAndDiagonal — a visible off-diagonal pair is conditionally independent of the crossing strips and the diagonal given its square context.
• TauCeti.Probability.JointlyExchangeable.iCondIndepFun_offDiagonalPairs — distinct visible off-diagonal pairs are conditionally independent given the crossing strips and the diagonal.
• TauCeti.Probability.JointlyExchangeable.exists_common_offDiagonalPairs_coding — one common coding function, oriented along any measurable set of square contexts, generates every finite family of visible off-diagonal pairs from their square contexts and independent uniform variables.
• TauCeti.Probability.JointlyExchangeable.exists_common_offDiagonalArray_coding — the same coding function generates all visible off-diagonal pairs at once, from i.i.d. uniform variables indexed by the visible unordered pairs.
• TauCeti.Probability.offDiagonalPairSquareContextOfStripsAndDiagonal — reads the square context of a pair off the crossing strips and the diagonal alone, so that an assembly generating those first can feed the pair 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.

Reading the square context off the crossing strips and the diagonal

def TauCeti.Probability.offDiagonalPairSquareContextOfStripsAndDiagonal {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (y : ↑(Set.univ ×ˢ Set.range e ∪ Set.range e ×ˢ Set.univ ∪ {p : ℕ × ℕ | p.1 = p.2}) → α) : ((((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × α × α

The square context of (i, j) read off the crossing strips and the diagonal: every position the context looks at lies in a hidden row, in a hidden column, or on the diagonal.

Equations

• One or more equations did not get rendered due to their size.

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

Reading the square context off the crossing strips and the diagonal is measurable.

@[simp]

theorem TauCeti.Probability.offDiagonalPairSquareContextOfStripsAndDiagonal_comp_domRestrict {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) : offDiagonalPairSquareContextOfStripsAndDiagonal e i j ∘ (Set.univ ×ˢ Set.range e ∪ Set.range e ×ˢ Set.univ ∪ {p : ℕ × ℕ | p.1 = p.2}).domRestrict = offDiagonalPairSquareContext e i j

Reading the square context off the crossing strips and the diagonal of an array recovers its square context: this is how a coding of the strips and the diagonal feeds the pair coding.

theorem TauCeti.Probability.offDiagonalPairSquareContextOfStripsAndDiagonal_swap {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (y : ↑(Set.univ ×ˢ Set.range e ∪ Set.range e ×ˢ Set.univ ∪ {p : ℕ × ℕ | p.1 = p.2}) → α) : offDiagonalPairSquareContextOfStripsAndDiagonal e j i y = Prod.map Prod.swap Prod.swap (offDiagonalPairSquareContextOfStripsAndDiagonal e i j y)

Reading the square context of the reversed pair off the crossing strips and the diagonal swaps both the two directed contexts and the two diagonal entries.

Conditional independence

theorem TauCeti.Probability.JointlyExchangeable.condIndepFun_offDiagonalPair_crossingStripsAndDiagonal {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e : ℕ → ℕ} (he : (Set.range e).Infinite) {i j : ℕ} (hij : i ≠ j) (hi : i ∉ Set.range e) (hj : j ∉ Set.range e) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (offDiagonalPairSquareContext e i j) inferInstance) ⋯ (fun (x : ℕ × ℕ → α) => (x (i, j), x (j, i))) (Set.univ ×ˢ Set.range e ∪ Set.range e ×ˢ Set.univ ∪ {p : ℕ × ℕ | p.1 = p.2}).domRestrict ρ

A visible off-diagonal pair sees the crossing strips and the diagonal only through its square context. Let e enumerate infinitely many hidden vertices of a jointly exchangeable array and let i ≠ j be visible vertices. Given the hidden block, the strips of i and j against the hidden vertices and the two diagonal entries x (i, i), x (j, j), the pair (x (i, j), x (j, i)) is conditionally independent of all entries in hidden rows, in hidden columns, or on the diagonal.

theorem TauCeti.Probability.JointlyExchangeable.iCondIndepFun_offDiagonalPairs {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {S : Set ℕ} (hS : S.Infinite) : have H := Set.univ ×ˢ S ∪ S ×ˢ Set.univ ∪ {p : ℕ × ℕ | p.1 = p.2}; have V₂ := {p : ℕ × ℕ | p.1 ∉ S ∧ p.2 ∉ S ∧ p.1 < p.2}; ProbabilityTheory.iCondIndepFun (MeasurableSpace.comap H.domRestrict inferInstance) ⋯ (fun (p : ↑V₂) (x : ℕ × ℕ → α) => (x ↑p, x (↑p).swap)) ρ

Distinct visible off-diagonal pairs are conditionally independent given the crossing strips and the diagonal. Let S be an infinite set of hidden vertices of a jointly exchangeable array. Index the visible off-diagonal unordered pairs by their increasing representatives p.1 < p.2, and read each as the pair of entries (x p, x p.swap). Given all entries in a hidden row, in a hidden column, or on the diagonal, these pairs form a conditionally independent family.

The common coding

theorem TauCeti.Probability.JointlyExchangeable.exists_common_offDiagonalPairs_coding {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] [Nonempty α] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e : ℕ → ℕ} (he : (Set.range e).Infinite) {O : Set (((((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × α × α)} (hO : MeasurableSet O) : have H := Set.univ ×ˢ Set.range e ∪ Set.range e ×ˢ Set.univ ∪ {p : ℕ × ℕ | p.1 = p.2}; have V₂ := {p : ℕ × ℕ | p.1 ∉ Set.range e ∧ p.2 ∉ Set.range e ∧ p.1 < p.2}; ∃ (g : ((((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × α × α → ↑unitInterval → α × α), Measurable (Function.uncurry g) ∧ (∀ (c : ((((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × α × α) (u : ↑unitInterval), (c ∈ O ↔ Prod.map Prod.swap Prod.swap c ∉ O) → g (Prod.map Prod.swap Prod.swap c) u = (g c u).swap) ∧ ∀ (F : Finset ↑V₂), MeasureTheory.Measure.map (fun (q : (ℕ × ℕ → α) × (↥F → ↑unitInterval)) => (H.domRestrict q.1, fun (p : ↥F) => g (offDiagonalPairSquareContext e (↑↑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, x (↑↑p).swap))) ρ

Every finite family of visible off-diagonal pairs of a jointly exchangeable array is generated from their square contexts by one common coding function and independent uniform variables. Let e enumerate infinitely many hidden vertices. Index the visible off-diagonal unordered pairs by their increasing representatives p.1 < p.2. There is a single measurable g such that, for every finite family of such pairs, feeding each pair's square context and its own independent uniform variable to g reproduces the joint law of the crossing strips, the diagonal and that whole family of pairs (x p, x p.swap).

The coding can moreover be oriented along any measurable set O of square contexts: whenever exactly one of a context c and its reversal Prod.map Prod.swap Prod.swap c lies in O, the coding of the reversal is the reversed coding of c. Reversing a square context is reversing the pair (offDiagonalPairSquareContext_swap), so on such contexts g produces the two orientations of one pair from one uniform variable consistently.

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

theorem TauCeti.Probability.JointlyExchangeable.exists_common_offDiagonalArray_coding {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] [Nonempty α] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e : ℕ → ℕ} (he : (Set.range e).Infinite) {O : Set (((((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × α × α)} (hO : MeasurableSet O) : have H := Set.univ ×ˢ Set.range e ∪ Set.range e ×ˢ Set.univ ∪ {p : ℕ × ℕ | p.1 = p.2}; have V₂ := {p : ℕ × ℕ | p.1 ∉ Set.range e ∧ p.2 ∉ Set.range e ∧ p.1 < p.2}; ∃ (g : ((((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × α × α → ↑unitInterval → α × α), Measurable (Function.uncurry g) ∧ (∀ (c : ((((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × α × α) (u : ↑unitInterval), (c ∈ O ↔ Prod.map Prod.swap Prod.swap c ∉ O) → g (Prod.map Prod.swap Prod.swap c) u = (g c u).swap) ∧ MeasureTheory.Measure.map (fun (q : (ℕ × ℕ → α) × (↑V₂ → ↑unitInterval)) => (H.domRestrict q.1, fun (p : ↑V₂) => g (offDiagonalPairSquareContext e (↑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, fun (p : ↑V₂) => (x ↑p, x (↑p).swap))) ρ

One common coding generates all visible off-diagonal pairs of a jointly exchangeable array. Let e enumerate infinitely many hidden vertices. There is a single measurable g such that feeding every visible off-diagonal pair's square context and its own fresh uniform variable to g, the uniform variables being i.i.d. over all visible increasing pairs, reproduces the joint law of the crossing strips, the diagonal and all the pairs (x p, x p.swap) at once.

As in JointlyExchangeable.exists_common_offDiagonalPairs_coding, the coding can be oriented along any measurable set O of square contexts: whenever exactly one of a context c and its reversal lies in O, the coding of the reversal is the reversed coding of c.

Together with the crossing strips and the diagonal, these pairs are the whole array, so this is the cell layer of a jointly exchangeable Aldous–Hoover representation. The orientation is what lets a coding that sees the two vertices of a pair but not their order produce both entries of the pair consistently.