Solution (source code)

= Solution

Give $X\times Y$ the uniform <probability measure> and let $f$ be the <indicator function> of the edge set. For partitions $\mathcal P=\{X_i\}$ and $\mathcal Q=\{Y_j\}$, define the energy
$$
\mathcal E(\mathcal P,\mathcal Q)
=\left\|\mathbb E(f\mid\mathcal P\otimes\mathcal Q)\right\|_2^2
=\sum_{i,j}\frac{|X_i||Y_j|}{|X||Y|}d(X_i,Y_j)^2.
$$
Because <conditional expectation> is an <orthogonal projection> in <L2 space>, $0\leq\mathcal E\leq\|f\|_2^2\leq1$.

Suppose the pair of partitions is not $\varepsilon$-regular. For each irregular $(X_i,Y_j)$ choose witnesses $A_{ij}\subseteq X_i$ and $B_{ij}\subseteq Y_j$ with
$$
|A_{ij}|\geq\varepsilon|X_i|,qquad
|B_{ij}|\geq\varepsilon|Y_j|,qquad
|d(A_{ij},B_{ij})-d(X_i,Y_j)|>\varepsilon.
$$
Refine each $X_i$ by all sets $A_{ij}$ and each $Y_j$ by all sets $B_{ij}$. If the old partitions have $r,s$ cells, the refined ones have at most $r2^s,s2^r$ cells.

The <Pythagorean theorem> for the two nested conditional-expectation projections gives
$$
\mathcal E(\mathcal P',\mathcal Q')-\mathcal E(\mathcal P,\mathcal Q)
=\left\|\mathbb E(f\mid\mathcal P'\otimes\mathcal Q')-
\mathbb E(f\mid\mathcal P\otimes\mathcal Q)\right\|_2^2.
$$
Inside an irregular $X_i\times Y_j$, the witness rectangle occupies at least an $\varepsilon^2$ proportion and the mean of the displayed difference over it has magnitude greater than $\varepsilon$. The <Cauchy-Schwarz inequality> therefore gives an energy gain greater than
$$
\varepsilon^4\frac{|X_i||Y_j|}{|X||Y|}
$$
from that pair. Since irregular pairs have total weight greater than $\varepsilon$, the complete refinement raises the energy by more than $\varepsilon^5$.

Energy is at most one, so after at most $\lceil\varepsilon^{-5}\rceil$ refinements the process stops at an $\varepsilon$-regular pair of partitions. Iterating the cell-count bounds $r\mapsto r2^s$ and $s\mapsto s2^r$ from $r=s=1$ a bounded number of times produces a finite $K(\varepsilon)$ independent of $G$. This proves the <Bipartite Szemerédi regularity lemma>.