$x\psi(x)$ is not square-integrable: $\psi\notin D(Q)$

Proved

HeathcoteUnbounded.psi_not_mem_positionDomain

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

functional-analysismathematical-physics

For the wave function $\psi$ of eq. (4),

\int_{\mathbb R}x^2\,|\psi(x)|^2\,dx=\int_1^\infty 1\,dx=\infty .

Thus $Q\psi=x\psi(x)$ is not in $L^2(\mathbb R)$ and $\psi$ is not in the domain $D(Q)$ of the position operator.

Preamble

import Mathlib
import Definitions.Def_HeathcoteUnbounded_Psi

open MeasureTheory

Formal statement

namespace HeathcoteUnbounded

theorem psi_not_mem_positionDomain : ∫⁻ x : ℝ, ‖x‖ₑ ^ 2 * ‖psi x‖ₑ ^ 2 = ⊤ := by sorry

end HeathcoteUnbounded

Source

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

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).

xψ(x)x\psi(x)xψ(x) is not square-integrable: ψ∉D(Q)\psi\notin D(Q)ψ∈/D(Q)