The finite-permutation action and its invariant σ-algebra (issue #59, part 1)

Infrastructure for the ergodic-decomposition form of extremality: the empirical limit limitGraphon is invariant under every finitely supported relabeling of ℕ, hence is measurable with respect to the permutation-invariant σ-algebra.

def InfiniteGraph.FinSupp (σ : Equiv.Perm ℕ) : Prop

A permutation of ℕ is finitely supported if it fixes all sufficiently large naturals.

Equations

• InfiniteGraph.FinSupp σ = ∃ (N : ℕ), ∀ (x : ℕ), N ≤ x → σ x = x

noncomputable def InfiniteGraph.relabelFin (σ : Equiv.Perm ℕ) (N n : ℕ) (hN : ∀ (x : ℕ), N ≤ x → σ x = x) (hn : N ≤ n + 1) : Equiv.Perm (Fin (n + 1))

A finitely supported permutation, restricted to a large enough initial segment, as a permutation of Fin (n+1).

Equations

• InfiniteGraph.relabelFin σ N n hN hn = { toFun := fun (a : Fin (n + 1)) => ⟨σ ↑a, ⋯⟩, invFun := fun (a : Fin (n + 1)) => ⟨(Equiv.symm σ) ↑a, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem InfiniteGraph.relabelFin_apply (σ : Equiv.Perm ℕ) (N n : ℕ) (hN : ∀ (x : ℕ), N ≤ x → σ x = x) (hn : N ≤ n + 1) (a : Fin (n + 1)) : ↑((relabelFin σ N n hN hn) a) = σ ↑a

theorem InfiniteGraph.restrictFin_relabel_eq_comap (σ : Equiv.Perm ℕ) {N : ℕ} (hN : ∀ (x : ℕ), N ≤ x → σ x = x) {n : ℕ} (hn : N ≤ n + 1) (G : InfiniteGraph) : restrictFin (n + 1) (relabel σ G) = SimpleGraph.comap (⇑(relabelFin σ N n hN hn)) (restrictFin (n + 1) G)

The restriction of a relabeled infinite graph is the relabeled restriction (for a window past the support).

theorem InfiniteGraph.empiricalGraphon_relabel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (σ : Equiv.Perm ℕ) {N : ℕ} (hN : ∀ (x : ℕ), N ≤ x → σ x = x) {n : ℕ} (hn : N ≤ n + 1) (G : InfiniteGraph) : GraphonSpace.empiricalGraphon n (relabel σ G) = GraphonSpace.empiricalGraphon n G

The empirical graphon is invariant under a finite relabeling, past its support.

def InfiniteGraph.invariantAlgebra : MeasurableSpace InfiniteGraph

The permutation-invariant σ-algebra: Borel events fixed by every finitely supported relabeling.

Equations

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

theorem InfiniteGraph.invariantAlgebra_le : invariantAlgebra ≤ inferInstance

theorem GraphonSpace.tendsto_empiricalGraphon_relabel_iff {σ : Equiv.Perm ℕ} (hfs : InfiniteGraph.FinSupp σ) (G : InfiniteGraph) (x : StandardGraphonSpace) : Filter.Tendsto (fun (n : ℕ) => empiricalGraphon n (InfiniteGraph.relabel σ G)) Filter.atTop (nhds x) ↔ Filter.Tendsto (fun (n : ℕ) => empiricalGraphon n G) Filter.atTop (nhds x)

Convergence of the empirical graphons is invariant under a finite relabeling.

theorem GraphonSpace.mem_empiricalConvergenceSet_relabel_iff {σ : Equiv.Perm ℕ} (hfs : InfiniteGraph.FinSupp σ) (G : InfiniteGraph) : InfiniteGraph.relabel σ G ∈ empiricalConvergenceSet ↔ G ∈ empiricalConvergenceSet

theorem GraphonSpace.limitGraphon_relabel {σ : Equiv.Perm ℕ} (hfs : InfiniteGraph.FinSupp σ) (G : InfiniteGraph) : limitGraphon (InfiniteGraph.relabel σ G) = limitGraphon G

The empirical limit is invariant under every finite relabeling — pointwise.

theorem GraphonSpace.measurable_limitGraphon_invariantAlgebra : Measurable limitGraphon

The empirical limit is invariant-measurable: its preimages are Borel events fixed by every finite relabeling (limitGraphon_relabel).

def Graphon.InfiniteExchangeableGraphLaw.IsErgodic (M : InfiniteExchangeableGraphLaw) : Prop

Ergodicity: every permutation-invariant Borel event has M.law-measure 0 or 1.

Equations

• M.IsErgodic = ∀ (s : Set InfiniteGraph), MeasurableSet s → ↑M.law s = 0 ∨ ↑M.law s = 1