Prove2Me

Existence and uniqueness of the fundamental solution of Ψ′=J0SΨ\Psi'=J_0S\Psi

Proved
CauchyRiemannIndex.fundamentalSolution_existsUnique

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

cauchy-riemannconley-zehnder-indexsymplectic-geometry

Let n≥0n\ge0, let J0=(0−IdId0)∈R2n×2nJ_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}\in\mathbb R^{2n\times2n}, and let S:R→R2n×2nS:\mathbb R\to\mathbb R^{2n\times2n} be continuous. Then there is exactly one map Ψ:R→R2n×2n\Psi:\mathbb R\to\mathbb R^{2n\times2n} such that

Ψ(0)=Id,Ψ′(t)=J0S(t)Ψ(t)for all t∈R.\Psi(0)=\mathrm{Id},\qquad \Psi'(t)=J_0S(t)\Psi(t)\quad\text{for all }t\in\mathbb R.

This is the fundamental solution through which nondegeneracy and the Conley–Zehnder index of the asymptotic operator −J0∂t−S-J_0\partial_t-S are defined (Wendl, Lecture 3, §3.4).

Formalization Note. R2n×2n\mathbb R^{2n\times2n} is Mat n (real matrices indexed by Fin n ⊕ Fin n) and J0=(0−IdId0)J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix} is Matrix.J. The two conditions are IsFundamentalSolution S Ψ (with HasDerivAt at every real tt). SS is only assumed continuous: neither periodicity nor symmetry is required.

Preamble
import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
Formal statement
namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

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

end CauchyRiemannIndex
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 3, §3.4, pp. 61-62 (Definition 3.30, Theorem 3.34), trivial bundle

View graph