Ergodic exchangeable relational laws are the extreme points (R3c step 2, #106)

Port of Mathlib/Dynamics/Ergodic/Extreme.lean from a single measure-preserving self-map to the countable group of finitely supported sortwise relabelings acting on RelStructure S (Vinfinite S):

• RelSignature.countable_setOf_sortwiseFinSupp — with finitely many sorts, the finitely supported sortwise permutation families form a countable set;
• InfiniteRelExchangeableLaw.measure_zero_or_one_of_ae_invariant — the zero-one law upgrades from strictly invariant to almost-everywhere invariant events, via the countable invariant hull ⋃ σ, relabel σ ⁻¹' E over the relabeling group;
• InfiniteRelExchangeableLaw.eq_of_absolutelyContinuous — a relabeling-invariant probability measure absolutely continuous with respect to an ergodic exchangeable law is equal to it (the Radon–Nikodym derivative is a.e. 1 by the zero-one law);
• InfiniteRelExchangeableLaw.isErgodic_iff_mem_extremePoints — the headline: ergodicity of an exchangeable relational law is equivalent to extremality among the relabeling-invariant probability measures.

Composition laws for relabeling

theorem RelSignature.RelStructure.relabel_relabel {S : RelSignature} {V : S.Srt → Type u_1} (σ τ : (s : S.Srt) → Equiv.Perm (V s)) (x : S.RelStructure V) : relabel σ (relabel τ x) = relabel (fun (s : S.Srt) => τ s * σ s) x

Relabelings compose contravariantly: relabeling by τ and then by σ is relabeling by the pointwise product fun s => τ s * σ s (definitional, via RelStructure.comap_comp).

theorem RelSignature.RelStructure.relabel_one {S : RelSignature} {V : S.Srt → Type u_1} (x : S.RelStructure V) : relabel (fun (s : S.Srt) => 1) x = x

Relabeling by the identity family is the identity (definitional).

Countability of the finitely supported relabeling group

theorem RelSignature.countable_setOf_sortwiseFinSupp {S : RelSignature} [Fintype S.Srt] : {σ : S.Srt → Equiv.Perm ℕ | SortwiseFinSupp σ}.Countable

With finitely many sorts, the finitely supported sortwise permutation families form a countable set: a family supported below N is determined by its values on Fin N, so each level of the exhaustion injects into the countable type S.Srt → Fin N → ℕ.

The zero-one law for almost invariant events

theorem RelSignature.InfiniteRelExchangeableLaw.measure_zero_or_one_of_ae_invariant {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) (hM : M.IsErgodic) {E : Set (S.RelStructure S.Vinfinite)} (hEm : MeasurableSet E) (hE : ∀ (σ : S.Srt → Equiv.Perm ℕ), SortwiseFinSupp σ → RelStructure.relabel σ ⁻¹' E =ᵐ[↑M.law] E) : ↑M.law E = 0 ∨ ↑M.law E = 1

Almost invariant events obey the zero-one law: if E is measurable and a.e. invariant under every finitely supported sortwise relabeling, then its invariant hull — the union of its preimages over the countable relabeling group — is measurable, strictly invariant, and a.e. equal to E, so ergodicity forces E itself to be null or conull.

Absolute continuity and ergodicity

theorem RelSignature.InfiniteRelExchangeableLaw.eq_of_absolutelyContinuous {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) (hM : M.IsErgodic) {ν : MeasureTheory.Measure (S.RelStructure S.Vinfinite)} [MeasureTheory.IsProbabilityMeasure ν] (hinv : ∀ (σ : S.Srt → Equiv.Perm ℕ), SortwiseFinSupp σ → MeasureTheory.Measure.map (RelStructure.relabel σ) ν = ν) (hac : ν.AbsolutelyContinuous ↑M.law) : ν = ↑M.law

An invariant probability measure absolutely continuous with respect to an ergodic exchangeable law equals it. The Radon–Nikodym derivative is a.e. invariant under each relabeling (MeasurePreserving.rnDeriv_comp_aeEq), so its sub- and super-level sets at 1 are a.e. invariant, hence null or conull by the zero-one upgrade; strict monotonicity of the set integral rules out the conull cases, so the derivative is a.e. 1.

The extreme-point characterization

@[simp]

theorem RelSignature.InfiniteRelExchangeableLaw.law_mem_invariantProbabilityMeasures {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : ↑M.law ∈ S.invariantProbabilityMeasures

The law of an exchangeable relational structure is an invariant probability measure: membership in the candidate set of the extreme-point characterization.

theorem RelSignature.InfiniteRelExchangeableLaw.isErgodic_of_mem_extremePoints {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) (h : ↑M.law ∈ Set.extremePoints ENNReal S.invariantProbabilityMeasures) : M.IsErgodic

An extreme invariant probability measure is ergodic: if some strictly invariant event had intermediate measure, conditioning on it and its complement would exhibit the law as a proper convex combination of two distinct invariant probability measures.

theorem RelSignature.InfiniteRelExchangeableLaw.mem_extremePoints_of_isErgodic {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) (hM : M.IsErgodic) : ↑M.law ∈ Set.extremePoints ENNReal S.invariantProbabilityMeasures

An ergodic exchangeable relational law is an extreme point of the relabeling-invariant probability measures: any measure appearing in a proper convex decomposition is absolutely continuous, hence equal to the law by eq_of_absolutelyContinuous.

theorem RelSignature.InfiniteRelExchangeableLaw.isErgodic_iff_mem_extremePoints {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) : M.IsErgodic ↔ ↑M.law ∈ Set.extremePoints ENNReal S.invariantProbabilityMeasures

Ergodicity is extremality (headline of R3c step 2): an exchangeable relational law is ergodic for the finitely supported sortwise relabeling group if and only if it is an extreme point of the set of relabeling-invariant probability measures on the infinite structure space.