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

Number of graph homomorphisms from $F$ to $G$, denoted $\mathrm{hom}(F, G)$.

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

Homomorphism density of $F$ in $G$, defined as $\mathrm{hom}(F, G) / |V(G)|^{|V(F)|}$.

def SidorenkoInequality.SidorenkoProperty {V : Type u_1} (F : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel F.Adj] [Fintype ↑F.edgeSet] : Prop

Sidorenko's property (Conjecture 10.3.2). A bipartite graph $F$ "satisfies Sidorenko" if for every graph $G$, $\mathrm{hom\text{-}density}(F, G) \ge \mathrm{hom\text{-}density}(K_2, G)^{|E(F)|}$, where $\mathrm{hom\text{-}density}(K_2, G)$ is the edge density of $G$.

theorem sidorenko_of_isTree {V : Type u_1} {F : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel F.Adj] [Fintype ↑F.edgeSet] (hF : F.IsTree) : SidorenkoInequality.SidorenkoProperty F

Theorem 10.3.5 (Sidorenko for trees, generalizing Theorem 10.3.3 for paths). Every finite tree $F$ satisfies the Sidorenko inequality.