Domain $D(P)$ of the momentum operator on $L^2(\mathbb R)$ (absolutely continuous elements)

Definition

HeathcoteUnbounded_MomentumDomain

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

functional-analysismathematical-physics

The momentum operator is $P\psi=\hbar\, i^{-1}\,\frac{d\psi}{dx}$ . Following p. 5 of the source, its domain $D(P)$ "consists of all absolutely continuous functions $f\in L^2(\mathbb R)$ ":

D(P)=\{\,f\in L^2(\mathbb R)\ :\ f \text{ has a representative } g \text{ that is absolutely continuous on every compact interval } [a,b]\,\}.

Formalization Note Absolute continuity on $[a,b]$ is Mathlib's AbsolutelyContinuousOnInterval. The source omits the usual extra condition $f'\in L^2(\mathbb R)$ of the standard self-adjoint momentum domain; the set defined here is therefore a superset of the standard domain, so showing that a state is not in it is a (slightly) stronger statement than non-membership in the standard domain.

Definition code

import Mathlib

open MeasureTheory

namespace HeathcoteUnbounded

/-- Domain of the momentum operator `P = ħ i⁻¹ d/dx` as described on p. 5 of the source:
the elements of `L²(ℝ)` that are (represented by) absolutely continuous functions, i.e. have a
representative that is absolutely continuous on every compact interval. -/
def momentumDomain : Set (Lp ℂ 2 (volume : Measure ℝ)) :=
  {f | ∃ g : ℝ → ℂ, (f : ℝ → ℂ) =ᵐ[volume] g ∧ ∀ a b : ℝ, AbsolutelyContinuousOnInterval g a b}

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

View graph

Domain D(P)D(P)D(P) of the momentum operator on L2(R)L^2(\mathbb R)L2(R) (absolutely continuous elements)

Domain $D(P)$ of the momentum operator on $L^2(\mathbb R)$ (absolutely continuous elements)