Sidorenko's inequality for sides of size at most $4$

Read-back of TenChallenges.challenge_04_r4. The declaration asserts the proposition $\mathrm{statement}_{04}(4)$, which unfolds as follows (the parameter $r$ is fixed to the natural number $r = 4$ throughout).

Quantified objects and hypotheses. For every set $W$ and every set $V$ (both are arbitrary types; they are implicit arguments), each equipped with a finiteness structure (so $W$ and $V$ are finite sets, and $W$ is allowed to be empty), with $V$ additionally assumed to be nonempty, and for every simple graph $H$ with vertex set $W$ and every simple graph $G$ with vertex set $V$ (a simple graph being a symmetric, irreflexive adjacency relation: no loops, no multiple edges, no orientation):

Both of these notions are defined in the bundle, not in Mathlib, and mean the following.

"$H$ is bipartite with sides bounded by $r$" (the bundle's BipartiteBoundedBy H 4) means: there exist two subsets $X, Y \subseteq W$ such that

• $X$ and $Y$ are disjoint, and every edge of $H$ goes between $X$ and $Y$: 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$) [this conjunction is Mathlib's notion "$H$ is bipartite with parts $X, Y$"];
• $X \cup Y = W$ (every vertex lies in one of the two parts);
• $|X| \le r$ and $|Y| \le r$, where $|\cdot|$ is the cardinality of a finite set (since $W$ is finite these are the genuine sizes; no junk value arises).

Hence $|W| = |X| + |Y| \le 2r$; each of $X$, $Y$ may be empty; $H$ may have no edges at all (every edgeless graph on at most $2r$ vertices qualifies, as does the graph on the empty vertex set); and $H$ may have isolated vertices inside $X$ or $Y$. Concretely, for $r = 4$ the graph $H$ has at most $8$ vertices, split into two parts of size at most $4$ each with all edges running between the parts; equivalently $H$ is isomorphic to a subgraph of the complete bipartite graph $K_{4,4}$ (so at most $8$ vertices and at most $16$ edges), including for instance $K_{4,4}$ itself, the cube graph $Q_3$, $C_8$, $C_6$, $C_4$, $K_{3,3}$, $K_{2,4}$, all bipartite graphs on at most $8$ vertices whose two parts both have size $\le 4$, graphs with isolated vertices, and edgeless graphs.

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

whose ingredients are:

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

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$). The statement is purely universal: for all finite $W$, all finite nonempty $V$, all $H$ on $W$, all $G$ on $V$, the implication above holds; no object is asserted to exist. Nothing is assumed about $G$ beyond being a simple graph on a finite nonempty vertex set (it may be edgeless, complete, disconnected, etc.), and nothing beyond the bounded bipartition is assumed about $H$ (it need not be connected, need not have all $2r$ vertices, and the bipartition $X, Y$ is merely required to exist, not to be unique or balanced). For $H$ violating the bipartition condition the implication is vacuously true and nothing is claimed.