Homomorphism density, Sidorenko's inequality, bipartite graphs with bounded sides

Conventions used throughout this file. A simple graph on a type of vertices is a symmetric and irreflexive adjacency relation $\sim$ (undirected, no loops, no multiple edges). $|S|$ denotes the cardinality of a set as a natural number. The file contains three definitions; their vertex types live in arbitrary universes, and their finiteness assumptions differ, so each is listed separately below.

Definition 1: homDensity, written $t(H,G)$. Parameters: a vertex type $W$ and a vertex type $V$, each equipped with a finiteness structure (so both are finite sets of vertices); a simple graph $H$ on $W$; a simple graph $G$ on $V$. The value is the real number

The numerator counts all functions $f$ from $W$ to $V$ (not required to be injective or surjective) such that every pair of $H$-adjacent vertices is sent to a pair of $G$-adjacent vertices (graph homomorphisms $H \to G$); because $G$ has no loops, a function that sends two $H$-adjacent vertices to the same vertex is not counted. The count is formed as a natural number (with the convention that an infinite set counts as $0$; this does not arise, since $W$ and $V$ are finite) and then cast to a real. The denominator is the real number $|V|$ raised to the natural-number power $|W|$. Edge cases the definition silently includes, using the conventions that real division by $0$ yields $0$ and that $x^0 = 1$: (i) if $W = \varnothing$, there is exactly one function (the empty map), the condition holds vacuously, the denominator is $|V|^0 = 1$, and $t(H,G) = 1$ — this holds even when $V = \varnothing$ (as $0^0 = 1$); (ii) if $V = \varnothing$ and $W \neq \varnothing$, there are no functions, the denominator is $0^{|W|} = 0$, and $t(H,G) = 0/0 = 0$; (iii) if $H$ has no edges and $V \neq \varnothing$, every function is counted and $t(H,G) = |V|^{|W|}/|V|^{|W|} = 1$.

Definition 2: SidorenkoFor $H$ $G$. Parameters: as in Definition 1 ($W$ and $V$ finite, $H$ a simple graph on $W$, $G$ a simple graph on $V$). It is the proposition, about these two specific graphs (nothing is quantified),

where: $K_2$ is the complete graph on the two-element vertex set $\{0,1\}$ (its two distinct vertices are adjacent, and nothing else); $t(K_2,G)$ is the density of Definition 1 with $W = \{0,1\}$, i.e. the number of maps $f : \{0,1\} \to V$ with $f(0) \sim_G f(1)$ divided by $|V|^2$ — equivalently, the number of ordered pairs $(u,v) \in V \times V$ with $u \sim_G v$ (which is twice the number of edges of $G$) divided by $|V|^2$, and equal to $0$ when $V = \varnothing$; and $e(H)$ is the number of edges of $H$, i.e. the number of unordered pairs $\{a,b\}$ with $a \sim_H b$, as a natural number (an infinite edge set would count as $0$, which does not arise because $W$ is finite). The exponent is a natural-number power of a real, so when $e(H) = 0$ the right-hand side equals $1$ regardless of $t(K_2,G)$ (even when $t(K_2,G) = 0$). The inequality is non-strict ($\ge$).

Definition 3: BipartiteBoundedBy $H$ $k$. Parameters: a vertex type $W$ with no finiteness assumption (this is the one definition in the file whose signature carries none); a simple graph $H$ on $W$; a natural number $k$. It is the proposition: there exist subsets $X, Y \subseteq W$ such that

• $X$ and $Y$ are disjoint, $X \cap Y = \varnothing$;
• for all $v, w \in W$: if $v \sim_H w$ then ($v \in X$ and $w \in Y$) or ($v \in Y$ and $w \in X$);
• $X \cup Y = W$ (every vertex lies in $X$ or in $Y$);
• $|X| \le k$ and $|Y| \le k$.

The first two bullets are exactly Mathlib's "$H$ is bipartite with parts $X$ and $Y$"; the third adds that the two parts cover all of $W$. Here $|X|$ and $|Y|$ are set cardinalities as natural numbers with the convention that an infinite set has cardinality $0$. Consequently, when $W$ is infinite an infinite part satisfies its bound $|X| \le k$ automatically, for every $k$ including $k = 0$; when $W$ is finite the cardinalities are the true ones. Nothing requires $X$ or $Y$ to be nonempty, nothing requires $H$ to have any edges (an edgeless graph satisfies the adjacency condition for any disjoint cover $X, Y$), and a vertex with no neighbours may be placed on either side. For finite $W$ and $k = 0$ the conditions force $W = \varnothing$.