Hudson's theorem

Open

Wigner.hudson

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

analysiscomplex-analysisquantum-mechanics

Hudson's theorem: the only pure states whose Wigner functions are nonnegative are Gaussian wave packets. Let $\psi : \mathbb{R} \to \mathbb{C}$ be a normalized pure state, $\int_{\mathbb{R}} |\psi|^2 = 1$ , and $\hbar > 0$ . If

W(x,p) \ge 0 \quad \text{for all } (x,p) \in \mathbb{R}^2,

then there exist complex numbers $a, b, c$ with $\mathrm{Re}(a) > 0$ such that

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

for almost every $x$ . This is the source text's characterization, proved by R. L. Hudson (1974) and extended to higher dimensions by Soto and Claverie (1983): a one-dimensional pure state has an everywhere nonnegative Wigner function if and only if it is a Gaussian wave packet. It delimits exactly which quantum states admit a classical phase-space probability description.

Formalization Note The conclusion holds almost everywhere: the Wigner function is insensitive to changes of $\psi$ on a Lebesgue-null set, so no pointwise conclusion is possible; this is the faithful reading of the source's "the wave function must have the form". No minimum-uncertainty property is claimed (the source explicitly notes that nonnegative-Wigner pure states need not be minimum-uncertainty states in Heisenberg's sense).

Preamble

import Mathlib
import Definitions.Def_wigner

open MeasureTheory

Formal statement

namespace Wigner

theorem hudson {ψ : ℝ → ℂ} {ℏ : ℝ} (hℏ : 0 < ℏ)
    (hnorm : ∫ y, ‖ψ y‖ ^ 2 = 1)
    (hW : ∀ x p, 0 ≤ wigner ψ ℏ x p) :
    ∃ a b c : ℂ, 0 < Complex.re a ∧
      ∀ᵐ y ∂volume, ψ y = Complex.exp (-(a * (y : ℂ) ^ 2) + b * (y : ℂ) + c) := by sorry

end Wigner

Source

Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), section "Positivity of the function" (Hudson's theorem). Primary source: R. L. Hudson, Reports on Mathematical Physics 6(2), 249-252 (1974), doi:10.1016/0034-4877(74)90007-X. https://en.wikipedia.org/wiki/Wigner_quasiprobability_distribution

Read-back

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

Let $\psi : \mathbb{R} \to \mathbb{C}$ and $\hbar \in \mathbb{R}$ be arbitrary, under three hypotheses: (a) $0 < \hbar$ ; (b) $\int_{\mathbb{R}} |\psi(y)|^2\, dy = 1$ (which forces $y \mapsto |\psi(y)|^2$ to be essentially strongly measurable); (c) for every real $x$ and $p$ , $0 \le \mathrm{wigner}(\psi, \hbar, x, p)$ , i.e.

\operatorname{Re}\!\left(\int_{\mathbb{R}} \overline{\psi(x+y)}\,\psi(x-y)\,e^{2ipyi/\hbar}\,dy\right) \big/ (\pi\hbar) \ge 0,

a condition that constrains only the real part of the defining integral.

The conclusion: there exist $a, b, c \in \mathbb{C}$ with $\operatorname{Re}(a) > 0$ such that $\psi(y) = e^{-ay^2 + by + c}$ for Lebesgue-almost-every $y \in \mathbb{R}$ . The equality is claimed only up to a Lebesgue-null set: $\psi$ may differ from the displayed exponential on a set of measure zero. No assertion is made about pointwise equality, uniqueness of $(a, b, c)$ , or minimum uncertainty.

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