Lemma 9.7 — the resolvent as an integral operator with Green function

Proved

TeschlQM.SturmLiouville.resolvent_green

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

green-functionp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1resolventsturm-liouville

Let $(a,b,p,q,r)$ be Sturm–Liouville data, let $v, w$ be as in Theorem 9.6, and let $A$ be the self-adjoint operator of Theorem 9.6. Suppose $z \in \rho(A)$ . Then there is a solution $u_a(z,x)$ of $(\tau - z)u = 0$ which is in $L^2((a,c), r\,dx)$ and satisfies the boundary condition $W_a(v, u_a) = 0$ at $a$ if $\tau$ is l.c. at $a$ ; similarly there is a solution $u_b(z, x)$ with the analogous properties near $b$ . Their Wronskian $W(u_b(z), u_a(z))$ is a nonzero constant, and for all $g \in L^2(I, r\,dx)$

(A - z)^{-1} g(x) = \int_a^b G(z, x, y) g(y) r(y)\,dy, \qquad G(z,x,y) = \frac{1}{W(u_b(z), u_a(z))}\begin{cases} u_b(z,x) u_a(z,y), & x \ge y,\\ u_a(z,x) u_b(z,y), & x \le y.\end{cases}

The Green function is the basic tool for the spectral analysis of Sturm–Liouville operators, and its solutions $u_a$ , $u_b$ are used in the proof of Weyl's alternative.

Formalization Note. The lemma as printed says "a solution $u_a(z,x)$ of $(\tau - z)u = g$ "; the proof and (9.28) require $(\tau - z) u = 0$ , which is what is stated. The boundary condition is stated as $W_x(v, u_a) \to 0$ as $x \to a$ . The resolvent is a bounded $R$ with IsResolventAt A z R, and the identity holds for almost every $x$ , with the integrand integrable for almost every $x$ .

Preamble

import Mathlib
import Definitions.Def_TeschlQM_SturmLiouville_operatorGraph
import Definitions.Def_TeschlQM_SturmLiouville_IsResolventAt
import Definitions.Def_TeschlQM_SturmLiouville_IsSqIntegrableNear

Formal statement

namespace TeschlQM.SturmLiouville

open MeasureTheory Filter Topology

/-- Teschl, Lemma 9.7, p. 188. Let `A` be the self-adjoint operator of Theorem 9.6 (graph (9.19),
domain (9.20)) and `z ∈ ρ(A)` with resolvent `R = (A − z)⁻¹`. Then there is a solution `u_a` of
`(τ − z) u = 0` that is in `L²((a, c), r dx)` and satisfies the boundary condition at `a`
(`W_a(v, u_a) = 0`) if `τ` is l.c. at `a`, and similarly `u_b` near `b`; `W(u_b, u_a)` is a nonzero
constant, and `(A − z)⁻¹ g (x) = ∫_a^b G(z, x, y) g(y) r(y) dy` (9.27) with the Green function (9.28).
The printed equation "`(τ − z) u = g`" in the lemma is read as `(τ − z) u = 0`, as the proof and
(9.28) require. The integral is `∫ … ∂(r dx)` over `I`; its integrand is stated to be integrable. -/
theorem resolvent_green (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)
    (hA : (A.graph : Set (Lp ℂ 2 L.measure × Lp ℂ 2 L.measure)) =
      operatorGraph L (bcDomain L v w))
    (z : ℂ) (R : Lp ℂ 2 L.measure →L[ℂ] Lp ℂ 2 L.measure) (hR : IsResolventAt A z R) :
    ∃ ua ub : ℝ → ℂ,
      IsSolution L z 0 ua ∧ IsSqIntegrableNearLeft L ua ∧
        (IsLimitCircleLeft L → Tendsto (fun x => wronskian L x v ua) L.atLeft (𝓝 0)) ∧
      IsSolution L z 0 ub ∧ IsSqIntegrableNearRight L ub ∧
        (IsLimitCircleRight L → Tendsto (fun x => wronskian L x w ub) L.atRight (𝓝 0)) ∧
      ∃ W₀ : ℂ, W₀ ≠ 0 ∧ (∀ x ∈ L.I, wronskian L x ub ua = W₀) ∧
        ∀ g : Lp ℂ 2 L.measure,
          (∀ᵐ x ∂L.measure, Integrable
            (fun y => (if y ≤ x then ub x * ua y else ua x * ub y) / W₀ * g y) L.measure) ∧
          (R g : ℝ → ℂ) =ᵐ[L.measure]
            fun x => ∫ y, (if y ≤ x then ub x * ua y else ua x * ub y) / W₀ * g y ∂L.measure := by sorry

