The Wigner function as the state in phase space: overlaps and Weyl expectations

Category: 1-Mathlib (staged for upstream). BACKLOG #63, the residue of #45.

Wigner.lean gives the Wigner function its marginals and its free transport. That makes W_ψ a phase-space picture of the position and momentum distributions; this file makes it the picture of the state:

• ★★★ integral_integral_wigner_mul_conj — the overlap (Moyal) identity ∫∫ W_φ(x, ξ) conj (W_ψ(x, ξ)) dξ dx = |∫ φ conj ψ|². Phase space recovers the inner product, so the Wigner map loses nothing: two states with the same Wigner function agree up to a phase. With φ = ψ it reads ∫∫ W_ψ² = (∫ |ψ|²)² (★★ integral_integral_wigner_sq);
• ★★★ integral_conj_mul_weylOp — the Weyl expectation formula ⟨ψ, Op(a) ψ⟩ = ∫∫ a(u, ξ) W_ψ(u, ξ) dξ du: the expectation of a Weyl-quantised observable is the phase-space average of its symbol against W_ψ, which is what "the state in phase space" means operationally.

How the symbol is presented, and why

A Weyl operator is (Op(a) ψ)(x) = ∫∫ a((x + y)/2, ξ) e^{2πi(x − y)ξ} ψ(y) dξ dy. The inner ξ-integral is the Fourier transform of the symbol in its second slot, so the operator only ever sees that transform, and this file takes that as the datum: a symbol is a family b : ℝ → 𝓢(ℝ, ℂ) of Schwartz slices, the operator is weylOp b ψ x = ∫ y, b ((x + y)/2) (x − y) ψ y, and the symbol itself is weylSymbol b u ξ = 𝓕 (b u) ξ. Presenting it this way buys two things: the ξ-integral converges by fiat rather than by an oscillatory-integral argument, and the Parseval step of the proof is Mathlib's Plancherel theorem for Schwartz functions, applied slicewise.

The substitutions x = u + w/2, y = u − w/2 turn the operator's (x, y) kernel into the Wigner kernel in (u, w), and Plancherel in w turns that into the symbol against W_ψ. The step needs the (x, u) integrand to be integrable on the plane, which is what the hypotheses hM, hbM (an integrable function dominating the slices) supply.

Honest scope

⚠️ No pseudodifferential calculus. weylOp is a function of x, not a continuous operator on 𝓢(ℝ, ℂ); nothing here says Op(a) maps Schwartz functions to Schwartz functions, composes, or has an adjoint. BACKLOG #92.

⚠️ Schwartz slices with an integrable dominating function, which excludes the symbols of temperate growth — a(x, ξ) = x, ξ, xξ — whose quantisations are the position, momentum and symmetrised product operators. Their moment identities are now proved in WignerCalculus.lean (★★ integral_integral_wigner_pos, ★★ integral_integral_wigner_mom, ★★★ integral_integral_wigner_posMom — the last being the symmetrised product ½(XP + PX)), so what is still missing for those symbols is Op(a) as an operator, not the physics: BACKLOG #92(a).

⚠️ The overlap identity here is an iterated integral, in the order ∫ x, ∫ ξ. The product-measure form on ℝ² is WignerCalculus.lean (★★★ integral_prod_wigner_mul_conj, on ★★★ integrable_wigner_mul_conj), which also gives joint measurability and square-integrability on the plane. The Schwartz property of (x, ξ) ↦ W_ψ(x, ξ) on ℝ² is still not proved, and is not needed for either.

⚠️ One dimension, Schwartz data, the conventions of Wigner.lean (𝓕 f ξ = ∫ e^{−2πiyξ} f y dy, momentum p = 2πξ).

References: J. E. Moyal, Quantum mechanics as a statistical theory, Proc. Cambridge Philos. Soc. 45 (1949) 99 §§3–4 (the overlap identity and the expectation formula); G. B. Folland, Harmonic Analysis in Phase Space (1989) §1.8; specs/BACKLOG.md #63; specs/future-work.md.

