Theorem 9.1 — existence and uniqueness for the initial value problem

Proved

TeschlQM.SturmLiouville.ivp_exists_unique

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

existence-uniquenessordinary-differential-equationsp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1sturm-liouville

Let $(a,b,p,q,r)$ be Sturm–Liouville data, and let $g$ be a function with $rg \in L^1_{loc}(I)$ . Fix $c \in I$ and $\alpha, \beta \in \mathbb{C}$ . Then for every $z \in \mathbb{C}$ there is a unique solution $f = f_z$ with $f, pf' \in AC_{loc}(I)$ of

(\tau - z) f = g, \qquad f(c) = \alpha,\quad (pf')(c) = \beta,

and for every $x \in I$ the map $z \mapsto f_z(x)$ is entire.

This is the basic existence theorem for Sturm–Liouville equations with merely locally integrable coefficients, where the classical Picard–Lindelöf theorem does not apply.

Formalization Note. The solutions form a family $F(z, \cdot)$ . Uniqueness is stated on $I$ (values outside $I$ are irrelevant); since the quasi-derivative is determined by $f$ on $I$ , it covers the pair $(f, pf')$ .

Preamble

import Mathlib
import Definitions.Def_TeschlQM_SturmLiouville_SolvesTau

Formal statement

namespace TeschlQM.SturmLiouville

open MeasureTheory

/-- Teschl, Theorem 9.1, p. 182. Suppose `r g ∈ L¹_loc(I)`. Then for every `z ∈ ℂ` there is a
unique solution `f, p f′ ∈ AC_loc(I)` of `(τ − z) f = g` (9.8) with `f(c) = α`, `(p f′)(c) = β`
(9.9), and `f` is entire in `z`. The solutions are given as a family `F z`; uniqueness is on `I`
(values outside `I` are irrelevant), and uniqueness of `p f′` on `I` follows from that of `f`. -/
theorem ivp_exists_unique (L : SLData) (g : ℝ → ℂ)
    (hg : LocallyIntegrableOn (fun x => (L.r x : ℂ) * g x) L.I)
    (c : ℝ) (hc : c ∈ L.I) (α β : ℂ) :
    ∃ F : ℂ → ℝ → ℂ,
      (∀ z : ℂ, IsSolution L z g (F z) ∧ F z c = α ∧ quasiDeriv L (F z) c = β) ∧
      (∀ (z : ℂ) (f : ℝ → ℂ), IsSolution L z g f → f c = α → quasiDeriv L f c = β →
        ∀ x ∈ L.I, f x = F z x) ∧
      (∀ x ∈ L.I, Differentiable ℂ (fun z => F z x)) := by sorry

end TeschlQM.SturmLiouville

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 182, Theorem 9.1

Read-back

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

Setting. Fix $L$ with interval $I = (a, b)$ and coefficients $p, q, r$ ( $p, r > 0$ on $I$ ; $1/p$ , $q$ , $r$ locally integrable on $I$ ). Also let:

$g : \mathbb{R} \to \mathbb{C}$ be such that $r g$ is locally integrable on $I$ ;
$c \in I$ ;
$\alpha, \beta \in \mathbb{C}$ .

" $f$ solves $(\tau - z) f = g$ " means: $f$ has a quasi-derivative, whose chosen value is $f^{[1]}$ (with $f^{[1]}$ an integral of a locally integrable function on $I$ , $f^{[1]}/p$ locally integrable on $I$ , and $f(y) - f(x) = \int_x^y f^{[1]}/p$ on $I$ ). In addition, $q f - r(z f + g)$ is locally integrable on $I$ and

f^{[1]}(y) - f^{[1]}(x) = \int_x^y \bigl(q f - r(z f + g)\bigr)\,dt \quad \text{for } x, y \in I .

Claim. There exists a family $F : \mathbb{C} \to (\mathbb{R} \to \mathbb{C})$ , $z \mapsto F_z$ , with three properties:

Existence. For every $z \in \mathbb{C}$ , $F_z$ solves $(\tau - z) F_z = g$ , and

F_z(c) = \alpha, \qquad F_z^{[1]}(c) = \beta .

Uniqueness. For every $z \in \mathbb{C}$ and every $f$ that solves $(\tau - z) f = g$ with $f(c) = \alpha$ and $f^{[1]}(c) = \beta$ , we have $f(x) = F_z(x)$ for all $x \in I$ .
Analyticity. For every $x \in I$ , the map $z \mapsto F_z(x)$ is complex-differentiable at every point of $\mathbb{C}$ .

Degenerate cases.

Uniqueness concerns only the values of $f$ on $I$ . It says nothing about $f^{[1]}$ and nothing outside $I$ .
$F_z^{[1]}(c)$ refers to the chosen quasi-derivative witness.
$g = 0$ and $\alpha = \beta = 0$ are allowed.
No square-integrability of $g$ or $F_z$ is assumed or asserted.
No differentiability in $z$ is asserted for $x \notin I$ .

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