Prove2Me

A normalized state of L2(R)L^2(\mathbb R) outside both D(Q)D(Q) and D(P)D(P)

Proved
HeathcoteUnbounded.state_outside_position_momentum_domains

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

functional-analysismathematical-physics

There is a unit vector φ∈L2(R)\varphi\in L^2(\mathbb R) — namely the class of Heathcote's function ψ(x)=x−11[1,∞)(x)\psi(x)=x^{-1}\mathbf 1_{[1,\infty)}(x) of eq. (4) — such that

∥φ∥L2=1,φ∉D(Q),φ∉D(P),\|\varphi\|_{L^2}=1,\qquad \varphi\notin D(Q),\qquad \varphi\notin D(P),

where D(Q)D(Q) and D(P)D(P) are the domains of the position and momentum operators. So, under Postulate 1 (every normed ray is a state), there are states on which neither the position nor the momentum operator acts.

Formalization Note φ\varphi is required to be a.e. equal to psi; the domains are the sets positionDomain and momentumDomain of L2L^2 elements.

Preamble
import Mathlib
import Definitions.Def_HeathcoteUnbounded_Psi
import Definitions.Def_HeathcoteUnbounded_PositionDomain
import Definitions.Def_HeathcoteUnbounded_MomentumDomain

open MeasureTheory
Formal statement
namespace HeathcoteUnbounded

theorem state_outside_position_momentum_domains :
    ∃ φ : Lp ℂ 2 (volume : Measure ℝ), (φ : ℝ → ℂ) =ᵐ[volume] psi ∧ ‖φ‖ = 1 ∧
      φ ∉ positionDomain ∧ φ ∉ momentumDomain := by sorry

end HeathcoteUnbounded
Source
A. Heathcote, "Unbounded Operators and the Incompleteness of Quantum Mechanics", Philosophy of Science 57 (1990), 523–534, pp. 4–6, eqs. (3)–(4)
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