Sidorenko's conjecture

Read-back of TenChallenges.challenge_04. The declaration is a theorem with the following explicit and implicit arguments, one hypothesis, and one conclusion.

Binders. Let $W$ and $V$ be two sets (arbitrary types; both are implicit arguments), each equipped with a finiteness structure, so that $W$ and $V$ are finite sets; $W$ is allowed to be empty, while $V$ is additionally assumed to be nonempty (a separate typeclass hypothesis). Let $H$ be a simple graph with vertex set $W$ and let $G$ be a simple graph with vertex set $V$ (a simple graph being a symmetric, irreflexive adjacency relation $\sim$: no loops, no multiple edges, no orientation). Both $H$ and $G$ are universally quantified; nothing further is assumed about $G$.

Hypothesis ($hH$). There exist two subsets $X, Y \subseteq W$ such that

• $H$ is bipartite with parts $X, Y$ in Mathlib's sense (IsBipartiteWith), which is the conjunction of two conditions: (i) $X$ and $Y$ are disjoint; (ii) for all vertices $a, b \in W$ with $a \sim_H b$, either ($a \in X$ and $b \in Y$) or ($a \in Y$ and $b \in X$), i.e. every edge of $H$ has one endpoint in $X$ and the other in $Y$; and
• $X \cup Y = W$ (every vertex of $H$ lies in one of the two parts).

Thus $X, Y$ form a partition of the vertex set $W$ (either part may be empty) with no edge of $H$ inside $X$ or inside $Y$. No bound on the sizes of $X$ or $Y$ is imposed in this hypothesis, and no bound on the number of vertices or edges of $H$: $H$ is an arbitrary finite bipartite graph. In particular the hypothesis is satisfied by every edgeless graph (take $X = W$, $Y = \emptyset$), by the graph on the empty vertex set, by graphs with isolated vertices, and by disconnected graphs; the bipartition is only required to exist, not to be unique, balanced, or connected. For a graph $H$ that is not bipartite (e.g. containing an odd cycle) the hypothesis fails and the theorem asserts nothing. (This hypothesis differs from the bundle's own BipartiteBoundedBy predicate, which is not used here: that predicate additionally requires $|X| \le k$ and $|Y| \le k$ for a parameter $k$.)

Conclusion. "Sidorenko holds for $H$ over $G$" (the bundle's SidorenkoFor H G), which is the single real-number inequality

whose ingredients are defined in the bundle as follows.

• Homomorphism density. For a graph $H'$ on a finite vertex set $W'$ and the graph $G$ on $V$,

the number of all maps from $W'$ to $V$ (not required to be injective) that send every adjacent pair of $H'$ to an adjacent pair of $G$, divided by $|V|$ raised to the natural-number power $|W'|$. Because $V$ is nonempty, $|V| \ge 1$ and the denominator is positive, so no division by zero occurs. If $W'$ is empty there is exactly one map and $|V|^0 = 1$, so $t(H', G) = 1$; if $H'$ has no edges then every map qualifies and again $t(H', G) = 1$.

• The edge $K_2$. $K_2$ denotes the complete graph on the two-element set $\{0, 1\}$ (two vertices, adjacent iff distinct). A map $f : \{0,1\} \to V$ is a homomorphism from $K_2$ to $G$ iff $f(0) \sim_G f(1)$, so $t(K_2, G) = \#\{(u, v) \in V^2 : u \sim_G v\} / |V|^2 = 2 e(G) / |V|^2$, where $e(G)$ is the number of edges of $G$. If $G$ has no edges, $t(K_2, G) = 0$.
• The exponent $e(H)$ is the number of edges of $H$, i.e. the cardinality of the (finite) set of unordered adjacent pairs of $H$; the right-hand side is the real number $t(K_2, G)$ raised to this natural number. When $e(H) = 0$ the right-hand side equals $1$, even if $t(K_2, G) = 0$ (the convention $0^0 = 1$ is in force).

Logical shape. The inequality is non-strict ($\ge$). Altogether the theorem states: for every finite set $W$, every finite nonempty set $V$, every simple graph $H$ on $W$ and every simple graph $G$ on $V$, if $H$ admits a bipartition $W = X \sqcup Y$ with all edges of $H$ crossing between $X$ and $Y$, then $t(H, G) \ge t(K_2, G)^{e(H)}$. The statement is purely universal (the only existential quantifier is inside the hypothesis, asserting that some bipartition exists); $G$ may be edgeless, complete, disconnected, or a single vertex, and $H$ may be any finite bipartite graph of any size.