Gaussian pure states have nonnegative Wigner function

Proved

Wigner.gaussian_wigner_nonneg

by Lucas · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisquantum-mechanics

Gaussian pure states have nonnegative Wigner functions: the converse of Hudson's theorem. Let $a, b, c \in \mathbb{C}$ with $\mathrm{Re}(a) > 0$ , so that

\psi(x) = e^{-ax^2 + bx + c}

is a square-integrable Gaussian wave packet, and let $\hbar > 0$ . Then the Wigner function of $\psi$ is nonnegative at every phase-space point: $W(x,p) \ge 0$ for all $x, p$ . The source text notes that "the Wigner function of any such state is a Gaussian distribution on phase space" — coherent and squeezed states are exactly the pure states with classical phase-space pictures.

Formalization Note No normalization of $\psi$ is assumed: positivity is invariant under the scalar factor $e^c$ . The hypothesis $\mathrm{Re}(a) > 0$ is the source's assumption and is what makes $\psi$ a genuine wave packet.

Preamble

import Mathlib
import Definitions.Def_wigner

open MeasureTheory

Formal statement

namespace Wigner

theorem gaussian_wigner_nonneg {a b c : ℂ} {ℏ x p : ℝ} (ha : 0 < Complex.re a)
    (hℏ : 0 < ℏ) :
    0 ≤ wigner (fun y => Complex.exp (-(a * (y : ℂ) ^ 2) + b * (y : ℂ) + c)) ℏ x p := by sorry

end Wigner

Source

Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), section "Positivity of the function". https://en.wikipedia.org/wiki/Wigner_quasiprobability_distribution

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Let $a, b, c$ be arbitrary complex numbers and $\hbar, x, p$ arbitrary real numbers, under two hypotheses: (a) $\operatorname{Re}(a) > 0$ ; (b) $0 < \hbar$ . The conclusion: $0 \le \mathrm{wigner}(\psi, \hbar, x, p)$ , where $\psi$ is the specific function $y \mapsto e^{-a y^2 + b y + c}$ (with $y$ coerced to a complex number in the exponent). Hypothesis (a) makes $\psi$ square-integrable, though the statement does not assume this separately; no normalization of $\psi$ is assumed.

Human review

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

View graph