Prove2Me

The position expectation ∫x∣ψ(x)∣2dx\int x|\psi(x)|^2dx of ψ\psi is infinite

Proved
HeathcoteUnbounded.psi_position_expectation_infinite

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

functional-analysismathematical-physics

For the wave function ψ\psi of eq. (4), the would-be expectation value of position

μψ=⟨ψ,Qψ⟩=∫Rx ∣ψ(x)∣2 dx\mu_\psi=\langle\psi,Q\psi\rangle=\int_{\mathbb R}x\,|\psi(x)|^2\,dx

is infinite: ∫R∣x∣ ∣ψ(x)∣2 dx=∫1∞x−1 dx=∞\int_{\mathbb R}|x|\,|\psi(x)|^2\,dx=\int_1^\infty x^{-1}\,dx=\infty. The source: "This expectation value, or mean value, is undefined precisely because it is infinite."

Formalization Note Stated with ∣x∣|x| as a Lebesgue integral in [0,∞][0,\infty]; since ψ\psi vanishes for x<1x<1 this equals ∫x∣ψ∣2\int x|\psi|^2.

Preamble
import Mathlib
import Definitions.Def_HeathcoteUnbounded_Psi

open MeasureTheory
Formal statement
namespace HeathcoteUnbounded

theorem psi_position_expectation_infinite : ∫⁻ x : ℝ, ‖x‖ₑ * ‖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. 9
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