Eq. (9.7) — Lagrange identity on $\mathfrak{D}(\tau)$

Proved

TeschlQM.SturmLiouville.lagrange_identity

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

lagrange-identityp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1sturm-liouvillewronskian

Let $(a,b,p,q,r)$ be Sturm–Liouville data and $f, g \in \mathfrak{D}(\tau)$ . Then the boundary Wronskians $W_a(g^*, f) = \lim_{x\to a} W_x(g^*, f)$ and $W_b(g^*, f) = \lim_{x \to b} W_x(g^*, f)$ exist, and

\langle g, \tau f\rangle = W_a(g^*, f) - W_b(g^*, f) + \langle \tau g, f\rangle,

where $\langle u, v\rangle = \int_a^b u(x)^* v(x) r(x)\,dx$ is the inner product of $L^2(I, r\,dx)$ .

The identity shows that $\tau$ on $\mathfrak{D}(\tau)$ fails to be symmetric exactly by boundary terms, which is why self-adjoint realizations are described by conditions on $W_a$ and $W_b$ .

Formalization Note. $\tau f$ and $\tau g$ are given as functions $F, G \in L^2(I, r\,dx)$ with $\tau f = F$ , $\tau g = G$ . Existence of the limits is stated as convergence of $W_x$ to $W_a$ (resp. $W_b$ ) as defined via limUnder. The two integrands are asserted to be integrable, so both sides are genuine inner products. The book prints the boundary term as $W_b(g^*, f) - W_a(g^*, f)$ , which has the wrong sign for the Wronskian (9.5): on $(0,1)$ with $p = r = 1$ , $q = 0$ , $f = x^2$ , $g = 1$ the left side is $-2$ and $W_1 - W_0 = 2$ . The corrected sign is stated.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_SturmLiouville_maxDomain
import Definitions.Def_TeschlQM_SturmLiouville_wronskian

Formal statement

namespace TeschlQM.SturmLiouville

open MeasureTheory Filter Topology

/-- Teschl, Eq. (9.7), p. 182. For `f, g ∈ D(τ)` (with `τ f = F`, `τ g = G`) the limits
`W_a(g*, f) = lim_{x→a} W_x(g*, f)` and `W_b(g*, f) = lim_{x→b} W_x(g*, f)` exist, and
`⟨g, τ f⟩ = W_a(g*, f) − W_b(g*, f) + ⟨τ g, f⟩`, where `⟨u, v⟩ = ∫_a^b u(x)* v(x) r(x) dx` (9.2).
The two integrands are integrable (as products of `L²(I, r dx)` functions), so both sides are the
book's inner products.
**Sign correction.** The page prints `W_b(g*, f) − W_a(g*, f)` (and `W_d − W_c` in (9.4)). With the
Wronskian (9.5), `W_x(f₁, f₂) = f₁ (p f₂′) − (p f₁′) f₂`, integration by parts gives the opposite
sign: on `(0, 1)` with `p = r = 1`, `q = 0`, `f = x²`, `g = 1` one has `⟨g, τ f⟩ = −2`,
`W_1(g*, f) − W_0(g*, f) = 2`, `⟨τ g, f⟩ = 0`. The corrected identity is stated. -/
theorem lagrange_identity (L : SLData) (f g F G : ℝ → ℂ)
    (hf : MemLp f 2 L.measure) (hg : MemLp g 2 L.measure)
    (hF : SolvesTau L f F) (hG : SolvesTau L g G)
    (hF2 : MemLp F 2 L.measure) (hG2 : MemLp G 2 L.measure) :
    Tendsto (fun x => wronskian L x (fun y => starRingEnd ℂ (g y)) f) L.atLeft
        (𝓝 (wronskianLeft L (fun y => starRingEnd ℂ (g y)) f)) ∧
      Tendsto (fun x => wronskian L x (fun y => starRingEnd ℂ (g y)) f) L.atRight
        (𝓝 (wronskianRight L (fun y => starRingEnd ℂ (g y)) f)) ∧
      Integrable (fun x => starRingEnd ℂ (g x) * F x) L.measure ∧
      Integrable (fun x => starRingEnd ℂ (G x) * f x) L.measure ∧
      ∫ x, starRingEnd ℂ (g x) * F x ∂L.measure =
        wronskianLeft L (fun y => starRingEnd ℂ (g y)) f -
          wronskianRight L (fun y => starRingEnd ℂ (g y)) f +
          ∫ x, starRingEnd ℂ (G x) * f x ∂L.measure := by sorry

end TeschlQM.SturmLiouville

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 182, Section 9.1, Eq. (9.7)

Read-back

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

Data. The statement is about:

a structure $L$ of type SLData, which is imported and not shown here;
four complex-valued functions on the whole real line, $f, g, F, G : \mathbb{R} \to \mathbb{C}$ .

