Vertex-tail infrastructure (issue #97, Campaign A, PR 2)

Tail restriction of infinite graphs, finite-deletion stability of empirical-graphon limits, and tail measurability of the universal empirical limit:

• GraphonSpace.graphClass_comap_perm — the graphon class of a finite graph is invariant under vertex permutations (hom densities are map averages, and precomposition by a permutation is a bijection on maps);
• InfiniteGraph.drop — the tail restriction: the graph induced on {k, k+1, …}, reindexed to ℕ; continuous and measurable, with the window identity restrictFin_drop;
• InfiniteGraph.tailAlgebra / InfiniteGraph.vertexTailAlgebra — the σ-algebra of events depending only on the graph on {k, k+1, …}, and their infimum over k;
• GraphonSpace.abs_homDensity_drop_window_sub_le — the counting comparison: the hom density of a window of the k-tail differs from that of the enlarged window of the original graph by at most q·k/(n+1);
• GraphonSpace.tendsto_empiricalGraphon_drop_iff — finite-deletion stability: the empirical graphons of the k-tail converge to x iff those of the original graph do;
• GraphonSpace.limitGraphon_drop — the universal empirical limit is invariant under tail restriction, pointwise everywhere;
• GraphonSpace.measurable_limitGraphon_vertexTailAlgebra — the empirical limit is vertex-tail measurable — the key input for the tail-triviality step of issue #91.

Permutation invariance of the finite graph classes

theorem GraphonSpace.graphClass_comap_perm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {n : ℕ} [NeZero n] (σ : Equiv.Perm (Fin n)) (H : SimpleGraph (Fin n)) : graphClass (SimpleGraph.comap (⇑σ) H) = graphClass H

Permutation invariance of the graphon class of a finite graph: relabeling the vertices by a permutation does not change the graphon class. Hom densities in an embedded finite graph are map averages (homDensity_ofSimpleGraphOn), and precomposition by a permutation is a bijection on vertex maps.

Tail restriction and the vertex-tail σ-algebra

def InfiniteGraph.drop (k : ℕ) (G : InfiniteGraph) : InfiniteGraph

Tail restriction: the graph induced on the vertices {k, k+1, …}, reindexed to ℕ.

Equations

• InfiniteGraph.drop k G = SimpleGraph.comap (fun (x : ℕ) => x + k) G

@[simp]

theorem InfiniteGraph.drop_adj (k : ℕ) (G : InfiniteGraph) (a b : ℕ) : (drop k G).Adj a b ↔ G.Adj (a + k) (b + k)

@[simp]

theorem InfiniteGraph.drop_zero (G : InfiniteGraph) : drop 0 G = G

theorem InfiniteGraph.drop_drop (k l : ℕ) (G : InfiniteGraph) : drop k (drop l G) = drop (k + l) G

Tail restrictions compose additively.

theorem InfiniteGraph.mem_edgeSet_drop (k : ℕ) (G : InfiniteGraph) (s : Sym2 ℕ) : s ∈ SimpleGraph.edgeSet (drop k G) ↔ Sym2.map (fun (x : ℕ) => x + k) s ∈ SimpleGraph.edgeSet G

Edge membership under tail restriction, in Sym2 form.

def InfiniteGraph.dropEdgeIndexMap (k : ℕ) (e : EdgeIndex) : EdgeIndex

The edge-index action of the tail shift.

Equations

• InfiniteGraph.dropEdgeIndexMap k e = ⟨Sym2.map (fun (x : ℕ) => x + k) ↑e, ⋯⟩

theorem InfiniteGraph.continuous_drop (k : ℕ) : Continuous (drop k)

Tail restriction is continuous: each output edge coordinate is an input edge coordinate.

theorem InfiniteGraph.measurable_drop (k : ℕ) : Measurable (drop k)

theorem InfiniteGraph.restrictFin_drop (m k : ℕ) (G : InfiniteGraph) : restrictFin m (drop k G) = SimpleGraph.comap (⇑(Fin.addNatEmb k)) (restrictFin (m + k) G)

The window identity: the first m vertices of the k-tail form the graph induced on the vertices {k, …, m + k − 1} of the original graph.

@[reducible]

noncomputable def InfiniteGraph.tailAlgebra (k : ℕ) : MeasurableSpace InfiniteGraph

The tail σ-algebra at level k: events depending only on the graph induced on the vertices {k, k+1, …} (the tail restriction drop k sees exactly the tail-induced subgraph, reindexed).

Equations

• InfiniteGraph.tailAlgebra k = MeasurableSpace.comap (InfiniteGraph.drop k) inferInstance

theorem InfiniteGraph.tailAlgebra_le (k : ℕ) : tailAlgebra k ≤ inferInstance

Each tail σ-algebra is a sub-σ-algebra of the Borel σ-algebra.

@[reducible]

noncomputable def InfiniteGraph.vertexTailAlgebra : MeasurableSpace InfiniteGraph

The vertex-tail σ-algebra ⋂ₖ σ(G|{k, k+1, …}): events depending only on arbitrarily late vertex tails.

Equations

• InfiniteGraph.vertexTailAlgebra = ⨅ (k : ℕ), InfiniteGraph.tailAlgebra k

theorem InfiniteGraph.tailAlgebra_antitone : Antitone tailAlgebra

The tail σ-algebras are antitone: a deeper tail carries less information.

theorem InfiniteGraph.vertexTailAlgebra_le_tailAlgebra (k : ℕ) : vertexTailAlgebra ≤ tailAlgebra k

theorem InfiniteGraph.vertexTailAlgebra_le : vertexTailAlgebra ≤ inferInstance

Finite-deletion stability of empirical limits

theorem GraphonSpace.abs_homDensity_drop_window_sub_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {q : ℕ} (F : SimpleGraph (Fin q)) [DecidableRel F.Adj] (k n : ℕ) (G : InfiniteGraph) : |Graphon.homDensity F (Graphon.ofSimpleGraphOn (InfiniteGraph.restrictFin (n + 1) (InfiniteGraph.drop k G))) - Graphon.homDensity F (Graphon.ofSimpleGraphOn (InfiniteGraph.restrictFin (n + k + 1) G))| ≤ ↑q * ↑k / (↑n + 1)

The counting comparison: the hom density of a size-(n+1) window of the k-tail differs from that of the size-(n+k+1) window of the original graph by at most q·k/(n+1). Both densities are normalized map counts (homDensity_ofSimpleGraphOn); the shift f ↦ f + k injects the tail-window maps into the big-window maps, the missing maps (those hitting the first k vertices) number at most (n+k+1)^q − (n+1)^q, and the normalization mismatch is controlled by Bernoulli's inequality.

theorem GraphonSpace.tendsto_empiricalGraphon_drop_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) (G : InfiniteGraph) (x : GraphonSpace α μ) : Filter.Tendsto (fun (n : ℕ) => empiricalGraphon n (InfiniteGraph.drop k G)) Filter.atTop (nhds x) ↔ Filter.Tendsto (fun (n : ℕ) => empiricalGraphon n G) Filter.atTop (nhds x)

