Counting Lemma for Graphons

This file proves the counting lemma, which relates the difference in homomorphism densities to the cut norm of the difference between graphons.

Main results

• Graphon.homDensity_sub_le - |t(F, U) - t(F, W)| ≤ |E(F)| · ‖U - W‖_□

Implementation notes

The counting lemma is one of the central results in graphon theory. It says that if two graphons are close in cut norm, then they have similar homomorphism densities for any fixed graph F.

The constant |E(F)| (number of edges in F) is optimal in general.

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Chapter 10

Counting lemma

Helper lemmas for product bounds

theorem Graphon.abs_prod_sub_prod_le {ι : Type u_3} [DecidableEq ι] (s : Finset ι) (f g : ι → ℝ) (hf : ∀ i ∈ s, f i ∈ Set.Icc 0 1) (hg : ∀ i ∈ s, g i ∈ Set.Icc 0 1) : |s.prod f - s.prod g| ≤ ∑ i ∈ s, |f i - g i|

Bound on absolute difference of products by sum of differences.

For values in [0,1], the difference of products is bounded by the sum of individual differences. This is used in the counting lemma proof.

Special case: Complete graph on 2 vertices (K₂)

The counting lemma for K₂ can be proven directly since homDensity K₂ W equals the integral of W over μ.prod μ, which is rectIntegralDiff over univ × univ.

theorem Graphon.homDensity_completeGraph_two {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : homDensity (SimpleGraph.completeGraph (Fin 2)) W = ∫ (p : α × α), ↑W.toAEEqFun p ∂μ.prod μ

For the complete graph K₂, homDensity equals the integral over μ.prod μ.

This uses the equivalence between Measure.pi (Fin 2 → α) and μ.prod μ via measurePreserving_finTwoArrow.

theorem Graphon.homDensity_sub_le_completeGraph_two {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon α μ) : |homDensity (SimpleGraph.completeGraph (Fin 2)) U - homDensity (SimpleGraph.completeGraph (Fin 2)) W| ≤ ↑(SimpleGraph.completeGraph (Fin 2)).edgeFinset.card * U.cutNormDiff W

Counting lemma for K₂: the complete graph on 2 vertices.

This is a base case that can be proven directly without the full layer cake machinery, since K₂ has exactly one edge and the homDensity integral directly equals the rectIntegralDiff over univ × univ.

General counting lemma

theorem Graphon.homDensity_sub_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {V : Type u_2} [Fintype V] [DecidableEq V] [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (U W : Graphon α μ) : |homDensity F U - homDensity F W| ≤ ↑F.edgeFinset.card * U.cutNormDiff W

The counting lemma: homomorphism density difference is bounded by cut norm.

For any graph F and graphons U, W on the same probability space: |t(F, U) - t(F, W)| ≤ |E(F)| · ‖U - W‖_□

This is the key result showing that cut norm controls homomorphism densities.

theorem Graphon.homDensity_sub_le_of_cutDistance {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {V : Type u_2} [Fintype V] [DecidableEq V] [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (U W : Graphon α μ) : |homDensity F U - homDensity F W| ≤ ↑F.edgeFinset.card * U.cutDistance W

Corollary: graphs with small cut distance have similar homomorphism densities.

The proof uses that homDensity is preserved under pullbacks (homDensity_pullback_mp):

• For any φ, ψ measure-preserving: homDensity F (pullback U φ) = homDensity F U
• So |homDensity F U - homDensity F W| = |homDensity F (pullback U φ) - homDensity F (pullback W ψ)|
• By homDensity_sub_le: ≤ |E(F)| * cutNormDiff (pullback U φ) (pullback W ψ)
• Taking inf over φ, ψ gives the bound by cutDistance

theorem Graphon.homDensity_eq_of_cutDistance_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {V : Type u_2} [Fintype V] [DecidableEq V] [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (U W : Graphon α μ) (h : U.cutDistance W = 0) : homDensity F U = homDensity F W

If cut distance is zero, homomorphism densities are equal.

This is a key consequence: weakly isomorphic graphons have the same homomorphism densities for all graphs F.

Continuity properties

theorem Graphon.homDensity_continuous_cutNormDiff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {V : Type u_2} [Fintype V] [DecidableEq V] [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (U W : Graphon α μ) (ε : ℝ) (hε : ε > 0) (h : U.cutNormDiff W < ε / ↑(max 1 F.edgeFinset.card)) : |homDensity F U - homDensity F W| < ε

Homomorphism density difference is bounded by edge count times cut norm difference.

This is the quantitative version of continuity with respect to cut norm.

Note: We use max 1 F.edgeFinset.card in the denominator to handle the empty graph case. For empty graphs, both homomorphism densities equal 1, so the bound is trivially satisfied.