The Aldous--Hoover representation of a jointly exchangeable array

Aldous--Hoover theorem, joint form. For every jointly exchangeable probability law ρ on arrays ℕ × ℕ → α with values in a standard Borel space, there is a measurable F : I × I × I × I → α such that ρ is the law of the array

X i j = F(U, U_i, U_j, U_{i,j}),

where U, the vertex variables U_i and the variables U_{i,j} indexed by unordered pairs are independent uniform variables. Together with TauCeti.Probability.AldousHoover.jointlyExchangeable_jointArray, the converse, this characterizes jointly exchangeable array laws as the laws of measurable joint Aldous--Hoover codings.

The vertex indices are split into three infinite classes: hidden vertices, a reservoir, and visible vertices. The array read along the visible vertices has the law of the whole array. Its entries are coded in three layers, from the outside in:

• the hidden square together with the reservoir vertex data is a random element of a standard Borel space, hence the image of the single global uniform variable U;
• given these, the data of each visible vertex — its strips against the hidden vertices in both orientations and its diagonal entry — are generated by one uniform variable per visible vertex (JointlyExchangeable.exists_vertex_strip_diagonal_coding);
• given all vertex data, both entries of every visible off-diagonal pair are generated from their square context and one uniform variable per unordered pair by a single common coding (JointlyExchangeable.exists_common_offDiagonalArray_coding).

In the last layer the common coding produces the pair (x (i, j), x (j, i)) in a chosen orientation, while F only sees the noise, not the indices. So F orients each pair by the order of its two vertex variables, which are almost surely distinct, and reads the diagonal entry off the vertex data when the two vertex variables coincide. Reversing the orientation of a pair does not change its conditional law given its square context: joint exchangeability exchanges the two vertices, so the common pair coding is equivariant in law under swapping its square context and its output.

Main results

• TauCeti.Probability.JointlyExchangeable.exists_map_jointArray_eq — every jointly exchangeable probability law on arrays is the law of a measurable joint Aldous--Hoover coding.
• TauCeti.Probability.jointlyExchangeable_iff_exists_map_jointArray_eq — an array process is jointly exchangeable if and only if its law is such a law.

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.
• D. N. Hoover, "Relations on probability spaces and arrays of random variables", preprint, Institute for Advanced Study, Princeton, 1979.
• 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.

Square contexts read off vertex data

Assembling an array from vertex data and off-diagonal pairs

The coding function

Swapping the orientation of a pair

The representation

theorem TauCeti.Probability.JointlyExchangeable.exists_map_jointArray_eq {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : ∃ (F : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α), Measurable F ∧ MeasureTheory.Measure.map (fun (u : AldousHoover.NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => AldousHoover.jointArray F p u) (AldousHoover.noiseMeasure Unit (Sym2 ℕ)) = ρ

The Aldous--Hoover representation of a jointly exchangeable array. Every jointly exchangeable probability law ρ on arrays with values in a standard Borel space is the law of a measurable joint Aldous--Hoover coding: there is a measurable F : I × I × I × I → α with ρ the law of X i j = F(U, U_i, U_j, U_{i,j}) under independent uniform noise, where the cell variable U_{i,j} is indexed by the unordered pair {i, j}.

theorem TauCeti.Probability.jointlyExchangeable_iff_exists_map_jointArray_eq {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ × ℕ → Ω → α} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : JointlyExchangeable μ X ↔ ∃ (F : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α), Measurable F ∧ MeasureTheory.Measure.map (fun (u : AldousHoover.NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => AldousHoover.jointArray F p u) (AldousHoover.noiseMeasure Unit (Sym2 ℕ)) = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ

Jointly exchangeable arrays are exactly the Aldous--Hoover codings in law. An array process with a.e.-measurable entries in a standard Borel space, on a probability space, is jointly exchangeable if and only if its law is the law of a measurable joint Aldous--Hoover coding X i j = F(U, U_i, U_j, U_{i,j}) under independent uniform noise.