Row exchangeable arrays and the factorization of their directing measure

An array Y : ι × ℕ → Ω → α is row exchangeable when its law is unchanged by permuting the entries of each row separately: for every family π : ι → Equiv.Perm ℕ of time permutations, one for each row, the array (a, k) ↦ Y (a, π a k) has the law of Y. This is the symmetry of the array of successors of a Markov exchangeable process, and it is stronger than asking that each row be exchangeable on its own, because the permutations may be chosen independently.

Reading an array column by column gives the process arrayColumn Y : ℕ → Ω → (ι → α), whose k-th value is the vector of the k-th entries of all rows. Row exchangeability contains the diagonal case π = fun _ => σ, so arrayColumn Y is a fully exchangeable process valued in ι → α, which for countable ι and standard Borel α is again standard Borel. De Finetti's theorem therefore hands the columns a directing measure λ : Ω → ProbabilityMeasure (ι → α).

The theorem of this file is that the extra, off-diagonal part of the symmetry makes that directing measure factor over the rows: almost surely, its mass on a finite box {x | ∀ a ∈ F, x a ∈ B a} is the product over a ∈ F of its one-row masses. So conditionally on the directing measure distinct rows are independent, while the entries are identically distributed within each row. This is the mixture-of-independent-i.i.d.-rows form that the Diaconis–Freedman representation of Markov exchangeable processes consumes.

Main definitions

• TauCeti.Probability.RowExchangeable: invariance of the array law under independent permutations of the individual rows;
• TauCeti.Probability.arrayColumn: the array read as a process of columns.

Main results

• TauCeti.Probability.RowExchangeable.fullyExchangeable_row and TauCeti.Probability.RowExchangeable.fullyExchangeable_arrayColumn: each row, and the column process, is fully exchangeable;
• TauCeti.Probability.rowExchangeable_iff_forall_prodCongrRight_mem_finitary: it suffices to check families of row permutations that move only finitely many cells altogether;
• TauCeti.Probability.RowExchangeable.map_values: closure under coordinatewise pushforward;
• TauCeti.Probability.RowExchangeable.measure_setOf_forall_pair_eq: the combinatorial core — the probability that each row of a finite set lands in its own target set at two prescribed times does not depend on which two times are prescribed;
• TauCeti.Probability.RowExchangeable.ae_apply_pi_union: the directing measure of the column process is almost surely multiplicative across disjoint sets of rows;
• TauCeti.Probability.RowExchangeable.ae_apply_pi_eq_prod and TauCeti.Probability.RowExchangeable.exists_directing_pi_eq_prod: the resulting product formula over a finite set of rows, at a given witness and at the witness de Finetti supplies;
• TauCeti.Probability.RowExchangeable.measure_setOf_forall_mem_eq_lintegral_prod: the mass of an event reading finitely many pairwise distinct cells is the mixture of the product of the row marginals' masses — the form in which a consumer reads a finite block of array entries.

Implementation

The multiplicativity is proved by a second-moment argument that never leaves the world of finite blocks. Write C and D for the boxes cut out by two disjoint finite sets of rows. The mixture identity turns each of

∫ λ(C ∩ D)²,      ∫ λ(C ∩ D) · λ(C) · λ(D),      ∫ λ(C)² · λ(D)²

into the probability of an array event in which every row involved is tested at exactly two times — times that differ from term to term. Row exchangeability moves those times back to 0 and 1 one row at a time, so the three integrals coincide, and the integral of (λ(C ∩ D) - λ(C) · λ(D))² vanishes.

Only the mixture identity MixedIIDWith is used, not the joint-law disintegration: the argument tests the directing measure against nothing but block probabilities, so the factorization theorem needs no standard Borel structure at all. That hypothesis enters exactly once, in the de Finetti wrapper at the end, which is what produces a witness in the first place. Countability of the row index is present throughout, since it is what makes an array with a.e. measurable entries an a.e. measurable map into ι × ℕ → α.

References

• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115–130.
• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 8, "Markov exchangeability".

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

def TauCeti.Probability.arrayColumn {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} (Y : ι × ℕ → Ω → α) (k : ℕ) (ω : Ω) : ι → α

The array Y read as a process of columns: the k-th column is the vector of the k-th entries of all rows.

Equations

• TauCeti.Probability.arrayColumn Y k ω a = Y (a, k) ω

@[simp]

theorem TauCeti.Probability.arrayColumn_apply {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} (Y : ι × ℕ → Ω → α) (k : ℕ) (ω : Ω) (a : ι) : arrayColumn Y k ω a = Y (a, k) ω

def TauCeti.Probability.RowExchangeable {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Y : ι × ℕ → Ω → α) : Prop

