Invariance of the lattice measure under global $U(1)$ rotations

Note — NON-BLIND read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle by Harmonic), with full knowledge of the source material and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; an independent blind read-back is still recommended before submission.

Throughout: $\mathbb C^N$ is the space of functions $\varphi:\{0,\dots,N-1\}\to\mathbb C$ (with $N\ge 0$ arbitrary, so the case $N=0$ of a one-point space is included), regarded as a real vector space of dimension $2N$ with the sup norm $\|\varphi\|=\max_y|\varphi_y|$ and with Lebesgue (product) measure $d\varphi$. All derivatives $D$ are real Fréchet derivatives. All integrals are Bochner integrals, which by convention equal $0$ when the integrand is not integrable. "Integrable" means Lebesgue integrable (including almost-everywhere strong measurability). $\delta_{ab}$ is $1$ if $a=b$ and $0$ otherwise.

For every natural number $N$ (including $N=0$) and every real number $\theta$: the map $R_\theta:\mathbb C^N\to\mathbb C^N$, $(R_\theta\varphi)_y=e^{i\theta}\varphi_y$, is measure preserving from Lebesgue measure on $\mathbb C^N$ to Lebesgue measure on $\mathbb C^N$; that is, $R_\theta$ is measurable and the push-forward of Lebesgue measure under $R_\theta$ equals Lebesgue measure. There are no further hypotheses.