The Wigner quasiprobability distribution

Definition

wigner

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

analysismeasure-theoryquantum-mechanics

The Wigner quasiprobability distribution (Wigner function) of a wavefunction. For a wavefunction $\psi : \mathbb{R} \to \mathbb{C}$ and a phase-space point $(x, p) \in \mathbb{R}^2$ , with $\hbar > 0$ the reduced Planck constant, the Wigner function is

W(x,p) = \frac{1}{\pi\hbar}\int_{-\infty}^{\infty}\overline{\psi(x+y)}\,\psi(x-y)\,e^{2ipy/\hbar}\,dy,

the transform introduced by E. Wigner in 1932 to study quantum corrections to classical statistical mechanics. It is the phase-space realization of the quantum state: integrating $W$ over momentum recovers the position probability density, integrating over position recovers the momentum density, and operator expectation values become phase-space averages against $W$ via Weyl quantization.

Formalization Note The integral is the Bochner integral with respect to Lebesgue measure on $\mathbb{R}$ . The code factors the formula into the integrand (Wigner.wignerIntegrand), the integral (Wigner.wignerIntegral), and the Wigner function itself (Wigner.wigner), defined as the real part of the integral divided by $\pi\hbar$ . That the discarded imaginary part vanishes is Property 1 of the source and the mission's first milestone; the definition is total, with value 0 wherever the integral does not exist.

Definition code

import Mathlib

open MeasureTheory
open ComplexConjugate

namespace Wigner

/-- The integrand of the Wigner function of the wavefunction psi at the phase-space
point (x, p), with hbar the reduced Planck constant:
conj (psi (x + y)) * psi (x - y) * exp (2 * p * y * i / hbar). -/
noncomputable def wignerIntegrand (ψ : ℝ → ℂ) (ℏ x p y : ℝ) : ℂ :=
  conj (ψ (x + y)) * ψ (x - y) *
    Complex.exp (Complex.ofReal (2 * p * y / ℏ) * Complex.I)

/-- The defining integral of the Wigner function of psi at (x, p):
the Bochner integral over y of wignerIntegrand psi hbar x p y. -/
noncomputable def wignerIntegral (ψ : ℝ → ℂ) (ℏ x p : ℝ) : ℂ :=
  ∫ y, wignerIntegrand ψ ℏ x p y

/-- The Wigner quasiprobability distribution (Wigner function) of psi at (x, p):
the real part of wignerIntegral, divided by pi * hbar. -/
noncomputable def wigner (ψ : ℝ → ℂ) (ℏ x p : ℝ) : ℝ :=
  (wignerIntegral ψ ℏ x p).re / (Real.pi * ℏ)

end Wigner

Source

Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), section "Definition and meaning", first displayed formula. https://en.wikipedia.org/wiki/Wigner_quasiprobability_distribution

Read-back

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

The code declares three definitions in the namespace Wigner and proves nothing.

For a function $\psi : \mathbb{R} \to \mathbb{C}$ and real numbers $\hbar, x, p, y$ , the value of wignerIntegrand at $(\psi, \hbar, x, p, y)$ is the complex number $\overline{\psi(x+y)} \cdot \psi(x-y) \cdot e^{(2py/\hbar) \cdot i}$ , with $i$ the imaginary unit.
wignerIntegral $(\psi, \hbar, x, p)$ is the Bochner integral over all $y \in \mathbb{R}$ , with respect to Lebesgue measure, of the map $y \mapsto$ wignerIntegrand $(\psi, \hbar, x, p, y)$ . This is a total function: by the junk-value convention of the Bochner integral, the value is 0 whenever the integrand is not essentially strongly measurable and integrable.
wigner $(\psi, \hbar, x, p)$ is the real part of wignerIntegral $(\psi, \hbar, x, p)$ , divided by the real number $\pi \cdot \hbar$ ; this is ordinary real division, which evaluates to 0 when $\hbar = 0$ .

No measurability, integrability, normalization, or positivity assumptions are attached to any of the three functions.

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