A Lean 4 formalization of graphons — the theory of limits of dense graph sequences — building on Mathlib.
Main Results
- Cut distance pseudometric — Cut distance is a pseudometric on graphons: symmetry, triangle inequality, and non-negativity, with pullback invariance under measure-preserving bijections.
- Frieze–Kannan weak regularity lemma — Every graphon admits arbitrarily fine regular step-function approximations, with quantitative energy increment bounds.
- Counting lemma — Small cut distance implies similar homomorphism densities for all finite graphs.
- Inverse counting lemma — For every ε > 0, finitely many test graphs control cut distance up to ε (the quantitative inverse counting lemma).
- Compactness — The cut-distance quotient modulo weak isomorphism is a compact metric space; concretely, we prove total boundedness and completeness of the graphon pseudometric space.
- Convergence equivalence — A sequence of graphons converges in cut distance if and only if all homomorphism densities converge.
Scope
The formalization covers:
- Graphon infrastructure — Graphons as symmetric measurable functions on probability spaces, with AE equivalence classes (
Graphon). - Cut distance — Cut norm, cut distance as infimum over measure-preserving couplings (
cutNormDiff,cutDistance), pseudometric properties including the triangle inequality via Rokhlin’s theorem. - Step graphons — Measurable partitions (
MeasurablePartition), step functions, stepification, and partition operations (splitting, refinement). - Regularity — Energy of partitions, energy increment under refinement, the Frieze–Kannan weak regularity lemma (
regularity). - Homomorphism densities — Graph homomorphism density (
homDensity), the counting lemma (homDensity_sub_le), and weighted homomorphism sums. - Compactness — Total boundedness via partition grids (
totallyBounded), completeness via limit construction (complete). - Inverse counting — Step inverse counting, quantitative inverse counting lemma (
cutDistance_le_of_homDensity_close), and convergence equivalence (cutDistance_tendsto_iff_homDensity_tendsto).
Proof Status
Three remaining sorry declarations, driven by two main missing mathematical inputs: a Rokhlin-style alignment theorem and the positive-weight algebraic determination core. No custom axioms are introduced; these are sorrys that will be replaced with proofs.
| Pending result | sorry location |
Used by | Progress |
|---|---|---|---|
| Rokhlin’s theorem (isomorphism of standard Borel probability spaces) | exists_common_extension |
Cut distance triangle inequality, partition alignment, compactness | Mathlib has PolishSpace.measurableEquiv but not the measure-preserving version; proving this is in progress |
| Algebraic determination (Lovász Theorem 5.30, k≥2) | matrix_quotient_of_weightedHomSum_eq (positive-weight case) |
Inverse counting lemma core | The k=1 case is fully proved; the k≥2 case requires graph algebra separation arguments that are partially built |
| Determination pending theorem (depends on the above two) | cutDistance_zero_of_homDensity_eq |
Convergence equivalence | Proved modulo Rokhlin + algebraic determination |
All other declarations contain no additional sorrys.
Components
| File | Status | Contents |
|---|---|---|
Graphon/Basic.lean |
Core | Graphon definition, symmetry, boundedness, AE equivalence |
Graphon/Pullback.lean |
Core | Pullback under measure-preserving maps |
Graphon/Step.lean |
Core | Measurable partitions, step functions, stepification |
Graphon/HomDensity.lean |
Core | Homomorphism density definition and basic properties |
Graphon/CutNorm.lean |
Core | Cut norm, graphon integrability |
Graphon/Approximation.lean |
Core | Rectangle averages, cut norm approximation, partition splitting |
Graphon/CutDistance.lean |
Core | Cut distance, pseudometric properties, Rokhlin interface |
Graphon/Regularity.lean |
Core | Energy, energy increment, Frieze–Kannan weak regularity lemma |
Graphon/Counting.lean |
Core | Homomorphism density, counting lemma |
Graphon/Compactness.lean |
Core | Total boundedness, completeness, limit construction |
Graphon/MatrixDetermination.lean |
Core | Algebraic determination of step graphons |
Graphon/InverseCounting.lean |
Core | Inverse counting lemma, convergence equivalence |
Graphon/Convergence.lean |
Core | Top-level convergence characterization |
Graphon/Operations.lean |
Experimental | Pointwise product |
Graphon/Operator.lean |
Experimental | Kernel operator (pointwise definition) |
Graphon/Sampling.lean |
Experimental | Expected edge density |
Resources
References
- Lovász, L. (2012). Large Networks and Graph Limits. AMS Colloquium Publications, vol. 60.
- Frieze, A. & Kannan, R. (1999). Quick approximation to matrices and applications. Combinatorica, 19(2), 175–220.
- Borgs, C., Chayes, J. T., Lovász, L., Sós, V. T., & Vesztergombi, K. (2008). Convergent sequences of dense graphs I. Advances in Mathematics, 219(6), 1801–1851.
- Borgs, C., Chayes, J. T., Lovász, L., Sós, V. T., & Vesztergombi, K. (2012). Convergent sequences of dense graphs II. Annals of Mathematics, 176(1), 151–219.