Theorem 10.3 — the virial theorem λ = −⟨ψ, H₀ψ⟩ = ½⟨ψ, Vψ⟩

Proved

TeschlQM.OneParticle.virial

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1schrodinger-operatorsspectral-theory

Let $n \ge 1$ and let $U(s)\psi(x) = e^{-ns/2}\psi(e^{-s}x)$ be the dilation group on $L^2(\mathbb R^n)$ . Suppose $V : \mathbb R^n \to \mathbb R$ is measurable with $U(-s) V U(s) = e^{-s} V$ for all $s \in \mathbb R$ , and let $H = H_0 + V$ on $\mathfrak D(H_0) \cap \mathfrak D(V)$ . Then any normalized eigenfunction $\psi$ of $H$ corresponding to an eigenvalue $\lambda$ satisfies

\lambda = -\langle \psi, H_0 \psi \rangle = \tfrac12 \langle \psi, V \psi \rangle .

In particular, every eigenvalue is real and negative.

The Coulomb potential $-\gamma/|x|$ is homogeneous of this kind, so the virial theorem shows that the hydrogen atom has no eigenvalues in $[0,\infty)$ .

Formalization Note. Since $U(-s) V U(s)$ is multiplication by $x \mapsto V(e^s x)$ , the hypothesis is stated as: for every $s$ , $V(e^s x) = e^{-s} V(x)$ for almost every $x$ . The eigenfunction $\psi$ lies in $\mathfrak D(H_0) \cap \mathfrak D(V)$ with $\|\psi\| = 1$ and $H_0\psi + V\psi = \lambda\psi$ . "Negative" is $\operatorname{Im}\lambda = 0$ and $\operatorname{Re}\lambda < 0$ .

Preamble

import Mathlib
import Definitions.Def_TeschlQM_OneParticle_multiplicationOperator
import Definitions.Def_TeschlQM_OneParticle_freeHamiltonian

Formal statement

namespace TeschlQM.OneParticle

open MeasureTheory
open scoped InnerProductSpace

/-- Teschl, Theorem 10.3 (virial theorem), p. 223. Suppose `H = H₀ + V` with
`U(-s) V U(s) = e^{-s} V`, where `U(s)ψ(x) = e^{-ns/2} ψ(e^{-s}x)` is the dilation group (10.8).
Then any normalized eigenfunction `ψ` corresponding to an eigenvalue `λ` satisfies
`λ = -⟨ψ, H₀ψ⟩ = ½⟨ψ, Vψ⟩` (10.13). In particular, all eigenvalues must be negative.

For the multiplication operator `V`, `U(-s) V U(s)` is multiplication by `x ↦ V(e^s x)`, so the
hypothesis is `V(e^s x) = e^{-s} V(x)` for a.e. `x`, for every `s ∈ ℝ`. `V` is measurable (2.21),
`H₀ + V` is the operator sum on `𝔇(H₀) ∩ 𝔇(V)`, and `n ≥ 1`. -/
theorem virial (n : ℕ) (hn : 1 ≤ n) (V : EuclideanSpace ℝ (Fin n) → ℝ) (hVm : Measurable V)
    (hV : ∀ s : ℝ, ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      V (Real.exp s • x) = Real.exp (-s) * V x)
    (lam : ℂ) (ψ : L2 n) (hψH₀ : ψ ∈ (freeHamiltonian n).domain)
    (hψV : ψ ∈ (multOp (fun x => (V x : ℂ))).domain) (hψ1 : ‖ψ‖ = 1)
    (heig : freeHamiltonian n ⟨ψ, hψH₀⟩ + multOp (fun x => (V x : ℂ)) ⟨ψ, hψV⟩ = lam • ψ) :
    lam = -⟪ψ, (freeHamiltonian n ⟨ψ, hψH₀⟩)⟫_ℂ ∧
      lam = (1 / 2 : ℂ) * ⟪ψ, (multOp (fun x => (V x : ℂ)) ⟨ψ, hψV⟩)⟫_ℂ ∧
      lam.im = 0 ∧ lam.re < 0 := by sorry

end TeschlQM.OneParticle

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 223, Theorem 10.3

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting.

$n\in\mathbb{N}$ with $n\ge1$ .
$L^2(\mathbb{R}^n)$ is the space of square-integrable complex functions on Euclidean $\mathbb{R}^n$ with Lebesgue measure, modulo equality almost everywhere. Its inner product $\langle\cdot,\cdot\rangle$ is conjugate-linear in the first argument.
$\hat\psi$ is Mathlib's unitary $L^2$ Fourier transform, the extension of $\int e^{-2\pi i\langle x,\xi\rangle}\psi(x)\,dx$ .
$H_0$ has domain $\{\psi:(2\pi\|\xi\|)^2\hat\psi\in L^2\}$ and acts by $H_0\psi=\mathcal{F}^{-1}[(2\pi\|\xi\|)^2\hat\psi]$ .
For a function $V$ , "multiplication by $V$ " has maximal domain $\{f\in L^2: Vf\in L^2\}$ and sends $f\mapsto Vf$ .

Hypotheses.

$V:\mathbb{R}^n\to\mathbb{R}$ is Borel measurable.
For every $s\in\mathbb{R}$ , for almost every $x\in\mathbb{R}^n$ ,

V(e^{s}x)=e^{-s}V(x).

The exceptional null set may depend on $s$ .

$\lambda\in\mathbb{C}$ and $\psi\in L^2(\mathbb{R}^n)$ .
$\psi$ lies in the domain of $H_0$ and in the domain of multiplication by $V$ , i.e. $V\psi\in L^2$ .
$\|\psi\|_{L^2}=1$ .
The eigenvalue equation holds:

H_0\psi+V\psi=\lambda\psi.

Conclusion. All four of the following hold:

\lambda=-\langle\psi,H_0\psi\rangle,\qquad \lambda=\tfrac12\langle\psi,V\psi\rangle,\qquad \operatorname{Im}\lambda=0,\qquad \operatorname{Re}\lambda<0 .

Degenerate cases:

$n=0$ . Excluded by the hypothesis $n\ge1$ .
$V\equiv0$ . Satisfies the scaling hypothesis. The statement then asserts that any normalized $\psi$ in the domain of $H_0$ with $H_0\psi=\lambda\psi$ has $\lambda=-\langle\psi,H_0\psi\rangle=0$ and $\lambda<0$ simultaneously.
No eigenpair. If no $(\lambda,\psi)$ satisfies the hypotheses for a given $V$ , the statement is vacuous for that $V$ .

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph