Sidorenko's conjecture (1993) #
References:
- Wikipedia
- [Si93] Sidorenko, A. (1993). "A correlation inequality for bipartite graphs." Graphs Combin. 9, pp. 201--204.
- [CoFo10] Conlon, D. and Fox, J. (2010). "Bounds for graph regularity and removal lemmas." Geom. Funct. Anal. 22, pp. 1191--1256.
- [KLL18] Kim, J.H., Lee, C., Lee, J. (2018). "Two approaches to Sidorenko's conjecture." Trans. Amer. Math. Soc. 370, pp. 8515--8552.
Sidorenko's conjecture (1993).
For every finite bipartite simple graph $H$ and every finite simple graph $G$:
$t(H, G) \ge t(K_2, G)^{e(H)}$, where $K_2$ denotes the single-edge graph on 2 vertices
(i.e. completeGraph (Fin 2)).
Case H = K_2 (single edge): Sidorenko's inequality holds trivially with equality.
When H is K_2 (the single-edge graph on 2 vertices), e(H) = 1, so the RHS of Sidorenko's
inequality is just t(K_2, G)^1 = t(K_2, G) = t(H, G), which equals the LHS. Hence the
inequality holds as equality.
The proof records that (completeGraph (Fin 2)).edgeFinset.card = 1 and then reduces the claim
to t(K_2, G) ≤ t(K_2, G), which is le_refl.
edgeCount of K_{2,2} (complete bipartite graph on Fin 2 + Fin 2) is 4.
The four edges are {inl 0, inr 0}, {inl 0, inr 1}, {inl 1, inr 0}, {inl 1, inr 1}.
Homomorphism count of K_2 into G equals 2 · #edgeFinset.
A homomorphism K_2 →g G is the same data as an ordered pair (f 0, f 1) of distinct
vertices with G.Adj (f 0) (f 1). These are in bijection with the Darts of G, and
#Darts(G) = 2 · #E(G) by dart_card_eq_twice_card_edges.
The Hom(K_{2,2}, G) decomposition. The number of homomorphisms from
K_{2,2} to G equals ∑_{(a, b) ∈ W × W} |N(a) ∩ N(b)|^2, where N(v) is the
neighbourhood of v in G. Equivalently, summing over ordered pairs
(b₀, b₁) ∈ W × W and counting common neighbours squared.
Math. A homomorphism K_{2,2} →g G is an assignment f : Fin 2 ⊕ Fin 2 → W
with G.Adj (f (inl i)) (f (inr j)) for all i, j ∈ Fin 2. Equivalently, choose
(a₀, a₁) := (f (inl 0), f (inl 1)) arbitrarily in W × W and require
(f (inr 0), f (inr 1)) to both lie in N(a₀) ∩ N(a₁). The count is thus
∑_{(a₀, a₁)} |N(a₀) ∩ N(a₁)|².
Proof. Construct an explicit bijection
(K_{2,2} →g G) ≃ Σ (p : W × W), (N(p.1) ∩ N(p.2)) × (N(p.1) ∩ N(p.2))
by sending a homomorphism f to ⟨(f (inl 0), f (inl 1)), ⟨f (inr 0), f (inr 1)⟩⟩.
The total cardinality of the sigma-product is then
∑_p (Fintype.card (N(p.1) ∩ N(p.2)))² = ∑_p |N(p.1) ∩ N(p.2)|².
K_{2,2} count via a re-indexed sum. Swapping the order of summation, the
Hom(K_{2,2}, G) count equals ∑_{a ∈ W} (G.degree a)² summed over... wait, more
precisely: the sum ∑_{(b₀, b₁)} |N(b₀) ∩ N(b₁)| (without the square) equals
∑_a (G.degree a)², by swapping (∑_{b₀, b₁} ∑_a [a ~ b₀][a ~ b₁]) = ∑_a (∑_b [a ~ b])².
This version of the identity is what appears in the Cauchy-Schwarz step.
Case H = K_{2,2} (four-cycle, also called C_4): Sidorenko's conjecture holds, by
Cauchy–Schwarz.
The textbook statement at H = K_{2,2} is
t(K_2, G)^{e(K_{2,2})} = t(K_2, G)^4 ≤ t(K_{2,2}, G).
Proof sketch. Write d(a) := G.degree a. Then
homCount(K_2, G) = ∑_a d(a) = 2·|E(G)|(handshaking).homCount(K_{2,2}, G) = ∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|²(product structure of bipartite homomorphism).∑_{b₀, b₁} |N(b₀) ∩ N(b₁)| = ∑_a d(a)²(swap sums).- Cauchy–Schwarz #1:
(∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|)² ≤ |W|² · ∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|². - Cauchy–Schwarz #2:
(∑_a d(a))² ≤ |W| · ∑_a d(a)². - Chain:
(∑_a d(a))⁴ ≤ |W|⁴ · homCount(K_{2,2}, G). - Divide by
|W|^8to gett(K_2, G)^4 ≤ t(K_{2,2}, G).
The proof uses Finset.sum_mul_sq_le_sq_mul_sq (discrete Cauchy–Schwarz) from
Mathlib.Algebra.Order.BigOperators.Ring.Finset.
Status (2026-04-22): main theorem closed sorry-free. See [Si93].
Consequence of homDensity_le_one: both sides of the Sidorenko K_{2,2}
inequality are bounded above by 1. This is a trivial consequence, recorded
as a sanity check on the helper infrastructure in
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HomDensity.
If the domain of H has at most one vertex, H has no edges.
Proof. SimpleGraph.Adj is irreflexive, so any adjacency H.Adj u v forces
u ≠ v; on a subsingleton that's impossible, so no edges exist.
If the domain of H has at most one vertex, every function V → W is a homomorphism
H →g G. Equivalently, homCount H G = |W|^|V|.
Proof. The adjacency H.Adj u v is irreflexive; on a subsingleton it is uninhabited,
so the homomorphism condition H.Adj u v → G.Adj (f u) (f v) is vacuous. Hence the
coe : (H →g G) → (V → W) map is a bijection.
Base case of Sidorenko for trees. When the tree H has at most one vertex,
both sides of Sidorenko's inequality evaluate to 1 (there are no edges, and every
function is a homomorphism). Thus the inequality 1 ≤ 1 holds trivially.
This covers the |V(T)| = 1 base case of the induction on tree size.
Case: H is a tree (Sidorenko 1993).
If H is a finite tree then Sidorenko's inequality holds.
Proof idea (Sidorenko 1993): by induction on the tree, applying Jensen / convexity. The
number of homomorphisms from a tree T with v vertices and v - 1 edges into G factors
nicely in the degree sequence of G, and AM–GM / convexity gives the required lower bound.
Current status (2026-04-22, partial):
- The subsingleton base case (
|V(T)| ≤ 1) is dispatched viasidorenko_tree_subsingleton. - The main inductive step (leaf extraction + AM–GM on the degree sequence) is deferred; it requires a walk-parametrised homomorphism count for trees and a discrete Jensen inequality. See [Si93].
The full proof is left as sorry; the subsingleton case is closed.