Position-space marginal of the Wigner function

Proved

Wigner.wigner_marginal_position

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

analysismeasure-theoryquantum-mechanics

Integrating the Wigner function over momentum recovers the position probability density. Let $\psi : \mathbb{R} \to \mathbb{C}$ be a Schwartz function, $\hbar > 0$ , and $x \in \mathbb{R}$ . Then

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

where $W$ is the Wigner function of $\psi$ . For a pure state, $|\psi(x)|^2$ is the probability density of finding the particle at position $x$ , so the momentum-marginal of the Wigner function is exactly the Born position distribution. This is the first marginal identity of Property 2 in the source text, $\int dp\, W(x,p) = \langle x|\hat\rho|x\rangle$ , which for a pure state reads $\langle x|\hat\rho|x\rangle = |\psi(x)|^2$ .

Formalization Note Schwartz regularity is assumed so that the identity holds at every point $x$ ; it is the standing regularity convention of the source. The integral over $p$ is a Lebesgue (Bochner) integral of a real-valued function.

Preamble

import Mathlib
import Definitions.Def_wigner

open MeasureTheory

Formal statement

namespace Wigner

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

end Wigner

Source

Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), section "Mathematical properties", Property 2, first marginal 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 elements of the Schwartz space of smooth rapidly decreasing maps $\mathbb{R} \to \mathbb{C}$ (the statement's only quantification over $\psi$ ), and let $\hbar, x$ be real numbers with $0 < \hbar$ . The claim: the Lebesgue (Bochner) integral over $p \in \mathbb{R}$ of the real number $\mathrm{wigner}(\psi, \hbar, x, p)$ — which by definition equals $\operatorname{Re}(\int \overline{\psi(x+y)}\psi(x-y)e^{2ipyi/\hbar}\,dy)/(\pi\hbar)$ — equals $|\psi(x)|^2$ , the square of the modulus of the complex number $\psi(x)$ .

Both sides are total: the outer integral is $0$ if the integrand is not integrable (for Schwartz $\psi$ this does not occur, but the statement does not assume it). The identity is claimed for every $x$ , not merely almost everywhere.

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