The structural laws of a homomorphism density

Read as a function of its first argument, t(·, W) is a real-valued parameter of finite simple graphs. This file proves the three laws that make it one, together with invariance under embedding the graph into a larger vertex type:

• isomorphism invariance — t(F, W) depends on F only up to ≃g;
• embedding invariance — adding vertices outside an embedded copy of F does not change its density;
• normalization — t(F, W) = 1 when F has no edges, in particular on a one-vertex graph;
• multiplicativity — t(F₁ ⊕g F₂, W) = t(F₁, W) · t(F₂, W) over a disjoint sum.

Each result is a change of variables in the defining integral, made along a measure-preserving map. Relabelling the vertices is MeasureTheory.measurePreserving_arrowCongr', restricting coordinates along an embedding is TauCeti.measurePreserving_pi_comp_embedding, and splitting the assignments on a disjoint sum of vertex sets into a pair is MeasureTheory.measurePreserving_sumPiEquivProdPi_symm, after which the two halves separate by Fubini (MeasureTheory.integral_prod_mul). What each change of variables has to be matched with is the corresponding reindexing of the edges, supplied by Mathlib's SimpleGraph.Iso.mapEdgeSet and SimpleGraph.edgeSetSumEquiv.

Multiplicativity is the sharpest of the three: it says the vertices of the two summands are integrated independently, which is exactly the statement that a graphon has no memory across components.

Main results

• TauCeti.DenseGraphLimits.homDensity_eq_of_iso — t(·, W) is a graph isomorphism invariant;
• TauCeti.DenseGraphLimits.homDensity_map_embedding — mapping into a larger vertex type preserves density;
• TauCeti.DenseGraphLimits.homDensity_bot — t(⊥, W) = 1;
• TauCeti.DenseGraphLimits.homDensity_sum — t(F₁ ⊕g F₂, W) = t(F₁, W) · t(F₂, W).

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §7.2 and §5.2.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensity_bot {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V₁ : Type u_2} [Fintype V₁] (W : Graphon Ω μ) : homDensity ⊥ W = 1

Normalization. t(⊥, W) = 1; in particular t(K₁, W) = 1 for the one-vertex graph ⊥ : SimpleGraph (Fin 1).

theorem TauCeti.DenseGraphLimits.homDensity_eq_of_iso {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V₁ : Type u_2} {V₂ : Type u_3} [Fintype V₁] [Fintype V₂] {F₁ : SimpleGraph V₁} [DecidableRel F₁.Adj] {F₂ : SimpleGraph V₂} [DecidableRel F₂.Adj] (φ : F₁ ≃g F₂) (W : Graphon Ω μ) : homDensity F₂ W = homDensity F₁ W

Isomorphism invariance. A homomorphism density depends on its graph only up to isomorphism: relabelling the vertices along φ permutes the coordinates of the product measure, which preserves it, and carries the edges of F₁ onto those of F₂.

@[simp]

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

Mapping a finite graph along an embedding preserves its homomorphism density. Vertices outside the embedding's range are isolated in the mapped graph, so integrating their independent coordinates contributes a factor of one.

@[simp]

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

Multiplicativity over disjoint unions. t(F₁ ⊕g F₂, W) = t(F₁, W) · t(F₂, W).

An assignment of vertices of the disjoint sum is a pair of assignments, one for each summand, and the product measure on the sum of the index types is the product of the two product measures; the edges of the sum likewise split, so the integrand is a product of a function of the first assignment and a function of the second, and Fubini separates the two integrals.