Prove2Me

Lemma 9.2 — variation of constants

Proved
TeschlQM.SturmLiouville.variation_of_constants

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

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

Let (a,b,p,q,r)(a,b,p,q,r) be Sturm–Liouville data, z∈Cz \in \mathbb{C}, and gg with rg∈Lloc1(I)rg \in L^1_{loc}(I). Suppose u1,u2u_1, u_2 are solutions of (τ−z)u=0(\tau - z)u = 0 with W(u1,u2)=1W(u_1, u_2) = 1, and fix c∈Ic \in I. Then every solution ff of (τ−z)f=g(\tau - z) f = g can be written, for some α,β∈C\alpha, \beta \in \mathbb{C} and all x∈Ix \in I, as

f(x)=u1(x)(α+∫cxu2g r dy)+u2(x)(β−∫cxu1g r dy),f(x) = u_1(x)\Big(\alpha + \int_c^x u_2 g\, r\,dy\Big) + u_2(x)\Big(\beta - \int_c^x u_1 g\, r\,dy\Big), (pf′)(x)=(pu1′)(x)(α+∫cxu2g r dy)+(pu2′)(x)(β−∫cxu1g r dy).(pf')(x) = (pu_1')(x)\Big(\alpha + \int_c^x u_2 g\, r\,dy\Big) + (pu_2')(x)\Big(\beta - \int_c^x u_1 g\, r\,dy\Big).

The formula expresses solutions of the inhomogeneous equation through a fundamental system, and underlies the Green function of Lemma 9.7.

Formalization Note. The book states the second line for f′f'; here it is stated for the quasi-derivatives (the book's line multiplied by pp), which holds at every point of II. W(u1,u2)=1W(u_1,u_2) = 1 is stated as Wx(u1,u2)=1W_x(u_1,u_2) = 1 for all x∈Ix \in I (the Wronskian of two solutions is constant, (9.6)).

Preamble
import Mathlib
import Definitions.Def_TeschlQM_SturmLiouville_SolvesTau
import Definitions.Def_TeschlQM_SturmLiouville_wronskian
Formal statement
namespace TeschlQM.SturmLiouville

open MeasureTheory

/-- Teschl, Lemma 9.2, p. 183. Let `u₁, u₂` solve `(τ − z) u = 0` with `W(u₁, u₂) = 1`. Then every
solution `f` of `(τ − z) f = g` (9.8), `r g ∈ L¹_loc(I)`, has the form (9.10) for some
`α, β ∈ ℂ`. The second line of (9.10), stated in the book for `f′`, is stated here for the
quasi-derivatives `p f′`, `p u₁′`, `p u₂′` (the book's line multiplied by `p > 0`), which holds at
every point of `I`. -/
theorem variation_of_constants (L : SLData) (z : ℂ) (g : ℝ → ℂ)
    (hg : LocallyIntegrableOn (fun x => (L.r x : ℂ) * g x) L.I)
    (u₁ u₂ : ℝ → ℂ) (h₁ : IsSolution L z 0 u₁) (h₂ : IsSolution L z 0 u₂)
    (hW : ∀ x ∈ L.I, wronskian L x u₁ u₂ = 1)
    (c : ℝ) (hc : c ∈ L.I) (f : ℝ → ℂ) (hf : IsSolution L z g f) :
    ∃ α β : ℂ, ∀ x ∈ L.I,
      f x = u₁ x * (α + ∫ y in c..x, u₂ y * g y * (L.r y : ℂ)) +
        u₂ x * (β - ∫ y in c..x, u₁ y * g y * (L.r y : ℂ)) ∧
      quasiDeriv L f x = quasiDeriv L u₁ x * (α + ∫ y in c..x, u₂ y * g y * (L.r y : ℂ)) +
        quasiDeriv L u₂ x * (β - ∫ y in c..x, u₁ y * g y * (L.r y : ℂ)) := by sorry

end TeschlQM.SturmLiouville
Source
Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 183, Lemma 9.2, Eq. (9.10)
Read-back

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

Setting. Fix LL with interval II, coefficients p,q,rp, q, r, and z∈Cz \in \mathbb{C}. The notions used are:

  • f[1]f^{[1]}: the chosen quasi-derivative of ff, or 00 if none exists.
  • Wx(f1,f2)=f1(x)f2[1](x)−f1[1](x)f2(x)W_x(f_1, f_2) = f_1(x) f_2^{[1]}(x) - f_1^{[1]}(x) f_2(x).
  • "ff solves (τ−z)f=h(\tau - z) f = h": ff has a quasi-derivative, qf−r(zf+h)q f - r(z f + h) is locally integrable on II, and f[1](y)−f[1](x)=∫xy(qf−r(zf+h))f^{[1]}(y) - f^{[1]}(x) = \int_x^y (q f - r(z f + h)) for x,y∈Ix, y \in I.

Hypotheses.

  • g:R→Cg : \mathbb{R} \to \mathbb{C} with rgr g locally integrable on II.
  • u1,u2:R→Cu_1, u_2 : \mathbb{R} \to \mathbb{C} both solve (τ−z)u=0(\tau - z) u = 0.
  • Wx(u1,u2)=1W_x(u_1, u_2) = 1 for every x∈Ix \in I.
  • c∈Ic \in I.
  • ff solves (τ−z)f=g(\tau - z) f = g.

Claim. There exist α,β∈C\alpha, \beta \in \mathbb{C} such that for every x∈Ix \in I both of the following hold:

f(x)=u1(x)(α+∫cxu2(y)g(y)r(y) dy)+u2(x)(β−∫cxu1(y)g(y)r(y) dy),f(x) = u_1(x)\Bigl(\alpha + \int_c^x u_2(y) g(y) r(y)\,dy\Bigr) + u_2(x)\Bigl(\beta - \int_c^x u_1(y) g(y) r(y)\,dy\Bigr), f[1](x)=u1[1](x)(α+∫cxu2gr dy)+u2[1](x)(β−∫cxu1gr dy).f^{[1]}(x) = u_1^{[1]}(x)\Bigl(\alpha + \int_c^x u_2 g r\,dy\Bigr) + u_2^{[1]}(x)\Bigl(\beta - \int_c^x u_1 g r\,dy\Bigr).

The integrals are oriented, so for x<cx < c they are minus the integral over [x,c][x, c]. By convention they are 00 if the integrand is not integrable on the segment.

Degenerate cases.

  • The same α,β\alpha, \beta serve for all x∈Ix \in I and for both equations.
  • Nothing is asserted outside II.
  • No square-integrability is assumed for u1u_1, u2u_2, ff or gg.
  • If no pair u1,u2u_1, u_2 with Wronskian identically 11 on II exists for the given zz, the statement is vacuous. The code does not settle whether such a pair exists.
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