Two substitutions on the line

theorem WignerFunction.integral_comp_affine_shift (f : ℝ → ℂ) (x s : ℝ) : ∫ (y : ℝ), f (x + s * y) = |s⁻¹| • ∫ (z : ℝ), f z

Substitution y ↦ x + s y in an integral over the line.

The pointwise product φ · conj ψ as a Schwartz function

noncomputable def WignerFunction.mulConj (φ ψ : SchwartzMap ℝ ℂ) : SchwartzMap ℝ ℂ

The Schwartz function v ↦ φ v * conj (ψ v), whose integral is the L² pairing.

Equations

• WignerFunction.mulConj φ ψ = (SchwartzMap.bilinLeftCLM (ContinuousLinearMap.mul ℝ ℂ) ⋯) φ

theorem WignerFunction.mulConj_apply (φ ψ : SchwartzMap ℝ ℂ) (v : ℝ) : (mulConj φ ψ) v = φ v * (starRingEnd ℂ) (ψ v)

theorem WignerFunction.wignerKernel_mul_conj (φ ψ : SchwartzMap ℝ ℂ) (x y : ℝ) : (wignerKernel φ x) y * (starRingEnd ℂ) ((wignerKernel ψ x) y) = (mulConj φ ψ) (x + y / 2) * (starRingEnd ℂ) ((mulConj φ ψ) (x - y / 2))

The Wigner kernels of two states multiply into the product φ · conj ψ at the two shifted points.

The overlap identity

