The free Wigner equation

Category: 1-Mathlib (CSD-free; staged for upstream).

Wigner.lean proves that the free group transports the Wigner function rigidly, W_{U₀(t)ψ}(x, ξ) = W_ψ(x − 2πtξ, ξ), and MoyalBracket.lean proves that the potential term of the Wigner equation is the Wigner transform of the commutator, with its ℏ² remainder. Both are statements about the generator. This module (BACKLOG #64, the time-dependent half) writes the evolution equation itself, for the free Hamiltonian:

• ★ norm_mul_norm_le — the Wigner integrand ψ(x + y/2) conj ψ(x − y/2) decays like 1/(1 + y²) uniformly in the position: the two arguments differ by y, so 1 + y² ≤ 2(1 + (x + y/2)²)(1 + (x − y/2)²) and the two Schwartz bounds (exists_bound_one_add_sq) multiply with no x left over;
• ★★ hasDerivAt_wigner_left — the Wigner function is differentiable in the position, and ∂_x W_ψ = W(ψ', ψ) + W(ψ, ψ') (wignerPosDeriv), a sum of the cross Wigner functions of MoyalBracket.lean. The derivative passes under the Fourier integral by Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le, dominated by the uniform bound above; the deriv form is deriv_wigner_left;
• ★ hasDerivAt_wigner_freeSchrodingerS_pos — the x-derivative of the evolved function is the transported x-derivative (the flow moves W rigidly, so it moves its derivative with it);
• ★★ hasDerivAt_wigner_freeSchrodingerS_time — the time derivative is −2πξ times that same transported derivative, by differentiating the transport identity in t;
• ★★★ wigner_liouville — the free Wigner equation: ∂_t W_t(x, ξ) = − 2πξ ∂_x W_t(x, ξ) for W_t = W_{U₀(t)ψ}, which in the momentum p = 2πξ is ∂_t W + p ∂_x W = 0 (wigner_liouville_add_eq_zero) — the classical Liouville equation, exact, with no quantum correction. Both derivatives are of the same function at the same point, so this is a partial differential equation satisfied by the quantum phase-space density, not a pair of separately computed expressions.

Honest scope

⚠️ Free Hamiltonian only, in this file. The interacting equation ∂_t W_{U_V(t)ψ} = − 2πξ ∂_x W + moyalPot V ψ is proved on L² in WignerPotential.lean (★★★ hasDerivAt_wignerL2_schrodinger_eq, 2026-10-21), through WignerL2.lean (#167) and WignerFree.lean (#168), once Semigroup/PhaseGeneratorDomain.lean (#154) had made the H₀ + V propagator classical on dom H₀. The orbit U_V(t)ψ leaves Schwartz space, which is why that equation is stated for the L² Wigner function wignerL2, not for this file's wigner; the two agree on Schwartz states (wignerL2_toLp).

⚠️ What the pin does have, contrary to #64's earlier measurement, is first-order differentiation under the integral sign (Mathlib/Analysis/Calculus/ParametricIntegral.lean), which is all ∂_x W needs. What is absent is the all-orders-with-bounds version — that file has no ContDiff or iteratedFDeriv lemma at all (MATHLIB-ABSENT(contDiff_integral)) — and that, not this, is the gap #92(a) runs into.

⚠️ One dimension, Schwartz data. No statement is made about W as a function of two variables beyond the slicewise derivatives, and nothing here is a smoothness claim about W on the plane.

References: J. E. Moyal, Quantum mechanics as a statistical theory, Proc. Cambridge Philos. Soc. 45 (1949) 99 §7; M. Hillery, R. F. O'Connell, M. O. Scully, E. P. Wigner, Phys. Rep. 106 (1984) 121 §3.1 (the Wigner equation and its free case); Wigner.lean, MoyalBracket.lean; specs/BACKLOG.md #64; specs/future-work.md.

A bound on the Wigner integrand, uniform in the position

theorem WignerFunction.exists_bound_one_add_sq (f : SchwartzMap ℝ ℂ) : ∃ (C : ℝ), 0 < C ∧ ∀ (z : ℝ), (1 + z ^ 2) * ‖f z‖ ≤ C

Schwartz decay in the form the parametric derivative needs: (1 + z²)‖f z‖ is bounded.

theorem WignerFunction.norm_mul_norm_le {f g : SchwartzMap ℝ ℂ} {C D : ℝ} (hf : ∀ (z : ℝ), (1 + z ^ 2) * ‖f z‖ ≤ C) (hg : ∀ (z : ℝ), (1 + z ^ 2) * ‖g z‖ ≤ D) (x y : ℝ) : ‖f (x + y / 2)‖ * ‖g (x - y / 2)‖ ≤ 2 * C * D * (1 + y ^ 2)⁻¹

★ The Wigner integrand decays in y, uniformly in the position x. The two arguments x ± y/2 differ by y, so 1 + y² ≤ 2(1 + (x + y/2)²)(1 + (x − y/2)²) and the two Schwartz bounds multiply with no x left over. This uniformity is what lets the x-derivative pass under the Fourier integral.

theorem WignerFunction.integrable_phase_mul_kernel₂ (φ ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => ↑(Real.fourierChar (-(y * ξ))) * (φ (x + y / 2) * (starRingEnd ℂ) (ψ (x - y / 2)))) MeasureTheory.volume

The Wigner integrand is integrable: the kernel is Schwartz and the character is unimodular.

The x-derivative of the Wigner function

noncomputable def WignerFunction.wignerPosDeriv (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : ℂ

The x-derivative of the Wigner function, written as a sum of cross Wigner functions: ∂_x W_ψ = W(ψ', ψ) + W(ψ, ψ'). That this is the derivative is hasDerivAt_wigner_left.

Equations

• WignerFunction.wignerPosDeriv ψ x ξ = WignerFunction.wigner₂ ((SchwartzMap.derivCLM ℂ ℂ) ψ) ψ x ξ + WignerFunction.wigner₂ ψ ((SchwartzMap.derivCLM ℂ ℂ) ψ) x ξ

theorem WignerFunction.hasDerivAt_wignerKernel_left (ψ : SchwartzMap ℝ ℂ) (x y : ℝ) : HasDerivAt (fun (z : ℝ) => ψ (z + y / 2) * (starRingEnd ℂ) (ψ (z - y / 2))) (deriv (⇑ψ) (x + y / 2) * (starRingEnd ℂ) (ψ (x - y / 2)) + ψ (x + y / 2) * (starRingEnd ℂ) (deriv (⇑ψ) (x - y / 2))) x

The x-derivative of the integrand, pointwise in y: the product rule, with conj carried through by HasDerivAt.star.

theorem WignerFunction.hasDerivAt_wigner_left (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : HasDerivAt (fun (z : ℝ) => wigner ψ z ξ) (wignerPosDeriv ψ x ξ) x

★★ The Wigner function is differentiable in the position, and the derivative is a sum of cross Wigner functions: ∂_x W_ψ(x, ξ) = W(ψ', ψ)(x, ξ) + W(ψ, ψ')(x, ξ).

The derivative passes under the Fourier integral by Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le, dominated by 4CD/(1 + y²) — a bound that does not depend on the position at all (norm_mul_norm_le), which is why no local-uniformity argument is needed.

theorem WignerFunction.deriv_wigner_left (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : deriv (fun (z : ℝ) => wigner ψ z ξ) x = wignerPosDeriv ψ x ξ

The free Wigner equation

theorem WignerFunction.hasDerivAt_wigner_freeSchrodingerS_pos (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : HasDerivAt (fun (z : ℝ) => wigner ((SchrodingerGroup.freeSchrodingerS t) ψ) z ξ) (wignerPosDeriv ψ (x - 2 * Real.pi * t * ξ) ξ) x

★ The x-derivative of the evolved Wigner function is the transported x-derivative: the free flow moves W rigidly, so it moves its derivative with it.

theorem WignerFunction.hasDerivAt_wigner_freeSchrodingerS_time (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : HasDerivAt (fun (s : ℝ) => wigner ((SchrodingerGroup.freeSchrodingerS s) ψ) x ξ) (-(2 * ↑Real.pi * ↑ξ) * wignerPosDeriv ψ (x - 2 * Real.pi * t * ξ) ξ) t

★★ The time derivative of the free Wigner function is −2πξ times its x-derivative: differentiating the exact transport W_t(x, ξ) = W_0(x − 2πtξ, ξ) in the time.

theorem WignerFunction.wigner_liouville (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : deriv (fun (s : ℝ) => wigner ((SchrodingerGroup.freeSchrodingerS s) ψ) x ξ) t = -(2 * ↑Real.pi * ↑ξ) * deriv (fun (z : ℝ) => wigner ((SchrodingerGroup.freeSchrodingerS t) ψ) z ξ) x

★★★ The free Wigner equation: for W_t = W_{U₀(t)ψ}, ∂_t W_t(x, ξ) = −2πξ ∂_x W_t(x, ξ) — in the momentum p = 2πξ, ∂_t W + p ∂_x W = 0, the classical Liouville equation, exactly and with no quantum correction. Both derivatives are of the same function at the same point: the identity closes because the free flow transports W rigidly (hasDerivAt_wigner_freeSchrodingerS_pos).

theorem WignerFunction.wigner_liouville_add_eq_zero (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : deriv (fun (s : ℝ) => wigner ((SchrodingerGroup.freeSchrodingerS s) ψ) x ξ) t + 2 * ↑Real.pi * ↑ξ * deriv (fun (z : ℝ) => wigner ((SchrodingerGroup.freeSchrodingerS t) ψ) z ξ) x = 0

★★ The same equation in the form the physics writes it: ∂_t W + p ∂_x W = 0 with p = 2πξ.