Prove2Me

The wave function (4) is a normalized element of L2(R)L^2(\mathbb R)

Proved
HeathcoteUnbounded.psi_unit_norm

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

functional-analysismathematical-physics

Let ψ(x)=x−1\psi(x)=x^{-1} for x≥1x\ge1 and ψ(x)=0\psi(x)=0 for x<1x<1 (eq. (4)). Then ψ∈L2(R)\psi\in L^2(\mathbb R) and

∫R∣ψ(x)∣2 dx=∫1∞x−2 dx=1.\int_{\mathbb R}|\psi(x)|^2\,dx=\int_1^{\infty}x^{-2}\,dx=1 .

Hence ψ\psi is a unit vector and, by Postulate 1, represents a state.

Preamble
import Mathlib
import Definitions.Def_HeathcoteUnbounded_Psi

open MeasureTheory
Formal statement
namespace HeathcoteUnbounded

theorem psi_unit_norm : MemLp psi 2 volume ∧ ∫⁻ x : ℝ, ‖psi x‖ₑ ^ 2 = 1 := by sorry

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