Homomorphism densities on graphon space

Homomorphism density is invariant under zero cut distance, so it descends from strict graphon representatives to GraphonSpace. The descended observable retains the quantitative counting bound: for a finite graph F, it is Lipschitz with constant equal to the number of edges of F. In particular every homomorphism density is continuous on graphon space. Homomorphism densities are also preserved by the isometric embedding of every fixed-carrier graphon space into the unit-interval one.

These quotient-stable observables are the coordinates used by graphon separation, compactness, and the equivalence between cut-distance convergence and convergence of all homomorphism densities.

The structural identities of homomorphism density descend as well: t(⊥, ·) = 1, relabelling along an embedding changes nothing, and t(F₁ ⊕ F₂, ·) = t(F₁, ·) t(F₂, ·). So, as bounded continuous functions on graphon space, the homomorphism densities form a submonoid. This is the shape in which they serve as test functions: by Stone–Weierstrass a point-separating submonoid of bounded continuous functions determines finite measures (TauCeti.MeasureTheory.ext_of_forall_mem_submonoid_integral_eq_of_polish), so wherever the densities separate points, the integrals of all t(F, ·) determine a finite measure on graphon space.

Main definitions

• TauCeti.DenseGraphLimits.homDensityOnSpace is homomorphism density on the cut-distance quotient.
• TauCeti.DenseGraphLimits.homDensityBCF is the same function, bundled as a bounded continuous function.
• TauCeti.DenseGraphLimits.homDensitySubmonoid is the submonoid of bounded continuous functions on graphon space formed by the homomorphism densities of finite graphs.

Main results

• TauCeti.DenseGraphLimits.lipschitzWith_homDensity is the edge-count Lipschitz bound on strict graphons, which makes the descent well defined;
• TauCeti.DenseGraphLimits.homDensityOnSpace_mk computes it on a representative;
• TauCeti.DenseGraphLimits.homDensityOnSpace_nonneg and TauCeti.DenseGraphLimits.homDensityOnSpace_le_one bound it in [0, 1];
• TauCeti.DenseGraphLimits.lipschitzWith_homDensityOnSpace gives the edge-count Lipschitz bound;
• TauCeti.DenseGraphLimits.continuous_homDensityOnSpace gives continuity on every fixed-carrier graphon space;
• TauCeti.DenseGraphLimits.Graphon.homDensity_unitIntervalRepr and TauCeti.DenseGraphLimits.homDensityOnSpace_toGraphonSpaceI say that the unit-interval representative and the embedding into the unit-interval graphon space preserve homomorphism densities;
• TauCeti.DenseGraphLimits.homDensityOnSpace_bot, TauCeti.DenseGraphLimits.homDensityOnSpace_map_embedding and TauCeti.DenseGraphLimits.homDensityOnSpace_sum are normalization, relabelling invariance and multiplicativity over disjoint unions on graphon space;
• TauCeti.DenseGraphLimits.homDensityBCF_mem_homDensitySubmonoid says the homomorphism density of a graph on any finite vertex type lies in homDensitySubmonoid.

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 descent of homomorphism density to GraphonSpace. The signatures follow TauCetiRoadmap/DenseGraphLimits/Suggested.lean.

theorem TauCeti.DenseGraphLimits.lipschitzWith_homDensity {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] : LipschitzWith (↑F.edgeFinset.card) (homDensity F)

Homomorphism density is Lipschitz for the cut-distance pseudometric on strict graphons, with constant the number of edges of the finite graph.

noncomputable def TauCeti.DenseGraphLimits.homDensityOnSpace {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] : GraphonSpace Ω μ → ℝ

The homomorphism density of a finite graph, as a function on graphon space.

It is well defined because homomorphism density is continuous for the cut-distance pseudometric, hence constant on inseparable graphons.

Equations

• TauCeti.DenseGraphLimits.homDensityOnSpace F = SeparationQuotient.lift (TauCeti.DenseGraphLimits.homDensity F) ⋯

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityOnSpace_mk {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) : homDensityOnSpace F (SeparationQuotient.mk W) = homDensity F W

Homomorphism density on graphon space computes as the original density on representatives.

