Ergodicity links for exchangeable relational laws (R3c step 3, #106)

The generic port of the undirected fixed-fiber ergodicity argument (Graphon/ErgodicDecomposition.lean): a sortwise-permutation-invariant event has law-measure 0 or 1 under restriction independence, closing ergodicity into the R3b triangle.

Infrastructure:

• RelSignature.sortwiseSwapBlock k — the sortwise involution swapping the block [0, k s) with [k s, 2 k s) in each sort (fixing everything past 2 k s), finitely supported with a common bound under [Fintype S.Srt] (sortwiseFinSupp_swapBlock);
• RelStructure.restrictFin_relabel_sortwiseSwapBlock — the block swap moves the initial k-window onto the k-tail window; hence
• RelStructure.relabel_sortwiseSwapBlock_preimage_mem_tailAlgebra — the block-swap relabeling carries every initialAlgebra k event into a tailAlgebra k event;
• RelSignature.exists_initialAlgebra_measure_symmDiff_lt — in-measure approximation by initial cylinders: every measurable event is approximated in law-measure by an event depending on only an initial block (the initial cylinders form a set-ring generating the σ-algebra).

Fixed-fiber ergodicity:

• RelStructure.vertexTailAlgebra_le_invariantAlgebra — every vertex-tail event is invariant under all finitely supported sortwise relabelings;
• InfiniteRelExchangeableLaw.measure_invariant_eq_zero_or_one_of_restrictionIndependent — under restriction independence, every invariant event is null or conull (the 4ε approximate-independence estimate);
• RestrictionIndependent.isErgodic and IsErgodic.vertexTailTrivial — the two links closing RestrictionIndependent ⟹ IsErgodic ⟹ VertexTailTrivial;
• isErgodic_iff_isDissociated / isErgodic_iff_restrictionIndependent / isErgodic_iff_vertexTailTrivial — ergodicity joins the R3b equivalences.

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

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

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

Equations

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

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

def RelSignature.sortwiseSwapBlock {S : RelSignature} (k : S.Srt → ℕ) : S.Srt → Equiv.Perm ℕ

The sortwise block swap [0, k s) ↔ [k s, 2 k s): in each sort, the involution of ℕ swapping the initial k s-block with the following one.

Equations

• RelSignature.sortwiseSwapBlock k s = Function.Involutive.toPerm (RelSignature.swapBlockFun (k s)) ⋯

@[simp]

theorem RelSignature.sortwiseSwapBlock_apply {S : RelSignature} (k : S.Srt → ℕ) (s : S.Srt) (i : ℕ) : (sortwiseSwapBlock k s) i = swapBlockFun (k s) i

theorem RelSignature.sortwiseSwapBlock_apply_of_lt {S : RelSignature} (k : S.Srt → ℕ) (s : S.Srt) {i : ℕ} (hi : i < k s) : (sortwiseSwapBlock k s) i = i + k s

theorem RelSignature.sortwiseFinSupp_swapBlock {S : RelSignature} [Fintype S.Srt] (k : S.Srt → ℕ) : SortwiseFinSupp (sortwiseSwapBlock k)

The sortwise block swap is finitely supported with a common bound: each sort's swap fixes everything past 2 * k s, and finitely many sorts have a common bound.

The block swap carries initial cylinders to tail cylinders

theorem RelSignature.RelStructure.restrictFin_relabel_sortwiseSwapBlock {S : RelSignature} (k : S.Srt → ℕ) : restrictFin k ∘ relabel (sortwiseSwapBlock k) = restrict (shiftEmb k k)

The block swap moves the initial window onto the tail window: restricting the swapped structure to the initial k-block is restricting the original structure to the k-block after k.

theorem RelSignature.RelStructure.relabel_sortwiseSwapBlock_preimage_mem_tailAlgebra {S : RelSignature} (k : S.Srt → ℕ) {B : Set (S.RelStructure S.Vinfinite)} (hB : MeasurableSet B) : MeasurableSet (relabel (sortwiseSwapBlock k) ⁻¹' B)

The block-swap relabeling carries an initialAlgebra k event into a tailAlgebra k event: it moves dependence on the initial k-block to dependence on the following k-block, which is contained in the k-tail.

In-measure approximation by initial cylinders

theorem RelSignature.isSetRing_iUnion_initialAlgebra {S : RelSignature} : MeasureTheory.IsSetRing (⋃ (k : S.Srt → ℕ), {A : Set (S.RelStructure S.Vinfinite) | MeasurableSet A})

The events depending on only an initial block form a ring of sets.

theorem RelSignature.generateFrom_iUnion_initialAlgebra {S : RelSignature} : inferInstance = MeasurableSpace.generateFrom (⋃ (k : S.Srt → ℕ), {A : Set (S.RelStructure S.Vinfinite) | MeasurableSet A})

The product σ-algebra is generated by the initial-block events.

theorem RelSignature.InfiniteRelExchangeableLaw.exists_initialAlgebra_measure_symmDiff_lt {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) {s : Set (S.RelStructure S.Vinfinite)} (hs : MeasurableSet s) {ε : ENNReal} (hε : 0 < ε) : ∃ (k : S.Srt → ℕ) (t : Set (S.RelStructure S.Vinfinite)), MeasurableSet t ∧ ↑M.law (symmDiff t s) < ε

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

Fixed-fiber ergodicity: invariant events are trivial

theorem RelSignature.RelStructure.drop_comp_relabel_of_sortwiseFinSupp {S : RelSignature} {σ : S.Srt → Equiv.Perm ℕ} {N : ℕ} (hN : ∀ (s : S.Srt) (x : ℕ), N ≤ x → (σ s) x = x) : (drop fun (x : S.Srt) => N) ∘ relabel σ = drop fun (x : S.Srt) => N

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

theorem RelSignature.RelStructure.vertexTailAlgebra_le_invariantAlgebra {S : RelSignature} : vertexTailAlgebra ≤ invariantAlgebra

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

theorem RelSignature.InfiniteRelExchangeableLaw.measure_invariant_eq_zero_or_one_of_restrictionIndependent {S : RelSignature} [Fintype S.Srt] {M : S.InfiniteRelExchangeableLaw} (hM : M.RestrictionIndependent) {A : Set (S.RelStructure S.Vinfinite)} (hA : MeasurableSet A) : ↑M.law A = 0 ∨ ↑M.law A = 1

Fixed-fiber ergodicity: under restriction independence, every event strictly invariant under all finitely supported sortwise relabelings 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 (sortwiseSwapBlock 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².

The ergodicity links of the R3b triangle

theorem RelSignature.InfiniteRelExchangeableLaw.RestrictionIndependent.isErgodic {S : RelSignature} [Fintype S.Srt] {M : S.InfiniteRelExchangeableLaw} (hM : M.RestrictionIndependent) : M.IsErgodic

Restriction independence implies ergodicity.

theorem RelSignature.InfiniteRelExchangeableLaw.IsErgodic.vertexTailTrivial {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (hM : M.IsErgodic) : M.VertexTailTrivial

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

theorem RelSignature.isErgodic_iff_isDissociated {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) : M.IsErgodic ↔ M.IsDissociated

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

theorem RelSignature.isErgodic_iff_restrictionIndependent {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) : M.IsErgodic ↔ M.RestrictionIndependent

Ergodicity ↔ restriction independence.

theorem RelSignature.isErgodic_iff_vertexTailTrivial {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) : M.IsErgodic ↔ M.VertexTailTrivial

Ergodicity ↔ vertex-tail triviality.