Row exchangeability. The law of the array is invariant under permuting the entries of each row by a permutation of time chosen separately for that row.

Taking one and the same permutation in every row recovers the exchangeability of the columns; the content beyond that is that the rows may be shuffled against one another.

Equations

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

theorem TauCeti.Probability.rowExchangeable_def {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} : RowExchangeable μ Y ↔ ∀ (π : ι → Equiv.Perm ℕ), MeasureTheory.Measure.map (fun (ω : Ω) (p : ι × ℕ) => Y (p.1, (π p.1) p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ι × ℕ) => Y p ω) μ

Characterization of row exchangeability by invariance under every family of row-wise time permutations.

theorem TauCeti.Probability.rowExchangeable_iff_forall_prodCongrRight_mem_finitary {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hY : AEMeasurable (fun (ω : Ω) (p : ι × ℕ) => Y p ω) μ) : RowExchangeable μ Y ↔ ∀ (π : ι → Equiv.Perm ℕ), Equiv.prodCongrRight π ∈ Equiv.Perm.finitary (ι × ℕ) → MeasureTheory.Measure.map (fun (ω : Ω) (p : ι × ℕ) => Y (p.1, (π p.1) p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ι × ℕ) => Y p ω) μ

It suffices to check row exchangeability for permutation families of finite total support. For a finite base measure and an a.e.-measurable array, invariance under every family π that moves only finitely many cells (a, k) implies invariance under arbitrary row-wise permutations.

theorem TauCeti.Probability.aemeasurable_arrayColumn {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} (hY : ∀ (p : ι × ℕ), AEMeasurable (Y p) μ) (k : ℕ) : AEMeasurable (arrayColumn Y k) μ

Every column of an array with a.e. measurable entries is a.e. measurable.

theorem TauCeti.Probability.RowExchangeable.fullyExchangeable_row {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} (h : RowExchangeable μ Y) (hY : ∀ (p : ι × ℕ), AEMeasurable (Y p) μ) (a : ι) : FullyExchangeable μ fun (k : ℕ) => Y (a, k)

Each row of a row exchangeable array is fully exchangeable.

theorem TauCeti.Probability.RowExchangeable.fullyExchangeable_arrayColumn {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} (h : RowExchangeable μ Y) (hY : ∀ (p : ι × ℕ), AEMeasurable (Y p) μ) : FullyExchangeable μ (arrayColumn Y)

The column process of a row exchangeable array is fully exchangeable. This is the diagonal case π = fun _ => σ of the definition.

theorem TauCeti.Probability.RowExchangeable.map_values {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} {β : Type u_4} [MeasurableSpace β] (h : RowExchangeable μ Y) (hY : ∀ (p : ι × ℕ), AEMeasurable (Y p) μ) {f : ι → α → β} (hf : ∀ (a : ι), Measurable (f a)) : RowExchangeable μ fun (p : ι × ℕ) (ω : Ω) => f p.1 (Y p ω)

Row exchangeability is closed under row-wise coordinatewise pushforward. Applying a measurable map, allowed to depend on the row, to every entry leaves the array row exchangeable.

theorem TauCeti.Probability.RowExchangeable.exchangeable_arrayColumn {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} (h : RowExchangeable μ Y) (hY : ∀ (p : ι × ℕ), AEMeasurable (Y p) μ) : Exchangeable μ (arrayColumn Y)

The exchangeability of the columns.

theorem TauCeti.Probability.RowExchangeable.measure_setOf_forall_pair_eq {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} (h : RowExchangeable μ Y) (hY : ∀ (p : ι × ℕ), AEMeasurable (Y p) μ) (F : Finset ι) {B₀ B₁ : ι → Set α} (hB₀ : ∀ a ∈ F, MeasurableSet (B₀ a)) (hB₁ : ∀ a ∈ F, MeasurableSet (B₁ a)) {c d : ι → ℕ} (hcd : ∀ a ∈ F, c a ≠ d a) : μ {ω : Ω | ∀ a ∈ F, Y (a, c a) ω ∈ B₀ a ∧ Y (a, d a) ω ∈ B₁ a} = μ {ω : Ω | ∀ a ∈ F, Y (a, 0) ω ∈ B₀ a ∧ Y (a, 1) ω ∈ B₁ a}

The two-time pattern lemma. Under row exchangeability the probability that every row of a finite set lands in two specified target sets at two prescribed times is the same for all choices of the two times, so long as the two times chosen in each row of that set are distinct.

This is the whole combinatorial input to the factorization theorem: each moment of the directing measure computes such a probability, with a different time pattern.

