Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Eqs. (27)–(28) — Gaussian moments are finite, Lorentzian moments diverge

Proved
UnphysicalHilbert.eq27_28_moments

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

momentsprobability

Let ψ(x)=e−x2/π\psi(x)=\sqrt{e^{-x^2}/\sqrt\pi}ψ(x)=e−x2/π​​ and ϕ(y)=1/π(y2+1)\phi(y)=1/\sqrt{\pi(y^2+1)}ϕ(y)=1/π(y2+1)​. Then

  1. ∫Rψ(x)2 dx=1\displaystyle\int_{\mathbb R}\psi(x)^2\,dx=1∫R​ψ(x)2dx=1 and ∫Rϕ(y)2 dy=1\displaystyle\int_{\mathbb R}\phi(y)^2\,dy=1∫R​ϕ(y)2dy=1;
  2. for every n∈Nn\in\mathbb Nn∈N, ∫R∣x∣n ψ(x)2 dx<∞\displaystyle\int_{\mathbb R}|x|^n\,\psi(x)^2\,dx<\infty∫R​∣x∣nψ(x)2dx<∞;
  3. for every n≥2n\ge2n≥2, ∫R∣y∣n ϕ(y)2 dy=∞\displaystyle\int_{\mathbb R}|y|^n\,\phi(y)^2\,dy=\infty∫R​∣y∣nϕ(y)2dy=∞.

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 ⟨X2⟩\langle X^2\rangle⟨X2⟩).

Formalization Note Finiteness of ∫g\int g∫g for a nonnegative ggg is expressed as Lebesgue integrability of ggg, 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
  • 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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me