Theorem 9.6 — self-adjoint realizations with separated boundary conditions

Proved

TeschlQM.SturmLiouville.selfAdjoint_bc

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

p2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1self-adjoint-extensionsself-adjoint-operatorssturm-liouville

Let $(a,b,p,q,r)$ be Sturm–Liouville data. If $\tau$ is l.c. at $a$ , let $v \in \mathfrak{D}(\tau)$ with $W_a(v^*, v) = 0$ and $W_a(v, f) \neq 0$ for some $f \in \mathfrak{D}(\tau)$ ; similarly, if $\tau$ is l.c. at $b$ , let $w$ be an analogous function at $b$ . Then the operator

A : \mathfrak{D}(A) \to L^2(I, r\,dx), \quad f \mapsto \tau f, \qquad \mathfrak{D}(A) = \{ f \in \mathfrak{D}(\tau) \mid W_a(v, f) = 0 \text{ if l.c. at } a,\ W_b(w, f) = 0 \text{ if l.c. at } b\}

is self-adjoint. Moreover the set $\mathfrak{D}_1$ of (9.21) is a core for $A$ : the closure of the restriction of $A$ to $\mathfrak{D}_1$ is $A$ .

This produces the self-adjoint Sturm–Liouville operators whose resolvents and spectra are studied in the rest of the chapter.

Formalization Note. The conclusion asserts that there is a LinearPMap $A$ on $L^2(I, r\,dx)$ whose graph is $\{(f, \tau f) \mid f \in \mathfrak{D}(A)\}$ (so $A$ is well defined), that $A$ is self-adjoint (Mathlib's IsSelfAdjoint), and that the operator $A_1$ with graph $\{(f, \tau f) \mid f \in \mathfrak{D}_1\}$ exists and has closure $A$ . When $\tau$ is l.p. at an endpoint the hypothesis on $v$ (resp. $w$ ) is vacuous and no condition is imposed there.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_SturmLiouville_operatorGraph

Formal statement

namespace TeschlQM.SturmLiouville

open MeasureTheory

/-- Teschl, Theorem 9.6, p. 187. If `τ` is l.c. at `a`, let `v ∈ D(τ)` with `W_a(v*, v) = 0` and
`W_a(v, f) ≠ 0` for some `f ∈ D(τ)`; similarly `w` at `b` if `τ` is l.c. at `b`. Then
`f ↦ τ f` on `𝔇(A)` (9.20) is a (well-defined) self-adjoint operator `A` in `L²(I, r dx)`, and
`D₁` (9.21) is a core for `A`: the closure of `A` restricted to `D₁` is `A`. -/
theorem selfAdjoint_bc (L : SLData) (v w : ℝ → ℂ)
    (hv : IsLimitCircleLeft L → InMaxDomain L v ∧
      wronskianLeft L (fun x => starRingEnd ℂ (v x)) v = 0 ∧
      ∃ f : ℝ → ℂ, InMaxDomain L f ∧ wronskianLeft L v f ≠ 0)
    (hw : IsLimitCircleRight L → InMaxDomain L w ∧
      wronskianRight L (fun x => starRingEnd ℂ (w x)) w = 0 ∧
      ∃ f : ℝ → ℂ, InMaxDomain L f ∧ wronskianRight L w f ≠ 0) :
    ∃ A : Lp ℂ 2 L.measure →ₗ.[ℂ] Lp ℂ 2 L.measure,
      (A.graph : Set (Lp ℂ 2 L.measure × Lp ℂ 2 L.measure)) =
          operatorGraph L (bcDomain L v w) ∧
        IsSelfAdjoint A ∧
        ∃ A₁ : Lp ℂ 2 L.measure →ₗ.[ℂ] Lp ℂ 2 L.measure,
          (A₁.graph : Set (Lp ℂ 2 L.measure × Lp ℂ 2 L.measure)) =
              operatorGraph L (coreDomain L v w) ∧
            A₁.closure = A := by sorry

end TeschlQM.SturmLiouville

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 187, Theorem 9.6, Eqs. (9.19)–(9.21)

Read-back

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

Setting. Fix $L$ with interval $I$ , $\mu = r\,dx$ on $I$ , and $L^2 = L^2(\mu)$ (a complex Hilbert space of a.e.-classes). The notions used are:

$D(\tau)$ : the maximal domain.
$W_x$ , $W_a$ , $W_b$ : the pointwise Wronskian and its boundary limits (an unspecified value when the limit does not exist).
"l.c. at $a$ ": there is $v' \in D(\tau)$ with $W_a(\bar v', v') = 0$ and $W_a(v', f) \neq 0$ for some $f \in D(\tau)$ . "l.c. at $b$ " is analogous.

Hypotheses. Functions $v, w : \mathbb{R} \to \mathbb{C}$ such that:

If $L$ is l.c. at $a$ : $v \in D(\tau)$ , $W_a(\bar v, v) = 0$ , and $W_a(v, f) \neq 0$ for some $f \in D(\tau)$ .
If $L$ is l.c. at $b$ : $w \in D(\tau)$ , $W_b(\bar w, w) = 0$ , and $W_b(w, f) \neq 0$ for some $f \in D(\tau)$ .

Claim. There exists a linear operator $A$ on $L^2$ , defined on a subspace, with the following properties:

Its graph equals the set of pairs $([f], [g])$ $([f], [g])$ with $f, g \in L^2(\mu)$ $f, g \in L^{2} (μ)$ and $\tau f = g$ $τ f = g$ , where $f$ $f$ satisfies:
- $f \in D(\tau)$ ;
- $W_a(v, f) = 0$ if l.c. at $a$ ;
- $W_b(w, f) = 0$ if l.c. at $b$ .
$A$ is self-adjoint: $A$ equals its adjoint $A^*$ . (Mathlib's adjoint of an operator whose domain is not dense is the zero map on the adjoint domain.)
There exists a further linear operator $A_1$ $A_{1}$ on $L^2$ $L^{2}$ with the following two properties.
- Its graph equals the set of pairs $([f], [g])$ $([f], [g])$ with $f, g \in L^2(\mu)$ $f, g \in L^{2} (μ)$ and $\tau f = g$ $τ f = g$ , where $f \in D(\tau)$ $f \in D (τ)$ and, in addition:
  - if l.c. at $a$ , there is $x_0 \in I$ with $W_x(v, f) = 0$ for all $x \in I$ with $x < x_0$ ;
  - if l.c. at $b$ , there is $x_1 \in I$ with $W_x(w, f) = 0$ for all $x \in I$ with $x > x_1$ .
- The closure of $A_1$ equals $A$ . Mathlib's closure of a non-closable operator is the operator itself, so in that case the requirement reads $A_1 = A$ .

Degenerate cases.

If $L$ is l.c. at neither endpoint, the hypotheses are vacuous and $v, w$ are arbitrary. The domain conditions then reduce to $f \in D(\tau)$ , and both graphs are those of $\tau$ on $D(\tau)$ .
Part of the claim is that these sets of pairs are graphs of linear operators at all.

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