It uses several objects built from $L$ in the imported files. Their definitions are not included with this declaration, so they are described below only by their names and how they are used:

a measure $\mu_L$ on $\mathbb{R}$ (L.measure);
two filters on $\mathbb{R}$ , $\mathcal{F}^{\mathrm{left}}_L$ and $\mathcal{F}^{\mathrm{right}}_L$ (L.atLeft, L.atRight). The names suggest approach to the left and right endpoints of some interval, but this is not confirmed here;
a relation $\mathrm{SolvesTau}_L(u, U)$ between two functions;
a complex number $W_x(u, v)$ for each point $x$ and pair of functions $u, v$ (wronskian L x u v);
two complex numbers $W^{\mathrm{left}}(u, v)$ and $W^{\mathrm{right}}(u, v)$ for each pair of functions (wronskianLeft, wronskianRight).

The doc-comment says these are the Sturm–Liouville measure $r\,dx$ , the endpoint limits, the equation $\tau u = U$ and the Wronskian. That is the author's description, not something the code shows. Write $\bar g$ for the pointwise complex conjugate $x \mapsto \overline{g(x)}$ .

Hypotheses. Assume all of the following:

$f$ is in $L^2(\mu_L)$ : it is a.e.-strongly measurable and $\int |f|^2\,d\mu_L < \infty$ .
$g$ is in $L^2(\mu_L)$ .
$F$ is in $L^2(\mu_L)$ .
$G$ is in $L^2(\mu_L)$ .
$\mathrm{SolvesTau}_L(f, F)$ holds.
$\mathrm{SolvesTau}_L(g, G)$ holds.

Conclusion. Under these hypotheses, all five of the following hold at once:

$W_x(\bar g, f) \to W^{\mathrm{left}}(\bar g, f)$ as $x$ runs along the filter $\mathcal{F}^{\mathrm{left}}_L$ .
$W_x(\bar g, f) \to W^{\mathrm{right}}(\bar g, f)$ as $x$ runs along the filter $\mathcal{F}^{\mathrm{right}}_L$ .
The function $x \mapsto \overline{g(x)}\,F(x)$ is Lebesgue (Bochner) integrable with respect to $\mu_L$ .
The function $x \mapsto \overline{G(x)}\,f(x)$ is integrable with respect to $\mu_L$ .
The following identity holds:

\int \overline{g(x)}\,F(x)\,d\mu_L(x) \;=\; W^{\mathrm{left}}(\bar g, f) \;-\; W^{\mathrm{right}}(\bar g, f) \;+\; \int \overline{G(x)}\,f(x)\,d\mu_L(x).

Both integrals are over all of $\mathbb{R}$ with respect to $\mu_L$ . The sign is fixed: the left-endpoint quantity is added and the right-endpoint quantity is subtracted.

The statement does not say how $W^{\mathrm{left}}$ and $W^{\mathrm{right}}$ are defined. They might be defined as limits, or by some other rule. Conclusions 1 and 2 are what claim that the pointwise Wronskians actually converge to them.

The statement also does not require $F$ or $G$ to be unique. It holds for every pair that satisfies $\mathrm{SolvesTau}_L$ together with the $L^2$ conditions.

Degenerate cases.

Integrals. Conclusions 3 and 4 assert integrability. So in conclusion 5, Lean's convention of assigning the integral $0$ to a non-integrable function is never what the identity relies on.
Zero measure. If $\mu_L$ is the zero measure, all four $L^2$ hypotheses hold trivially and both integrals equal $0$ . The identity then says $W^{\mathrm{left}}(\bar g, f) = W^{\mathrm{right}}(\bar g, f)$ , provided the $\mathrm{SolvesTau}_L$ hypotheses can still be satisfied.
Trivial filters. If $\mathcal{F}^{\mathrm{left}}_L$ or $\mathcal{F}^{\mathrm{right}}_L$ is the trivial (bottom) filter, for example because the underlying interval is empty, then conclusion 1 or 2 holds automatically and says nothing.
Behaviour outside the interval. The functions are defined on all of $\mathbb{R}$ . Their values outside the support of $\mu_L$ , and outside whatever set the filters and $\mathrm{SolvesTau}_L$ look at, have no effect on the integrals.
Unsatisfiable hypotheses. If $\mathrm{SolvesTau}_L$ can never be satisfied together with the $L^2$ conditions for a given $L$ , the theorem is vacuous for that $L$ . The definitions needed to decide this are not included in the code shown.

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

Eq. (9.7) — Lagrange identity on D(τ)\mathfrak{D}(\tau)D(τ)

Eq. (9.7) — Lagrange identity on $\mathfrak{D}(\tau)$