Mixing laws of separately exchangeable arrays

Applying de Finetti's theorem to the rows of a separately exchangeable array gives a random probability measure on row paths. The remaining column symmetry does not generally make this random measure exchangeable almost surely. For example, if every row equals one common i.i.d. random path Y, then the row directing measure is δ_Y, which is almost surely not an exchangeable measure.

The correct inherited symmetry is at the level of the mixing law. If ν is any mixing representative for the row process, then the law of ν is invariant under pushing every measure forward by a permutation of path coordinates:

μ.map (ω ↦ (ν ω).map (permReindex τ)) = μ.map ν.

The proof uses the opposite-axis half of separate exchangeability. Mapping each row path by permReindex τ preserves the row process's finite-dimensional laws by column exchangeability. The coordinatewise-map API for MixedIIDWith therefore supplies a second mixing representative for the original row process, and uniqueness of the mixing law identifies their laws. The column statement is the symmetric argument using row exchangeability.

The existential corollaries retain genuine directing measures: de Finetti supplies ConditionallyIIDWith, while the invariance follows after forgetting only to its mixture identity. These results are the next law-level input to the separately exchangeable-array branch of the Aldous–Hoover milestone in TauCetiRoadmap/Exchangeability/README.md, Layer 8.

Main results

• SeparatelyExchangeable.mixingLaw_map_permReindex_arrayRow_eq — the row mixing law is invariant under coordinate permutations;
• SeparatelyExchangeable.mixingLaw_map_permReindex_arrayCol_eq — the symmetric column statement;

Every result here holds of any supplied mixing representative; the existential versions, in which de Finetti produces one, are in Arrays.DeFinetti.

References

• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 7.
• D. Aldous, "Representations for partially exchangeable arrays of random variables", Journal of Multivariate Analysis 11 (1981), 581–598.

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

theorem TauCeti.Probability.mixingLaw_map_permReindex_arrayRow_eq_of_col_invariant {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α} {τ : Equiv.Perm ℕ} (hcol : MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X (p.1, τ p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ) {ν : Ω → MeasureTheory.ProbabilityMeasure (ℕ → α)} (hν : MixedIIDWith μ (arrayRow X) ν) : MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω).map fun (x : ℕ → α) (k : ℕ) => x (τ k)) μ = MeasureTheory.Measure.map ν μ

The row mixing law inherits column symmetry. For any mixing representative ν of the row process, invariance of the array law under the column permutation τ implies that pushing ν forward by τ does not change its law under μ.

This is a statement about the law μ.map ν, not an almost-sure assertion that each measure ν ω is exchangeable. The latter is false in general.

theorem TauCeti.Probability.SeparatelyExchangeable.mixingLaw_map_permReindex_arrayRow_eq {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) {ν : Ω → MeasureTheory.ProbabilityMeasure (ℕ → α)} (hν : MixedIIDWith μ (arrayRow X) ν) (τ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω).map fun (x : ℕ → α) (k : ℕ) => x (τ k)) μ = MeasureTheory.Measure.map ν μ

The row mixing law of a separately exchangeable array inherits the column symmetry.

theorem TauCeti.Probability.mixingLaw_map_permReindex_arrayCol_eq_of_row_invariant {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α} {σ : Equiv.Perm ℕ} (hrow : MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X (σ p.1, p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ) {ν : Ω → MeasureTheory.ProbabilityMeasure (ℕ → α)} (hν : MixedIIDWith μ (arrayCol X) ν) : MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω).map fun (x : ℕ → α) (k : ℕ) => x (σ k)) μ = MeasureTheory.Measure.map ν μ

The column mixing law inherits row symmetry. This is the transpose of mixingLaw_map_permReindex_arrayRow_eq_of_col_invariant.

theorem TauCeti.Probability.SeparatelyExchangeable.mixingLaw_map_permReindex_arrayCol_eq {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) {ν : Ω → MeasureTheory.ProbabilityMeasure (ℕ → α)} (hν : MixedIIDWith μ (arrayCol X) ν) (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω).map fun (x : ℕ → α) (k : ℕ) => x (σ k)) μ = MeasureTheory.Measure.map ν μ

The column mixing law of a separately exchangeable array inherits the row symmetry.