Total integral of the Wigner function

Proved

Wigner.wigner_norm

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

analysismeasure-theoryquantum-mechanics

The total integral of the Wigner function is the squared $L^2$ norm of the wavefunction. Let $\psi : \mathbb{R} \to \mathbb{C}$ be a Schwartz function and $\hbar > 0$ . Then

\int_{-\infty}^{\infty}\int_{-\infty}^{\infty} W(x,p)\,dp\,dx = \int_{-\infty}^{\infty} |\psi(x)|^2\,dx.

For a normalized pure state the right-hand side equals 1: this is the normalization identity of Property 2 in the source, $\int dx \int dp\, W(x,p) = \mathrm{Tr}(\hat\rho)$ , since the trace of a pure-state density matrix is the squared norm of the wavefunction.

Formalization Note Both sides are Lebesgue integrals of real-valued functions over $\mathbb{R}$ ; the left side is an iterated integral. Schwartz regularity is the standing convention under which all displayed integrals exist.

Preamble

import Mathlib
import Definitions.Def_wigner

open MeasureTheory

Formal statement

namespace Wigner

theorem wigner_norm (ψ : SchwartzMap ℝ ℂ) {ℏ : ℝ} (hℏ : 0 < ℏ) :
    ∫ x, ∫ p, wigner (⇑ψ) ℏ x p = ∫ x, ‖⇑ψ x‖ ^ 2 := by sorry

end Wigner

Source

Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), section "Mathematical properties", Property 2, third formula. 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$ range over all Schwartz maps $\mathbb{R} \to \mathbb{C}$ and let $\hbar$ be a real number with $0 < \hbar$ . The claim: the iterated integral

\int_{x \in \mathbb{R}} \left( \int_{p \in \mathbb{R}} \mathrm{wigner}(\psi, \hbar, x, p)\, dp \right) dx

equals $\int_{x \in \mathbb{R}} |\psi(x)|^2\, dx$ . Both are Lebesgue integrals of real-valued functions with the standard junk-value convention; the left side is an iterated (not double) integral.

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