The Weyl calculus: phase space as a measure space, and the temperate symbols

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

WignerWeyl.lean proves the overlap identity and the Weyl expectation formula as iterated integrals, for symbols with Schwartz slices. This file supplies the two things that were missing from that picture: the Wigner function as a function on the plane rather than a family of slices, and the three symbols of temperate growth whose quantisations are the position, momentum and symmetrised-product operators.

Phase space as a measure space

• ★ stronglyMeasurable_wigner — (x, ξ) ↦ W_ψ(x, ξ) is jointly measurable;
• wignerEnergy ψ x = ∫ |W_ψ(x, ξ)|² dξ, with ★★ integrable_wignerEnergy — the energy is integrable in the position, because slicewise Plancherel turns it into a convolution of two L¹ functions read at 2x;
• ★★ integrable_normSq_wigner_prod — W_ψ is square-integrable on the plane;
• ★★★ integrable_wigner_mul_conj — the overlap integrand is integrable on the plane, by |ab| ≤ (|a|² + |b|²)/2, and hence
• ★★★ integral_prod_wigner_mul_conj — the overlap identity against the product measure: ∫_{ℝ²} W_φ conj W_ψ = |⟨φ, ψ⟩|², with ★★ integral_prod_wigner_sq the purity form. This is what makes phase space a measure space for the state rather than a family of one-dimensional slices.

The three temperate symbols

weylOp of WignerWeyl.lean needs symbol slices dominated by an integrable function, which excludes a(x, ξ) = x, ξ and xξ. Their content is nevertheless available as moment identities, and in operator form:

• posCLM and momCLM — the position operator Xψ = xψ and, in the conventions of Wigner.lean (momentum p = 2πξ), the momentum operator P = (2πi)⁻¹ d/dx, both as continuous operators on 𝓢(ℝ, ℂ);
• ★★ integral_integral_wigner_pos and ★★ integral_integral_wigner_mom — the symbols x and ξ average against W_ψ to ⟨ψ, Xψ⟩ and ⟨ψ, Pψ⟩;
• ★★★ integral_integral_wigner_posMom — the symbol xξ averages to ⟨ψ, ½(XP + PX)ψ⟩, the symmetrised product. This is the one that is not a marginal: the ½ψ term is produced by the integration by parts that the weight x forces, and it is exactly the ordering correction that makes the Weyl quantisation of xξ symmetric.

Along the way, three lemmas that are about the Fourier transform rather than about W: ★ integral_fourier (∫ 𝓕f = f 0, by inversion), ★ integral_deriv (∫ f' = 0, because 𝓕 f' carries a factor ξ), and ★ integral_mul_fourier (the first moment of 𝓕f is (2πi)⁻¹ f'(0)), from which ★ integral_mul_deriv (∫ x f'(x) dx = −∫ f) and ★★ integral_mul_wigner_right (the ξ-moment of W_ψ at fixed x is the probability current).

Honest scope

⚠️ W_ψ is not proved to be Schwartz on ℝ² here. BACKLOG #92(c) asked for that, and what is proved here is what it was wanted for — joint measurability, square-integrability, and the product-measure form of the overlap identity — by a cheaper route: slicewise Plancherel plus a convolution, rather than seminorm estimates on the plane. The Schwartz property itself is now proved (2026-10-21): ★★★ SchwartzMap.wignerSchwartz ψ : 𝓢(ℝ × ℝ, ℂ) with wignerSchwartz_apply : wignerSchwartz ψ (x, ξ) = wigner ψ x ξ in PartialFourierCLM.lean, once the partial Fourier transform acted on 𝓢(ℝ², ℂ) (#170–#174); this file's route stands as the cheaper one for what it proves.

