Aldous--Hoover array codings are exchangeable

The functional forms in the Aldous--Hoover representation use four independent kinds of uniform randomness. A separately exchangeable array is coded from a global variable, one variable for each row, one for each column, and one for each cell:

X i j = f(U, U_row i, U_col j, U_cell i j).

For a jointly exchangeable array, the row and column variables are replaced by one family of vertex variables:

X i j = f(U, U_vert i, U_vert j, U_cell {i, j}).

This file defines canonical product probability spaces carrying those sources and proves the easy direction of the Aldous--Hoover representation theorem: every measurable coding of the first form is separately exchangeable, and every measurable coding of the second form is jointly exchangeable. The proof reindexes the independent source family. Row and column permutations act on their respective vertex variables and together on the cell variables, while leaving the global variable fixed.

Dropping the global variable — coding through a function that ignores its first argument — gives the ergodic form of the representation, whose arrays are dissociated as well as exchangeable. That is proved in Arrays.AldousHoover.Dissociated. The converse representation direction, which constructs the coding function from an exchangeable array, is proved for separately exchangeable arrays in Arrays.AldousHoover.Separate.Representation and for jointly exchangeable arrays in Arrays.AldousHoover.Joint.Representation.

Main definitions

• TauCeti.Probability.AldousHoover.Axis labels the row and column noise families;
• TauCeti.Probability.AldousHoover.NoiseIndex indexes global, vertex, and cell noise;
• TauCeti.Probability.AldousHoover.noiseMeasure is the corresponding i.i.d. uniform law;
• TauCeti.Probability.AldousHoover.separateArray and TauCeti.Probability.AldousHoover.jointArray are the two coding forms.

Main results

• TauCeti.Probability.AldousHoover.separatelyExchangeable_separateArray;
• TauCeti.Probability.AldousHoover.jointlyExchangeable_jointArray;
• TauCeti.Probability.AldousHoover.jointArray_symmetric_of.

References

