Homomorphism density for finite simple graphs

Mathlib does not (as of 2026-04) provide SimpleGraph.homDensity. We define a lightweight version here, specialised to finite vertex types on the host G, and prove the basic homDensity H G ≤ 1 upper bound used as a sanity check in Sidorenko-style arguments.

The extension to infinite hosts uses the same formula with Fintype.card replaced by measure-theoretic integrals; we do not need that generality here.

noncomputable def SimpleGraph.homCount {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (H : SimpleGraph V) (G : SimpleGraph W) [DecidableRel H.Adj] [DecidableRel G.Adj] : ℕ

The number of graph homomorphisms H → G, as a natural number. For finite vertex types this is just the cardinality of the Hom type.

Equations

• H.homCount G = Fintype.card (H →g G)

noncomputable def SimpleGraph.homDensity {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (H : SimpleGraph V) (G : SimpleGraph W) [DecidableRel H.Adj] [DecidableRel G.Adj] : ℝ

The homomorphism density t(H, G) of a simple graph H in a simple graph G with finite vertex sets is #Hom(H, G) / |V(G)|^{|V(H)|}.

Equations

• H.homDensity G = ↑(H.homCount G) / ↑(Fintype.card W) ^ Fintype.card V

theorem SimpleGraph.homDensity_le_one {V : Type u_3} {W : Type u_4} [Fintype V] [Fintype W] [Nonempty W] [DecidableEq V] [DecidableEq W] (H : SimpleGraph V) (G : SimpleGraph W) [DecidableRel H.Adj] [DecidableRel G.Adj] : H.homDensity G ≤ 1

The homomorphism density t(H, G) is at most 1.

Proof outline: the underlying function of a H →g G-homomorphism is an element of V → W, which has |W|^|V| elements, so homCount H G ≤ |W|^|V|. Divide.