The counting lemma

The counting lemma bounds the gap between the homomorphism densities of a finite graph F in two graphons on one carrier by the cut norm of their difference:

|t(F, U) - t(F, W)| ≤ e(F) · ‖U - W‖□.

It is what makes the cut norm the right notion of distance for dense graph limits: the graph observables t(F, ·) are Lipschitz in it, uniformly in everything but the number of edges of F.

Two graphons on different carriers are compared through a coupling π of the two carriers, which reads both as graphons on (Ω₁ × Ω₂, π); their difference there is the overlaid difference overlayDiff U W π. Since the coordinate projections out of a coupling are measure preserving, homDensity_comap says the two densities are unchanged by that reading, so the same-carrier statement transfers verbatim: counting_lemma_coupling. This is the cross-carrier engine of the separation layer, and the form in which the counting lemma meets the coupling-primary cutDist.

Since that bound holds along every coupling, taking the infimum over couplings replaces the overlaid cut norm by the cut distance itself:

|t(F, U) - t(F, W)| ≤ e(F) · δ□(U, W),

the cut-distance form abs_homDensity_sub_le_cutDist. It needs no standard-Borel, atomlessness, or common-carrier assumption, and it is what makes each t(F, ·) Lipschitz — hence continuous — for the cut metric.

The proof is a telescope over the edges. Swap the edges of F from W to U one at a time. Each swap changes the integrand at a single edge e₀ = s(a, b), weighted by the product of edge factors over the other edges of F; the gap it contributes is bounded by ‖U - W‖□, and there are e(F) swaps. The hybrid stage is indexed by a subset D of the edges — the edges already swapped — so the induction runs over D with the ambient edge set E fixed. That is the shape the argument needs: an induction on E alone would have to carry the already-fixed edge factor of the edge being peeled off, which is exactly the weight the single-edge bound consumes.

One swap is a rectangle test. F is a simple graph, so no edge other than e₀ joins a to b: every other edge misses a, or misses b, or both. Refreshing the two coordinates a and b (TauCeti.integral_pi_eq_integral_integral_update) therefore leaves an inner double integral whose weights factor — one [0, 1]-valued function of the new a-coordinate, one of the new b-coordinate — and abs_testIntegral_le_cutNorm bounds such a pairing by the cut norm, with no loss of constant. The outer integral is over a probability measure, so the bound survives it.

Main results

• TauCeti.DenseGraphLimits.counting_lemma — the forward counting lemma |t(F, U) - t(F, W)| ≤ e(F) · ‖U - W‖□;
• TauCeti.DenseGraphLimits.counting_lemma_top_fin_two and TauCeti.DenseGraphLimits.counting_lemma_top_fin_three — the one-edge and triangle specializations, with constants 1 and 3;
• TauCeti.DenseGraphLimits.counting_lemma_coupling — its cross-carrier coupling form, bounding the density gap of two graphons on different carriers by the cut norm of the overlaid difference along any coupling of the carriers;
• TauCeti.DenseGraphLimits.abs_homDensity_sub_le_cutDist — its cut-distance form |t(F,U) − t(F,W)| ≤ e(F) · δ□(U, W), obtained by taking the infimum over couplings.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Lemma 10.23.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Lemma 7.2.
• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 2 — the counting lemma and its coupling and cut-distance forms. The signatures follow TauCetiRoadmap/DenseGraphLimits/Suggested.lean.

theorem TauCeti.DenseGraphLimits.counting_lemma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (U W : Graphon Ω μ) : |homDensity F U - homDensity F W| ≤ ↑F.edgeFinset.card * cutNorm μ (U.toSymmKernel - W.toSymmKernel)

The counting lemma. The homomorphism densities of a finite graph F in two graphons on one carrier differ by at most e(F) times the cut norm of their difference. The argument to cutNorm is the kernel U - W: a difference of graphons is not a graphon, which is exactly why the cut norm is defined on symmetric kernels.

theorem TauCeti.DenseGraphLimits.counting_lemma_top_fin_two {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) : |homDensity ⊤ U - homDensity ⊤ W| ≤ cutNorm μ (U.toSymmKernel - W.toSymmKernel)

The counting lemma for one edge. The edge densities of two graphons differ by at most the cut norm of their difference.

theorem TauCeti.DenseGraphLimits.counting_lemma_top_fin_three {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) : |homDensity ⊤ U - homDensity ⊤ W| ≤ 3 * cutNorm μ (U.toSymmKernel - W.toSymmKernel)

The counting lemma for a triangle. The triangle densities of two graphons differ by at most three times the cut norm of their difference, one contribution for each edge.

theorem TauCeti.DenseGraphLimits.counting_lemma_coupling {V : Type u_2} [Fintype V] {Ω₁ : Type u_3} {Ω₂ : Type u_4} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (F : SimpleGraph V) [DecidableRel F.Adj] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) {π : MeasureTheory.Measure (Ω₁ × Ω₂)} (hπ : MeasureTheory.IsCoupling μ₁ μ₂ π) : |homDensity F U - homDensity F W| ≤ ↑F.edgeFinset.card * cutNorm π (overlayDiff U W π)

The counting lemma, coupling form. For any coupling π of the two carriers, the homomorphism densities of F in two graphons living on different probability spaces differ by at most e(F) times the cut norm of their overlaid difference along π.

This is the cross-carrier engine: taking the infimum over couplings turns it into a bound by the cut distance, and hence into the forward direction of the separation theorem. No standard Borel or atomless hypothesis is needed, on either carrier.

The proof is the same-carrier counting_lemma on the coupled space (Ω₁ × Ω₂, π). Reading U and W there — as the pullbacks along the two coordinate projections, whose difference is overlayDiff U W π — changes neither density, because the projections out of a coupling are measure preserving (homDensity_comap).

The IsFiniteMeasure instance the cut norm needs is supplied explicitly from the coupling, matching TauCeti.DenseGraphLimits.cutDist_le; being a Prop class it is interchangeable with any other.

theorem TauCeti.DenseGraphLimits.abs_homDensity_sub_le_cutDist {V : Type u_2} [Fintype V] {Ω₁ : Type u_3} {Ω₂ : Type u_4} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (F : SimpleGraph V) [DecidableRel F.Adj] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) : |homDensity F U - homDensity F W| ≤ ↑F.edgeFinset.card * cutDist U W

Homomorphism density is Lipschitz for the cross-carrier cut distance. For a finite graph F, the density gap between graphons on arbitrary probability carriers is at most the number of edges of F times their coupling cut distance.

This is the coupling form of the counting lemma with the infimum over couplings taken.