Inverse counting: homomorphism densities separate graphons

Two graphons with the same homomorphism density for every finite graph are at cut distance zero. Together with the forward direction TauCeti.DenseGraphLimits.forall_homDensity_eq_of_cutDist_eq_zero this is the separation theorem: the cut distance vanishes exactly when all homomorphism densities agree, and the homomorphism densities are a complete set of coordinates on graphon space.

The graphons may live on different probability spaces, and no standard-Borel or atomlessness hypothesis is needed on either carrier.

The inverse direction rests on the second sampling lemma TauCeti.DenseGraphLimits.sampleGraph_cutDist_tendsto_inProbability: the homomorphism densities determine the sampling laws (TauCeti.DenseGraphLimits.sampleGraph_eq_of_forall_homDensity_eq), and the sampling laws determine the graphon up to cut distance.

Main results

• TauCeti.DenseGraphLimits.cutDist_eq_zero_of_forall_homDensity_eq — graphons with the same homomorphism densities are at cut distance zero (the inverse counting lemma);
• TauCeti.DenseGraphLimits.cutDist_eq_zero_iff_forall_homDensity_eq — the separation theorem;
• TauCeti.DenseGraphLimits.graphonSpace_ext_iff_homDensity — points of graphon space are equal exactly when all their homomorphism densities agree.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Theorem 11.3 and Lemma 10.16.
• C. Borgs, J. Chayes, L. Lovász, V. Sós, K. Vesztergombi, Convergent sequences of dense graphs I: Subgraph frequencies, metric properties and testing, Adv. Math. 219 (2008), 1801–1851, Theorem 3.8.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Theorem 8.10.

theorem TauCeti.DenseGraphLimits.cutDist_eq_zero_of_forall_homDensity_eq {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (h : ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj], homDensity F U = homDensity F W) : cutDist U W = 0

The inverse counting lemma. Two graphons, on arbitrary probability carriers, with the same homomorphism density for every finite graph are at cut distance zero. The graphons need not share a carrier, and no standard-Borel or atomlessness hypothesis is needed on either carrier.

theorem TauCeti.DenseGraphLimits.cutDist_eq_zero_iff_forall_homDensity_eq {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) : cutDist U W = 0 ↔ ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj], homDensity F U = homDensity F W

Separation of graphons by homomorphism densities. Two graphons, on arbitrary probability carriers, are at cut distance zero if and only if every finite graph has the same homomorphism density in them.

theorem TauCeti.DenseGraphLimits.graphonSpace_ext_iff_homDensity {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : GraphonSpace Ω μ) : U = W ↔ ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj], homDensityOnSpace F U = homDensityOnSpace F W

Separation on graphon space. Two points of graphon space are equal if and only if every finite graph has the same homomorphism density at them: the homomorphism densities are a complete set of coordinates on graphon space.