Derivative correlations force additive frequency energy (source code)

= Derivative correlations force additive frequency energy
{title2=$E_\theta(H)\geq(\beta\eta)^4|G|^3$}

Suppose $|f|\leq1$ on a finite cyclic group, $H$ has density $\beta$, and for each $h\in H$ the <multiplicative derivative> has a <Fourier coefficient on a finite abelian group> of magnitude at least $\eta$ at $\theta(h)$. Align the correlation phases, apply <Cauchy-Schwarz>, group pairs by their shift and frequency differences, and apply <Parseval identity>. This proves the displayed lower bound on <additive energy of a frequency graph> without replacing exact frequency equalities by approximate ones.