Reality of the Wigner function

Proved

Wigner.wigner_real

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

analysisquantum-mechanics

The Wigner function is real-valued. Let $\psi : \mathbb{R} \to \mathbb{C}$ be a wavefunction, $\hbar > 0$ the reduced Planck constant, and $(x, p)$ a point of phase space, and assume the defining integral exists, that is, the map $y \mapsto \overline{\psi(x+y)}\,\psi(x-y)\,e^{2ipy/\hbar}$ is Lebesgue-integrable over $\mathbb{R}$ . Then

\int_{-\infty}^{\infty}\overline{\psi(x+y)}\,\psi(x-y)\,e^{2ipy/\hbar}\,dy \in \mathbb{R},

i.e. its imaginary part vanishes.

This is Property 1 of the Wigner function in the source text. It is what allows the Wigner function to be a real quantity, and it holds for every wavefunction for which the integral exists: the substitution $y \mapsto -y$ exhibits the integral as its own complex conjugate.

Formalization Note The statement is expressed through the imaginary part of the defining integral Wigner.wignerIntegral; the Wigner function itself is defined as the real part of the same integral, so this milestone discharges exactly the discarded imaginary part.

Preamble

import Mathlib
import Definitions.Def_wigner

open MeasureTheory

Formal statement

namespace Wigner

theorem wigner_real {ψ : ℝ → ℂ} {ℏ x p : ℝ} (hℏ : 0 < ℏ)
    (hint : Integrable (fun y => wignerIntegrand ψ ℏ x p y) volume) :
    (wignerIntegral ψ ℏ x p).im = 0 := by sorry

end Wigner

Source

Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), section "Mathematical properties", Property 1. 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$ be an arbitrary function $\mathbb{R} \to \mathbb{C}$ and let $\hbar, x, p$ be arbitrary real numbers, under two hypotheses: (a) $0 < \hbar$ ; (b) the map $y \mapsto \overline{\psi(x+y)} \cdot \psi(x-y) \cdot e^{(2py/\hbar) \cdot i}$ is Integrable with respect to Lebesgue measure on $\mathbb{R}$ , i.e. the displayed Bochner integral exists. The conclusion: the imaginary part of

\int_{\mathbb{R}} \overline{\psi(x+y)}\, \psi(x-y)\, e^{(2py/\hbar) \cdot i}\, dy

equals $0$ .

The statement quantifies over all such $\psi, \hbar, x, p$ ; nothing is asserted about the real part of the integral, nor about other phase-space points. Note that hypothesis (b) is what makes the statement about an existing integral: without it, the Bochner integral would be $0$ by the junk-value convention and the conclusion would hold trivially for every $\psi$ .

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