Finitary actions and ergodicity for exchangeable arrays

The finitely supported permutations of ℕ act diagonally on array path space: one permutation relabels both array coordinates. For a jointly exchangeable array law, this action is ergodic exactly when the coordinate array is jointly dissociated. By the corner-tail theorem in Arrays.ZeroOne, these are also equivalent to triviality of the corner-tail σ-algebra.

Together with the corner-tail theorem this closes a representation-free triangle for jointly exchangeable arrays: joint dissociation, triviality of the corner tail, and ergodicity of the diagonal relabelling action are the same condition. It is stated on the law alone, for any measurable value space. Where the Aldous--Hoover representation theorem applies (a standard Borel value space), it is the condition singling out the ergodic form of that representation, in which the array is coded without a global coordinate.

Independent finitary row and column relabelings give the corresponding action for separately exchangeable laws. Finitary invariance already implies full joint or separate exchangeability, because finite-dimensional marginals determine the array law.

Main declarations

• TauCeti.Probability.instSMulFinitaryPermArray — the diagonal action of the finitary symmetric group TauCeti.FinitaryPerm (defined in Algebra/GroupAction/FiniteSupportPerm.lean) on array path space, one permutation relabelling both coordinates;
• TauCeti.Probability.instSMulFinitaryPermPairArray — independent finitary row and column relabelings, with SeparatelyExchangeable.smulInvariantMeasure_pair and its converse linking separate exchangeability to invariance of the law;
• TauCeti.Probability.jointlyExchangeable_of_smulInvariantMeasure — invariance under the diagonal finitary action gives joint exchangeability;
• TauCeti.Probability.separatelyExchangeable_iff_map_pairReindex_finitary — finite-support reindexings suffice to test separate exchangeability;
• TauCeti.Probability.preimage_pairReindex_eq_self_of_measurableSet_arrayTail — a corner-tail event is fixed by every pair of finitely supported axis permutations, not only by the diagonal ones;
• TauCeti.Probability.jointlyDissociated_iff_ergodicSMul — joint dissociation is ergodicity of that action for a jointly exchangeable array law;
• TauCeti.Probability.jointlyDissociated_iff_ergodicSMul_pair — joint dissociation is ergodicity of the independent row-and-column action for a separately exchangeable array law.

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.

The block-swap argument adapts Graphon/RelErgodicLinks.lean in cameronfreer/graphon (Apache 2.0) at commit 175911f9d2e053f2a33d966658dfce0e4ae2811d.

The diagonal finitary-permutation action

@[instance_reducible]

instance TauCeti.Probability.instSMulFinitaryPermArray {α : Type u_1} : SMul FinitaryPerm (ℕ × ℕ → α)

Finitely supported vertex permutations act diagonally on array path space, by the inverse permutation so that reindexing is a left action.

Equations

• TauCeti.Probability.instSMulFinitaryPermArray = { smul := fun (g : TauCeti.FinitaryPerm) (x : ℕ × ℕ → α) => TauCeti.Probability.pairReindex g.toPerm⁻¹ g.toPerm⁻¹ x }

theorem TauCeti.Probability.finitaryPerm_smul_array_def {α : Type u_1} (g : FinitaryPerm) (x : ℕ × ℕ → α) : g • x = pairReindex g.toPerm⁻¹ g.toPerm⁻¹ x

The diagonal array action written as an explicit pair reindexing.

@[simp]

theorem TauCeti.Probability.finitaryPerm_smul_array_apply {α : Type u_1} (g : FinitaryPerm) (x : ℕ × ℕ → α) (p : ℕ × ℕ) : (g • x) p = x (g.toPerm⁻¹ p.1, g.toPerm⁻¹ p.2)

The diagonal array action relabels both coordinates by the inverse permutation.

@[instance_reducible]

instance TauCeti.Probability.instMulActionFinitaryPermArray {α : Type u_1} : MulAction FinitaryPerm (ℕ × ℕ → α)

Equations

