Limit circle at $a$ implies all solutions are square integrable near $a$ for some $z_0$

Proved

TeschlQM.SturmLiouville.sqIntegrable_of_limitCircle

by Gabewhigham · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

limit-circlesturm-liouville

Let $(a,b,p,q,r)$ be Sturm–Liouville data. If $\tau$ is limit circle at $a$ (Wronskian definition, Teschl p. 187), then there is $z_0\in\mathbb C$ such that every solution of $(\tau-z_0)u=0$ is square integrable near $a$ . Similarly at $b$ .

In Teschl this follows from Theorem 9.6 and Lemma 9.7. Take two real $v,\tilde v\in\mathfrak D(\tau)$ with $W_a(v,\tilde v)\neq0$ ; they give two self-adjoint realizations. For nonreal $z$ , the solutions $u_a$ and $\tilde u_a$ of Lemma 9.7 are square integrable near $a$ and linearly independent.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_SturmLiouville_IsLimitCircle
import Definitions.Def_TeschlQM_SturmLiouville_IsSqIntegrableNear

Formal statement

namespace TeschlQM.SturmLiouville

theorem sqIntegrable_of_limitCircle (L : SLData) :
    (IsLimitCircleLeft L →
      ∃ z₀ : ℂ, ∀ u : ℝ → ℂ, IsSolution L z₀ 0 u → IsSqIntegrableNearLeft 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, Section 9.2, proof of Theorem 9.9 (p. 191), the 'only if' direction

View graph

Limit circle at aaa implies all solutions are square integrable near aaa for some z0z_0z0​

Limit circle at $a$ implies all solutions are square integrable near $a$ for some $z_0$