def Sidorenko.HasUniversalVertex {A : Type u_1} {B : Type u_2} (F : SimpleGraph (A ⊕ B)) : Prop

A bipartite graph $F$ on $A \sqcup B$ has a "universal vertex" if some vertex in $A$ is adjacent to every vertex of $B$, or some vertex in $B$ is adjacent to every vertex of $A$. This is the hypothesis of the Conlon-Fox-Sudakov theorem on Sidorenko's conjecture.

theorem Sidorenko.entropy_bound_hom_count {A : Type u_1} {B : Type u_2} {W : Type u_3} [Fintype A] [Fintype B] [Fintype W] [DecidableEq A] [DecidableEq B] [DecidableEq W] (F : SimpleGraph (A ⊕ B)) [DecidableRel F.Adj] (G : SimpleGraph W) [DecidableRel G.Adj] (hF : HasUniversalVertex F) (hW : 0 < Fintype.card W) : ↑(Nat.card (F →g G)) ≥ (↑(Nat.card (⊤ →g G)) / ↑(Nat.card W) ^ Nat.card (Fin 2)) ^ F.edgeFinset.card * ↑(Nat.card W) ^ Nat.card (A ⊕ B)

Entropy-style hom-count lower bound underlying the Conlon-Fox-Sudakov theorem: for a bipartite graph $F$ with a universal vertex, $$ \mathrm{hom}(F, G) \ge \left( \frac{\mathrm{hom}(K_2, G)}{|V(G)|^2} \right)^{|E(F)|} \cdot |V(G)|^{|V(F)|}. $$

theorem Sidorenko.hasUniversalVertex_edgeFinset_pos {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (F : SimpleGraph (A ⊕ B)) [DecidableRel F.Adj] (hF : HasUniversalVertex F) : 0 < F.edgeFinset.card

A bipartite graph with a universal vertex has at least one edge, so its edge set is non-empty. Used to avoid degenerate corner cases.

theorem Sidorenko.sidorenko_of_hasUniversalVertex {A : Type u_1} {B : Type u_2} {W : Type u_3} [Fintype A] [Fintype B] [Fintype W] [DecidableEq A] [DecidableEq B] [DecidableEq W] [Nonempty A] [Nonempty B] (F : SimpleGraph (A ⊕ B)) [DecidableRel F.Adj] (G : SimpleGraph W) [DecidableRel G.Adj] (hF : HasUniversalVertex F) : homDensity F G ≥ homDensity ⊤ G ^ F.edgeFinset.card

Theorem 10.3.7 (Conlon-Fox-Sudakov 2010). Sidorenko's conjecture holds for any bipartite graph $F$ that has a universal vertex on one side: $\mathrm{hom\text{-}density}(F, G) \ge \mathrm{hom\text{-}density}(K_2, G)^{|E(F)|}$.