Prove2Me

Pointwise bound ∣W(x,p)∣≤2/h\lvert W(x,p)\rvert \le 2/h for pure states

Proved
Wigner.wigner_bound

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

analysisquantum-mechanics

The Wigner function of a pure state is bounded pointwise. Let ψ:R→C\psi : \mathbb{R} \to \mathbb{C} be a normalized pure state, ∫∣ψ∣2=1\int |\psi|^2 = 1, and ℏ>0\hbar > 0. Then for every phase-space point,

−2h≤W(x,p)≤2h,equivalently∣W(x,p)∣≤1πℏ,-\frac{2}{h} \le W(x,p) \le \frac{2}{h}, \qquad \text{equivalently} \qquad |W(x,p)| \le \frac{1}{\pi\hbar},

where h=2πℏh = 2\pi\hbar is Planck's constant. This is Property 9 of the source text: by the Cauchy-Schwarz inequality the Wigner function of a pure state is bounded by 2/h2/h in absolute value, so it is never a delta spike on phase space — a reflection of the uncertainty principle — and the bound disappears in the classical limit ℏ→0\hbar \to 0, where Wigner functions concentrate into delta functions.

Formalization Note The bound is stated with the normalization 1/(πℏ)=2/h1/(\pi\hbar) = 2/h used by the definition; it is sharp, attained by Gaussian (coherent) states at their center.

Preamble
import Mathlib
import Definitions.Def_wigner

open MeasureTheory
Formal statement
namespace Wigner

theorem wigner_bound {ψ : ℝ → ℂ} {ℏ x p : ℝ} (hℏ : 0 < ℏ)
    (hnorm : ∫ y, ‖ψ y‖ ^ 2 = 1) :
    |wigner ψ ℏ x p| ≤ 1 / (Real.pi * ℏ) := by sorry

end Wigner
Source
Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), section "Mathematical properties", Property 9. https://en.wikipedia.org/wiki/Wigner_quasiprobability_distribution
Read-back

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

Let ψ:R→C\psi : \mathbb{R} \to \mathbb{C} and ℏ,x,p∈R\hbar, x, p \in \mathbb{R} be arbitrary, under two hypotheses: (a) 0<ℏ0 < \hbar; (b) the Lebesgue integral ∫R∣ψ(y)∣2 dy\int_{\mathbb{R}} |\psi(y)|^2\, dy equals 11 — this is the Bochner integral of the real-valued map y↦∣ψ(y)∣2y \mapsto |\psi(y)|^2, and it forces that map to be essentially strongly measurable (a non-measurable integrand would integrate to 00, contradicting the value 11). The conclusion:

∣wigner(ψ,ℏ,x,p)∣≤1πℏ,|\mathrm{wigner}(\psi, \hbar, x, p)| \le \frac{1}{\pi \hbar},

where wigner\mathrm{wigner} is the real part of the defining integral divided by πℏ\pi\hbar. The statement is universally quantified over all ψ,ℏ,x,p\psi, \hbar, x, p satisfying the hypotheses; no measurability of ψ\psi itself is assumed beyond what hypothesis (b) forces.

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