theorem WignerFunction.integral_wigner_mul_conj (φ ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ∫ (ξ : ℝ), wigner φ x ξ * (starRingEnd ℂ) (wigner ψ x ξ) = ∫ (y : ℝ), (wignerKernel φ x) y * (starRingEnd ℂ) ((wignerKernel ψ x) y)

Plancherel slicewise: at a fixed x the ξ-integral of W_φ · conj (W_ψ) is the y-integral of K_φ · conj (K_ψ).

theorem WignerFunction.integral_mulConj_shift (G : SchwartzMap ℝ ℂ) (x : ℝ) : ∫ (y : ℝ), G (x + y / 2) * (starRingEnd ℂ) (G (x - y / 2)) = 2 * MeasureTheory.convolution (fun (v : ℝ) => G v) (fun (v : ℝ) => (starRingEnd ℂ) (G v)) (ContinuousLinearMap.mul ℝ ℂ) MeasureTheory.volume (2 * x)

The y-integral of G(x + y/2) conj (G(x − y/2)) is twice the convolution of G with conj ∘ G at 2x.

theorem WignerFunction.integral_integral_wigner_mul_conj (φ ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ) (ξ : ℝ), wigner φ x ξ * (starRingEnd ℂ) (wigner ψ x ξ) = (∫ (v : ℝ), φ v * (starRingEnd ℂ) (ψ v)) * (starRingEnd ℂ) (∫ (v : ℝ), φ v * (starRingEnd ℂ) (ψ v))

★★★ The overlap identity (Moyal 1949): the phase-space overlap of two Wigner functions is the squared modulus of the states' inner product, so nothing is lost in passing from the state to its Wigner function.

theorem WignerFunction.integral_integral_wigner_sq (ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ) (ξ : ℝ), wigner ψ x ξ * wigner ψ x ξ = (∫ (v : ℝ), ↑‖ψ v‖ ^ 2) * ∫ (v : ℝ), ↑‖ψ v‖ ^ 2

★★ The purity form: the phase-space square of a Wigner function is the square of the state's mass.

Weyl quantisation and the expectation formula

theorem WignerFunction.exists_norm_le (ψ : SchwartzMap ℝ ℂ) : ∃ (C : ℝ), ∀ (v : ℝ), ‖ψ v‖ ≤ C

A uniform bound for a Schwartz function.

theorem WignerFunction.integral_fourier_mul_conj (f g : SchwartzMap ℝ ℂ) : ∫ (ξ : ℝ), (FourierTransform.fourier f) ξ * (starRingEnd ℂ) ((FourierTransform.fourier g) ξ) = ∫ (y : ℝ), f y * (starRingEnd ℂ) (g y)

Plancherel in product form: ∫ 𝓕 f conj (𝓕 g) = ∫ f conj g.

noncomputable def WignerFunction.weylOp (b : ℝ → SchwartzMap ℝ ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ℂ

The Weyl operator of a symbol given in kernel form: b u is the Fourier transform, in the frequency slot, of the symbol's slice at the midpoint u, and the operator is the integral against the kernel b ((x + y)/2) (x − y).

Equations

• WignerFunction.weylOp b ψ x = ∫ (y : ℝ), (b ((x + y) / 2)) (x - y) * ψ y

noncomputable def WignerFunction.weylSymbol (b : ℝ → SchwartzMap ℝ ℂ) (u ξ : ℝ) : ℂ

The symbol of a Weyl operator presented in kernel form.

Equations

• WignerFunction.weylSymbol b u ξ = (FourierTransform.fourier (b u)) ξ

theorem WignerFunction.integrable_weylPair (b : ℝ → SchwartzMap ℝ ℂ) (ψ : SchwartzMap ℝ ℂ) (hbc : Continuous fun (p : ℝ × ℝ) => (b p.1) p.2) {M : ℝ → ℝ} (hM : MeasureTheory.Integrable M MeasureTheory.volume) (hbM : ∀ (u w : ℝ), ‖(b u) w‖ ≤ M u) : MeasureTheory.Integrable (Function.uncurry fun (x u : ℝ) => (starRingEnd ℂ) (ψ x) * ((b u) (2 * x - 2 * u) * ψ (2 * u - x))) (MeasureTheory.volume.prod MeasureTheory.volume)

After the substitution y = 2u − x the Weyl expectation's integrand is dominated by a product of integrable functions of the two variables separately, hence is integrable on the plane.

theorem WignerFunction.conj_mul_weylOp_eq (b : ℝ → SchwartzMap ℝ ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : (starRingEnd ℂ) (ψ x) * weylOp b ψ x = 2 * ∫ (u : ℝ), (starRingEnd ℂ) (ψ x) * ((b u) (2 * x - 2 * u) * ψ (2 * u - x))

The Weyl expectation's inner integral after the substitution y = 2u − x.

theorem WignerFunction.integral_weylPair_x (b : ℝ → SchwartzMap ℝ ℂ) (ψ : SchwartzMap ℝ ℂ) (u : ℝ) : ∫ (x : ℝ), (starRingEnd ℂ) (ψ x) * ((b u) (2 * x - 2 * u) * ψ (2 * u - x)) = 2⁻¹ * ∫ (w : ℝ), (b u) w * (starRingEnd ℂ) ((wignerKernel ψ u) w)

The inner x-integral, after the substitution x = u + w/2, is the Wigner kernel against the symbol's slice.

theorem WignerFunction.integral_conj_mul_weylOp (b : ℝ → SchwartzMap ℝ ℂ) (ψ : SchwartzMap ℝ ℂ) (hbc : Continuous fun (p : ℝ × ℝ) => (b p.1) p.2) {M : ℝ → ℝ} (hM : MeasureTheory.Integrable M MeasureTheory.volume) (hbM : ∀ (u w : ℝ), ‖(b u) w‖ ≤ M u) : ∫ (x : ℝ), (starRingEnd ℂ) (ψ x) * weylOp b ψ x = ∫ (u : ℝ) (ξ : ℝ), weylSymbol b u ξ * wigner ψ u ξ

★★★ The Weyl expectation formula. For a symbol presented in kernel form, with slices dominated by an integrable function, the expectation of the Weyl operator in a state is the phase-space average of the symbol against the state's Wigner function. So W_ψ carries every Weyl expectation, not only the position and momentum ones.