noncomputable def SidorenkoCompleteBipartite.homCountBip {W : Type u_1} [Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] (s t : ℕ) : ℕ

Homomorphism count $\mathrm{hom}(K_{s,t}, G)$ from the complete bipartite graph $K_{s,t}$ into $G$: choose an $s$-tuple $\mathbf{x}$ in $V(G)$, then count its common neighborhood and raise to the power $t$.

theorem SidorenkoCompleteBipartite.nat_jensen_pow {ι : Type u_1} (s : Finset ι) (f : ι → ℕ) (n : ℕ) : (∑ i ∈ s, f i) ^ (n + 1) ≤ s.card ^ n * ∑ i ∈ s, f i ^ (n + 1)

Jensen-style inequality for $\mathbb{N}$-valued sums: $(\sum_i f(i))^{n+1} \le |s|^n \sum_i f(i)^{n+1}$.

theorem SidorenkoCompleteBipartite.key_inequality {W : Type u_1} [Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] (s t : ℕ) (hs : 0 < s) (ht : 0 < t) (_hW : 0 < Fintype.card W) : (2 * G.edgeFinset.card) ^ (s * t) ≤ Fintype.card W ^ (2 * s * t - s - t) * homCountBip G s t

Core inequality for Sidorenko on complete bipartite graphs: twice the edge count to the power $st$ is at most $n^{2st - s - t}$ times the homomorphism count $\mathrm{hom}(K_{s,t}, G)$, where $n = |V(G)|$.

theorem SidorenkoCompleteBipartite.sidorenko_completeBipartite (s t : ℕ) (hs : 0 < s) (ht : 0 < t) {W : Type u_1} [Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] (hW : 0 < Fintype.card W) : ↑(homCountBip G s t) / ↑(Fintype.card W) ^ (s + t) ≥ (2 * ↑G.edgeFinset.card / ↑(Fintype.card W) ^ 2) ^ (s * t)

Theorem 10.3.6 (Sidorenko for complete bipartite graphs). For any graph $G$ on $n$ vertices and $m$ edges, the homomorphism density of $K_{s,t}$ in $G$ is bounded below by the $(st)$-th power of the edge density: $$ \frac{\mathrm{hom}(K_{s,t}, G)}{n^{s+t}} \ge \left( \frac{2m}{n^2} \right)^{st}. $$