Domain $D(Q)$ of the position operator on $L^2(\mathbb R)$ , eq. (3)

Definition

HeathcoteUnbounded_PositionDomain

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

functional-analysismathematical-physics

The position operator $Q$ on $L^2(\mathbb R)$ acts by $(Q\psi)(x)=x\,\psi(x)$ . Its domain, equation (3) of the source, is

D(Q)=\Big\{\psi\in L^2(\mathbb R)\ :\ \int_{\mathbb R} x^2\,|\psi(x)|^2\,dx<\infty\Big\},

i.e. exactly those square-integrable $\psi$ for which $x\psi(x)$ is again square-integrable.

Formalization Note $D(Q)$ is a subset of Mathlib's Lp ℂ 2 volume on ℝ; the integral is a Lebesgue integral in $[0,\infty]$ of $|x|^2|\psi(x)|^2$ , which does not depend on the chosen representative.

Definition code

import Mathlib

open MeasureTheory

namespace HeathcoteUnbounded

/-- Domain of the position operator `(Qψ)(x) = x ψ(x)` on `L²(ℝ)`, eq. (3):
`D(Q) = {ψ ∈ L²(ℝ) : ∫ x² |ψ(x)|² dx < ∞}`. -/
def positionDomain : Set (Lp ℂ 2 (volume : Measure ℝ)) :=
  {f | ∫⁻ x : ℝ, ‖x‖ₑ ^ 2 * ‖(f : ℝ → ℂ) x‖ₑ ^ 2 < ⊤}

end HeathcoteUnbounded

Source

A. Heathcote, "Unbounded Operators and the Incompleteness of Quantum Mechanics", Philosophy of Science 57 (1990), 523–534, p. 4, eq. (3)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Domain D(Q)D(Q)D(Q) of the position operator on L2(R)L^2(\mathbb R)L2(R), eq. (3)

Domain $D(Q)$ of the position operator on $L^2(\mathbb R)$ , eq. (3)