Theorem 10.11 — for a positivity improving operator, ‖A‖ is a simple eigenvalue with positive eigenfunction

Proved

TeschlQM.OneParticle.positivityImproving_eigenvalue

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

functional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1perron-frobeniuspositivity

Let $A$ be a bounded self-adjoint operator on $L^2(\mathbb R^n)$ which is positivity improving (it maps every positive function to a strictly positive one) and real (it maps real functions to real functions). If $\|A\|$ is an eigenvalue of $A$ , then it is simple and the corresponding eigenfunction is strictly positive:

\dim \operatorname{Ker}(A - \|A\|) = 1, \qquad \operatorname{Ker}(A - \|A\|) \ni \psi \text{ with } \psi > 0 \text{ a.e.}

This is an infinite-dimensional Perron–Frobenius theorem; applied to resolvents it yields nondegeneracy of ground states.

Formalization Note. "Self-adjoint" is Mathlib's IsSelfAdjoint for L2 n →L[ℂ] L2 n, " $\|A\|$ is an eigenvalue" is the existence of $\psi \ne 0$ with $A\psi = \|A\|\psi$ , and "simple" is Module.finrank ℂ (Module.End.eigenspace A ‖A‖) = 1 (an infinite-dimensional eigenspace would have finrank $0$ ). Positivity uses ComplexOrder pointwise almost everywhere.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_OneParticle_multiplicationOperator
import Definitions.Def_TeschlQM_OneParticle_positivity

Formal statement

namespace TeschlQM.OneParticle

/-- Teschl, Theorem 10.11, p. 236. Suppose `A ∈ 𝔏(L²(ℝⁿ))` is a self-adjoint, positivity improving
and real (i.e., it maps real functions to real functions) operator. If `‖A‖` is an eigenvalue,
then it is simple and the corresponding eigenfunction is strictly positive: the eigenspace of
`‖A‖` is one-dimensional and contains a strictly positive function. -/
theorem positivityImproving_eigenvalue (n : ℕ) (A : L2 n →L[ℂ] L2 n) (hA : IsSelfAdjoint A)
    (hpos : IsPositivityImproving A) (hreal : IsRealOperator A)
    (heig : ∃ ψ : L2 n, ψ ≠ 0 ∧ A ψ = (‖A‖ : ℂ) • ψ) :
    Module.finrank ℂ (Module.End.eigenspace (A : Module.End ℂ (L2 n)) (‖A‖ : ℂ)) = 1 ∧
      ∃ ψ : L2 n, A ψ = (‖A‖ : ℂ) • ψ ∧ IsStrictlyPositive ψ := by sorry

end TeschlQM.OneParticle

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 236, Theorem 10.11

Read-back

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

Space and ordering. $n\in\mathbb{N}$ is arbitrary, including $0$ . $L^2(\mathbb{R}^n)$ is the space of complex square-integrable functions on Euclidean $\mathbb{R}^n$ with Lebesgue measure, modulo equality almost everywhere. For a class $f$ :

$f$ is positive when $f(x)$ is a nonnegative real number for almost every $x$ and $f\neq0$ ;
$f$ is strictly positive when $f(x)$ is a strictly positive real number for almost every $x$ .

Hypotheses on $A$ . $A$ is a bounded (continuous) complex-linear operator on $L^2(\mathbb{R}^n)$ with operator norm $\|A\|$ . It satisfies:

$A$ is self-adjoint: $A^*=A$ .
$A$ is positivity improving: $Af$ is strictly positive for every positive $f$ .
$A$ is real: whenever $\operatorname{Im}f=0$ almost everywhere, also $\operatorname{Im}(Af)=0$ almost everywhere.
$\|A\|$ , viewed as a complex number, is an eigenvalue: there is $\psi\neq0$ with $A\psi=\|A\|\psi$ .

Claim. Both of the following hold:

The eigenspace $\{\psi: A\psi=\|A\|\psi\}$ has dimension exactly $1$ over $\mathbb{C}$ . A finite-rank value of $1$ excludes the infinite-dimensional case, since the rank convention returns $0$ there.
There exists $\psi$ with $A\psi=\|A\|\psi$ that is strictly positive. Such a $\psi$ is automatically nonzero.

Degenerate case: $n=0$ . $L^2(\mathbb{R}^0)\cong\mathbb{C}$ and $A$ is multiplication by some $c\in\mathbb{C}$ . The hypotheses then force $c$ to be a positive real number with $\|A\|=c$ . The claim becomes: the whole one-dimensional space is the eigenspace, and it contains a positive real number.

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