• TauCeti.Probability.instMulActionFinitaryPermArray = { toSMul := TauCeti.Probability.instSMulFinitaryPermArray, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

instance TauCeti.Probability.instSMulFinitaryPermPairArray {α : Type u_1} : SMul (FinitaryPerm × FinitaryPerm) (ℕ × ℕ → α)

Independent finitely supported permutations act on the two axes of an array. The inverse permutations make reindexing a left action.

Equations

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

@[simp]

theorem TauCeti.Probability.finitaryPermPair_smul_array_apply {α : Type u_1} (g : FinitaryPerm × FinitaryPerm) (x : ℕ × ℕ → α) (p : ℕ × ℕ) : (g • x) p = x (g.1.toPerm⁻¹ p.1, g.2.toPerm⁻¹ p.2)

The separate action is coordinate reindexing on each axis.

@[instance_reducible]

instance TauCeti.Probability.instMulActionFinitaryPermPairArray {α : Type u_1} : MulAction (FinitaryPerm × FinitaryPerm) (ℕ × ℕ → α)

Independent row and column permutations compose as a left action on arrays.

Equations

• TauCeti.Probability.instMulActionFinitaryPermPairArray = { toSMul := TauCeti.Probability.instSMulFinitaryPermPairArray, mul_smul := ⋯, one_smul := ⋯ }

instance TauCeti.Probability.instMeasurableConstSMulFinitaryPermArray {α : Type u_1} [MeasurableSpace α] : MeasurableConstSMul FinitaryPerm (ℕ × ℕ → α)

theorem TauCeti.Probability.JointlyExchangeable.smulInvariantMeasure {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : MeasureTheory.SMulInvariantMeasure FinitaryPerm (ℕ × ℕ → α) ρ

A jointly exchangeable array law is invariant under diagonal finitary relabeling.

Corner-tail events are invariant

theorem TauCeti.Probability.preimage_pairReindex_eq_self_of_measurableSet_arrayTail {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ × ℕ → α)} (hs : MeasurableSet s) {σ τ : Equiv.Perm ℕ} (hσ : (MulAction.fixedBy ℕ σ)ᶜ.Finite) (hτ : (MulAction.fixedBy ℕ τ)ᶜ.Finite) : pairReindex σ τ ⁻¹' s = s

Every corner-tail event is fixed by a finitely supported separate relabelling: permuting the two axes independently by finitely supported permutations fixes every sufficiently far corner, which is all that a corner-tail event reads.

theorem TauCeti.Probability.preimage_finitaryPerm_smul_array_eq_self_of_measurableSet_arrayTail {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ × ℕ → α)} (hs : MeasurableSet s) (g : FinitaryPerm) : (fun (x : ℕ × ℕ → α) => g • x) ⁻¹' s = s

Every corner-tail event is fixed by the diagonal action: a finitely supported relabelling of both coordinates changes only finitely many entries, and a corner-tail event does not read them.

The block-swap zero-one argument

