The Wigner function on Schwartz space

Category: 1-Mathlib (staged for upstream). BACKLOG #45 — the Wigner–Moyal phase-space formulation, the part that is Fourier analysis.

Glossary: https://glossary.constraintsurfacedynamics.com/wigner-function/ Plain-language, CSD-role and formal statements of the Wigner function, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

For ψ ∈ 𝓢(ℝ, ℂ) the Wigner function is the Fourier transform in y of the kernel y ↦ ψ(x + y/2) · conj ψ(x − y/2), in Mathlib's convention 𝓕 f (ξ) = ∫ e^{−2πiyξ} f(y) dy:

W_ψ(x, ξ) = ∫ e^{−2πiyξ} ψ(x + y/2) conj ψ(x − y/2) dy.

The variable ξ is the frequency; the momentum is p = 2πξ (ℏ = m = 1, the convention of SchrodingerGroup.lean, where the free Hamiltonian is the multiplier 2π²ξ²).

• affineCLM x hs, modCLM a — the reparametrisation ψ ↦ ψ(x + s ·) (s ≠ 0) and the modulation ψ ↦ e^{2πia·} ψ as continuous linear maps of Schwartz space;
• wignerKernel ψ x : 𝓢(ℝ, ℂ) — the kernel is Schwartz in y; wigner ψ x ξ — its Fourier transform at ξ;
• ★ conj_wigner, im_wigner — the Wigner function is real;
• ★ integral_wigner_right — the ξ-marginal is the position density: ∫ W_ψ(x, ξ) dξ = |ψ(x)|² (Fourier inversion at the origin);
• ★★ wigner_fourier — the momentum representation: W_{𝓕ψ}(ξ, −x) = W_ψ(x, ξ), by Parseval for Schwartz functions (SchwartzMap.integral_inner_fourier_fourier) applied to the modulated reparametrisations, together with the Fourier transform of an affine reparametrisation (fourier_comp_affine) and of a modulation (fourier_char_mul);
• ★ integral_wigner_left — the x-marginal is the momentum density: ∫ W_ψ(x, ξ) dx = |𝓕ψ(ξ)|²; integral_integral_wigner — total mass ∫|ψ|²; integral_integral_mul_wigner_left/right — the position and momentum expectations are the phase-space moments;
• ★ wigner_gaussianS — the Gaussian is positive: W_{g_σ}(x, ξ) = √(2/σ) e^{−2πσx²} e^{−2πξ²/σ} for the Schwartz Gaussian g_σ = e^{−πσx²}, σ > 0 (wigner_gaussianS_pos);
• ★ wigner_zero_zero_of_odd, re_wigner_zero_zero_neg — negativity is a witness of non-classicality: an odd ψ ≠ 0 has W_ψ(0, 0) = −2∫|ψ|² < 0;
• ★★ wigner_freeSchrodingerS — the free evolution is the classical free flow: W_{U₀(t)ψ}(x, ξ) = W_ψ(x − 2πtξ, ξ), i.e. W_t(x, p) = W_0(x − pt, p) in the momentum p = 2πξ — Liouville transport, exact for the free Hamiltonian (the phase e^{−2π²it[(ξ+η/2)² − (ξ−η/2)²]} = e^{−4π²itξη} is the character of the shift).

Honest scope

