Heathcote's wave function $\psi(x)=x^{-1}\mathbf 1_{[1,\infty)}(x)$ , eq. (4)

Definition

HeathcoteUnbounded_Psi

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

functional-analysismathematical-physics

The complex-valued function $\psi:\mathbb R\to\mathbb C$ of equation (4) in the source,

\psi(x)=\begin{cases} x^{-1} & \text{if } x\ge 1,\\ 0 & \text{if } x<1.\end{cases}

It is the explicit wave function used to exhibit a normalized state of $L^2(\mathbb R)$ that lies outside the domains of the position and momentum operators.

Formalization Note psi is an ordinary function ℝ → ℂ; its class in $L^2(\mathbb R)$ is produced in the goal theorem.

Definition code

import Mathlib

namespace HeathcoteUnbounded

/-- Heathcote's wave function, eq. (4): `ψ(x) = x⁻¹` for `x ≥ 1` and `ψ(x) = 0` for `x < 1`. -/
noncomputable def psi : ℝ → ℂ := fun x => if 1 ≤ x then ((x : ℂ))⁻¹ else 0

end HeathcoteUnbounded

Source

A. Heathcote, "Unbounded Operators and the Incompleteness of Quantum Mechanics", Philosophy of Science 57 (1990), 523–534, p. 5, eq. (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

Heathcote's wave function ψ(x)=x−11[1,∞)(x)\psi(x)=x^{-1}\mathbf 1_{[1,\infty)}(x)ψ(x)=x−11[1,∞)​(x), eq. (4)

Heathcote's wave function $\psi(x)=x^{-1}\mathbf 1_{[1,\infty)}(x)$ , eq. (4)