Ergodic decomposition of exchangeable graph laws (issue #59, part 2)

The fixed-fiber ergodicity argument: a permutation-invariant event has M.law-measure 0 or 1, giving the ergodicity links of the DJ 5.5 / #59 equivalence.

Infrastructure:

• InfiniteGraph.FinSupp.one / .inv / .mul — the finitely supported permutations of ℕ are closed under identity, inverse, and composition (a subgroup of Equiv.Perm ℕ);
• InfiniteGraph.swapBlock k — the involution swapping the block [0, k) with [k, 2k) (fixing everything past 2k), a finitely supported permutation;
• InfiniteGraph.restrictFin_relabel_swapBlock — relabeling by swapBlock k moves the initial k-window onto the k-tail window: restrictFin k (relabel (swapBlock k) G) = restrictFin k (drop k G); hence
• InfiniteGraph.relabel_swapBlock_preimage_mem_tailAlgebra — the swapBlock k relabeling carries every initialAlgebra k event into a tailAlgebra k event;
• Graphon.InfiniteExchangeableGraphLaw.exists_initialAlgebra_measure_symmDiff_lt — in-measure approximation by initial cylinders: every Borel event is approximated in M.law-measure by an event depending on only finitely many vertices (via exists_measure_symmDiff_lt_of_generateFrom_isSetRing, the initial cylinders being a set-ring that generates the Borel σ-algebra).

Fixed-fiber ergodicity:

• InfiniteGraph.vertexTailAlgebra_le_invariantAlgebra — every vertex-tail event is finite-permutation invariant;
• Graphon.InfiniteExchangeableGraphLaw.measure_invariant_eq_zero_or_one_of_restrictionIndependent — under restriction independence, every invariant event is null or conull (the 4ε approximate-independence estimate);
• isErgodic_of_restrictionIndependent and vertexTailTrivial_of_isErgodic — the two new links closing RestrictionIndependent ⟹ IsErgodic ⟹ VertexTailTrivial.

Packaging and the generation statement:

• isErgodic_iff_isDissociated (and the restriction-independent / vertex-tail corollaries) and tfae_ergodic_extremality — the six-way ergodic-decomposition form of Diaconis–Janson Theorem 5.5;
• invariant_ae_eq_limitGraphon_classifier — limitGraphon generates the invariant σ-algebra modulo null sets: every invariant event agrees M.law-a.e. with a limitGraphon-preimage (the barycenter / fiber-ergodicity identification).

The finitely supported permutations form a subgroup

theorem InfiniteGraph.FinSupp.one : FinSupp 1

The identity is finitely supported.

theorem InfiniteGraph.FinSupp.inv {σ : Equiv.Perm ℕ} (hσ : FinSupp σ) : FinSupp σ⁻¹

The inverse of a finitely supported permutation is finitely supported.

theorem InfiniteGraph.FinSupp.mul {σ τ : Equiv.Perm ℕ} (hσ : FinSupp σ) (hτ : FinSupp τ) : FinSupp (σ * τ)

The composition of two finitely supported permutations is finitely supported.

The block swap [0, k) ↔ [k, 2k)

def InfiniteGraph.swapBlockFun (k i : ℕ) : ℕ

The block-swap function: exchange [0, k) with [k, 2k), fixing the rest.

Equations

• InfiniteGraph.swapBlockFun k i = if i < k then i + k else if i < 2 * k then i - k else i

theorem InfiniteGraph.swapBlockFun_involutive (k : ℕ) : Function.Involutive (swapBlockFun k)

def InfiniteGraph.swapBlock (k : ℕ) : Equiv.Perm ℕ

The block swap [0, k) ↔ [k, 2k): a finitely supported involution of ℕ.

Equations

• InfiniteGraph.swapBlock k = Function.Involutive.toPerm (InfiniteGraph.swapBlockFun k) ⋯

@[simp]

theorem InfiniteGraph.swapBlock_apply (k i : ℕ) : (swapBlock k) i = swapBlockFun k i

theorem InfiniteGraph.swapBlock_apply_of_lt (k : ℕ) {i : ℕ} (hi : i < k) : (swapBlock k) i = i + k

theorem InfiniteGraph.finSupp_swapBlock (k : ℕ) : FinSupp (swapBlock k)

The block swap is finitely supported (it fixes everything past 2k).

The block swap carries initial cylinders to tail cylinders

theorem InfiniteGraph.restrictFin_relabel_swapBlock (k : ℕ) (G : InfiniteGraph) : restrictFin k (relabel (swapBlock k) G) = restrictFin k (drop k G)

The block swap moves the initial window onto the tail window: the graph induced on the first k vertices after relabeling by swapBlock k equals the graph induced on {k, …, 2k−1} — the first k vertices of the k-tail.

theorem InfiniteGraph.relabel_swapBlock_preimage_mem_tailAlgebra (k : ℕ) {B : Set InfiniteGraph} (hB : MeasurableSet B) : MeasurableSet (relabel (swapBlock k) ⁻¹' B)

The block-swap relabeling carries an initialAlgebra k event into a tailAlgebra k event: it moves dependence on the first k vertices to dependence on {k, …, 2k−1}, which is contained in the tail {k, k+1, …}.

In-measure approximation by initial cylinders

theorem InfiniteGraph.isSetRing_iUnion_initialAlgebra : MeasureTheory.IsSetRing (⋃ (k : ℕ), {A : Set InfiniteGraph | MeasurableSet A})

The events depending on only finitely many vertices form a ring of sets.

theorem InfiniteGraph.generateFrom_iUnion_initialAlgebra : inferInstance = MeasurableSpace.generateFrom (⋃ (k : ℕ), {A : Set InfiniteGraph | MeasurableSet A})

The Borel σ-algebra is generated by the finite-vertex events.

theorem Graphon.InfiniteExchangeableGraphLaw.exists_initialAlgebra_measure_symmDiff_lt (M : InfiniteExchangeableGraphLaw) {s : Set InfiniteGraph} (hs : MeasurableSet s) {ε : ENNReal} (hε : 0 < ε) : ∃ (k : ℕ) (t : Set InfiniteGraph), MeasurableSet t ∧ ↑M.law (symmDiff t s) < ε

In-measure approximation by initial cylinders: every Borel event s is approximated in M.law-measure, to within any ε > 0, by an event t depending on only the first k vertices for some k. The initial cylinders form a set-ring generating the Borel σ-algebra, so exists_measure_symmDiff_lt_of_generateFrom_isSetRing applies.

Fixed-fiber ergodicity: invariant events are trivial

theorem InfiniteGraph.drop_comp_relabel_of_finSupp {σ : Equiv.Perm ℕ} {N : ℕ} (hN : ∀ (x : ℕ), N ≤ x → σ x = x) : drop N ∘ relabel σ = drop N

A permutation supported below N acts trivially past the N-tail: drop N ∘ relabel σ = drop N.

theorem InfiniteGraph.vertexTailAlgebra_le_invariantAlgebra : vertexTailAlgebra ≤ invariantAlgebra

Every vertex-tail event is permutation-invariant: the vertex-tail σ-algebra is a sub-σ-algebra of the finite-permutation-invariant σ-algebra. A finitely supported permutation acts trivially on all sufficiently late tails.

theorem Graphon.InfiniteExchangeableGraphLaw.measure_invariant_eq_zero_or_one_of_restrictionIndependent {M : InfiniteExchangeableGraphLaw} (hM : M.RestrictionIndependent) {A : Set InfiniteGraph} (hA : MeasurableSet A) : ↑M.law A = 0 ∨ ↑M.law A = 1

Fixed-fiber ergodicity: under restriction independence, every finite-permutation- invariant event has M.law-measure 0 or 1. Approximate the invariant A by an initial cylinder B, move B to a disjoint tail block B' = relabel (swapBlock k) ⁻¹' B (invariance keeps μ (A ∆ B') < ε, exchangeability keeps μ B' = μ B, independence gives μ (B ∩ B') = μ B · μ B'); comparing A with B ∩ B' yields |a − a²| ≤ 4ε for every ε, where a = μ.real A, so a is a fixed point of t ↦ t².

theorem Graphon.InfiniteExchangeableGraphLaw.isErgodic_of_restrictionIndependent {M : InfiniteExchangeableGraphLaw} (hM : M.RestrictionIndependent) : M.IsErgodic

Restriction independence implies ergodicity (a link of the DJ 5.5 / #59 chain).

theorem Graphon.InfiniteExchangeableGraphLaw.vertexTailTrivial_of_isErgodic {M : InfiniteExchangeableGraphLaw} (hM : M.IsErgodic) : M.VertexTailTrivial

Ergodicity implies vertex-tail triviality: every vertex-tail event is permutation-invariant (vertexTailAlgebra_le_invariantAlgebra).

The ergodicity links of the extremality equivalence (#59)

theorem Graphon.InfiniteExchangeableGraphLaw.isErgodic_iff_isDissociated (M : InfiniteExchangeableGraphLaw) : M.IsErgodic ↔ M.IsDissociated

Ergodicity ↔ dissociation: closing RestrictionIndependent ⟹ IsErgodic ⟹ VertexTailTrivial against the #91 equivalences.

theorem Graphon.InfiniteExchangeableGraphLaw.isErgodic_iff_restrictionIndependent (M : InfiniteExchangeableGraphLaw) : M.IsErgodic ↔ M.RestrictionIndependent

Ergodicity ↔ restriction independence.

theorem Graphon.InfiniteExchangeableGraphLaw.isErgodic_iff_vertexTailTrivial (M : InfiniteExchangeableGraphLaw) : M.IsErgodic ↔ M.VertexTailTrivial

Ergodicity ↔ vertex-tail triviality.

theorem Graphon.InfiniteExchangeableGraphLaw.tfae_ergodic_extremality (M : InfiniteExchangeableGraphLaw) : [∃ (x : StandardGraphonSpace), GraphonSpace.infiniteMixtureLawEquiv.symm M = MeasureTheory.diracProba x, ∃ (x : StandardGraphonSpace), M = GraphonSpace.infiniteSampleExchangeableLaw x, M.IsDissociated, M.RestrictionIndependent, M.VertexTailTrivial, M.IsErgodic].TFAE

The ergodic-decomposition form of Diaconis–Janson Theorem 5.5 (issue 59): the six-way extremality equivalence, adjoining ergodicity under the finite-permutation action to the five-way tfae_extremality.

limitGraphon generates the invariant σ-algebra modulo null sets (#59)

theorem Graphon.InfiniteExchangeableGraphLaw.invariant_ae_eq_limitGraphon_classifier (M : InfiniteExchangeableGraphLaw) {A : Set InfiniteGraph} (hA : MeasurableSet A) : A =ᵐ[↑M.law] GraphonSpace.limitGraphon ⁻¹' {x : StandardGraphonSpace | ↑(GraphonSpace.infiniteSampleLaw x) A = 1}

The empirical limit generates the invariant σ-algebra modulo null sets (issue 59): every finite-permutation-invariant event A agrees, up to an M.law-null set, with the limitGraphon-preimage of the classifier {x | A is conull in the fiber sampled from x}. Via the barycenter M.law = ∫ (infiniteSampleLaw x) dP(x), in each fiber A is null or conull (fiber ergodicity) and limitGraphon = x almost surely, so the classifier and A have zero fiber-symmetric-difference; integrating gives M.law (A ∆ classifier) = 0.