theorem TauCeti.Probability.ergodicSMul_of_jointlyDissociated {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsZeroOrProbabilityMeasure ρ] [MeasureTheory.SMulInvariantMeasure FinitaryPerm (ℕ × ℕ → α) ρ] (hdiss : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : ErgodicSMul FinitaryPerm (ℕ × ℕ → α) ρ

Joint dissociation makes the diagonal finitary-permutation action ergodic, for a law invariant under that action; joint exchangeability supplies the invariance (JointlyExchangeable.smulInvariantMeasure).

theorem TauCeti.Probability.jointlyDissociated_of_ergodicSMul {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsZeroOrProbabilityMeasure ρ] [ErgodicSMul FinitaryPerm (ℕ × ℕ → α) ρ] (hexch : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p

Ergodicity of the diagonal finitary-permutation action makes a jointly exchangeable array law jointly dissociated.

theorem TauCeti.Probability.jointlyDissociated_iff_ergodicSMul {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsZeroOrProbabilityMeasure ρ] (hexch : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : (JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ↔ ErgodicSMul FinitaryPerm (ℕ × ℕ → α) ρ

Joint dissociation is ergodicity for a jointly exchangeable array law. The acting group simultaneously applies one finitely supported permutation to both coordinates.

Finitary tests and the separate action

theorem TauCeti.Probability.jointlyExchangeable_of_smulInvariantMeasure {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] [MeasureTheory.SMulInvariantMeasure FinitaryPerm (ℕ × ℕ → α) ρ] : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p

A finite law on ℕ × ℕ → α invariant under the finitary diagonal action is jointly exchangeable: invariant under the diagonal relabelling by every permutation of ℕ.

theorem TauCeti.Probability.separatelyExchangeable_of_map_pairReindex_finitary {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (h : ∀ (σ τ : Equiv.Perm ℕ), (MulAction.fixedBy ℕ σ)ᶜ.Finite → (MulAction.fixedBy ℕ τ)ᶜ.Finite → MeasureTheory.Measure.map (pairReindex σ τ) ρ = ρ) : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p

Finitely supported permutations already test separate exchangeability. A finite law on array path space invariant under every pair of finitely supported axis relabellings is invariant under every pair of axis relabellings: the law is determined by its finite-dimensional marginals, and on finitely many indices any permutation agrees with a finitely supported one.

This is the separate counterpart of jointlyExchangeable_of_smulInvariantMeasure; it is stated through the two permutations rather than through a group action because the two axes are relabelled independently.

theorem TauCeti.Probability.separatelyExchangeable_iff_map_pairReindex_finitary {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] : (SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ↔ ∀ (σ τ : Equiv.Perm ℕ), (MulAction.fixedBy ℕ σ)ᶜ.Finite → (MulAction.fixedBy ℕ τ)ᶜ.Finite → MeasureTheory.Measure.map (pairReindex σ τ) ρ = ρ

A finite law on array path space is separately exchangeable if and only if it is invariant under every pair of finitely supported axis relabellings.

theorem TauCeti.Probability.jointlyExchangeable_iff_smulInvariantMeasure {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] : (JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ↔ MeasureTheory.SMulInvariantMeasure FinitaryPerm (ℕ × ℕ → α) ρ

A finite law is jointly exchangeable if and only if it is invariant under the finitary diagonal action.

instance TauCeti.Probability.instMeasurableConstSMulFinitaryPermPairArray {α : Type u_1} [MeasurableSpace α] : MeasurableConstSMul (FinitaryPerm × FinitaryPerm) (ℕ × ℕ → α)

Each independent finitary relabeling is measurable.

theorem TauCeti.Probability.SeparatelyExchangeable.smulInvariantMeasure_pair {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : MeasureTheory.SMulInvariantMeasure (FinitaryPerm × FinitaryPerm) (ℕ × ℕ → α) ρ

A separately exchangeable array law is invariant under the separate finitary action.

theorem TauCeti.Probability.separatelyExchangeable_of_smulInvariantMeasure_pair {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] [MeasureTheory.SMulInvariantMeasure (FinitaryPerm × FinitaryPerm) (ℕ × ℕ → α) ρ] : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p

Finitary invariance under independent row and column relabelings implies separate exchangeability, by finite-dimensional determinacy of the array law.

theorem TauCeti.Probability.preimage_finitaryPermPair_smul_array_eq_self_of_measurableSet_arrayTail {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ × ℕ → α)} (hs : MeasurableSet s) (g : FinitaryPerm × FinitaryPerm) : (fun (x : ℕ × ℕ → α) => g • x) ⁻¹' s = s

A corner-tail event is fixed by every separate finitary relabeling.

theorem TauCeti.Probability.jointlyDissociated_iff_ergodicSMul_pair {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsZeroOrProbabilityMeasure ρ] (hexch : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : (JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ↔ ErgodicSMul (FinitaryPerm × FinitaryPerm) (ℕ × ℕ → α) ρ

Joint dissociation is ergodicity for the independent row-and-column action on a separately exchangeable array law.