⚠️ One dimension, Schwartz data. Only the position and momentum moments of W are here; the Weyl expectation formula for a general symbol, and the overlap identity ∫∫ W_φ conj (W_ψ) = |⟨φ, ψ⟩|² that makes W determine the state, are WignerWeyl.lean (BACKLOG #63). What stays open there: Op(a) as a continuous operator on 𝒮(ℝ, ℂ), symbols of temperate growth, and the Schwartz property of (x, ξ) ↦ W_ψ(x, ξ) on ℝ² with the joint integrability it gives (BACKLOG #92). The Moyal bracket with its ℏ² expansion is MoyalBracket.lean (BACKLOG #64): the potential term of the Wigner equation is the Wigner transform of −i[V, ·] (★★★ moyalPot_eq_comm), it differs from the Poisson bracket by at most (sup|V'''|/24) times the third moment of the kernel (★★★ norm_moyalPot_sub_poisson_le), and the two agree exactly when V''' = 0 (★★★ moyalPot_eq_poisson_of_third_deriv_zero). The remaining part of #64 is the time-dependent equation for U_V(t)ψ, which needs a propagator differentiable on Schwartz functions.

References: E. Wigner, Phys. Rev. 40 (1932) 749; J. E. Moyal, Proc. Cambridge Philos. Soc. 45 (1949) 99; G. B. Folland, Harmonic Analysis in Phase Space (1989) §1.8; Mathlib/Analysis/Semigroup/SchrodingerSchwartz.lean, GaussianPacket.lean; specs/BACKLOG.md #45; specs/future-work.md.

Two continuous linear maps of Schwartz space

theorem WignerFunction.hasTemperateGrowth_affine (x s : ℝ) : Function.HasTemperateGrowth fun (y : ℝ) => x + s * y

y ↦ x + s y has temperate growth.

theorem WignerFunction.antilipschitzWith_affine (x : ℝ) {s : ℝ} (hs : s ≠ 0) : AntilipschitzWith ⟨|s|⁻¹, ⋯⟩ fun (y : ℝ) => x + s * y

y ↦ x + s y is antilipschitz for s ≠ 0.

noncomputable def WignerFunction.affineCLM (x : ℝ) {s : ℝ} (hs : s ≠ 0) : SchwartzMap ℝ ℂ →L[ℂ] SchwartzMap ℝ ℂ

The reparametrisation ψ ↦ (y ↦ ψ(x + s y)), s ≠ 0, on Schwartz space.

Equations

• WignerFunction.affineCLM x hs = SchwartzMap.compCLMOfAntilipschitz ℂ ⋯ ⋯

@[simp]

theorem WignerFunction.affineCLM_apply (x : ℝ) {s : ℝ} (hs : s ≠ 0) (ψ : SchwartzMap ℝ ℂ) (y : ℝ) : ((affineCLM x hs) ψ) y = ψ (x + s * y)

theorem WignerFunction.hasTemperateGrowth_char (a : ℝ) : Function.HasTemperateGrowth fun (y : ℝ) => ↑(Real.fourierChar (a * y))

The character y ↦ e^{2πiay} has temperate growth.

noncomputable def WignerFunction.modCLM (a : ℝ) : SchwartzMap ℝ ℂ →L[ℂ] SchwartzMap ℝ ℂ

The modulation ψ ↦ (y ↦ e^{2πiay} ψ(y)) on Schwartz space.

Equations

• WignerFunction.modCLM a = SchwartzMap.smulLeftCLM ℂ fun (y : ℝ) => ↑(Real.fourierChar (a * y))

@[simp]

theorem WignerFunction.modCLM_apply (a : ℝ) (ψ : SchwartzMap ℝ ℂ) (y : ℝ) : ((modCLM a) ψ) y = ↑(Real.fourierChar (a * y)) * ψ y

Two Fourier identities on ℝ

theorem WignerFunction.conj_fourierChar (t : ℝ) : (starRingEnd ℂ) ↑(Real.fourierChar t) = ↑(Real.fourierChar (-t))

theorem WignerFunction.fourier_char_mul (φ : ℝ → ℂ) (a w : ℝ) : FourierTransform.fourier (fun (y : ℝ) => ↑(Real.fourierChar (a * y)) * φ y) w = FourierTransform.fourier φ (w - a)

Modulation shifts the Fourier transform: 𝓕 (e^{2πia·} φ) (w) = 𝓕 φ (w − a).

theorem WignerFunction.fourier_comp_affine (φ : ℝ → ℂ) (x : ℝ) {s : ℝ} (hs : s ≠ 0) (w : ℝ) : FourierTransform.fourier (fun (y : ℝ) => φ (x + s * y)) w = |s⁻¹| • (↑(Real.fourierChar (x * (w / s))) * FourierTransform.fourier φ (w / s))

The Fourier transform of an affine reparametrisation: 𝓕 (φ(x + s ·)) (w) = |s|⁻¹ e^{2πixw/s} 𝓕 φ (w/s), s ≠ 0.

The Wigner function

theorem WignerFunction.half_ne_zero' : 1 / 2 ≠ 0

theorem WignerFunction.neg_half_ne_zero' : -1 / 2 ≠ 0

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

The Wigner kernel y ↦ ψ(x + y/2) · conj ψ(x − y/2) as a Schwartz function of y.

Equations

• WignerFunction.wignerKernel ψ x = (SchwartzMap.bilinLeftCLM (ContinuousLinearMap.mul ℝ ℂ) ⋯) ((WignerFunction.affineCLM x WignerFunction.half_ne_zero') ψ)

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

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

The Wigner function W_ψ(x, ξ) = ∫ e^{−2πiyξ} ψ(x + y/2) conj ψ(x − y/2) dy.

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)))

