Exchangeable laws and ergodicity of the finitely supported permutation action

An exchangeable path law is invariant under the group of finitely supported permutations of the time index. This file records the resulting group action on path space and identifies ergodicity of that action with triviality of the exchangeable σ-algebra:

(∀ s, MeasurableSet[exchangeableSigma α] s → ρ s = 0 ∨ ρ s = 1)
  ↔  ErgodicSMul FinitaryPerm (ℕ → α) ρ

(exchangeableSigma_trivial_iff_ergodicSMul).

The two sides are not the same statement. exchangeableSigma collects the events that are exactly fixed by every finitely supported reindexing, while Mathlib's ErgodicSMul quantifies over the almost invariant events. The bridge is the countability of the acting group: an almost invariant event agrees almost everywhere with an exchangeable one (exists_measurableSet_exchangeableSigma_ae_eq), by the saturation argument of TauCeti.MeasureTheory.exists_smul_invariant_ae_eq.

⚠ The permutation action here is the one on the time index, and ergodicity for it is a different statement from ergodicity of the one-sided shift, which concerns the smaller σ-algebra of shift-invariant events. For an i.i.d. product law both hold: ergodic_shift_infinitePi_const is the shift form and ergodicSMul_infinitePi_const below is the permutation form.

Main declarations

• instSMulFinitaryPermPath — the path action of the finitary symmetric group TauCeti.FinitaryPerm (defined in Algebra/GroupAction/FiniteSupportPerm.lean) on ℕ → α by finitary reindexing of the time index, (g • x) n = x (g⁻¹ n);
• ExchangeableLaw.smulInvariantMeasure — an exchangeable path law is invariant under it.

Main results

• exchangeableLaw_iff_smulInvariantMeasure — a finite law is exchangeable exactly when it is invariant under the finitely supported permutation action.
• exists_measurableSet_exchangeableSigma_ae_eq — an almost invariant event agrees almost everywhere with an exchangeableSigma-measurable one.
• exchangeableSigma_trivial_iff_ergodicSMul — the zero-one law for exchangeableSigma is ergodicity of the finitely supported permutation action.
• ergodicSMul_infinitePi_const — Hewitt–Savage in ergodic form: the finitely supported permutations act ergodically on an i.i.d. product law.

This discharges the ErgodicSMul interface, item (1) ⇔ (2) of the zero-one/ergodic/extreme interfaces of Layer 6 of the Exchangeability roadmap. No material is adapted from cameronfreer/exchangeability.

@[instance_reducible]

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

The finitely supported time permutations act on path space by reindexing along the inverse, (g • x) n = x (g⁻¹ n). The inverse is what makes reindexing a left action.

Equations

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

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

@[simp]

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

@[instance_reducible]

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

Equations

• TauCeti.Probability.instMulActionFinitaryPermPath = { toSMul := TauCeti.Probability.instSMulFinitaryPermPath, mul_smul := ⋯, one_smul := ⋯ }

theorem TauCeti.Probability.preimage_finitaryPerm_smul_path {α : Type u_1} (g : FinitaryPerm) (s : Set (ℕ → α)) : (fun (x : ℕ → α) => g • x) ⁻¹' s = permReindex g.toPerm⁻¹ ⁻¹' s

Reindexing along a permutation is the same map whether it is read as an action of FinitaryPerm or written out with permReindex. This is the form in which the exchangeable σ-algebra, which is stated with permReindex, meets the action.

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

theorem TauCeti.Probability.ExchangeableLaw.smulInvariantMeasure {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ExchangeableLaw ρ) : MeasureTheory.SMulInvariantMeasure FinitaryPerm (ℕ → α) ρ

An exchangeable path law is invariant under the finitely supported permutation action.

theorem TauCeti.Probability.exchangeableLaw_of_smulInvariantMeasure {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] [MeasureTheory.SMulInvariantMeasure FinitaryPerm (ℕ → α) ρ] : ExchangeableLaw ρ

