Lemma 9.5 — boundary Wronskian conditions

Proved

TeschlQM.SturmLiouville.wronskian_bc_symmetric

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

p2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1sturm-liouvillewronskian

Let $(a,b,p,q,r)$ be Sturm–Liouville data. Suppose $v \in \mathfrak{D}(\tau)$ with $W_a(v^*, v) = 0$ , and suppose there is an $\hat f \in \mathfrak{D}(\tau)$ with $W_a(v^*, \hat f) \neq 0$ . Then for all $f, g \in \mathfrak{D}(\tau)$ :

$W_a(v, f) = 0 \iff W_a(v, f^*) = 0$ ;
$W_a(v, f) = W_a(v, g) = 0 \implies W_a(g^*, f) = 0$ .

The second statement makes the boundary condition $W_a(v, \cdot) = 0$ symmetric (the boundary term in the Lagrange identity vanishes), which is the first step to self-adjointness in Theorem 9.6.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_SturmLiouville_maxDomain
import Definitions.Def_TeschlQM_SturmLiouville_wronskian

Formal statement

namespace TeschlQM.SturmLiouville

/-- Teschl, Lemma 9.5, p. 186. Let `v ∈ D(τ)` with `W_a(v*, v) = 0`, and let `f̂ ∈ D(τ)` with
`W_a(v*, f̂) ≠ 0`. Then for `f, g ∈ D(τ)`:
`W_a(v, f) = 0 ⇔ W_a(v, f*) = 0` (9.15) and
`W_a(v, f) = W_a(v, g) = 0 ⇒ W_a(g*, f) = 0` (9.16). -/
theorem wronskian_bc_symmetric (L : SLData) (v fhat : ℝ → ℂ) (hv : InMaxDomain L v)
    (hvv : wronskianLeft L (fun x => starRingEnd ℂ (v x)) v = 0)
    (hfhat : InMaxDomain L fhat)
    (hne : wronskianLeft L (fun x => starRingEnd ℂ (v x)) fhat ≠ 0)
    (f g : ℝ → ℂ) (hf : InMaxDomain L f) (hg : InMaxDomain L g) :
    (wronskianLeft L v f = 0 ↔ wronskianLeft L v (fun x => starRingEnd ℂ (f x)) = 0) ∧
      (wronskianLeft L v f = 0 → wronskianLeft L v g = 0 →
        wronskianLeft L (fun x => starRingEnd ℂ (g x)) f = 0) := by sorry

end TeschlQM.SturmLiouville

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 186, Lemma 9.5, Eqs. (9.15)–(9.16)

Read-back

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

Setting. Fix $L$ with interval $I$ . The notions used are:

$D(\tau)$ : the maximal domain, meaning $h \in L^2(I, r\,dx)$ and $\tau h = k$ for some $k \in L^2(I, r\,dx)$ . Here $\tau h = k$ means $h$ has a quasi-derivative $h^{[1]}$ , $q h - r k$ is locally integrable on $I$ , and $h^{[1]}(y) - h^{[1]}(x) = \int_x^y (q h - r k)$ on $I$ .
$W_x(f_1, f_2) = f_1(x) f_2^{[1]}(x) - f_1^{[1]}(x) f_2(x)$ .
$W_a(f_1, f_2)$ : the limit of $W_x(f_1, f_2)$ as $x \to a$ inside $I$ , or an unspecified number if that limit does not exist.
$\bar h$ : the pointwise complex conjugate of $h$ .

Hypotheses.

$v \in D(\tau)$ with $W_a(\bar v, v) = 0$ .
$\hat f \in D(\tau)$ with $W_a(\bar v, \hat f) \neq 0$ . Note that the conjugate $\bar v$ , not $v$ , appears here.
$f, g \in D(\tau)$ .

Claim. Both of the following hold:

$W_a(v, f) = 0$ if and only if $W_a(v, \bar f) = 0$ .
If $W_a(v, f) = 0$ and $W_a(v, g) = 0$ , then $W_a(\bar g, f) = 0$ .

Degenerate cases.

The statement concerns the left endpoint $a$ only. If $a = -\infty$ , the limits are taken as $x \to -\infty$ .
$f = g$ , $f = v$ or $\hat f = f$ are allowed.
Neither the hypotheses nor the claim assert that the limits defining $W_a$ exist. Each " $= 0$ " or " $\neq 0$ " about a non-existent limit is a statement about the unspecified fallback value.

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