Finite-deletion stability of empirical limits (issue #97): the empirical graphons of the k-tail of an infinite graph converge to x iff those of the original graph do. Via the hom-density characterization of cut-distance convergence (cutDistance_tendsto_iff_homDensity_tendsto), the counting comparison, and the index shift n ↦ n + k.

theorem GraphonSpace.mem_empiricalConvergenceSet_drop_iff (k : ℕ) (G : InfiniteGraph) : InfiniteGraph.drop k G ∈ empiricalConvergenceSet ↔ G ∈ empiricalConvergenceSet

Finite-deletion stability of the empirical convergence set: the k-tail of an infinite graph has convergent empirical graphons iff the graph does.

theorem GraphonSpace.limitGraphon_drop (k : ℕ) (G : InfiniteGraph) : limitGraphon (InfiniteGraph.drop k G) = limitGraphon G

The universal empirical limit is invariant under tail restriction — pointwise, everywhere: on the convergence set by uniqueness of limits, off it both sides take the canonical default (membership transfers).

Tail measurability of the universal empirical limit

theorem GraphonSpace.measurable_limitGraphon_tailAlgebra (k : ℕ) : Measurable limitGraphon

The universal empirical limit is measurable with respect to every tail σ-algebra: limitGraphon factors pointwise through drop k (limitGraphon_drop), so every preimage is a drop k-preimage of a Borel set.

theorem GraphonSpace.measurable_limitGraphon_vertexTailAlgebra : Measurable limitGraphon

The empirical limit is vertex-tail measurable (issue #97): limitGraphon is measurable with respect to the vertex-tail σ-algebra ⋂ₖ σ(G|{k, k+1, …}) — the key input for the tail-triviality step of issue #91.