Compactness of Graphon Space

This file develops compactness of the graphon pseudometric space (total boundedness and completeness), from which compactness of the cut-distance quotient modulo weak isomorphism follows.

Main definitions

• Graphon.WeaklyIsomorphic — Weak isomorphism (cut distance zero)
• Graphon.mkStepGraphon — Step graphon from partition and coefficients
• Graphon.IsCauchy — Cauchy sequence in cut distance

Main results

• Graphon.totallyBounded — Finite ε-net in cut distance
• Graphon.complete — Cauchy sequences converge
• Graphon.compact — Every sequence has a convergent subsequence

Implementation notes

The cut-distance quotient modulo weak isomorphism is a compact metric space. Concretely, we prove total boundedness and completeness of the graphon pseudometric space.

The compactness follows from:

1. The regularity lemma gives total boundedness
2. Completeness follows from a direct limit construction via Radon–Nikodym

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 9.3

Quotient by weak isomorphism

def Graphon.WeaklyIsomorphic {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon α μ) : Prop

Two graphons are weakly isomorphic iff their cut distance is zero.

Equations

• U.WeaklyIsomorphic W = (U.cutDistance W = 0)

theorem Graphon.WeaklyIsomorphic.refl {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : W.WeaklyIsomorphic W

Weak isomorphism is reflexive.

theorem Graphon.WeaklyIsomorphic.symm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {U W : Graphon α μ} (h : U.WeaklyIsomorphic W) : W.WeaklyIsomorphic U

Weak isomorphism is symmetric.

Note: With the two-sided cut distance definition, this no longer requires StandardBorelSpace.

theorem Graphon.WeaklyIsomorphic.trans {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] {U V W : Graphon α μ} (hUV : U.WeaklyIsomorphic V) (hVW : V.WeaklyIsomorphic W) : U.WeaklyIsomorphic W

Weak isomorphism is transitive (on standard Borel spaces).

theorem Graphon.weaklyIsomorphic_equivalence {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] : Equivalence WeaklyIsomorphic

Weak isomorphism is an equivalence relation (on standard Borel spaces).

Note: Only trans still requires StandardBorelSpace (for the triangle inequality).

theorem Graphon.WeakIso.weaklyIsomorphic {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {U W : Graphon α μ} (h : U.WeakIso W) : U.WeaklyIsomorphic W

Relationship between WeaklyIsomorphic and WeakIso:

WeakIso U W (one-sided pullback relation) implies WeaklyIsomorphic U W (cutDistance = 0).

The converse direction (cutDistance = 0 implies WeakIso in both directions) requires additional structure on the probability space (e.g., standard Borel).

Total boundedness

noncomputable def Graphon.mkStepFun {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) (c : Set α → Set α → ℝ) : α × α → ℝ

Step graphon from explicit coefficients on a partition.

Given a partition P and a symmetric coefficient function c : Set α → Set α → ℝ valued in [0,1], builds the step graphon constant on each rectangle with value c S T.

Equations

• Graphon.mkStepFun P c p = ∑ S ∈ P.parts, ∑ T ∈ P.parts, (S ×ˢ T).indicator (fun (x : α × α) => c S T) p

noncomputable def Graphon.mkStepGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (c : Set α → Set α → ℝ) (hc_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T = c T S) (hc_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T ∈ Set.Icc 0 1) : Graphon α μ

Build a Graphon from explicit coefficients on a partition.

Equations

• Graphon.mkStepGraphon P c hc_symm hc_mem = { toAEEqFun := MeasureTheory.AEEqFun.mk (Graphon.mkStepFun P c) ⋯, symm' := ⋯, ae_mem_Icc := ⋯ }

theorem Graphon.cutNormDiff_mkStepGraphon_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (c c' : Set α → Set α → ℝ) (hc_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T = c T S) (hc_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T ∈ Set.Icc 0 1) (hc'_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c' S T = c' T S) (hc'_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c' S T ∈ Set.Icc 0 1) (δ : ℝ) (hδ : ∀ S ∈ P.parts, ∀ T ∈ P.parts, |c S T - c' S T| ≤ δ) : (mkStepGraphon P c hc_symm hc_mem).cutNormDiff (mkStepGraphon P c' hc'_symm hc'_mem) ≤ δ

cutNormDiff between step graphons on the same partition with close coefficients is controlled by the coefficient difference.

theorem Graphon.totallyBounded {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (ε : ℝ) (hε : ε > 0) : ∃ (S : Finset (Graphon α μ)), ∀ (W : Graphon α μ), ∃ V ∈ S, W.cutDistance V ≤ ε

The space of graphons is totally bounded with respect to cut distance.

For any ε > 0, there exists a finite set of graphons such that every graphon is within ε (in cut distance) of some element of the set.

This follows from the regularity lemma: step graphons with bounded number of parts form an ε-net.

Proof outline:

1. Let k = regularityBound(ε/2) be the max number of partition parts
2. For any W, regularity gives P_W with ≤ k parts and cutNormDiff ≤ ε/2
3. stepify P_W W is a step graphon with coefficients in [0,1]
4. Quantize coefficients to grid with spacing δ, giving ε/2 error in cutNormDiff
5. Gridpoints on P_W = gridpoints on any other partition up to cutDistance 0 (via measure-preserving map between partitions, needs StandardBorelSpace)
6. Triangle: W within ε of nearest gridpoint

Completeness

def Graphon.IsCauchy {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : ℕ → Graphon α μ) : Prop

A sequence of graphons is Cauchy with respect to cut distance.

Equations

• Graphon.IsCauchy W = ∀ ε > 0, ∃ (N : ℕ), ∀ (m n : ℕ), m ≥ N → n ≥ N → (W m).cutDistance (W n) < ε

theorem Graphon.complete {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (W : ℕ → Graphon α μ) (hW : IsCauchy W) : ∃ (V : Graphon α μ), ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, (W n).cutDistance V < ε

The space of graphons is complete with respect to cut distance.

Every Cauchy sequence of graphons converges (modulo weak isomorphism).

Proof structure: From the Cauchy sequence, extract a rapidly converging subsequence (with cutDistance(W_{φ(k+1)}, W_{φ(k)}) ≤ 1/2^k). Apply the limit construction for rapidly converging sequences. Then show the full Cauchy sequence converges to the same limit using the triangle inequality.

Depends on: exists_limit_of_rapid_convergence (proved from exists_aligned_cutNormDiff_limit, sorry'd), cutDistance_triangle (proved modulo Rokhlin).

Compactness

theorem Graphon.compact {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (W : ℕ → Graphon α μ) : ∃ (V : Graphon α μ) (φ : ℕ → ℕ), StrictMono φ ∧ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, (W (φ n)).cutDistance V < ε

The space of graphons (modulo weak isomorphism) is compact.

This is the fundamental compactness theorem for graphon theory. It follows from total boundedness (regularity lemma) and completeness.

Structure: This is sequential compactness, equivalent to compactness for metric spaces (which graphon space is, modulo weak isomorphism).

Depends on: totallyBounded (sorry), complete (sorry), cutDistance_triangle (proved modulo Rokhlin sorry).