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 α] [MeasureTheory.NullSingletonClass μ] {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 α] [MeasureTheory.NullSingletonClass μ] : Equivalence WeaklyIsomorphic

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

Note: Only trans still requires StandardBorelSpace and NullSingletonClass (for the triangle inequality, whose corrected coupling proof needs an atomless space).

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

theorem Graphon.mkStepFun_measurable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (c : Set α → Set α → ℝ) : Measurable (mkStepFun P c)

(de-privatized 2026-07-07 for the sampling layer)

theorem Graphon.mkStepFun_eq_at {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (c : Set α → Set α → ℝ) {p : α × α} {S : Set α} (hS : S ∈ P.parts) {T : Set α} (hT : T ∈ P.parts) (hp : p ∈ S ×ˢ T) : mkStepFun P c p = c S T

(de-privatized 2026-07-07 for the sampling layer)

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.cutNormDiff_le_of_ae_agree_off_strip {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (U W : Graphon α μ) (E : Set α) (hE : MeasurableSet E) (h_agree : ∀ᵐ (p : α × α) ∂μ.prod μ, p.1 ∉ E → p.2 ∉ E → ↑U.toAEEqFun p = ↑W.toAEEqFun p) : U.cutNormDiff W ≤ 2 * (μ E).toReal

If two graphons agree a.e. off a "strip" E × univ ∪ univ × E, then their cut norm difference is at most 2 * (μ E).toReal.

theorem Graphon.stepGraphon_reround_to_equipartition {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (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) {q : ℕ} (hq : 0 < q) : ∃ (Q : MeasurablePartition α μ) (cQ : Set α → Set α → ℝ) (hcQ_symm : ∀ A ∈ Q.parts, ∀ B ∈ Q.parts, cQ A B = cQ B A) (hcQ_mem : ∀ A ∈ Q.parts, ∀ B ∈ Q.parts, cQ A B ∈ Set.Icc 0 1), Q.parts.card = q ∧ (∀ A ∈ Q.parts, μ A = 1 / ↑q) ∧ (mkStepGraphon P c hc_symm hc_mem).cutNormDiff (mkStepGraphon Q cQ hcQ_symm hcQ_mem) ≤ 2 * ↑P.parts.card / ↑q

Re-rounding a step graphon to an equipartition. A step graphon on an arbitrary partition P can be approximated, in cut-norm difference, by a step graphon on an equal-measure q-cell partition Q, with crude error O(P.card / q).

The q equal cells of Q almost refine P (off a small "bad" set of measure at most P.card / q), so we reassign each cell of Q the coefficient of its parent P-cell. The two step graphons then agree off the strip bad × univ ∪ univ × bad, and cutNormDiff_le_of_ae_agree_off_strip yields the bound 2 * P.card / q.

theorem Graphon.totallyBounded {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (ε : ℝ) (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 α] [MeasureTheory.NullSingletonClass μ] (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) and cutDistance_triangle — fully proved.

Compactness

theorem Graphon.compact {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (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, complete, cutDistance_triangle — all fully proved (Rokhlin campaigns R0–R3).

Step-graphon weight stability (moved from Graphon/InverseCounting.lean)

theorem Graphon.cutDistance_step_weight_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {K : ℕ} (P Q : MeasurablePartition α μ) (c_P c_Q : Set α → Set α → ℝ) (hc_P_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c_P S T = c_P T S) (hc_P_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c_P S T ∈ Set.Icc 0 1) (hc_Q_symm : ∀ S ∈ Q.parts, ∀ T ∈ Q.parts, c_Q S T = c_Q T S) (hc_Q_mem : ∀ S ∈ Q.parts, ∀ T ∈ Q.parts, c_Q S T ∈ Set.Icc 0 1) (ι_P ι_Q : Fin K → Set α) (hι_P : ∀ (i : Fin K), ι_P i ∈ P.parts) (hι_Q : ∀ (i : Fin K), ι_Q i ∈ Q.parts) (hι_P_inj : Function.Injective ι_P) (hι_Q_inj : Function.Injective ι_Q) (hι_P_surj : ∀ S ∈ P.parts, ∃ (i : Fin K), ι_P i = S) (hι_Q_surj : ∀ S ∈ Q.parts, ∃ (i : Fin K), ι_Q i = S) (h_coeff_eq : ∀ (i j : Fin K), c_P (ι_P i) (ι_P j) = c_Q (ι_Q i) (ι_Q j)) : (mkStepGraphon P c_P hc_P_symm hc_P_mem).cutDistance (mkStepGraphon Q c_Q hc_Q_symm hc_Q_mem) ≤ 2 * ∑ i : Fin K, |(μ (ι_P i)).toReal - (μ (ι_Q i)).toReal|

Weight stability for step graphons on different partitions with the same coefficient matrix (moved here from Graphon/InverseCounting.lean, 2026-07-07, and de-privatized: it is the API boundary for the sampling layer's frequency-term bound).

NOTE: its proof uses MeasurePreserving.exists_controlled_cell_alignment (Rokhlin core, proved in campaign R2) for partition alignment; fully axiom-clean.