end TeschlQM.SturmLiouville

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 188, Lemma 9.7, Eqs. (9.27)–(9.28)

Read-back

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

Setting. Fix $L$ with interval $I = (a, b)$ , $\mu = r\,dx$ on $I$ , and $L^2 = L^2(\mu)$ . The notions used are:

$D(\tau)$ : the maximal domain.
$h^{[1]}$ : the chosen quasi-derivative of $h$ .
$W_x(f_1, f_2) = f_1(x) f_2^{[1]}(x) - f_1^{[1]}(x) f_2(x)$ .
$W_a$ , $W_b$ : the boundary limits of $W_x$ (an unspecified value when the limit does not exist).
"l.c. at $a$ / $b$ ": the limit-circle properties.
" $u$ solves $(\tau - z) u = 0$ ": $u$ has a quasi-derivative, $q u - r z u$ is locally integrable on $I$ , and $u^{[1]}(y) - u^{[1]}(x) = \int_x^y (q - r z) u$ on $I$ .

Hypotheses.

$v, w : \mathbb{R} \to \mathbb{C}$ $v, w : R \to C$ with:
- if 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.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)$ .
$A$ is a linear operator on $L^2$ , defined on a subspace, whose graph is the set of pairs $([f], [g])$ with $f, g \in L^2(\mu)$ , $\tau f = g$ , $f \in D(\tau)$ , $W_a(v, f) = 0$ if l.c. at $a$ , and $W_b(w, f) = 0$ if l.c. at $b$ . Self-adjointness of $A$ is not assumed.
$z \in \mathbb{C}$ .
$R$ $R$ is a bounded linear operator on $L^2$ $L^{2}$ such that:
- for every $\varphi$ , $R\varphi \in \mathfrak{D}(A)$ and $(A - z) R\varphi = \varphi$ ;
- for every $\psi \in \mathfrak{D}(A)$ , $R(A - z)\psi = \psi$ .

Claim. There exist functions $u_a, u_b : \mathbb{R} \to \mathbb{C}$ with the following properties.

Conditions on $u_a$ :

$u_a$ solves $(\tau - z) u = 0$ .
$\int_a^c |u_a|^2 r\,dx < \infty$ for some $c \in I$ (with $u_a$ a.e. strongly measurable there).
If l.c. at $a$ , then $W_x(v, u_a) \to 0$ as $x \to a$ inside $I$ .

Conditions on $u_b$ :

$u_b$ solves $(\tau - z) u = 0$ .
$\int_{c'}^b |u_b|^2 r\,dx < \infty$ for some $c' \in I$ .
If l.c. at $b$ , then $W_x(w, u_b) \to 0$ as $x \to b$ inside $I$ .

In addition, there is $W_0 \in \mathbb{C}$ with $W_0 \neq 0$ and $W_x(u_b, u_a) = W_0$ for every $x \in I$ . With

G(x, y) = \frac{1}{W_0}\begin{cases} u_b(x)\, u_a(y), & y \le x,\\ u_a(x)\, u_b(y), & y > x,\end{cases}

every $g \in L^2$ (identified with a fixed representative function) satisfies both of the following:

For $\mu$ -almost every $x$ , the function $y \mapsto G(x, y)\, g(y)$ is $\mu$ -integrable.
For $\mu$ -almost every $x$ ,

(R g)(x) = \int_I G(x, y)\, g(y)\, r(y)\,dy,

where $Rg$ also denotes a representative function.

Degenerate cases.

If no linear operator has the stated graph, or no such $R$ exists for this $z$ , the statement is vacuous. Nothing restricts $z$ to be non-real.
If $L$ is l.c. at neither endpoint, $v, w$ are arbitrary and the boundary conditions on $u_a, u_b$ are absent.
The boundary conditions are stated as convergence of $W_x$ to $0$ , not through the boundary-value definitions $W_a$ , $W_b$ .
The Green-function identity is asserted only $\mu$ -almost everywhere. Because integrability is asserted in item 1, the convention that non-integrable integrals are $0$ matters only on a $\mu$ -null set of $x$ .

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