Lemma 3.11 — Liouville's formula (Abel's identity) for the Wronski determinant

Proved

TeschlODE.Linear.liouville_formula

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

linear-systemsliouville-formulaordinary-differential-equationsp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1wronskian

Let $I$ be an interval, $A \in C(I, \mathbb{R}^{n\times n})$ , and let $U(t) = (\varphi_1(t), \dots, \varphi_n(t))$ be a matrix whose columns are solutions of $\dot x = A(t)x$ on $I$ . Then the Wronski determinant $W(t) = \det U(t)$ satisfies

W(t) = W(t_0)\,\exp\Big(\int_{t_0}^{t} \operatorname{tr}(A(s))\,ds\Big), \qquad t_0, t \in I. \qquad (3.91)

In particular $\det U(t) \neq 0$ at one point of $I$ implies it at every point, and for periodic $A$ the determinant of the monodromy matrix is $\exp\big(\int_0^T \operatorname{tr} A\big) > 0$ (3.122), which is what makes a matrix logarithm of it available in Floquet's theorem.

Formalization Note. The book writes $U$ with the solutions as columns ("using the solutions as columns", (3.81)); the Lean hypothesis is that each column fun t i => U t i j is an IsSolution A I. The integral is the interval integral ∫ s in t₀..t, which is oriented (so $t < t_0$ is allowed) and is a genuine integral because $\operatorname{tr} A$ is continuous on $[t_0,t] \subseteq I$ .

Preamble

import Mathlib
import Definitions.Def_TeschlODE_Linear_IsSolution

Formal statement

namespace TeschlODE.Linear

/-- Teschl, Lemma 3.11 (p. 83), Abel's identity / Liouville's formula (3.91): if the columns of
`U(t)` are `n` solutions of (3.79) on the interval `I`, the Wronski determinant
`W(t) = det U(t)` satisfies `W(t) = W(t₀) exp (∫_{t₀}^{t} tr A(s) ds)` for all `t₀, t ∈ I`. -/
theorem liouville_formula {n : ℕ} (A : ℝ → Matrix (Fin n) (Fin n) ℝ) (I : Set ℝ)
    (hI : I.OrdConnected) (hA : ContinuousOn A I) (U : ℝ → Matrix (Fin n) (Fin n) ℝ)
    (hU : ∀ j : Fin n, IsSolution A I (fun t i => U t i j)) (t₀ t : ℝ) (ht₀ : t₀ ∈ I)
    (ht : t ∈ I) :
    (U t).det = (U t₀).det * Real.exp (∫ s in t₀..t, (A s).trace) := by sorry

end TeschlODE.Linear

Source

Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012), p. 83, Lemma 3.11

Read-back

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

Setting. Let $n \in \mathbb{N}$ , let $A : \mathbb{R} \to \mathbb{R}^{n\times n}$ , and let $I \subseteq \mathbb{R}$ . The theorem assumes:

$I$ is order-connected (an interval of any kind);
$A$ is continuous on $I$ ;
$U : \mathbb{R} \to \mathbb{R}^{n\times n}$ is a matrix-valued function whose every column is a solution on $I$ . For each column index $j$ , the vector function

t \mapsto \bigl(U(t)_{1j}, \dots, U(t)_{nj}\bigr)

has, at every $t \in I$ , derivative $A(t)$ times that column relative to $I$ . (Limits are taken only along points of $I$ , so the derivative is one-sided at an endpoint in $I$ .)

$t_0$ and $t$ are two points of $I$ .

Claim.

\det U(t) = \det U(t_0)\cdot \exp\!\left(\int_{t_0}^{t} \operatorname{tr} A(s)\,ds\right).

Here $\operatorname{tr}$ is the sum of the diagonal entries. The integral is the oriented Lebesgue integral: over $(t_0, t]$ if $t_0 \le t$ , and minus the integral over $(t, t_0]$ if $t < t_0$ . Because $I$ is order-connected, the segment between $t_0$ and $t$ lies in $I$ , where $A$ is continuous. No linear independence of the columns of $U$ is assumed; $\det U$ may be zero.

Degenerate cases.

$t = t_0$ : the integral is $0$ , and the claim reads $\det U(t_0) = \det U(t_0)$ .
$I$ a single point: only $t = t_0$ is possible.
$n = 0$ : the determinant of the empty matrix is $1$ and its trace is $0$ , so the claim reads $1 = 1\cdot e^0$ .
Non-integrable integrand: if $\operatorname{tr}A$ were not integrable on the segment, the integral would be taken to be $0$ by convention. Under the continuity hypothesis on the compact segment, however, it is integrable.

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