• D. Aldous, ["Representations for partially exchangeable arrays of random variables"] (https://doi.org/10.1016/0047-259X(81)90099-3), Journal of Multivariate Analysis 11 (1981), 581--598.
• O. Kallenberg, [Probabilistic Symmetries and Invariance Principles] (https://doi.org/10.1007/0-387-28836-4), Springer, 2005, Chapter 7.

No material is adapted from cameronfreer/exchangeability, which treats sequences rather than exchangeable arrays.

inductive TauCeti.Probability.AldousHoover.NoiseIndex (κ : Type u_1) (ι : Type u_2) : Type (max u_1 u_2)

Indices for the independent noise in an Aldous--Hoover coding. The parameter κ indexes families of vertex variables, while ι indexes the cell variables.

• global {κ : Type u_1} {ι : Type u_2} : NoiseIndex κ ι
• vertex {κ : Type u_1} {ι : Type u_2} (axis : κ) (i : ℕ) : NoiseIndex κ ι
• cell {κ : Type u_1} {ι : Type u_2} (p : ι) : NoiseIndex κ ι

inductive TauCeti.Probability.AldousHoover.Axis : Type

The two vertex-noise families in the separately exchangeable coding.

• row : Axis
• column : Axis

def TauCeti.Probability.AldousHoover.indexEquiv {κ : Type u_1} {ι : Type u_2} (vertexPerm : κ → Equiv.Perm ℕ) (cellPerm : ι ≃ ι) : NoiseIndex κ ι ≃ NoiseIndex κ ι

Reindex Aldous--Hoover noise by a permutation of each vertex family and of the cell indices.

Equations

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

@[simp]

theorem TauCeti.Probability.AldousHoover.indexEquiv_global {κ : Type u_1} {ι : Type u_2} (vertexPerm : κ → Equiv.Perm ℕ) (cellPerm : ι ≃ ι) : (indexEquiv vertexPerm cellPerm) NoiseIndex.global = NoiseIndex.global

@[simp]

theorem TauCeti.Probability.AldousHoover.indexEquiv_vertex {κ : Type u_1} {ι : Type u_2} (vertexPerm : κ → Equiv.Perm ℕ) (cellPerm : ι ≃ ι) (a : κ) (i : ℕ) : (indexEquiv vertexPerm cellPerm) (NoiseIndex.vertex a i) = NoiseIndex.vertex a ((vertexPerm a) i)

@[simp]

theorem TauCeti.Probability.AldousHoover.indexEquiv_cell {κ : Type u_1} {ι : Type u_2} (vertexPerm : κ → Equiv.Perm ℕ) (cellPerm : ι ≃ ι) (p : ι) : (indexEquiv vertexPerm cellPerm) (NoiseIndex.cell p) = NoiseIndex.cell (cellPerm p)

noncomputable def TauCeti.Probability.AldousHoover.noiseMeasure (κ : Type u_1) (ι : Type u_2) : MeasureTheory.Measure (NoiseIndex κ ι → ↑unitInterval)

The canonical law of the independent uniform variables used by an Aldous--Hoover coding.

Equations

• TauCeti.Probability.AldousHoover.noiseMeasure κ ι = MeasureTheory.Measure.infinitePi fun (x : TauCeti.Probability.AldousHoover.NoiseIndex κ ι) => MeasureTheory.volume

theorem TauCeti.Probability.AldousHoover.noiseMeasure_def (κ : Type u_1) (ι : Type u_2) : noiseMeasure κ ι = MeasureTheory.Measure.infinitePi fun (x : NoiseIndex κ ι) => MeasureTheory.volume

The canonical Aldous--Hoover noise law is the product of uniform laws over all noise indices.

instance TauCeti.Probability.AldousHoover.instIsProbabilityMeasureNoiseMeasure (κ : Type u_1) (ι : Type u_2) : MeasureTheory.IsProbabilityMeasure (noiseMeasure κ ι)

The canonical Aldous--Hoover noise law is a probability measure.

@[simp]

theorem TauCeti.Probability.AldousHoover.map_eval_noiseMeasure {κ : Type u_1} {ι : Type u_2} (q : NoiseIndex κ ι) : MeasureTheory.Measure.map (fun (u : NoiseIndex κ ι → ↑unitInterval) => u q) (noiseMeasure κ ι) = MeasureTheory.volume

Each coordinate of the canonical Aldous--Hoover noise law is uniform on the unit interval.

theorem TauCeti.Probability.AldousHoover.iIndepFun_eval_noiseMeasure (κ : Type u_1) (ι : Type u_2) : ProbabilityTheory.iIndepFun (fun (q : NoiseIndex κ ι) (u : NoiseIndex κ ι → ↑unitInterval) => u q) (noiseMeasure κ ι)

The coordinates of the canonical Aldous--Hoover noise law are independent.

@[reducible, inline]

abbrev TauCeti.Probability.AldousHoover.noiseCongr {κ : Type u_1} {ι : Type u_2} (vertexPerm : κ → Equiv.Perm ℕ) (cellPerm : ι ≃ ι) : (NoiseIndex κ ι → ↑unitInterval) ≃ᵐ (NoiseIndex κ ι → ↑unitInterval)

Reindexing a realization of the Aldous--Hoover noise by a permutation of each vertex family and of the cell indices, as a measurable equivalence.

Equations

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

@[simp]

theorem TauCeti.Probability.AldousHoover.noiseCongr_apply {κ : Type u_1} {ι : Type u_2} (vertexPerm : κ → Equiv.Perm ℕ) (cellPerm : ι ≃ ι) (u : NoiseIndex κ ι → ↑unitInterval) (q : NoiseIndex κ ι) : (noiseCongr vertexPerm cellPerm) u q = u ((indexEquiv vertexPerm cellPerm) q)

@[simp]

theorem TauCeti.Probability.AldousHoover.map_noiseCongr_noiseMeasure {κ : Type u_1} (vertexPerm : κ → Equiv.Perm ℕ) {ι : Type u_2} (cellPerm : ι ≃ ι) : MeasureTheory.Measure.map (⇑(noiseCongr vertexPerm cellPerm)) (noiseMeasure κ ι) = noiseMeasure κ ι

The independent uniform noise law is invariant under reindexing its vertex and cell coordinates.

Noise actions for array codings

def TauCeti.Probability.AldousHoover.separateVertexPerm (rowPerm colPerm : Equiv.Perm ℕ) : Axis → Equiv.Perm ℕ

The action on the two vertex-noise families associated to two axis permutations.

Equations

• TauCeti.Probability.AldousHoover.separateVertexPerm rowPerm colPerm TauCeti.Probability.AldousHoover.Axis.row = rowPerm
• TauCeti.Probability.AldousHoover.separateVertexPerm rowPerm colPerm TauCeti.Probability.AldousHoover.Axis.column = colPerm

@[simp]

theorem TauCeti.Probability.AldousHoover.separateVertexPerm_row (rowPerm colPerm : Equiv.Perm ℕ) : separateVertexPerm rowPerm colPerm Axis.row = rowPerm

@[simp]

theorem TauCeti.Probability.AldousHoover.separateVertexPerm_column (rowPerm colPerm : Equiv.Perm ℕ) : separateVertexPerm rowPerm colPerm Axis.column = colPerm

def TauCeti.Probability.AldousHoover.separateCellPerm (rowPerm colPerm : Equiv.Perm ℕ) : ℕ × ℕ ≃ ℕ × ℕ

The action on cell-noise coordinates associated to two axis permutations.

Equations

• TauCeti.Probability.AldousHoover.separateCellPerm rowPerm colPerm = Equiv.prodCongr rowPerm colPerm

@[simp]

theorem TauCeti.Probability.AldousHoover.separateCellPerm_apply (rowPerm colPerm : Equiv.Perm ℕ) (p : ℕ × ℕ) : (separateCellPerm rowPerm colPerm) p = (rowPerm p.1, colPerm p.2)

def TauCeti.Probability.AldousHoover.separateNoiseCongr (rowPerm colPerm : Equiv.Perm ℕ) : (NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) ≃ᵐ (NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval)

The measurable equivalence reindexing the separate-coding noise by two axis permutations.

Equations

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

@[simp]

theorem TauCeti.Probability.AldousHoover.separateNoiseCongr_apply_global (rowPerm colPerm : Equiv.Perm ℕ) (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) : (separateNoiseCongr rowPerm colPerm) u NoiseIndex.global = u NoiseIndex.global

@[simp]

theorem TauCeti.Probability.AldousHoover.separateNoiseCongr_apply_vertex (rowPerm colPerm : Equiv.Perm ℕ) (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (a : Axis) (i : ℕ) : (separateNoiseCongr rowPerm colPerm) u (NoiseIndex.vertex a i) = u (NoiseIndex.vertex a ((separateVertexPerm rowPerm colPerm a) i))

@[simp]

theorem TauCeti.Probability.AldousHoover.separateNoiseCongr_apply_cell (rowPerm colPerm : Equiv.Perm ℕ) (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) : (separateNoiseCongr rowPerm colPerm) u (NoiseIndex.cell p) = u (NoiseIndex.cell ((separateCellPerm rowPerm colPerm) p))

@[simp]

theorem TauCeti.Probability.AldousHoover.map_separateNoiseCongr_noiseMeasure (rowPerm colPerm : Equiv.Perm ℕ) : MeasureTheory.Measure.map (⇑(separateNoiseCongr rowPerm colPerm)) (noiseMeasure Axis (ℕ × ℕ)) = noiseMeasure Axis (ℕ × ℕ)

The separate noise reindexing preserves the canonical independent-uniform noise law.

def TauCeti.Probability.AldousHoover.jointCellPerm (perm : Equiv.Perm ℕ) : Sym2 ℕ ≃ Sym2 ℕ

The action on unordered-pair cell indices associated to a permutation of the vertex indices.

Equations

• TauCeti.Probability.AldousHoover.jointCellPerm perm = { toFun := Sym2.map ⇑perm, invFun := Sym2.map ⇑(Equiv.symm perm), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.Probability.AldousHoover.jointCellPerm_apply (perm : Equiv.Perm ℕ) (p : Sym2 ℕ) : (jointCellPerm perm) p = Sym2.map (⇑perm) p

def TauCeti.Probability.AldousHoover.jointNoiseCongr (perm : Equiv.Perm ℕ) : (NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) ≃ᵐ (NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval)

The measurable equivalence reindexing the joint-coding noise by one vertex permutation.

Equations

• TauCeti.Probability.AldousHoover.jointNoiseCongr perm = TauCeti.Probability.AldousHoover.noiseCongr (fun (x : Unit) => perm) (TauCeti.Probability.AldousHoover.jointCellPerm perm)

@[simp]

theorem TauCeti.Probability.AldousHoover.jointNoiseCongr_apply_global (perm : Equiv.Perm ℕ) (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) : (jointNoiseCongr perm) u NoiseIndex.global = u NoiseIndex.global

@[simp]

theorem TauCeti.Probability.AldousHoover.jointNoiseCongr_apply_vertex (perm : Equiv.Perm ℕ) (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (i : ℕ) : (jointNoiseCongr perm) u (NoiseIndex.vertex () i) = u (NoiseIndex.vertex () (perm i))

@[simp]

theorem TauCeti.Probability.AldousHoover.jointNoiseCongr_apply_cell (perm : Equiv.Perm ℕ) (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : Sym2 ℕ) : (jointNoiseCongr perm) u (NoiseIndex.cell p) = u (NoiseIndex.cell ((jointCellPerm perm) p))

@[simp]

theorem TauCeti.Probability.AldousHoover.map_jointNoiseCongr_noiseMeasure (perm : Equiv.Perm ℕ) : MeasureTheory.Measure.map (⇑(jointNoiseCongr perm)) (noiseMeasure Unit (Sym2 ℕ)) = noiseMeasure Unit (Sym2 ℕ)

The joint noise reindexing preserves the canonical independent-uniform noise law.

def TauCeti.Probability.AldousHoover.separateArray {α : Type u_1} (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (p : ℕ × ℕ) (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) : α

The separately exchangeable Aldous--Hoover coding.

Equations

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

@[simp]

theorem TauCeti.Probability.AldousHoover.separateArray_apply {α : Type u_1} (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (p : ℕ × ℕ) (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) : separateArray f p u = f (u NoiseIndex.global, u (NoiseIndex.vertex Axis.row p.1), u (NoiseIndex.vertex Axis.column p.2), u (NoiseIndex.cell p))

theorem TauCeti.Probability.AldousHoover.separateArray_reindex {α : Type u_1} (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (rowPerm colPerm : Equiv.Perm ℕ) (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) : separateArray f (rowPerm p.1, colPerm p.2) u = separateArray f p ((separateNoiseCongr rowPerm colPerm) u)

Pathwise equivariance of the separate coding under the corresponding noise reindexing.

theorem TauCeti.Probability.AldousHoover.measurable_separateArray {α : Type u_1} [MeasurableSpace α] (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (hf : Measurable f) : Measurable fun (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) => separateArray f p u

A measurable separate Aldous--Hoover coding is measurable as an array-valued random variable.

theorem TauCeti.Probability.AldousHoover.separatelyExchangeable_separateArray {α : Type u_1} [MeasurableSpace α] (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (hf : Measurable f) : SeparatelyExchangeable (noiseMeasure Axis (ℕ × ℕ)) (separateArray f)

Every measurable separate Aldous--Hoover coding is separately exchangeable.

def TauCeti.Probability.AldousHoover.jointArray {α : Type u_1} (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (p : ℕ × ℕ) (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) : α

The jointly exchangeable Aldous--Hoover coding, using one common family of vertex variables for the two axes.

Equations

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

@[simp]

theorem TauCeti.Probability.AldousHoover.jointArray_apply {α : Type u_1} (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (p : ℕ × ℕ) (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) : jointArray f p u = f (u NoiseIndex.global, u (NoiseIndex.vertex () p.1), u (NoiseIndex.vertex () p.2), u (NoiseIndex.cell s(p.1, p.2)))

theorem TauCeti.Probability.AldousHoover.jointArray_reindex {α : Type u_1} (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (perm : Equiv.Perm ℕ) (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) : jointArray f (perm p.1, perm p.2) u = jointArray f p ((jointNoiseCongr perm) u)

Pathwise equivariance of the joint coding under the corresponding noise reindexing.

theorem TauCeti.Probability.AldousHoover.jointArray_apply_swap {α : Type u_1} (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (i j : ℕ) (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) : jointArray f (j, i) u = f (u NoiseIndex.global, u (NoiseIndex.vertex () j), u (NoiseIndex.vertex () i), u (NoiseIndex.cell s(i, j)))

Swapping the two indices of a joint coding only swaps its two vertex-noise arguments. The cell-noise argument is unchanged because it is indexed by the unordered pair Sym2.mk i j.

theorem TauCeti.Probability.AldousHoover.jointArray_symmetric_of {α : Type u_1} (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (hf : ∀ (a b c d : ↑unitInterval), f (a, b, c, d) = f (a, c, b, d)) (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (i j : ℕ) : jointArray f (i, j) u = jointArray f (j, i) u

A kernel symmetric in its two vertex variables produces a pathwise symmetric array. This is the symmetry condition needed when the jointly exchangeable Aldous--Hoover coding is specialized to random graphs and other undirected arrays.

theorem TauCeti.Probability.AldousHoover.measurable_jointArray {α : Type u_1} [MeasurableSpace α] (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (hf : Measurable f) : Measurable fun (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => jointArray f p u

A measurable joint Aldous--Hoover coding is measurable as an array-valued random variable.

theorem TauCeti.Probability.AldousHoover.jointlyExchangeable_jointArray {α : Type u_1} [MeasurableSpace α] (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (hf : Measurable f) : JointlyExchangeable (noiseMeasure Unit (Sym2 ℕ)) (jointArray f)

Every measurable joint Aldous--Hoover coding is jointly exchangeable.