Inverse Counting Lemma

This file proves the inverse counting lemma: if two graphons have similar homomorphism densities for all graphs, then they are close in cut distance.

Main results

• Graphon.cutDistance_zero_of_homDensity_eq - Equal hom densities ⟹ cutDistance = 0
• Graphon.cutDistance_le_of_homDensity_close - The quantitative inverse counting lemma

Implementation notes

The counting lemma (in Counting.lean) shows: small cut distance ⟹ similar homomorphism densities

The inverse counting lemma shows the converse: similar homomorphism densities ⟹ small cut distance

Together, these establish that cut distance convergence is equivalent to convergence of all homomorphism densities.

The proof uses:

1. Algebraic determination for step graphons (MatrixDetermination.lean)
2. Partition alignment via Rokhlin's theorem (CutDistance.lean)
3. Regularity lemma for step approximation
4. Compactness of graphon space

References

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

Step graphon inverse counting

The algebraic core: step graphons on the same partition with equal hom densities for all graphs have cut distance zero. This connects the measure-theoretic homDensity to the finite weightedHomSum and uses matrix_quotient_of_weightedHomSum_eq (the algebraic determination axiom) plus partition alignment (Rokhlin).

Main inverse counting lemma

theorem Graphon.cutDistance_zero_of_homDensity_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] (U W : Graphon α μ) (h : ∀ (k : ℕ) (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], homDensity F U = homDensity F W) : U.cutDistance W = 0

Algebraic determination: two graphons with equal homomorphism densities for all finite graphs have cut distance zero (are weakly isomorphic).

The proof combines simultaneous_regularity (which gives a cardinality bound K = 4 ^ (2 * (⌈1/δ²⌉ + 1))) with step_quantitative_icl_bounded K (ε/3) (uniform compactness over all partitions with ≤ K parts) and the counting lemma. For any ε > 0:

1. Apply step_quantitative_icl_bounded K (ε/3) to get (δ_step, m) uniform over all partitions with ≤ K parts
2. Choose δ so that (a) δ ≤ ε/3 and (b) the counting lemma converts cutNormDiff ≤ δ into hom density differences < δ_step for all graphs on ≤ m vertices
3. Apply simultaneous_regularity U W δ to get partition P with P.parts.card ≤ K, cutNormDiff U (stepify P U) ≤ δ, cutNormDiff W (stepify P W) ≤ δ
4. By the counting lemma (step 2b), step graphons on P satisfy the δ_step condition, so step_quantitative_icl_bounded gives cutDistance(stepify P U, stepify P W) < ε/3
5. Triangle inequality: cutDistance(U, W) ≤ cutNormDiff(U, stepify P U) + cutDistance(stepify P U, stepify P W) + cutNormDiff(W, stepify P W) < ε

The key insight is that step_quantitative_icl_bounded eliminates the circular dependency: δ_step and m depend only on K and ε, not on the specific partition P. The cardinality bound K from simultaneous_regularity depends only on the regularity parameter δ, which is chosen AFTER obtaining (δ_step, m).

Sorry traces to: step_quantitative_icl_bounded (compactness over bounded partitions) → step_quantitative_icl → cutDistance_zero_of_step_homDensity_eq → matrix_quotient_of_weightedHomSum_eq (algebraic core) + MeasurePreserving.exists_common_extension (Rokhlin).

theorem Graphon.cutDistance_le_of_homDensity_close {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] (ε : ℝ) (hε : ε > 0) : ∃ (δ : ℝ) (_ : δ > 0) (k : ℕ), ∀ (U W : Graphon α μ), (∀ (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], |homDensity F U - homDensity F W| < δ) → U.cutDistance W < ε

The inverse counting lemma: similar homomorphism densities imply small cut distance.

For any ε > 0, there exists δ > 0 and a finite set of graphs F₁,...,Fₖ such that if |t(Fᵢ, U) - t(Fᵢ, W)| < δ for all i, then δ□(U, W) < ε.

theorem Graphon.cutDistance_tendsto_iff_homDensity_tendsto {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] (W : ℕ → Graphon α μ) (V : Graphon α μ) : (∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, (W n).cutDistance V < ε) ↔ ∀ (k : ℕ) (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |homDensity F (W n) - homDensity F V| < ε

Corollary: a sequence converges in cut distance iff all homomorphism densities converge.

This is the fundamental characterization of graph limit convergence.

Uniqueness of limits

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

If a sequence converges to two limits, they are weakly isomorphic.

theorem Graphon.weaklyIsomorphic_of_homDensity_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] (U W : Graphon α μ) (h : ∀ (k : ℕ) (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], homDensity F U = homDensity F W) : U.WeaklyIsomorphic W

Homomorphism densities determine the graphon up to weak isomorphism.