A common conditional law for off-diagonal pairs

For a jointly exchangeable array, the entries at (i,j) and (j,i) must be generated together: the two entries can be dependent, and the Aldous--Hoover coding gives their unordered pair a single cell-noise variable. Fix a hidden sequence of vertices. The context of an ordered pair of visible, distinct vertices records the hidden block and both vertices' strips against it.

Every such ordered pair has the same joint law with its context. Hence Mathlib's canonical conditional distribution gives one kernel for all off-diagonal pairs, and a single measurable randomization of that kernel works at every visible pair. This is the pair-valued counterpart of SeparatelyExchangeable.exists_common_cell_coding; the diagonal has a different orbit and must be treated separately. The randomization statement concerns each pair's conditional law; it does not yet assert conditional independence between different pairs.

The simultaneous coding of all pairs needs a larger context. The square context of a pair extends its context by the two diagonal entries x (i, i) and x (j, j); its entries are exactly those of the square spanned by the hidden vertices and i, j, other than the pair itself. The diagonal entries cannot be left out: no relabelling of the vertices separates the pair from the diagonal entries at i and j, since all four cells live on the same two vertices. The square context has the same transport and common-law results as the context, and its common conditional kernel is the one realized in Cell/OffDiagonalCoding.lean.

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.offDiagonalPairContext {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) : (((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)) × ((ℕ × ℕ → α) × (ℕ → α)) × (ℕ → α)

The hidden block and the two adjacent vertex contexts of an ordered pair of visible vertices. Both orientations are retained because a jointly exchangeable array need not be symmetric.

Equations

• TauCeti.Probability.offDiagonalPairContext e i j x = (TauCeti.Probability.cellContext e e i j x, TauCeti.Probability.cellContext e e j i x)

@[simp]

theorem TauCeti.Probability.offDiagonalPairContext_fst {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) : (offDiagonalPairContext e i j x).1 = cellContext e e i j x

The first component is the context of the forward directed cell.

@[simp]

theorem TauCeti.Probability.offDiagonalPairContext_snd {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) : (offDiagonalPairContext e i j x).2 = cellContext e e j i x

The second component is the context of the reverse directed cell.

theorem TauCeti.Probability.offDiagonalPairContext_swap {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) : offDiagonalPairContext e j i x = (offDiagonalPairContext e i j x).swap

Reversing the visible vertices swaps their two directed contexts.

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

Reading the context of an off-diagonal pair is measurable.

theorem TauCeti.Probability.offDiagonalPairContext_pairReindex {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (perm : Equiv.Perm ℕ) (he : ∀ (a : ℕ), perm (e a) = e a) (x : ℕ × ℕ → α) : offDiagonalPairContext e i j (pairReindex perm perm x) = offDiagonalPairContext e (perm i) (perm j) x

A common relabelling fixing the hidden vertices transports the context of a visible pair.

theorem TauCeti.Probability.JointlyExchangeable.map_offDiagonalPairContext_entries_eq_of_fixed {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (e : ℕ → ℕ) (i j : ℕ) (perm : Equiv.Perm ℕ) (he : ∀ (a : ℕ), perm (e a) = e a) : MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (offDiagonalPairContext e (perm i) (perm j) x, x (perm i, perm j), x (perm j, perm i))) ρ = MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (offDiagonalPairContext e i j x, x (i, j), x (j, i))) ρ

Joint exchangeability transports the law of a pair and its hidden context along any permutation that fixes the hidden vertices.

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

The joint law of a hidden context and its two directed off-diagonal entries is independent of the visible ordered pair, provided its vertices are distinct.

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

All off-diagonal visible pairs have the same canonical conditional kernel, including its values on contexts outside the support of the observed law.

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

One measurable randomization of the common conditional kernel generates either orientation of every off-diagonal visible pair from its context and a fresh uniform variable.

The square context of an off-diagonal pair

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

The square context of the ordered pair (i, j) of visible vertices: the contexts of both directed cells, that is the hidden block and the strips of i and of j against the hidden vertices, together with the two diagonal entries x (i, i) and x (j, j). Its entries are exactly those of the square spanned by the hidden vertices and i, j, other than (i, j) and (j, i).

Equations

• TauCeti.Probability.offDiagonalPairSquareContext e i j x = (TauCeti.Probability.offDiagonalPairContext e i j x, x (i, i), x (j, j))

@[simp]

theorem TauCeti.Probability.offDiagonalPairSquareContext_fst {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) : (offDiagonalPairSquareContext e i j x).1 = offDiagonalPairContext e i j x

The first component of the square context is the context of the two directed cells.

@[simp]

theorem TauCeti.Probability.offDiagonalPairSquareContext_snd {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) : (offDiagonalPairSquareContext e i j x).2 = (x (i, i), x (j, j))

The second component of the square context is the pair of diagonal entries.

theorem TauCeti.Probability.offDiagonalPairSquareContext_swap {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (x : ℕ × ℕ → α) : offDiagonalPairSquareContext e j i x = Prod.map Prod.swap Prod.swap (offDiagonalPairSquareContext e i j x)

Reversing the visible vertices swaps both the two directed contexts and the two diagonal entries of the square context.

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

Reading the square context of an off-diagonal pair is measurable.

theorem TauCeti.Probability.offDiagonalPairSquareContext_pairReindex {α : Type u_1} (e : ℕ → ℕ) (i j : ℕ) (perm : Equiv.Perm ℕ) (he : ∀ (a : ℕ), perm (e a) = e a) (x : ℕ × ℕ → α) : offDiagonalPairSquareContext e i j (pairReindex perm perm x) = offDiagonalPairSquareContext e (perm i) (perm j) x

A common relabelling fixing the hidden vertices transports the square context of a visible pair.

A common conditional law

theorem TauCeti.Probability.JointlyExchangeable.map_offDiagonalPairSquareContext_entries_eq_of_fixed {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (e : ℕ → ℕ) (i j : ℕ) (perm : Equiv.Perm ℕ) (he : ∀ (a : ℕ), perm (e a) = e a) : MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (offDiagonalPairSquareContext e (perm i) (perm j) x, x (perm i, perm j), x (perm j, perm i))) ρ = MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (offDiagonalPairSquareContext e i j x, x (i, j), x (j, i))) ρ

Joint exchangeability transports the law of a pair and its square context along any permutation that fixes the hidden vertices.

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

The joint law of a square context and its two directed off-diagonal entries is the same at every visible ordered pair of distinct vertices.

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

All visible off-diagonal pairs have the same conditional law given their square contexts. The equality is of Mathlib's canonical kernel versions, so it holds everywhere on the context space, not only on the support of the observed law.