theorem WignerFunction.conj_wigner (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : (starRingEnd ℂ) (wigner ψ x ξ) = wigner ψ x ξ

★ The Wigner function is real.

theorem WignerFunction.im_wigner (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : (wigner ψ x ξ).im = 0

theorem WignerFunction.integral_wigner_right (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ∫ (ξ : ℝ), wigner ψ x ξ = ↑‖ψ x‖ ^ 2

★ The ξ-marginal is the position density: ∫ W_ψ(x, ξ) dξ = |ψ(x)|².

The momentum representation

theorem WignerFunction.wigner_fourier (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : wigner (FourierTransform.fourier ψ) ξ (-x) = wigner ψ x ξ

★★ The momentum representation: W_{𝓕ψ}(ξ, −x) = W_ψ(x, ξ) — the Wigner function of the Fourier transform is the Wigner function with the roles of position and frequency exchanged (Parseval on the modulated reparametrisations).

theorem WignerFunction.integral_wigner_left (ψ : SchwartzMap ℝ ℂ) (ξ : ℝ) : ∫ (x : ℝ), wigner ψ x ξ = ↑‖(FourierTransform.fourier ψ) ξ‖ ^ 2

★ The x-marginal is the momentum density: ∫ W_ψ(x, ξ) dx = |𝓕ψ(ξ)|².

theorem WignerFunction.integral_integral_wigner (ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ) (ξ : ℝ), wigner ψ x ξ = ∫ (x : ℝ), ↑‖ψ x‖ ^ 2

Total mass: ∫∫ W_ψ = ∫ |ψ|².

theorem WignerFunction.integral_integral_mul_wigner_left (ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ) (ξ : ℝ), ↑x * wigner ψ x ξ = ∫ (x : ℝ), ↑x * ↑‖ψ x‖ ^ 2

The position expectation is the first x-moment of W_ψ: ∫∫ x W_ψ = ∫ x |ψ(x)|².

theorem WignerFunction.integral_integral_mul_wigner_right (ψ : SchwartzMap ℝ ℂ) : ∫ (ξ : ℝ) (x : ℝ), ↑ξ * wigner ψ x ξ = ∫ (ξ : ℝ), ↑ξ * ↑‖(FourierTransform.fourier ψ) ξ‖ ^ 2

The momentum expectation is the first ξ-moment of W_ψ: ∫∫ ξ W_ψ = ∫ ξ |𝓕ψ(ξ)|² (the momentum is p = 2πξ).

Positivity of the Gaussian, negativity of odd states

theorem WignerFunction.re_ofReal_pos {σ : ℝ} (hσ : 0 < σ) : 0 < (↑σ).re

theorem WignerFunction.wignerKernel_gaussianS {σ : ℝ} (hσ : 0 < σ) (x : ℝ) : wignerKernel (SchrodingerGroup.gaussianS ↑σ ⋯) x = Complex.exp ↑(-(2 * Real.pi * σ * x ^ 2)) • SchrodingerGroup.gaussianS ↑(σ / 2) ⋯

The Wigner kernel of the Gaussian e^{−πσx²} is e^{−2πσx²} · e^{−π(σ/2)y²}.

theorem WignerFunction.wigner_gaussianS {σ : ℝ} (hσ : 0 < σ) (x ξ : ℝ) : wigner (SchrodingerGroup.gaussianS ↑σ ⋯) x ξ = ↑(√(2 / σ) * Real.exp (-(2 * Real.pi * σ * x ^ 2)) * Real.exp (-(2 * Real.pi * ξ ^ 2 / σ)))

★ The Wigner function of the Gaussian g_σ = e^{−πσx²} (σ > 0) is the positive Gaussian √(2/σ) e^{−2πσx²} e^{−2πξ²/σ}.

theorem WignerFunction.wigner_gaussianS_pos {σ : ℝ} (hσ : 0 < σ) (x ξ : ℝ) : 0 < (wigner (SchrodingerGroup.gaussianS ↑σ ⋯) x ξ).re

★ The Wigner function of the Gaussian is positive everywhere.

theorem WignerFunction.wigner_zero_zero_of_odd (ψ : SchwartzMap ℝ ℂ) (hψ : ∀ (y : ℝ), ψ (-y) = -ψ y) : wigner ψ 0 0 = -(2 * ∫ (y : ℝ), ↑(‖ψ y‖ ^ 2))

★ Negativity at the origin for odd states: if ψ(−y) = −ψ(y) then W_ψ(0, 0) = −2 ∫ |ψ|².

theorem WignerFunction.integral_norm_sq_pos (ψ : SchwartzMap ℝ ℂ) (hψ : ψ ≠ 0) : 0 < ∫ (y : ℝ), ‖ψ y‖ ^ 2

A nonzero Schwartz function has positive L² mass.

theorem WignerFunction.re_wigner_zero_zero_neg (ψ : SchwartzMap ℝ ℂ) (hψ : ∀ (y : ℝ), ψ (-y) = -ψ y) (h0 : ψ ≠ 0) : (wigner ψ 0 0).re < 0

★ Negativity is a witness of non-classicality: an odd nonzero ψ has W_ψ(0, 0) < 0.

The free evolution is the classical free flow

theorem WignerFunction.wigner_freeSchrodingerS (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : wigner ((SchrodingerGroup.freeSchrodingerS t) ψ) x ξ = wigner ψ (x - 2 * Real.pi * t * ξ) ξ

★★ Liouville transport for the free Schrödinger group: W_{U₀(t)ψ}(x, ξ) = W_ψ(x − 2πtξ, ξ) — in the momentum p = 2πξ, W_t(x, p) = W_0(x − pt, p), the classical free flow, exact (the quadratic Hamiltonian has no ℏ² Moyal correction).