Homomorphism densities satisfy the representability axioms

The homomorphism density t(·, W) of a graphon W is a graph parameter (TauCeti.DenseGraphLimits.homDensityParam) that is isomorphism invariant, multiplicative, normalized and reflection positive. These are the four structural conditions of the Lovász–Szegedy characterization of homomorphism densities, so this is its easy direction.

The first three conditions are structural laws of homDensity. Reflection positivity follows from the gluing formula for labeled graphs and positivity of the resulting connection matrices.

Main definitions

• TauCeti.DenseGraphLimits.homDensityParam — the graph parameter t(·, W).

Main results

• TauCeti.DenseGraphLimits.isIsoInvariant_homDensityParam, TauCeti.DenseGraphLimits.isMultiplicative_homDensityParam and TauCeti.DenseGraphLimits.isNormalized_homDensityParam — the three structural laws;
• TauCeti.DenseGraphLimits.isReflectionPositive_homDensityParam — t(·, W) is reflection positive.

References

• L. Lovász, B. Szegedy, Limits of dense graph sequences, JCTB 96 (2006), 933–957, Section 2 — connection matrices and the reflection positivity of homomorphism densities.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Section 7.1.

noncomputable def TauCeti.DenseGraphLimits.homDensityParam {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : GraphParam

The homomorphism density t(·, W) of a graphon, as a graph parameter.

Equations

• TauCeti.DenseGraphLimits.homDensityParam W x✝ F = TauCeti.DenseGraphLimits.homDensity F W

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityParam_apply {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) {n : ℕ} (F : SimpleGraph (Fin n)) [DecidableRel F.Adj] : homDensityParam W n F = homDensity F W

The value of homDensityParam W at F is t(F, W), for any decidability instance on the adjacency of F.

theorem TauCeti.DenseGraphLimits.isIsoInvariant_homDensityParam {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : IsIsoInvariant (homDensityParam W)

t(·, W) is isomorphism invariant.

theorem TauCeti.DenseGraphLimits.isMultiplicative_homDensityParam {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : IsMultiplicative (homDensityParam W)

t(·, W) is multiplicative over disjoint unions.

theorem TauCeti.DenseGraphLimits.isNormalized_homDensityParam {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : IsNormalized (homDensityParam W)

t(·, W) is normalized: t(K₁, W) = 1.

Reflection positivity

theorem TauCeti.DenseGraphLimits.isReflectionPositive_homDensityParam {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : IsReflectionPositive (homDensityParam W)

Homomorphism densities are reflection positive: every connection matrix of t(·, W) is positive semidefinite.