Eqs. (27)–(28) — Gaussian moments are finite, Lorentzian moments diverge
ProvedUnphysicalHilbert.eq27_28_momentsmomentsprobability
Let and . Then
- and ;
- for every , ;
- for every , .
The Gaussian state has finite position moments of all orders, while the Lorentzian state has infinite position moments from the second on (in particular infinite ).
Formalization Note Finiteness of for a nonnegative is expressed as Lebesgue integrability of , and infiniteness as its failure.
Preamble
import Definitions.Def_UnphysicalHilbert_Position
Formal statement
namespace UnphysicalHilbert
open MeasureTheory
/-- Equations (27)–(28): both wave functions are normalized; the Gaussian state has finite
moments of every order, while the Lorentzian state has divergent moments of every order
`n ≥ 2`. -/
theorem eq27_28_moments :
∫ x, gaussianWave x ^ 2 = 1 ∧ ∫ y, lorentzianWave y ^ 2 = 1 ∧
(∀ n : ℕ, Integrable (fun x : ℝ => |x| ^ n * gaussianWave x ^ 2)) ∧
(∀ n : ℕ, 2 ≤ n → ¬ Integrable (fun y : ℝ => |y| ^ n * lorentzianWave y ^ 2)) := by
sorry
end UnphysicalHilbert
Source
G. Carcassi, C. A. Aidala, F. Calderón, *The unphysicality of Hilbert spaces*, arXiv:2308.06669v3 [quant-ph], 22 Dec 2024, https://arxiv.org/abs/2308.06669, Section VI, pp. 11–12, eqs. (27)–(28) and the paragraph following them
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.