Finitely supported permutations already test exchangeability. A finite law on ℕ → α invariant under the finitary permutation action is exchangeable: invariant under the relabelling by every permutation of ℕ.

The converse of ExchangeableLaw.smulInvariantMeasure; the sequence form of the reduction jointlyExchangeable_of_smulInvariantMeasure for arrays in Arrays/Extreme/Basic.lean.

theorem TauCeti.Probability.exchangeableLaw_iff_smulInvariantMeasure {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] : ExchangeableLaw ρ ↔ MeasureTheory.SMulInvariantMeasure FinitaryPerm (ℕ → α) ρ

A finite law on ℕ → α is exchangeable if and only if it is invariant under the finitary permutation action.

theorem TauCeti.Probability.exists_measurableSet_exchangeableSigma_ae_eq {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} {s : Set (ℕ → α)} (hs : MeasurableSet s) (hinv : ∀ (π : Equiv.Perm ℕ), (MulAction.fixedBy ℕ π)ᶜ.Finite → permReindex π ⁻¹' s =ᵐ[ρ] s) : ∃ (t : Set (ℕ → α)), MeasurableSet t ∧ t =ᵐ[ρ] s

An almost invariant path event agrees almost everywhere with an exchangeable event.

The exchangeable σ-algebra is defined by exact invariance under finitely supported reindexings, while a.e. invariance is what Mathlib's ergodicity predicate supplies. Because the group of finitely supported permutations of ℕ is countable, the two agree modulo null sets: the saturation of s under the whole group is an exchangeable event almost equal to s.

theorem TauCeti.Probability.measure_eq_zero_or_one_of_ergodicSMul {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] [ErgodicSMul FinitaryPerm (ℕ → α) ρ] {s : Set (ℕ → α)} (hs : MeasurableSet s) : ρ s = 0 ∨ ρ s = 1

Ergodicity of the permutation action makes every exchangeable event trivial.

This is the easy direction: an exchangeableSigma-measurable event is exactly invariant, hence almost invariant.

theorem TauCeti.Probability.ergodicSMul_of_exchangeableSigma_trivial {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hρ : ExchangeableLaw ρ) (htrivial : ∀ (s : Set (ℕ → α)), MeasurableSet s → ρ s = 0 ∨ ρ s = 1) : ErgodicSMul FinitaryPerm (ℕ → α) ρ

Triviality of the exchangeable σ-algebra makes the permutation action ergodic.

This is the substantive direction: the a.e.-invariant events Mathlib's predicate quantifies over are handled through exists_measurableSet_exchangeableSigma_ae_eq, which is where countability of the acting group is used.

theorem TauCeti.Probability.exchangeableSigma_trivial_iff_ergodicSMul {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hρ : ExchangeableLaw ρ) : (∀ (s : Set (ℕ → α)), MeasurableSet s → ρ s = 0 ∨ ρ s = 1) ↔ ErgodicSMul FinitaryPerm (ℕ → α) ρ

The zero-one law for exchangeableSigma is ergodicity of the finitely supported permutation action.

Both sides say that an exchangeable path law admits no nontrivial permutation-invariant event; the content of the equivalence is that it does not matter whether "invariant" is read exactly, as in the σ-algebra exchangeableSigma α, or almost everywhere, as in Mathlib's ErgodicSMul.

⚠ The action is by finitely supported permutations of the time index. This is not one-sided shift ergodicity: the shift-invariant events form a smaller σ-algebra, so the two statements are not interchangeable.

theorem TauCeti.Probability.ergodicSMul_infinitePi_const {α : Type u_1} [MeasurableSpace α] (P : MeasureTheory.ProbabilityMeasure α) : ErgodicSMul FinitaryPerm (ℕ → α) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P)

Hewitt–Savage in ergodic form. The finitely supported permutations of the time index act ergodically on an i.i.d. product law P^{⊗ℕ}.

This is the zero-one law exchangeableSigma_trivial_of_infinitePi read through exchangeableSigma_trivial_iff_ergodicSMul. It is the permutation-action counterpart of the shift ergodicity recorded by ergodic_shift_infinitePi_const.