Theorem 9.9 — Weyl's limit circle / limit point alternative

Proved

TeschlQM.SturmLiouville.weyl_alternative

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

limit-circlep2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1sturm-liouvilleweyl-alternative

Let $(a,b,p,q,r)$ be Sturm–Liouville data on $I = (a,b)$ and let $\tau f = \frac{1}{r}(-(pf')' + qf)$ . Then:

$\tau$ is limit circle at $a$ if and only if for one $z_0 \in \mathbb{C}$ all solutions of $(\tau - z_0)u = 0$ are square integrable near $a$ ;
if $\tau$ is limit circle at $a$ , then for all $z \in \mathbb{C}$ all solutions of $(\tau - z)u = 0$ are square integrable near $a$ ;
and similarly for $b$ .

\tau \text{ l.c. at } a \iff \exists z_0 \in \mathbb{C}\ \forall u:\ (\tau - z_0)u = 0 \Rightarrow u \in L^2((a,c), r\,dx) \text{ for some } c \in I.

Limit circle is defined through boundary Wronskians on the maximal domain $\mathfrak{D}(\tau)$ (p. 187), so the theorem converts a statement about boundary conditions of self-adjoint realizations into a statement about the solutions of an ordinary differential equation, which can be checked in examples.

Formalization Note. Solutions are complex-valued with $u, pu' \in AC_{loc}(I)$ ; the coefficients are only locally integrable. "Square integrable near $a$ " is IsSqIntegrableNearLeft (some $c \in I$ , weight $r$ ).

Preamble

import Mathlib
import Definitions.Def_TeschlQM_SturmLiouville_IsLimitCircle
import Definitions.Def_TeschlQM_SturmLiouville_IsSqIntegrableNear

Formal statement

namespace TeschlQM.SturmLiouville

/-- Teschl, Theorem 9.9 (Weyl alternative), p. 191. `τ` is l.c. at `a` if and only if for one
`z₀ ∈ ℂ` all solutions of `(τ − z₀) u = 0` are square integrable near `a`. This then holds for all
`z ∈ ℂ`, and similarly for `b`. Limit circle is the Wronskian notion of p. 187, not square
integrability. -/
theorem weyl_alternative (L : SLData) :
    (IsLimitCircleLeft L ↔
        ∃ z₀ : ℂ, ∀ u : ℝ → ℂ, IsSolution L z₀ 0 u → IsSqIntegrableNearLeft L u) ∧
      (IsLimitCircleLeft L →
        ∀ z : ℂ, ∀ u : ℝ → ℂ, IsSolution L z 0 u → IsSqIntegrableNearLeft L u) ∧
      (IsLimitCircleRight L ↔
        ∃ z₀ : ℂ, ∀ u : ℝ → ℂ, IsSolution L z₀ 0 u → IsSqIntegrableNearRight L u) ∧
      (IsLimitCircleRight L →
        ∀ z : ℂ, ∀ u : ℝ → ℂ, IsSolution L z 0 u → IsSqIntegrableNearRight L u) := by sorry

end TeschlQM.SturmLiouville

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 191, Theorem 9.9

Read-back

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

Fix a Sturm–Liouville datum $L$ of type SLData. This type comes from an imported definitions file that is not shown here, so its fields (the interval endpoints $a<b$ and the coefficient functions, for example) cannot be listed from this code. The statement uses four predicates from the imported definitions, and their bodies are not shown either:

$\mathrm{LC}_{\mathrm{left}}(L)$ (IsLimitCircleLeft L): the property named "limit circle at the left endpoint."
$\mathrm{LC}_{\mathrm{right}}(L)$ (IsLimitCircleRight L): the same at the right endpoint.
$\mathrm{Sol}(L,z,0,u)$ (IsSolution L z 0 u): a relation between $L$ , a complex number $z$ , the constant $0$ in a third argument slot, and a function $u:\mathbb{R}\to\mathbb{C}$ . By its name it means " $u$ solves the equation for $L$ at spectral parameter $z$ with right-hand side $0$ ." The exact meaning, including any regularity conditions and what is required of $u$ outside the interval, is whatever the unseen definition says.
$\mathrm{SqInt}_{\mathrm{left}}(L,u)$ and $\mathrm{SqInt}_{\mathrm{right}}(L,u)$ (IsSqIntegrableNearLeft L u, IsSqIntegrableNearRight L u): the properties named " $u$ is square integrable near the left (respectively right) endpoint." Which weight and measure are used, and what "near" means, are fixed by the unseen definitions.

The doc comment says that "limit circle" is a Wronskian notion rather than square integrability. That is a comment only; the code shown does not establish it.

The theorem asserts that the following four statements all hold, for every such $L$ :

Left endpoint, equivalence. $\mathrm{LC}_{\mathrm{left}}(L)$ holds if and only if some $z_0\in\mathbb{C}$ makes every solution square integrable near the left endpoint:

\mathrm{LC}_{\mathrm{left}}(L)\iff \exists z_0\in\mathbb{C}\ \ \forall u:\mathbb{R}\to\mathbb{C},\ \ \mathrm{Sol}(L,z_0,0,u)\implies \mathrm{SqInt}_{\mathrm{left}}(L,u).

Left endpoint, every parameter. If $\mathrm{LC}_{\mathrm{left}}(L)$ holds, then for every $z\in\mathbb{C}$ and every $u:\mathbb{R}\to\mathbb{C}$ with $\mathrm{Sol}(L,z,0,u)$ , the function $u$ is square integrable near the left endpoint:

\mathrm{LC}_{\mathrm{left}}(L)\implies \forall z\in\mathbb{C}\ \ \forall u,\ \ \mathrm{Sol}(L,z,0,u)\implies \mathrm{SqInt}_{\mathrm{left}}(L,u).

Right endpoint, equivalence. The same as (1), with $\mathrm{LC}_{\mathrm{right}}$ and $\mathrm{SqInt}_{\mathrm{right}}$ in place of the left-endpoint predicates.
Right endpoint, every parameter. The same as (2), with $\mathrm{LC}_{\mathrm{right}}$ and $\mathrm{SqInt}_{\mathrm{right}}$ in place of the left-endpoint predicates.

The quantifier over $u$ ranges over all functions $\mathbb{R}\to\mathbb{C}$ that satisfy the solution predicate, with no further condition. That includes the zero function, if $\mathrm{Sol}$ admits it. Parts (2) and (4) are one-way implications: the statement does not assert their converses separately. Those converses follow from (1) and (3) only because "for all $z$ " implies "for some $z$ ."

Degenerate cases. The theorem places no hypothesis on $L$ beyond its type, so it applies to every value the type SLData admits, including any degenerate interval or coefficient choices the definition allows.

If for some $z_0$ no function satisfies $\mathrm{Sol}(L,z_0,0,\cdot)$ , the right-hand side of (1) or (3) is true vacuously. The theorem then forces $\mathrm{LC}_{\mathrm{left}}(L)$ , or $\mathrm{LC}_{\mathrm{right}}(L)$ , to hold.
The same happens if every solution at some $z_0$ passes the square-integrability test for a trivial reason, for example because of how that predicate treats an empty or zero-length neighbourhood, or non-integrable functions.
If $\mathrm{SqInt}$ is defined through a Lebesgue integral, non-integrable functions get the default integral value, and that value can affect when the predicate holds. The code shown does not settle this.
Whether these vacuous cases can actually occur depends entirely on the unseen definitions of SLData, IsSolution, IsLimitCircleLeft/Right and IsSqIntegrableNearLeft/Right.

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