Weighted Szemerédi regularity lemma (source code)

= Weighted Szemerédi regularity lemma
{title2=$\sum_{(i,j)\text{ irregular}}|V_i||V_j|\leq\varepsilon n^2$}

For every $\varepsilon>0$, all sufficiently large finite <graphs> admit a <set partition> into at most $M(\varepsilon)$ nonempty cells, each of size at most $\varepsilon n$, with the displayed ordered irregular-pair weight bound. Start with small cells. Use <regularity energy> including diagonal rectangles, refine simultaneously by the witness subsets of all <irregular pairs>, and apply the <refinement variance identity for regularity energy>. Each failing round raises energy by more than $\varepsilon^5$, while energy lies in $[0,1]$. The recurrence $k\mapsto k2^k$ bounds the final cell count. Equitability is unnecessary for this weighted version.