theorem TauCeti.DenseGraphLimits.homDensityOnSpace_nonneg {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (W : GraphonSpace Ω μ) : 0 ≤ homDensityOnSpace F W

Homomorphism density on graphon space is nonnegative.

theorem TauCeti.DenseGraphLimits.homDensityOnSpace_le_one {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (W : GraphonSpace Ω μ) : homDensityOnSpace F W ≤ 1

Homomorphism density on graphon space is at most 1.

theorem TauCeti.DenseGraphLimits.lipschitzWith_homDensityOnSpace {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] : LipschitzWith (↑F.edgeFinset.card) (homDensityOnSpace F)

Homomorphism density on graphon space is Lipschitz with constant the number of edges of the finite graph.

theorem TauCeti.DenseGraphLimits.continuous_homDensityOnSpace {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] : Continuous (homDensityOnSpace F)

Every finite-graph homomorphism density is continuous on graphon space.

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.homDensity_unitIntervalRepr {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) : homDensity F W.unitIntervalRepr = homDensity F W

The unit-interval representative has the same homomorphism densities as the original graphon.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityOnSpace_toGraphonSpaceI {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (x : GraphonSpace Ω μ) : homDensityOnSpace F (toGraphonSpaceI x) = homDensityOnSpace F x

Homomorphism densities are preserved by the embedding into the unit-interval graphon space.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityOnSpace_bot {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (x : GraphonSpace Ω μ) : homDensityOnSpace ⊥ x = 1

Normalization on graphon space. The edgeless graph has homomorphism density 1.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityOnSpace_map_embedding {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V₁ : Type u_3} {V₂ : Type u_4} [Fintype V₁] [Fintype V₂] [DecidableEq V₂] (F : SimpleGraph V₁) [DecidableRel F.Adj] (f : V₁ ↪ V₂) (x : GraphonSpace Ω μ) : homDensityOnSpace (SimpleGraph.map (⇑f) F) x = homDensityOnSpace F x

Relabelling a finite graph along an embedding does not change its homomorphism density on graphon space.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityOnSpace_sum {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V₁ : Type u_3} {V₂ : Type u_4} [Fintype V₁] [Fintype V₂] (F₁ : SimpleGraph V₁) [DecidableRel F₁.Adj] (F₂ : SimpleGraph V₂) [DecidableRel F₂.Adj] (x : GraphonSpace Ω μ) : homDensityOnSpace (F₁ ⊕g F₂) x = homDensityOnSpace F₁ x * homDensityOnSpace F₂ x

Multiplicativity on graphon space. t(F₁ ⊕g F₂, x) = t(F₁, x) · t(F₂, x).

Homomorphism densities as bounded continuous functions

noncomputable def TauCeti.DenseGraphLimits.homDensityBCF {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] : BoundedContinuousFunction (GraphonSpace Ω μ) ℝ

The homomorphism density of a finite graph, as a bounded continuous function on graphon space. It takes values in [0, 1].

Equations

• TauCeti.DenseGraphLimits.homDensityBCF F = BoundedContinuousFunction.mkOfBound { toFun := TauCeti.DenseGraphLimits.homDensityOnSpace F, continuous_toFun := ⋯ } 1 ⋯

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityBCF_apply {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] (x : GraphonSpace Ω μ) : (homDensityBCF F) x = homDensityOnSpace F x

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityBCF_bot {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : homDensityBCF ⊥ = 1

The edgeless graph has constant homomorphism density 1 as a bounded continuous function.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityBCF_map_embedding {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V₁ : Type u_3} {V₂ : Type u_4} [Fintype V₁] [Fintype V₂] [DecidableEq V₂] (F : SimpleGraph V₁) [DecidableRel F.Adj] (f : V₁ ↪ V₂) : homDensityBCF (SimpleGraph.map (⇑f) F) = homDensityBCF F

Relabelling along an embedding preserves the bounded continuous homomorphism density.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityBCF_sum {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V₁ : Type u_3} {V₂ : Type u_4} [Fintype V₁] [Fintype V₂] (F₁ : SimpleGraph V₁) [DecidableRel F₁.Adj] (F₂ : SimpleGraph V₂) [DecidableRel F₂.Adj] : homDensityBCF (F₁ ⊕g F₂) = homDensityBCF F₁ * homDensityBCF F₂

The homomorphism density of a disjoint union is the product of the homomorphism densities, as bounded continuous functions on graphon space.

def TauCeti.DenseGraphLimits.homDensitySubmonoid {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : Submonoid (BoundedContinuousFunction (GraphonSpace Ω μ) ℝ)

The homomorphism-density submonoid. The bounded continuous functions on graphon space of the form t(F, ·) for a finite graph F, indexed by graphs on Fin n. They are closed under products, since t(F₁, ·) t(F₂, ·) = t(F₁ ⊕g F₂, ·), and contain the constant 1 = t(⊥, ·). homDensityBCF_mem_homDensitySubmonoid admits graphs on any finite vertex type.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.DenseGraphLimits.mem_homDensitySubmonoid_iff {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {g : BoundedContinuousFunction (GraphonSpace Ω μ) ℝ} : g ∈ homDensitySubmonoid ↔ ∃ (n : ℕ) (F : SimpleGraph (Fin n)) (x : DecidableRel F.Adj), homDensityBCF F = g

A member of the homomorphism-density submonoid is the density of a graph on some Fin n.

theorem TauCeti.DenseGraphLimits.homDensityBCF_mem_homDensitySubmonoid {V : Type u_1} {Ω : Type u_2} [Fintype V] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph V) [DecidableRel F.Adj] : homDensityBCF F ∈ homDensitySubmonoid

The homomorphism density of a graph on any finite vertex type lies in the homomorphism-density submonoid.