The Moyal bracket of a potential, and the classical limit

Category: 1-Mathlib (staged for upstream). BACKLOG #64.

For H(x, ξ) = 2π²ξ² + V(x) the Wigner function obeys ∂_t W = −2πξ ∂_x W + (the potential term). The kinetic half is exactly classical and is already proved, as a flow rather than as a PDE: ★★ wigner_freeSchrodingerS of Wigner.lean says the free evolution moves W along x ↦ x − 2πtξ, with no quantum correction at all. This file does the potential half, where the correction lives.

• wignerKernel₂, wigner₂ — the cross Wigner function, of which wigner is the diagonal case (wignerKernel₂_self);
• moyalPot V ψ — the potential term, the Wigner transform of −i[V, ·] on the kernel, with ★★★ moyalPot_eq_comm identifying it with −i times a difference of cross Wigner functions — so the integral against the symmetric difference V(x + y/2) − V(x − y/2) really is the commutator;
• ★★ deriv_wigner_right — the ξ-derivative of W brings the factor −2πiy into the integral, which is what turns the leading Taylor term of the symmetric difference into a Poisson bracket;
• ★★ norm_symmDiff_sub_le — |V(x+h) − V(x−h) − 2hV'(x)| ≤ Ch³/3 when |V'''| ≤ C, by three integrations by parts of the symmetric differences; norm_symmDiff_sub_le' is the either-sign form;
• ★★★ norm_moyalPot_sub_poisson_le — the classical limit with its remainder: ‖moyalPot V ψ (x, ξ) − (1/2π) V'(x) ∂_ξ W‖ ≤ (sup|V'''|/24) ∫ |y|³ |K_ψ(x, y)| dy. The constant 1/24 is the textbook one, and in the scaling ξ = p/2πℏ the third moment carries the ℏ²: this is {H, W}_M = {H, W} + O(ℏ²) for the potential term;
• ★★★ moyalPot_eq_poisson_of_third_deriv_zero — and when V''' = 0 the two brackets are equal. Linear and quadratic potentials — the uniform force and the harmonic oscillator — evolve their Wigner functions exactly classically, which with the free case covers the whole exactly-classical family.

Honest scope

⚠️ This is the generator, not the evolution. moyalPot is the potential term of the Wigner equation, and the theorems compare it with the Poisson bracket pointwise in (x, ξ). The time-dependent statement ∂_t W_{U_V(t)ψ} = − 2πξ ∂_x W + moyalPot V ψ is not proved here; it is now proved on L², in WignerPotential.lean (★★★ hasDerivAt_wignerL2_schrodinger_eq, 2026-10-21), with the potential term moyalPotL2 V ψ_t ψ_t, which is this file's moyalPot V ψ on Schwartz states (moyalPotL2_toLp). The route: the free group case on Schwartz states in WignerEvolution.lean (★★★ wigner_liouville, 2026-10-01); the Wigner function moved to L² and differentiated along the interacting orbit in WignerL2.lean (#167), the H₀ half in WignerFree.lean (#168), the V half and the assembly in WignerPotential.lean (#169). Differentiating W in x needs only first-order differentiation under the integral sign, which the pin has (Mathlib/Analysis/Calculus/ParametricIntegral.lean); what it lacks is the all-orders version, which is #92(a)'s gap, not this one. The propagator obstacle this paragraph once named (no generator or domain theory for H₀ + V) was removed by Semigroup/PhaseGeneratorDomain.lean (#154).

⚠️ ℏ is not a variable here. The convention is the one of Wigner.lean (𝓕 f ξ = ∫ e^{−2πiyξ} f y dy, momentum p = 2πξ, so ℏ = 1). The ℏ² of the row is the third moment ∫ |y|³ |K| under ξ = p/2πℏ; no ℏ-indexed family of transforms is defined, so the ℏ → 0 statement is the remainder bound read in that scaling, not a limit theorem about a family.

⚠️ One dimension; V real, three times differentiable with bounded third derivative. The commutator form moyalPot_eq_comm additionally needs V of temperate growth, so that Vψ is Schwartz; the remainder bound does not.

References: J. E. Moyal, Quantum mechanics as a statistical theory, Proc. Cambridge Philos. Soc. 45 (1949) 99 §7 (the bracket and its ℏ² term); M. Hillery, R. F. O'Connell, M. O. Scully, E. P. Wigner, Distribution functions in physics: fundamentals, Phys. Rep. 106 (1984) 121 §3.2; specs/BACKLOG.md #64; #45; #63.

The symmetric difference of a potential is cubic in the step

theorem WignerFunction.norm_symmDiff_V''_le {V'' V''' : ℝ → ℝ} {C : ℝ} (hV'' : ∀ (x : ℝ), HasDerivAt V'' (V''' x) x) (hV''' : Continuous V''') (hC : ∀ (x : ℝ), ‖V''' x‖ ≤ C) (x : ℝ) {u : ℝ} (hu : 0 ≤ u) : ‖V'' (x + u) - V'' (x - u)‖ ≤ 2 * C * u

The symmetric difference of V'' is linear in the step.

theorem WignerFunction.norm_symmDiff_V'_le {V' V'' V''' : ℝ → ℝ} {C : ℝ} (hV' : ∀ (x : ℝ), HasDerivAt V' (V'' x) x) (hV'' : ∀ (x : ℝ), HasDerivAt V'' (V''' x) x) (hV''' : Continuous V''') (hC : ∀ (x : ℝ), ‖V''' x‖ ≤ C) (x : ℝ) {s : ℝ} (hs : 0 ≤ s) : ‖V' (x + s) + V' (x - s) - 2 * V' x‖ ≤ C * s ^ 2

The symmetric second difference of V' is quadratic in the step.

theorem WignerFunction.norm_symmDiff_sub_le {V V' V'' V''' : ℝ → ℝ} {C : ℝ} (hV : ∀ (x : ℝ), HasDerivAt V (V' x) x) (hV' : ∀ (x : ℝ), HasDerivAt V' (V'' x) x) (hV'' : ∀ (x : ℝ), HasDerivAt V'' (V''' x) x) (hV''' : Continuous V''') (hC : ∀ (x : ℝ), ‖V''' x‖ ≤ C) (x : ℝ) {h : ℝ} (hh : 0 ≤ h) : ‖V (x + h) - V (x - h) - 2 * h * V' x‖ ≤ C * h ^ 3 / 3

★★ The odd symmetric difference of a potential is cubic in the step: |V(x+h) − V(x−h) − 2hV'(x)| ≤ C h³/3 when |V'''| ≤ C. This is the Taylor estimate the Moyal remainder is made of. It is proved by hand because the pin's taylor_mean_remainder_lagrange expands about one endpoint of an interval, while the cancellation here is between the two sides of a point — the zeroth, first and second order terms cancel pairwise — so a one-sided expansion does not exhibit it.

The cross Wigner function

theorem WignerFunction.fourier_eq_integral (g : SchwartzMap ℝ ℂ) (ξ : ℝ) : (FourierTransform.fourier g) ξ = ∫ (y : ℝ), ↑(Real.fourierChar (-(y * ξ))) * g y

The Fourier transform of a Schwartz function, written as the integral this file uses.

noncomputable def WignerFunction.wignerKernel₂ (φ ψ : SchwartzMap ℝ ℂ) (x : ℝ) : SchwartzMap ℝ ℂ

The cross Wigner kernel φ(x + y/2) conj (ψ(x − y/2)), of which wignerKernel is the diagonal case.

Equations

• WignerFunction.wignerKernel₂ φ ψ x = WignerFunction.mulConj ((WignerFunction.affineCLM x WignerFunction.half_ne_zero') φ) ((WignerFunction.affineCLM x WignerFunction.neg_half_ne_zero') ψ)

@[simp]

theorem WignerFunction.wignerKernel₂_apply (φ ψ : SchwartzMap ℝ ℂ) (x y : ℝ) : (wignerKernel₂ φ ψ x) y = φ (x + y / 2) * (starRingEnd ℂ) (ψ (x - y / 2))

theorem WignerFunction.wignerKernel₂_self (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : wignerKernel₂ ψ ψ x = wignerKernel ψ x

noncomputable def WignerFunction.wigner₂ (φ ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : ℂ

The cross Wigner function.

Equations

• WignerFunction.wigner₂ φ ψ x ξ = (FourierTransform.fourier (WignerFunction.wignerKernel₂ φ ψ x)) ξ

theorem WignerFunction.wigner₂_eq_integral (φ ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : wigner₂ φ ψ x ξ = ∫ (y : ℝ), ↑(Real.fourierChar (-(y * ξ))) * (φ (x + y / 2) * (starRingEnd ℂ) (ψ (x - y / 2)))

The potential term of the Wigner evolution equation

noncomputable def WignerFunction.mulPot (V : ℝ → ℝ) : SchwartzMap ℝ ℂ →L[ℂ] SchwartzMap ℝ ℂ

Multiplication by a real potential, on Schwartz space.

Equations

• WignerFunction.mulPot V = SchwartzMap.smulLeftCLM ℂ fun (x : ℝ) => ↑(V x)

theorem WignerFunction.mulPot_apply {V : ℝ → ℝ} (hV : Function.HasTemperateGrowth fun (x : ℝ) => ↑(V x)) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ((mulPot V) ψ) x = ↑(V x) * ψ x

noncomputable def WignerFunction.moyalPot (V : ℝ → ℝ) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : ℂ

The potential term of the Wigner (Moyal) evolution equation: the Wigner transform of −i[V, ·] applied to the kernel. For H = 2π²ξ² + V the Wigner function obeys ∂_t W = −2πξ ∂_x W + moyalPot V ψ, the first term being the free transport of wigner_freeSchrodingerS.

Equations

• WignerFunction.moyalPot V ψ x ξ = ∫ (y : ℝ), ↑(Real.fourierChar (-(y * ξ))) * (-Complex.I * ↑(V (x + y / 2) - V (x - y / 2)) * (WignerFunction.wignerKernel ψ x) y)

theorem WignerFunction.integrable_char_mul (g : SchwartzMap ℝ ℂ) (ξ : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => ↑(Real.fourierChar (-(y * ξ))) * g y) MeasureTheory.volume

theorem WignerFunction.moyalPot_eq_comm {V : ℝ → ℝ} (hV : Function.HasTemperateGrowth fun (x : ℝ) => ↑(V x)) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : moyalPot V ψ x ξ = -Complex.I * (wigner₂ ((mulPot V) ψ) ψ x ξ - wigner₂ ψ ((mulPot V) ψ) x ξ)

★★★ The potential term is the Wigner transform of the commutator. moyalPot is defined as an integral against the symmetric difference of V; this identifies it with −i times the difference of two cross Wigner functions, which is the Wigner transform of −i[V, ρ].

The ξ-derivative, and the classical limit

theorem WignerFunction.deriv_wigner_right (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : deriv (fun (ξ : ℝ) => wigner ψ x ξ) ξ = ∫ (y : ℝ), ↑(Real.fourierChar (-(y * ξ))) * (-(2 * ↑Real.pi * Complex.I) * ↑y * (wignerKernel ψ x) y)

★★ The ξ-derivative of the Wigner function brings the factor −2πiy into the integral.

theorem WignerFunction.norm_symmDiff_sub_le' {V V' V'' V''' : ℝ → ℝ} {C : ℝ} (hV : ∀ (x : ℝ), HasDerivAt V (V' x) x) (hV' : ∀ (x : ℝ), HasDerivAt V' (V'' x) x) (hV'' : ∀ (x : ℝ), HasDerivAt V'' (V''' x) x) (hV''' : Continuous V''') (hC : ∀ (x : ℝ), ‖V''' x‖ ≤ C) (x y : ℝ) : ‖V (x + y / 2) - V (x - y / 2) - y * V' x‖ ≤ C / 24 * |y| ^ 3

The bound on the symmetric difference, for either sign of the step.

The classical limit

theorem WignerFunction.continuous_potential {V V' : ℝ → ℝ} (hV : ∀ (x : ℝ), HasDerivAt V (V' x) x) : Continuous V

theorem WignerFunction.integrable_moyalPot_integrand {V V' V'' V''' : ℝ → ℝ} {C : ℝ} (hV : ∀ (x : ℝ), HasDerivAt V (V' x) x) (hV' : ∀ (x : ℝ), HasDerivAt V' (V'' x) x) (hV'' : ∀ (x : ℝ), HasDerivAt V'' (V''' x) x) (hV''' : Continuous V''') (hC : ∀ (x : ℝ), ‖V''' x‖ ≤ C) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => ↑(Real.fourierChar (-(y * ξ))) * (-Complex.I * ↑(V (x + y / 2) - V (x - y / 2)) * (wignerKernel ψ x) y)) MeasureTheory.volume

The Moyal integrand is integrable: the symmetric difference of V grows at most like |y|³ against a Schwartz kernel.

theorem WignerFunction.poisson_eq_integral {V' : ℝ → ℝ} (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : 1 / (2 * ↑Real.pi) * ↑(V' x) * deriv (fun (ξ : ℝ) => wigner ψ x ξ) ξ = ∫ (y : ℝ), ↑(Real.fourierChar (-(y * ξ))) * (-Complex.I * ↑(y * V' x) * (wignerKernel ψ x) y)

The Poisson-bracket term, written as the same kind of integral.

theorem WignerFunction.integrable_poisson_integrand {V' : ℝ → ℝ} (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => ↑(Real.fourierChar (-(y * ξ))) * (-Complex.I * ↑(y * V' x) * (wignerKernel ψ x) y)) MeasureTheory.volume

theorem WignerFunction.norm_moyalPot_sub_poisson_le {V V' V'' V''' : ℝ → ℝ} {C : ℝ} (hV : ∀ (x : ℝ), HasDerivAt V (V' x) x) (hV' : ∀ (x : ℝ), HasDerivAt V' (V'' x) x) (hV'' : ∀ (x : ℝ), HasDerivAt V'' (V''' x) x) (hV''' : Continuous V''') (hC : ∀ (x : ℝ), ‖V''' x‖ ≤ C) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : ‖moyalPot V ψ x ξ - 1 / (2 * ↑Real.pi) * ↑(V' x) * deriv (fun (ξ : ℝ) => wigner ψ x ξ) ξ‖ ≤ C / 24 * ∫ (y : ℝ), |y| ^ 3 * ‖(wignerKernel ψ x) y‖

★★★ The classical limit of the Moyal bracket, with its remainder. The potential term of the Wigner evolution differs from the Poisson-bracket term (1/2π) V'(x) ∂_ξ W by at most (sup |V'''| / 24) · ∫ |y|³ |K_ψ(x, y)| dy. In the scaling ξ = p/2πℏ the third moment carries ℏ², so this is the ℏ² remainder of the Moyal series: the Moyal bracket is the Poisson bracket up to the third derivative of the potential.

theorem WignerFunction.moyalPot_eq_poisson_of_third_deriv_zero {V V' V'' V''' : ℝ → ℝ} (hV : ∀ (x : ℝ), HasDerivAt V (V' x) x) (hV' : ∀ (x : ℝ), HasDerivAt V' (V'' x) x) (hV'' : ∀ (x : ℝ), HasDerivAt V'' (V''' x) x) (hV''' : Continuous V''') (hV0 : ∀ (x : ℝ), V''' x = 0) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : moyalPot V ψ x ξ = 1 / (2 * ↑Real.pi) * ↑(V' x) * deriv (fun (ξ : ℝ) => wigner ψ x ξ) ξ

★★★ For a potential with vanishing third derivative the Moyal bracket is the Poisson bracket. Linear and quadratic potentials — the free particle, the uniform force, the harmonic oscillator — have exactly classical phase-space evolution, which is the companion of wigner_freeSchrodingerS for the potential term.