Existence and uniqueness of the fundamental solution $\Psi' = J_0 S \Psi$

Proved

AsymptoticOperator.fundamentalSolution_existsUnique

by Mazecto · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptotic-operatorconley-zehnder-indexspectral-theorysymplectic-geometryunbounded-operator

Let $S:S^1\to\mathbb{R}^{2n\times2n}$ be continuous. There is exactly one map $\Psi:\mathbb{R}\to\mathbb{R}^{2n\times2n}$ with $\Psi(0)=\mathrm{Id}$ that is differentiable everywhere with

\Psi'(t)=J_0\,S(t)\,\Psi(t)\qquad(t\in\mathbb{R}),

where $S$ is viewed as a $1$ -periodic function on $\mathbb{R}$ .

Preamble

import Definitions.Def_AsymptoticOperator_Setting

Formal statement

namespace AsymptoticOperator

open ConleyZehnder

/-- Every continuous loop `S` has exactly one fundamental solution `Ψ`:
`Ψ(0) = Id`, `Ψ' = J₀ S Ψ` on `ℝ`. -/
theorem fundamentalSolution_existsUnique {n : ℕ} (S : C(UnitAddCircle, Mat n)) :
    ∃! Ψ : ℝ → Mat n, IsFundamentalSolution S Ψ := by sorry

end AsymptoticOperator

Source

Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, §3.4, p. 61 (informal there)

Read-back

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

Setting. Let $n \ge 0$ be a natural number (the case $n = 0$ is included; then all matrices below are $0 \times 0$ ). Write $\mathrm{Mat}_n$ for the real $2n \times 2n$ matrices, with rows and columns indexed by two disjoint copies of $\{0,\dots,n-1\}$ (a "first block" and a "second block"). Let

J_0 = \begin{pmatrix} 0 & -I_n \\ I_n & 0 \end{pmatrix} \in \mathrm{Mat}_n .

Let $S^1 = \mathbb{R}/\mathbb{Z}$ and let $S : S^1 \to \mathrm{Mat}_n$ be an arbitrary continuous map (continuity with respect to the entrywise topology). No further hypothesis is placed on $S$ : in particular $S(t)$ is not assumed symmetric. For $t \in \mathbb{R}$ , $S(t)$ means $S$ evaluated at the class $t \bmod 1$ , so $t \mapsto S(t)$ is a $1$ -periodic continuous matrix function on $\mathbb{R}$ .

A function $\Psi : \mathbb{R} \to \mathrm{Mat}_n$ (no continuity or other regularity is assumed a priori) is called a fundamental solution of $S$ if

$\Psi(0) = I_{2n}$ , and
for every $t \in \mathbb{R}$ , $\Psi$ is differentiable at $t$ (as a map into $\mathrm{Mat}_n$ with its entrywise/finite-dimensional topology) with derivative

\Psi'(t) = J_0\, S(t)\, \Psi(t)

(matrix products, in this order).

Statement. For every $n$ and every continuous loop $S : \mathbb{R}/\mathbb{Z} \to \mathrm{Mat}_n$ , there exists exactly one function $\Psi : \mathbb{R} \to \mathrm{Mat}_n$ that is a fundamental solution of $S$ in the above sense: some such $\Psi$ exists, and any two such functions are equal at every $t \in \mathbb{R}$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Existence and uniqueness of the fundamental solution Ψ′=J0SΨ\Psi' = J_0 S \PsiΨ′=J0​SΨ

Existence and uniqueness of the fundamental solution $\Psi' = J_0 S \Psi$