/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Analysis.Normed.Ring.Basic
public import Mathlib.Combinatorics.SimpleGraph.Maps@[expose] public sectionHomomorphism 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.
namespace SimpleGraphvariable {V W : Type*}
The number of graph homomorphisms H → G, as a natural number. For finite vertex
types this is just the cardinality of the Hom type.
noncomputable def homCount [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W]
(H : SimpleGraph V) (G : SimpleGraph W) [DecidableRel H.Adj] [DecidableRel G.Adj] : ℕ :=
Fintype.card (H →g G)
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)|}.
noncomputable def homDensity [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W]
(H : SimpleGraph V) (G : SimpleGraph W) [DecidableRel H.Adj] [DecidableRel G.Adj] : ℝ :=
(homCount H G : ℝ) / (Fintype.card W : ℝ) ^ (Fintype.card V)
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.
V:Type u_3W:Type u_4inst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:Nonempty Winst✝³:DecidableEq Vinst✝²:DecidableEq WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.AdjhWpos:0 < Fintype.card Wh₁:Fintype.card (H →g G) ≤ Fintype.card (V → W)h₂:Fintype.card (V → W) = Fintype.card W ^ Fintype.card Vhnat:H.homCount G ≤ Fintype.card W ^ Fintype.card Vhle:↑(H.homCount G) ≤ ↑(Fintype.card W) ^ Fintype.card Vhpos:0 < ↑(Fintype.card W) ^ Fintype.card V⊢ ↑(H.homCount G) ≤ ↑(Fintype.card W) ^ Fintype.card V
All goals completed! 🐙end SimpleGraph