Wigner function

In plain terms

Classical mechanics describes a system by a point in phase space, position and momentum at once, and statistical mechanics by a probability distribution over such points. Quantum mechanics is usually said to forbid this, as position and momentum have no joint distribution, and the Wigner function is the precise sense in which that's both true and false.

Wigner's construction takes a quantum state and produces a function of position and momentum. Integrate it over momentum and you get the position probability density; integrate over position and you get the momentum density. Average any position or momentum quantity against it and you get the quantum expectation. In every respect that a probability distribution is used for, it works.

There is a sharper way to say the same thing. The overlap of two Wigner functions over the whole of phase space equals the squared overlap of the two states, so nothing is lost in passing from a state to its Wigner function, and every quantity a measurement can produce is an average of some function against it.

Except that it can be negative. For any state that isn't a Gaussian bump, the function dips below zero somewhere, and a negative probability is no probability at all. Negativity is therefore a sharp, quantitative signature of non-classicality, and it's used that way in the laboratory, where measured Wigner functions with negative regions are the standard evidence that an optical or mechanical state has no classical description.

In CSD

The phase-space formulation is one of the pictures the programme keeps agreeing with, and the corpus proves the parts that are Fourier analysis, for states in the Schwartz class in one dimension. The function is real, its two marginals are the position and momentum densities, the total mass is the norm, the position and momentum expectations are the phase-space moments, and the momentum representation is the same function with its arguments exchanged, which follows from Parseval's theorem for Schwartz functions.

Two results are the interpretive ones. A Gaussian state has a positive Wigner function, explicitly computed, while any odd state has a strictly negative value at the origin, so negativity is exhibited rather than described. And the free evolution moves the Wigner function exactly as classical free motion moves a phase-space density, which shows the classical flow isn't an approximation in that case but the exact answer. For CSD the lesson is a negative one worth stating: the Wigner function is a representation of a state and not a candidate for the programme's ontic measure, since the measure that weights regions is nonnegative by construction and this function isn't. The Moyal bracket is now proved where it can be: the potential term of the Wigner equation is the Wigner transform of the quantum commutator, it differs from the classical Poisson bracket by a bounded correction of the order of the third derivative of the potential, and the two agree exactly when that derivative vanishes, which is the classical limit as a theorem rather than a slogan. The free evolution is now an equation and not only a flow: the Wigner function is differentiable in the position, its position derivative is a sum of cross Wigner functions, and the time derivative is minus the momentum times that derivative, which is the classical Liouville equation satisfied exactly by the quantum phase-space density. What is still open is the same equation with a potential, which needs a propagator differentiable on Schwartz functions, and for general Weyl-quantised observables the symbol class itself, since a quantisation of an arbitrary symbol need not even be continuous.

Mathematically

For a Schwartz psi the Wigner function is the Fourier transform in y of y to psi(x + y/2) times conj psi(x - y/2), in Mathlib's convention, with momentum p = 2 pi xi. wignerKernel shows the kernel is Schwartz in y; conj_wigner and im_wigner give reality; integral_wigner_right gives the position marginal by Fourier inversion at the origin; wigner_fourier is the momentum representation W of the transform at (xi, -x) equal to W at (x, xi), by SchwartzMap.integral_inner_fourier_fourier applied to modulated affine reparametrisations; integral_wigner_left is the momentum marginal, and integral_integral_mul_wigner_left and its partner are the moments.

wigner_gaussianS computes the Gaussian case and wigner_gaussianS_pos its positivity; wigner_zero_zero_of_odd gives the value minus twice the norm squared at the origin for odd states. wigner_freeSchrodingerS is the free transport W_t(x, p) = W_0(x - p t, p), exact because the phase of the free propagator is the character of the shift.

Two further results make W the state rather than a pair of marginals (WignerWeyl.lean). integral_integral_wigner_mul_conj is the overlap identity: the phase-space overlap of two Wigner functions is the squared modulus of the states' inner product, by slicewise Plancherel and the convolution integral, with integral_integral_wigner_sq its purity form. And integral_conj_mul_weylOp is the Weyl expectation formula, for a symbol presented as a family of Schwartz Fourier slices. One dimension, Schwartz data.

Row 92 (b) and (c) landed 2026-09-30 in WignerCalculus.lean: integral_prod_wigner_mul_conj is the overlap identity against the product measure on the plane, through integrable_normSq_wigner_prod, and integral_integral_wigner_pos, _mom and _posMom are the phase-space moments in operator form, the xi-weighted one giving the symmetrised product of position and momentum. The Schwartz property of W on the plane is not proved and is not needed: slicewise Plancherel makes the xi-integral of the squared modulus a convolution of two L^1 functions, which is what Fubini wants. What remains of row 92 is (a), Op(a) as a continuous operator for symbols of temperate growth, which needs differentiation under the integral sign to all orders with bounds. Row 64 landed its generator half 2026-09-30 in MoyalBracket.lean: moyalPot_eq_comm, norm_moyalPot_sub_poisson_le with its hbar-squared remainder, and moyalPot_eq_poisson_of_third_deriv_zero. Its time-dependent half landed its free part 2026-10-01 in WignerEvolution.lean: hasDerivAt_wigner_left is the position derivative as W(psi', psi) + W(psi, psi'), passing under the Fourier integral against a bound uniform in the position, and wigner_liouville is the free equation d/dt W = -2 pi xi d/dx W. The interacting equation stays open on the propagator, not on the derivative.

The name

Eugene Wigner introduced the function in 1932, in a paper on quantum corrections to thermodynamic equilibrium, and treated it as a calculational device rather than a foundational statement. Jose Enrique Moyal worked out in 1949 that the whole of quantum mechanics can be rewritten in these terms, with a deformed product in place of the operator product, which is the phase-space formulation as a formulation.

Hilbrand Groenewold had reached much of the same ground in 1946, and the construction now carries all three names in different communities, with the deformed product called the Moyal or star product.

Related entries

• Wigner rigidityPreserve the overlaps between quantum states and you have no freedom left, as the rearrangement must be a unitary or an anti-unitary transformation whether or not you intended it to be.
• quantum Fourier transformThe quantum Fourier transform runs Fourier's transform as a single reversible motion of a quantum register, and it's the lens that turns hidden periods and phases into outcomes a measurement can land on.
• Born ruleQuantum probabilities aren't a law of nature in CSD, as they're the sizes of regions in the space of states, measured with a ruler nobody was free to choose.
• Liouville measureA deterministic substrate needs a notion of volume that its own motion can't distort, and on CSD's sector that volume is forced and it's the Born measure.
• Koopman operatorClassical mechanics has a Hilbert space and a unitary time evolution of its own, so neither of those is what makes a theory quantum, and what's left as the difference is that quantum observables don't commute.