The Lovász–Szegedy characterization of homomorphism densities

A graph parameter is the homomorphism density t(·, W) of a graphon W on an atomless standard Borel probability space (Ω, μ), such as the unit interval, if and only if it is isomorphism invariant, multiplicative, normalized and reflection positive (lovasz_szegedy_representability).

The hard direction is exists_graphon_of_representability_axioms: a parameter f satisfying the four axioms is t(·, W) for a graphon W on (Ω, μ). The easy direction is that t(·, W) satisfies them, for a graphon on any probability space (isReflectionPositive_homDensityParam and its three companions).

As a consequence such a parameter takes values in [0, 1] (graphParam_mem_Icc_of_representability_axioms): boundedness follows from the four axioms and is not one of them.

Main results

• TauCeti.DenseGraphLimits.lovasz_szegedy_representability — a graph parameter is t(·, W) for a graphon W on an atomless standard Borel carrier iff it satisfies the four representability axioms.
• TauCeti.DenseGraphLimits.exists_graphon_of_representability_axioms — the hard direction: a graph parameter satisfying the four representability axioms is t(·, W) for a graphon W on every atomless standard Borel carrier.
• TauCeti.DenseGraphLimits.graphParam_mem_Icc_of_representability_axioms — such a parameter takes values in [0, 1].

References

• L. Lovász, B. Szegedy, Limits of dense graph sequences, JCTB 96 (2006), 933–957, Theorem 2.2.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Section 11.3.

theorem TauCeti.DenseGraphLimits.exists_graphon_of_representability_axioms {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (hrp : IsReflectionPositive f) : ∃ (W : Graphon Ω μ), ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj], f n F = homDensity F W

Representability, hard direction. An isomorphism-invariant, multiplicative, normalized, reflection-positive graph parameter is the homomorphism density of a graphon on every atomless standard Borel carrier (Ω, μ), such as the unit interval.

theorem TauCeti.DenseGraphLimits.graphParam_mem_Icc_of_representability_axioms (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (hrp : IsReflectionPositive f) (n : ℕ) (F : SimpleGraph (Fin n)) : f n F ∈ Set.Icc 0 1

A graph parameter satisfying the four representability axioms takes values in [0, 1].

theorem TauCeti.DenseGraphLimits.lovasz_szegedy_representability {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] (f : GraphParam) : (∃ (W : Graphon Ω μ), ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj], f n F = homDensity F W) ↔ IsIsoInvariant f ∧ IsMultiplicative f ∧ IsNormalized f ∧ IsReflectionPositive f

The Lovász–Szegedy characterization of homomorphism densities. A graph parameter is the homomorphism density of a graphon on an atomless standard Borel carrier (Ω, μ), such as the unit interval, if and only if it is isomorphism invariant, multiplicative, normalized and reflection positive.