⚠️ Op(a) is still not an operator on 𝓢(ℝ, ℂ) (#92(a)). Nothing here maps Schwartz functions to Schwartz functions, composes symbols, or takes adjoints. With weylOp's datum — a family b : ℝ → 𝓢(ℝ, ℂ) with no regularity in its first slot — weylOp b ψ need not even be continuous, so this is not a gap in the proofs but a statement that needs a different symbol class (a jointly Schwartz kernel), and then differentiation under the integral sign to all orders with bounds, which neither Mathlib nor this corpus has (MATHLIB-ABSENT(file:Mathlib/Analysis/Calculus/ParametricIntegralContDiff)): ContDiffParametricIntervalIntegral.lean covers C^n dependence for interval integrals only.

⚠️ The three temperate symbols appear as moment identities, not as operators Op(x), Op(ξ), Op(xξ); the identification of the symmetrised product with a Weyl quantisation is the physics reading of integral_integral_wigner_posMom, not a theorem about weylOp.

⚠️ One dimension, Schwartz states, 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 (the moments of W); G. B. Folland, Harmonic Analysis in Phase Space (1989) §1.8 (the symmetrised product as the Weyl quantisation of xξ); specs/BACKLOG.md #92; specs/future-work.md.

The mass and the first moment of a Fourier transform

theorem WignerFunction.lineDerivOp_one (f : SchwartzMap ℝ ℂ) : LineDeriv.lineDerivOp 1 f = (SchwartzMap.derivCLM ℂ ℂ) f

The line derivative at 1 is the ordinary derivative.

theorem WignerFunction.fourier_apply_zero (f : SchwartzMap ℝ ℂ) : (FourierTransform.fourier f) 0 = ∫ (y : ℝ), f y

The Fourier transform at the origin is the mass.

theorem WignerFunction.integral_fourier (f : SchwartzMap ℝ ℂ) : ∫ (ξ : ℝ), (FourierTransform.fourier f) ξ = f 0

★ The mass of a Fourier transform is the value at the origin, by inversion.

theorem WignerFunction.fourier_deriv_apply (f : SchwartzMap ℝ ℂ) (ξ : ℝ) : (FourierTransform.fourier (LineDeriv.lineDerivOp 1 f)) ξ = 2 * ↑Real.pi * Complex.I * (↑ξ * (FourierTransform.fourier f) ξ)

The Fourier transform of a derivative, pointwise: the factor 2πiξ.

theorem WignerFunction.integral_deriv (f : SchwartzMap ℝ ℂ) : ∫ (x : ℝ), deriv (⇑f) x = 0

★ The integral of a derivative vanishes: the Fourier transform of f' carries a factor ξ, which kills it at the origin.

theorem WignerFunction.integral_mul_fourier (f : SchwartzMap ℝ ℂ) : ∫ (ξ : ℝ), ↑ξ * (FourierTransform.fourier f) ξ = (2 * ↑Real.pi * Complex.I)⁻¹ * deriv (⇑f) 0

★ The first ξ-moment of a Fourier transform is the derivative at the origin.

The position and momentum operators

theorem WignerFunction.hasTemperateGrowth_ofReal : Function.HasTemperateGrowth fun (x : ℝ) => ↑x

noncomputable def WignerFunction.posCLM : SchwartzMap ℝ ℂ →L[ℂ] SchwartzMap ℝ ℂ

The position operator on Schwartz space: multiplication by the coordinate.

Equations

• WignerFunction.posCLM = SchwartzMap.smulLeftCLM ℂ fun (x : ℝ) => ↑x

@[simp]

theorem WignerFunction.posCLM_apply (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : (posCLM ψ) x = ↑x * ψ x

noncomputable def WignerFunction.momCLM : SchwartzMap ℝ ℂ →L[ℂ] SchwartzMap ℝ ℂ

The momentum operator in the conventions of Wigner.lean, where the momentum is p = 2πξ: P = (2πi)⁻¹ d/dx.

Equations

• WignerFunction.momCLM = (2 * ↑Real.pi * Complex.I)⁻¹ • SchwartzMap.derivCLM ℂ ℂ

@[simp]

theorem WignerFunction.momCLM_apply (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : (momCLM ψ) x = (2 * ↑Real.pi * Complex.I)⁻¹ * deriv (⇑ψ) x

theorem WignerFunction.deriv_posCLM (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : deriv (⇑(posCLM ψ)) x = ψ x + ↑x * deriv (⇑ψ) x

The derivative of x ψ(x).

theorem WignerFunction.integral_mul_deriv (ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ), ↑x * deriv (⇑ψ) x = -∫ (x : ℝ), ψ x

★ Integration by parts against the coordinate: ∫ x ψ'(x) dx = −∫ ψ.

The ξ-moment of the Wigner function at a fixed position

theorem WignerFunction.hasDerivAt_mulConj (φ ψ : SchwartzMap ℝ ℂ) (x : ℝ) : HasDerivAt (fun (y : ℝ) => (mulConj φ ψ) y) (deriv (⇑φ) x * (starRingEnd ℂ) (ψ x) + φ x * (starRingEnd ℂ) (deriv (⇑ψ) x)) x

The derivative of the pointwise product φ · conj ψ.

theorem WignerFunction.hasDerivAt_affine (ψ : SchwartzMap ℝ ℂ) (x s y : ℝ) : HasDerivAt (fun (t : ℝ) => ψ (x + s * t)) (↑s * deriv (⇑ψ) (x + s * y)) y

The chain rule for the affine reparametrisations of Wigner.lean.

theorem WignerFunction.hasDerivAt_wignerKernel_zero (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : HasDerivAt (fun (y : ℝ) => (wignerKernel ψ x) y) (2⁻¹ * (deriv (⇑ψ) x * (starRingEnd ℂ) (ψ x) - ψ x * (starRingEnd ℂ) (deriv (⇑ψ) x))) 0

The y-derivative of the Wigner kernel at the origin is the probability current, up to the factor 2πi.

theorem WignerFunction.integral_mul_wigner_right (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ∫ (ξ : ℝ), ↑ξ * wigner ψ x ξ = (2 * ↑Real.pi * Complex.I)⁻¹ * (2⁻¹ * (deriv (⇑ψ) x * (starRingEnd ℂ) (ψ x) - ψ x * (starRingEnd ℂ) (deriv (⇑ψ) x)))

★★ The first ξ-moment of the Wigner function at a fixed position is the probability current — the local momentum density, whose integral is the momentum expectation.

Integrability of the products that appear

theorem WignerFunction.integrable_mulConj (φ ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => φ x * (starRingEnd ℂ) (ψ x)) MeasureTheory.volume

theorem WignerFunction.integrable_mul_mulConj (φ ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => ↑x * (φ x * (starRingEnd ℂ) (ψ x))) MeasureTheory.volume

theorem WignerFunction.integrable_deriv_mul_conj (ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => deriv (⇑ψ) x * (starRingEnd ℂ) (ψ x)) MeasureTheory.volume

theorem WignerFunction.integrable_mul_conj_deriv (ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => ψ x * (starRingEnd ℂ) (deriv (⇑ψ) x)) MeasureTheory.volume

theorem WignerFunction.integrable_mul_deriv_mul_conj (ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => ↑x * (deriv (⇑ψ) x * (starRingEnd ℂ) (ψ x))) MeasureTheory.volume

theorem WignerFunction.integrable_mul_mul_conj_deriv (ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => ↑x * (ψ x * (starRingEnd ℂ) (deriv (⇑ψ) x))) MeasureTheory.volume

The two current identities

theorem WignerFunction.deriv_mulConj_self (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : deriv (⇑(mulConj ψ ψ)) x = deriv (⇑ψ) x * (starRingEnd ℂ) (ψ x) + ψ x * (starRingEnd ℂ) (deriv (⇑ψ) x)

The derivative of |ψ|².

theorem WignerFunction.integral_deriv_mul_conj_add (ψ : SchwartzMap ℝ ℂ) : (∫ (x : ℝ), deriv (⇑ψ) x * (starRingEnd ℂ) (ψ x)) + ∫ (x : ℝ), ψ x * (starRingEnd ℂ) (deriv (⇑ψ) x) = 0

★ The current integrates to zero: ∫ (ψ' conj ψ + ψ conj ψ') = 0, since it is the integral of the derivative of |ψ|².

theorem WignerFunction.integral_mul_deriv_mul_conj_add (ψ : SchwartzMap ℝ ℂ) : (∫ (x : ℝ), ↑x * (deriv (⇑ψ) x * (starRingEnd ℂ) (ψ x))) + ∫ (x : ℝ), ↑x * (ψ x * (starRingEnd ℂ) (deriv (⇑ψ) x)) = -∫ (x : ℝ), ψ x * (starRingEnd ℂ) (ψ x)

★★ The weighted current identity: ∫ x (ψ' conj ψ + ψ conj ψ') = −∫ |ψ|², which is integration by parts against the coordinate.

The three temperate symbols

theorem WignerFunction.integral_integral_wigner_pos (ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ) (ξ : ℝ), ↑x * wigner ψ x ξ = ∫ (x : ℝ), (starRingEnd ℂ) (ψ x) * (posCLM ψ) x

★★ The symbol a(x, ξ) = x quantises to the position operator.

theorem WignerFunction.integral_integral_wigner_mom (ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ) (ξ : ℝ), ↑ξ * wigner ψ x ξ = ∫ (x : ℝ), (starRingEnd ℂ) (ψ x) * (momCLM ψ) x

★★ The symbol a(x, ξ) = ξ quantises to the momentum operator P = (2πi)⁻¹ d/dx.

theorem WignerFunction.integral_integral_wigner_posMom (ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ) (ξ : ℝ), ↑x * ↑ξ * wigner ψ x ξ = ∫ (x : ℝ), (starRingEnd ℂ) (ψ x) * (2⁻¹ * ((posCLM (momCLM ψ)) x + (momCLM (posCLM ψ)) x))

★★★ The symbol a(x, ξ) = xξ quantises to the symmetrised product ½(XP + PX). This is the third temperate symbol and the only one that is not a marginal: the phase-space average of xξ against W_ψ is the expectation of the symmetrised product, the extra ½ψ coming from the integration by parts that the weight x forces.

The Wigner function as a function on the plane

theorem WignerFunction.integrable_normSq (g : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (y : ℝ) => ‖g y‖ ^ 2) MeasureTheory.volume

The square of the modulus of a Schwartz function is integrable.

theorem WignerFunction.stronglyMeasurable_wigner (ψ : SchwartzMap ℝ ℂ) : MeasureTheory.StronglyMeasurable fun (p : ℝ × ℝ) => wigner ψ p.1 p.2

★ The Wigner function is jointly measurable on the plane.

noncomputable def WignerFunction.wignerEnergy (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ℝ

The ξ-energy of the Wigner function at a fixed position: ∫ |W_ψ(x, ξ)|² dξ.

Equations

• WignerFunction.wignerEnergy ψ x = ∫ (ξ : ℝ), ‖WignerFunction.wigner ψ x ξ‖ ^ 2

theorem WignerFunction.integrable_normSq_wigner (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : MeasureTheory.Integrable (fun (ξ : ℝ) => ‖wigner ψ x ξ‖ ^ 2) MeasureTheory.volume

theorem WignerFunction.wignerEnergy_eq (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ↑(wignerEnergy ψ x) = ∫ (ξ : ℝ), wigner ψ x ξ * (starRingEnd ℂ) (wigner ψ x ξ)

The energy is the slicewise overlap of the Wigner function with itself.

theorem WignerFunction.integrable_wignerEnergy (ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (wignerEnergy ψ) MeasureTheory.volume

★★ The energy is an integrable function of the position: it is a convolution of two integrable functions, read at 2x.

theorem WignerFunction.integrable_normSq_wigner_prod (ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => ‖wigner ψ p.1 p.2‖ ^ 2) (MeasureTheory.volume.prod MeasureTheory.volume)

★★ The Wigner function is square-integrable on the plane.

theorem WignerFunction.integrable_wigner_mul_conj (φ ψ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (Function.uncurry fun (x ξ : ℝ) => wigner φ x ξ * (starRingEnd ℂ) (wigner ψ x ξ)) (MeasureTheory.volume.prod MeasureTheory.volume)

★★★ The overlap integrand is integrable on the plane, so the overlap identity is an integral against the product measure and not only an iterated integral. The bound is the elementary |ab| ≤ (|a|² + |b|²)/2, which is what square-integrability buys.

theorem WignerFunction.integral_prod_wigner_mul_conj (φ ψ : SchwartzMap ℝ ℂ) : ∫ (p : ℝ × ℝ), wigner φ p.1 p.2 * (starRingEnd ℂ) (wigner ψ p.1 p.2) = (∫ (v : ℝ), φ v * (starRingEnd ℂ) (ψ v)) * (starRingEnd ℂ) (∫ (v : ℝ), φ v * (starRingEnd ℂ) (ψ v))

★★★ The overlap identity against the product measure on the plane. This is integral_integral_wigner_mul_conj with the iterated integral replaced by a single integral over phase space, which is what makes W_ψ a function on the plane rather than a family of slices.

theorem WignerFunction.integral_prod_wigner_sq (ψ : SchwartzMap ℝ ℂ) : ∫ (p : ℝ × ℝ), wigner ψ p.1 p.2 * wigner ψ p.1 p.2 = (∫ (v : ℝ), ↑‖ψ v‖ ^ 2) * ∫ (v : ℝ), ↑‖ψ v‖ ^ 2

★★ The purity form on the plane.