The finitely-supported relabeling action and its invariant σ-algebra (R3c step 1, #106)

The generic invariant-action layer for the relational extremality theory: the group of finitely supported sortwise permutations of ℕ, the σ-algebra of strictly invariant events, and ergodicity of an exchangeable relational law:

• RelSignature.SortwiseFinSupp — a sortwise family of permutations with common finite support, with closure under composition and inverse;
• RelStructure.invariantAlgebra — the measurable sets strictly invariant under every finitely supported sortwise relabeling;
• InfiniteRelExchangeableLaw.IsErgodic — every invariant event has law-measure 0 or 1.

This mirrors the undirected Graphon/InvariantAction.lean. The arrows into the dissociation triangle live in Graphon.RelErgodicLinks, the ergodic ↔ extreme-point theorem in Graphon.RelErgodicExtreme, and the five-way equivalence in Graphon.RelExtremality; invariantProbabilityMeasures (below) is the convex set those results are stated over, with the finitary-invariance bridge mem_invariantProbabilityMeasures_iff_exists_law identifying it with the laws of InfiniteRelExchangeableLaw.

Finitely supported sortwise permutations

def RelSignature.SortwiseFinSupp {S : RelSignature} (σ : S.Srt → Equiv.Perm ℕ) : Prop

A sortwise family of permutations with common finite support: beyond some N, every sort's permutation is the identity.

Equations

• RelSignature.SortwiseFinSupp σ = ∃ (N : ℕ), ∀ (s : S.Srt) (x : ℕ), N ≤ x → (σ s) x = x

theorem RelSignature.SortwiseFinSupp.one {S : RelSignature} : SortwiseFinSupp fun (x : S.Srt) => 1

theorem RelSignature.SortwiseFinSupp.mul {S : RelSignature} {σ τ : S.Srt → Equiv.Perm ℕ} (hσ : SortwiseFinSupp σ) (hτ : SortwiseFinSupp τ) : SortwiseFinSupp fun (s : S.Srt) => σ s * τ s

theorem RelSignature.SortwiseFinSupp.inv {S : RelSignature} {σ : S.Srt → Equiv.Perm ℕ} (hσ : SortwiseFinSupp σ) : SortwiseFinSupp fun (s : S.Srt) => (σ s)⁻¹

def RelSignature.sortwiseFinSuppSubgroup (S : RelSignature) : Subgroup (S.Srt → Equiv.Perm ℕ)

The finitely supported sortwise permutations, as a subgroup of the full sortwise permutation group. The closure proofs are exactly SortwiseFinSupp.one, .mul, and .inv.

This is the symmetry group the relational layer actually acts by. Stating it as a subgroup — rather than carrying a raw permutation family plus a SortwiseFinSupp side condition — matters downstream: the constructions there provide, and the arguments there use, closure under finitely supported relabelings only; closure of a chosen countable event family under the full permutation group is neither constructed nor countable in general.

Equations

• S.sortwiseFinSuppSubgroup = { carrier := {σ : S.Srt → Equiv.Perm ℕ | RelSignature.SortwiseFinSupp σ}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[reducible, inline]

abbrev RelSignature.FinSuppPerm (S : RelSignature) : Subgroup (S.Srt → Equiv.Perm ℕ)

A finitely supported sortwise permutation family, bundled with its support bound. A Group by construction, so identity, composition, and inverses are all available without side conditions.

Equations

• S.FinSuppPerm = S.sortwiseFinSuppSubgroup

@[simp]

theorem RelSignature.mem_sortwiseFinSuppSubgroup {S : RelSignature} {σ : S.Srt → Equiv.Perm ℕ} : σ ∈ S.sortwiseFinSuppSubgroup ↔ SortwiseFinSupp σ

theorem RelSignature.FinSuppPerm.sortwiseFinSupp {S : RelSignature} (σ : ↥S.FinSuppPerm) : SortwiseFinSupp ↑σ

The invariant σ-algebra

@[implicit_reducible]

def RelSignature.RelStructure.invariantAlgebra {S : RelSignature} : MeasurableSpace (S.RelStructure S.Vinfinite)

The invariant σ-algebra: measurable sets strictly invariant under every finitely supported sortwise relabeling.

Equations

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

theorem RelSignature.RelStructure.invariantAlgebra_le {S : RelSignature} : invariantAlgebra ≤ inferInstance

Ergodicity

def RelSignature.InfiniteRelExchangeableLaw.IsErgodic {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : Prop

Ergodicity of an exchangeable relational law: every event strictly invariant under all finitely supported sortwise relabelings has law-measure 0 or 1.

Equations

• M.IsErgodic = ∀ (A : Set (S.RelStructure S.Vinfinite)), MeasurableSet A → ↑M.law A = 0 ∨ ↑M.law A = 1

The invariant probability simplex

def RelSignature.invariantProbabilityMeasures (S : RelSignature) : Set (MeasureTheory.Measure (S.RelStructure S.Vinfinite))

The invariant probability measures: the convex set of probability measures on the infinite structure space invariant under every finitely supported sortwise relabeling. By mem_invariantProbabilityMeasures_iff_exists_law (finite-restriction extensionality), these are exactly the laws of InfiniteRelExchangeableLaw — finitary invariance already implies invariance under every sortwise permutation.

Equations

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

theorem RelSignature.exists_finSupp_perm_extend {k : ℕ} (g : Fin k ↪ ℕ) : ∃ (π : Equiv.Perm ℕ) (N : ℕ), (∀ (x : ℕ), N ≤ x → π x = x) ∧ ∀ (a : Fin k), π ↑a = g a

Every injection of a finite window extends to a finitely supported permutation — the finitary strengthening of exists_perm_extend, by induction on the window with one transposition per step.

theorem RelSignature.map_relabel_of_mem_invariantProbabilityMeasures {S : RelSignature} [Fintype S.Srt] {ν : MeasureTheory.Measure (S.RelStructure S.Vinfinite)} (hν : ν ∈ S.invariantProbabilityMeasures) (σ : S.Srt → Equiv.Perm ℕ) : MeasureTheory.Measure.map (RelStructure.relabel σ) ν = ν

Finitary invariance implies full sortwise invariance: a probability measure invariant under every finitely supported sortwise relabeling is invariant under every sortwise relabeling — by finite-restriction extensionality, since on each finite window an arbitrary permutation family agrees with a finitely supported one.

theorem RelSignature.mem_invariantProbabilityMeasures_iff_exists_law {S : RelSignature} [Fintype S.Srt] {ν : MeasureTheory.Measure (S.RelStructure S.Vinfinite)} : ν ∈ S.invariantProbabilityMeasures ↔ ∃ (M : S.InfiniteRelExchangeableLaw), ↑M.law = ν

The invariant simplex is exactly the exchangeable laws (packaging/range lemma): a measure is finitarily invariant and probability iff it is the law of an infinite exchangeable relational law.