Entries of a fundamental solution of a smooth loop are smooth

Proved

FiniteEnergyPlane.contDiff_apply_of_isFundamentalSolution

by Mazecto · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

symplectic-geometry

Let $S_\infty$ be a loop of matrices with smooth entries and $\Psi$ its fundamental solution, $\Psi(0) = I$ , $\Psi' = J_0 S_\infty \Psi$ . Then every entry of $\Psi$ is smooth.

Role. This gives the regularity needed to apply statements about smooth symplectic paths to fundamental solutions.

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

open scoped ContDiff

/-- The entries of the fundamental solution of a loop with smooth entries are smooth. -/
theorem contDiff_apply_of_isFundamentalSolution (Sinf : ℝ → CauchyRiemannIndex.Mat 1)
    (hS : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j))
    (Ψ : ℝ → CauchyRiemannIndex.Mat 1) (hΨ : CauchyRiemannIndex.IsFundamentalSolution Sinf Ψ) :
    ∀ i j, ContDiff ℝ ∞ (fun t => Ψ t i j) := by
  sorry

end FiniteEnergyPlane

Source

Standard regularity for linear ordinary differential equations

View graph