Integration by parts for a local phase rotation: $\int \delta_x G = 0$

Proved

WardTakahashi.integral_localVar_eq_zero

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsquantum-field-theoryward-identity

Let $G:\mathbb C^N\to\mathbb C$ be continuously (real-)differentiable, let $x$ be a site, and assume that

$\varphi\mapsto\|\varphi\|\,|G(\varphi)|$ is integrable, and
$\varphi\mapsto\|\varphi\|\,\|DG(\varphi)\|$ is integrable (operator norm).

Then

\int_{\mathbb C^N}\delta_xG(\varphi)\,d\varphi=\int_{\mathbb C^N}DG(\varphi)\,[g_x\varphi]\,d\varphi=0 .

This is the infinitesimal statement that Lebesgue measure is invariant under local phase rotations of a single site; the integrability conditions play the role of the source's assumption that surface terms can be neglected.

Formalization Note $\|\varphi\|$ is the sup norm on $\mathbb C^N$ .

Preamble

import Mathlib
import Definitions.Def_WardTakahashi_LatticeU1

open MeasureTheory Complex

Formal statement

namespace WardTakahashi

theorem integral_localVar_eq_zero {N : ℕ} (G : FieldConfig N → ℂ) (hG : ContDiff ℝ 1 G)
    (x : Fin N)
    (h1 : Integrable (fun φ : FieldConfig N => ‖φ‖ * ‖G φ‖))
    (h2 : Integrable (fun φ : FieldConfig N => ‖φ‖ * ‖fderiv ℝ G φ‖)) :
    ∫ φ, localVar x G φ = 0 := by sorry

end WardTakahashi

Source

Wikipedia, "Ward–Takahashi identity" (revision oldid=1374751657), https://en.wikipedia.org/w/index.php?title=Ward%E2%80%93Takahashi_identity&oldid=1374751657 ; section "Derivation in the path integral formulation" (finite-dimensional lattice model)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — NON-BLIND, same agent that drafted the statements

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 $N$ , every function $G:\mathbb C^N\to\mathbb C$ that is continuously real-differentiable ( $C^1$ over $\mathbb R$ ), every site $x$ , provided

the function $\varphi\mapsto\|\varphi\|\cdot|G(\varphi)|$ is Lebesgue integrable on $\mathbb C^N$ , and
the function $\varphi\mapsto\|\varphi\|\cdot\|DG(\varphi)\|$ is Lebesgue integrable, where $\|DG(\varphi)\|$ is the operator norm of the real derivative,

it holds that

\int_{\mathbb C^N}DG(\varphi)\,[g_x\varphi]\,d\varphi=0,

where $g_x\varphi$ equals $i\varphi_x$ at site $x$ and $0$ elsewhere, and $\|\varphi\|=\max_y|\varphi_y|$ . (If the integrand were not integrable the left side would be $0$ by convention.) Note that integrability of $G$ itself is not assumed.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Integration by parts for a local phase rotation: ∫δxG=0\int \delta_x G = 0∫δx​G=0

Integration by parts for a local phase rotation: $\int \delta_x G = 0$