theorem TauCeti.Probability.RowExchangeable.ae_apply_pi_union {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} {lam : Ω → MeasureTheory.ProbabilityMeasure (ι → α)} [MeasureTheory.IsFiniteMeasure μ] (h : RowExchangeable μ Y) (hlam : MixedIIDWith μ (arrayColumn Y) lam) {F G : Finset ι} (hFG : Disjoint F G) {B : ι → Set α} (hB : ∀ (a : ι), a ∈ F ∨ a ∈ G → MeasurableSet (B a)) : ∀ᵐ (ω : Ω) ∂μ, ↑(lam ω) ((↑F ∪ ↑G).pi B) = ↑(lam ω) ((↑F).pi B) * ↑(lam ω) ((↑G).pi B)

Multiplicativity of the directing measure across disjoint sets of rows. If the columns of a row exchangeable array are mixed i.i.d. with mixing representative lam, then almost surely lam gives the box over F ∪ G the product of the masses of its two halves.

The proof is the second-moment computation described in the module docstring: the three integrals that make up the mean square of the difference are, by the two-block pattern lemma, one and the same array probability.

theorem TauCeti.Probability.RowExchangeable.ae_apply_pi_eq_prod {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} {lam : Ω → MeasureTheory.ProbabilityMeasure (ι → α)} [MeasureTheory.IsFiniteMeasure μ] (h : RowExchangeable μ Y) (hlam : MixedIIDWith μ (arrayColumn Y) lam) {B : ι → Set α} (F : Finset ι) (hB : ∀ a ∈ F, MeasurableSet (B a)) : ∀ᵐ (ω : Ω) ∂μ, ↑(lam ω) ((↑F).pi B) = ∏ a ∈ F, ↑(lam ω) {x : ι → α | x a ∈ B a}

The directing measure of a row exchangeable array factors over the rows. For a finite set F of rows and measurable target sets B, the mass that the mixing representative of the columns gives to the box {x | ∀ a ∈ F, x a ∈ B a} is almost surely the product of the masses it gives to the individual rows.

theorem TauCeti.Probability.RowExchangeable.measure_setOf_forall_mem_eq_lintegral_prod {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} {lam : Ω → MeasureTheory.ProbabilityMeasure (ι → α)} [MeasureTheory.IsFiniteMeasure μ] (h : RowExchangeable μ Y) (hlam : MixedIIDWith μ (arrayColumn Y) lam) {r : ℕ} {c : Fin r → ι × ℕ} (hc : Function.Injective c) {B : Fin r → Set α} (hB : ∀ (t : Fin r), MeasurableSet (B t)) : μ {ω : Ω | ∀ (t : Fin r), Y (c t) ω ∈ B t} = ∫⁻ (ω : Ω), ∏ t : Fin r, ↑(lam ω) {v : ι → α | v (c t).1 ∈ B t} ∂μ

Distinct cells of a row exchangeable array are conditionally independent given the mixing representative of its columns. The joint mass of finitely many pairwise distinct cells landing in prescribed measurable sets is the mixture, over the mixing representative, of the product of the masses that its individual row marginals give those sets.

This is the form the array law is consumed in downstream: an event that reads finitely many entries of the array, no two of them the same cell, has the mass of an independent product, once the mixing representative is integrated out. Distinctness is essential — a repeated cell is read twice and is of course not independent of itself.

The cells are grouped by their column index, where the mixture identity of the columns applies, and the row factorization TauCeti.Probability.RowExchangeable.ae_apply_pi_eq_prod splits each column's contribution into one factor per row it constrains. Injectivity enters twice: it makes the cells in a single column pairwise distinct as rows, and it makes the two nested products a single product over cells.

theorem TauCeti.Probability.RowExchangeable.exists_directing_pi_eq_prod {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure Ω} {Y : ι × ℕ → Ω → α} [StandardBorelSpace α] [Nonempty α] [MeasureTheory.IsFiniteMeasure μ] (h : RowExchangeable μ Y) (hY : ∀ (p : ι × ℕ), AEMeasurable (Y p) μ) : ∃ (lam : Ω → MeasureTheory.ProbabilityMeasure (ι → α)), ConditionallyIIDWith μ (arrayColumn Y) lam ∧ ∀ (B : ι → Set α) (F : Finset ι), (∀ a ∈ F, MeasurableSet (B a)) → ∀ᵐ (ω : Ω) ∂μ, ↑(lam ω) ((↑F).pi B) = ∏ a ∈ F, ↑(lam ω) {x : ι → α | x a ∈ B a}

De Finetti for a row exchangeable array. Over a countable row index and a nonempty standard Borel state space, the columns of a row exchangeable array are conditionally i.i.d., and their directing measure almost surely factors over the rows: conditionally on it, the rows are independent as well as identically distributed within each row.