From 74fbb84888a6f48ea493e59d5e83ce84de595970 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Fri, 21 Aug 2026 10:26:59 +1000
Subject: [PATCH 1/8] stuff

---
 DynamicalSystems.lean                         |   1 +
 .../Mathlib/Analysis/ODE/ExistUnique.lean     |   1 +
 .../Analysis/ODE/GlobalExistenceBounded.lean  | 126 ++++++++++++++++++
 3 files changed, 128 insertions(+)
 create mode 100644 DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceBounded.lean

diff --git a/DynamicalSystems.lean b/DynamicalSystems.lean
index 831aa85..3e47419 100644
--- a/DynamicalSystems.lean
+++ b/DynamicalSystems.lean
@@ -11,6 +11,7 @@ import DynamicalSystems.Mathlib.Analysis.Calculus
 import DynamicalSystems.Mathlib.Analysis.ODE.Caratheodory
 import DynamicalSystems.Mathlib.Analysis.ODE.ExistUnique
 import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistence
+import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistenceBounded
 import DynamicalSystems.Mathlib.Analysis.ODE.UniformlyLocallyLipschitz
 import DynamicalSystems.Mathlib.Dynamics.Basic
 import DynamicalSystems.Mathlib.Topology.Antitone
diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/ExistUnique.lean b/DynamicalSystems/Mathlib/Analysis/ODE/ExistUnique.lean
index 777b4a0..61dcb2c 100644
--- a/DynamicalSystems/Mathlib/Analysis/ODE/ExistUnique.lean
+++ b/DynamicalSystems/Mathlib/Analysis/ODE/ExistUnique.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.ODE.Basic
 public import Mathlib.Analysis.ODE.Gronwall
 public import Mathlib.Analysis.ODE.PicardLindelof
+public import Mathlib.Analysis.ODE.ExistUnique
 
 /-!
 # Existence and uniqueness of integral curves in normed spaces
diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceBounded.lean b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceBounded.lean
new file mode 100644
index 0000000..263f669
--- /dev/null
+++ b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceBounded.lean
@@ -0,0 +1,126 @@
+module
+
+public import Mathlib.Analysis.ODE.Basic
+import Mathlib.Analysis.ODE.Gronwall
+import Mathlib.Analysis.ODE.PicardLindelof
+import Mathlib.Analysis.ODE.ExistUnique
+
+/-!
+# Global existence for ODEs with a globally Lipschitz, bounded vector field
+
+We prove that a continuous globally Lipschitz vector field admits a global solution.
+This is a direct consequence of the construction of the Picard iteration.
+
+This file was mainly generated by Aristotle AI.
+
+-/
+
+open scoped NNReal
+open Metric Set
+
+/-! ## Global existence -/
+
+section GlobalExistence
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+  {f : ℝ → E → E} {C : ℝ} {K : ℝ≥0}
+
+/-- Local (in fact, on an arbitrarily large compact time interval) existence, from the
+Picard-Lindelöf theorem. -/
+theorem exists_solution_Icc (h_lip : ∀ t, LipschitzWith K (f t))
+    (h_cont : ∀ x, Continuous (f · x)) (h_bdd : ∀ t x, ‖f t x‖ ≤ C)
+    (t₀ : ℝ) (x₀ : E) (R : ℝ) (hR : 0 ≤ R) :
+    ∃ α : ℝ → E, α t₀ = x₀ ∧ ∀ t ∈ Icc (t₀ - R) (t₀ + R),
+      HasDerivWithinAt α (f t (α t)) (Icc (t₀ - R) (t₀ + R)) t := by
+  have hC : 0 ≤ C := le_trans (norm_nonneg _) (h_bdd 0 0)
+  have ht₀ : t₀ ∈ Icc (t₀ - R) (t₀ + R) := ⟨by linarith, by linarith⟩
+  have hpl : IsPicardLindelof f (tmin := t₀ - R) (tmax := t₀ + R) ⟨t₀, ht₀⟩ x₀
+      ⟨C * R, by positivity⟩ 0 ⟨C, hC⟩ K := by
+    refine ⟨fun t _ ↦ (h_lip t).lipschitzOnWith, fun x _ ↦ (h_cont x).continuousOn,
+      fun t _ x _ ↦ h_bdd t x, ?_⟩
+    change (C : ℝ) * max (t₀ + R - t₀) (t₀ - (t₀ - R)) ≤ (C * R : ℝ) - ((0 : ℝ≥0) : ℝ)
+    rw [show t₀ + R - t₀ = R by ring, show t₀ - (t₀ - R) = R by ring, max_self]
+    simp
+  exact hpl.exists_eq_forall_mem_Icc_hasDerivWithinAt₀
+
+omit [CompleteSpace E] in
+/-- Two solutions with the same initial condition agree on any open interval on which
+they are both defined. -/
+public theorem solution_eqOn_Ioo (h_lip : ∀ t, LipschitzWith K (f t))
+    {α β : ℝ → E} {t₀ a b : ℝ} (ht₀ : t₀ ∈ Ioo a b) (hαβ : α t₀ = β t₀)
+    (hα : ∀ t ∈ Ioo a b, HasDerivAt α (f t (α t)) t)
+    (hβ : ∀ t ∈ Ioo a b, HasDerivAt β (f t (β t)) t) :
+    EqOn α β (Ioo a b) :=
+  ODE_solution_unique_of_mem_Ioo (K := K) (s := fun _ ↦ univ)
+    (fun t _ ↦ (h_lip t).lipschitzOnWith) ht₀
+    (fun t ht ↦ ⟨hα t ht, trivial⟩) (fun t ht ↦ ⟨hβ t ht, trivial⟩) hαβ
+
+/-- A continuous vector field that is bounded and Lipschitz in the second variable admits a
+global fundamental solution. -/
+public theorem exists_isIntegralCurve_of_bounded (h_lip : ∀ t, LipschitzWith K (f t))
+    (h_bdd : ∀ t x, ‖f t x‖ ≤ C) (h' : Continuous f.uncurry) :
+    ∃ Φ : ℝ → E → ℝ → E, ∀ t₀ x₀, IsIntegralCurve (Φ t₀ x₀) f ∧ Φ t₀ x₀ t₀ = x₀ := by
+  have h_cont : ∀ x, Continuous (f · x) := fun x ↦
+    h'.comp (continuous_id.prodMk continuous_const)
+  -- For each initial condition and each `n : ℕ`, a solution on `[t₀ - (n+1), t₀ + (n+1)]`.
+  have H : ∀ (t₀ : ℝ) (x₀ : E) (n : ℕ), ∃ α : ℝ → E, α t₀ = x₀ ∧
+      ∀ t ∈ Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1)),
+        HasDerivWithinAt α (f t (α t)) (Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1))) t :=
+    fun t₀ x₀ n ↦ exists_solution_Icc h_lip h_cont h_bdd t₀ x₀ ((n : ℝ) + 1) (by positivity)
+  choose α hα0 hα using H
+  -- At interior times these are genuine solutions.
+  have hderiv : ∀ (t₀ : ℝ) (x₀ : E) (n : ℕ) (t : ℝ), |t - t₀| < (n : ℝ) + 1 →
+      HasDerivAt (α t₀ x₀ n) (f t (α t₀ x₀ n t)) t := by
+    intro t₀ x₀ n t ht
+    rw [abs_lt] at ht
+    obtain ⟨h1, h2⟩ := ht
+    exact (hα t₀ x₀ n t ⟨by linarith, by linarith⟩).hasDerivAt
+      (Icc_mem_nhds (by linarith) (by linarith))
+  -- Solutions for different `n` agree wherever both are defined.
+  have hagree : ∀ (t₀ : ℝ) (x₀ : E) (m n : ℕ), m ≤ n → ∀ t : ℝ, |t - t₀| < (m : ℝ) + 1 →
+      α t₀ x₀ m t = α t₀ x₀ n t := by
+    intro t₀ x₀ m n hmn t ht
+    have hmn' : (m : ℝ) ≤ (n : ℝ) := by exact_mod_cast hmn
+    have hsub : ∀ s ∈ Ioo (t₀ - ((m : ℝ) + 1)) (t₀ + ((m : ℝ) + 1)), |s - t₀| < (m : ℝ) + 1 := by
+      intro s hs
+      rw [abs_lt]
+      exact ⟨by linarith [hs.1], by linarith [hs.2]⟩
+    have hm0 : (0 : ℝ) < (m : ℝ) + 1 := by positivity
+    refine solution_eqOn_Ioo (t₀ := t₀) h_lip (a := t₀ - ((m : ℝ) + 1)) (b := t₀ + ((m : ℝ) + 1))
+      ⟨by linarith, by linarith⟩
+      ((hα0 _ _ _).trans (hα0 _ _ _).symm)
+      (fun s hs ↦ hderiv t₀ x₀ m s (hsub s hs))
+      (fun s hs ↦ hderiv t₀ x₀ n s ((hsub s hs).trans_le (by linarith))) ?_
+    rw [abs_lt] at ht
+    exact ⟨by linarith [ht.1], by linarith [ht.2]⟩
+  refine ⟨fun t₀ x₀ t ↦ α t₀ x₀ ⌈|t - t₀|⌉₊ t, fun t₀ x₀ ↦ ⟨fun t ↦ ?_, by simp [hα0]⟩⟩
+  set N : ℕ := ⌈|t - t₀|⌉₊ with hN
+  have hNle : |t - t₀| ≤ (N : ℝ) := Nat.le_ceil _
+  -- Near `t`, the constructed flow coincides with the single solution of index `N + 1`.
+  have key : ∀ s : ℝ, |s - t| < 1 / 2 → α t₀ x₀ ⌈|s - t₀|⌉₊ s = α t₀ x₀ (N + 1) s := by
+    intro s hs
+    have hst : |s - t₀| ≤ (N : ℝ) + 1 / 2 := by
+      calc |s - t₀| ≤ |s - t| + |t - t₀| := by
+            simpa using abs_sub_le s t t₀
+        _ ≤ (N : ℝ) + 1 / 2 := by linarith
+    refine hagree t₀ x₀ _ (N + 1) ?_ s ?_
+    · refine Nat.ceil_le.mpr ?_
+      push_cast
+      linarith
+    · exact lt_of_le_of_lt (Nat.le_ceil _) (by linarith)
+  have hev : (fun s ↦ α t₀ x₀ ⌈|s - t₀|⌉₊ s) =ᶠ[nhds t] α t₀ x₀ (N + 1) := by
+    have hball : ∀ᶠ s in nhds t, |s - t| < 1 / 2 := by
+      filter_upwards [Metric.ball_mem_nhds t (by norm_num : (0 : ℝ) < 1 / 2)] with s hs
+      simpa [Real.dist_eq] using hs
+    filter_upwards [hball] with s hs using key s hs
+  have hval : α t₀ x₀ N t = α t₀ x₀ (N + 1) t := by
+    simpa using key t (by norm_num)
+  have hd : HasDerivAt (α t₀ x₀ (N + 1)) (f t (α t₀ x₀ (N + 1) t)) t := by
+    refine hderiv t₀ x₀ (N + 1) t ?_
+    push_cast
+    linarith
+  change HasDerivAt (fun s ↦ α t₀ x₀ ⌈|s - t₀|⌉₊ s) (f t (α t₀ x₀ N t)) t
+  rw [hval]
+  exact hd.congr_of_eventuallyEq hev
+
+end GlobalExistence

From f08c29d4add4b35479f1a25803b77f38f4a5bf25 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Sun, 23 Aug 2026 00:50:17 +1000
Subject: [PATCH 2/8] linearization and global existence

---
 DynamicalSystems/Basic/Autonomous.lean        |   5 +
 .../Mathlib/Analysis/Calculus/Flow.lean       |   7 +-
 .../Analysis/ODE/GlobalExistenceLinear.lean   | 246 +++++++++++++
 .../Analysis/ODE/RadialTruncation.lean        | 115 ++++++
 DynamicalSystems/Stability/Linearization.lean |  68 ++++
 DynamicalSystems/Stability/Lyapunov.lean      | 337 +++++++++++++++---
 6 files changed, 724 insertions(+), 54 deletions(-)
 create mode 100644 DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceLinear.lean
 create mode 100644 DynamicalSystems/Mathlib/Analysis/ODE/RadialTruncation.lean
 create mode 100644 DynamicalSystems/Stability/Linearization.lean

diff --git a/DynamicalSystems/Basic/Autonomous.lean b/DynamicalSystems/Basic/Autonomous.lean
index aa08f1b..5c697d3 100644
--- a/DynamicalSystems/Basic/Autonomous.lean
+++ b/DynamicalSystems/Basic/Autonomous.lean
@@ -29,6 +29,11 @@ variable (Φ : ι → E → E)
 def IsInvariantOn (s : Set E) (I : Set ι) : Prop :=
   ∀ ⦃t⦄, t ∈ I → Set.MapsTo (Φ t) s s
 
+variable {s : Set E} {I : Set ι}
+
+theorem isInvariantOn_iff : IsInvariantOn Φ s I ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃t⦄, t ∈ I → Φ t x ∈ s := by
+  grind [IsInvariantOn, Set.MapsTo]
+
 @[fun_prop]
 theorem IsInvariant.isInvariantOn {s : Set E} (h : IsInvariant Φ s) (I : Set ι) :
     IsInvariantOn Φ s I :=
diff --git a/DynamicalSystems/Mathlib/Analysis/Calculus/Flow.lean b/DynamicalSystems/Mathlib/Analysis/Calculus/Flow.lean
index 8cced47..23a6684 100644
--- a/DynamicalSystems/Mathlib/Analysis/Calculus/Flow.lean
+++ b/DynamicalSystems/Mathlib/Analysis/Calculus/Flow.lean
@@ -34,7 +34,6 @@ theorem DifferentiableAt.deriv_eq_deriv_zero (h : ∀ x, DifferentiableAt ℝ (
 theorem deriv_comp_flow {v : E → F} (hv : Differentiable ℝ v) (h : ∀ x, Differentiable ℝ (Φ · x))
     (t : ℝ) (x : E) :
     deriv (v <| Φ · x) t = fderiv ℝ v (Φ t x) (deriv (Φ · (Φ t x)) 0) := calc
-  _ = (fderiv ℝ v (Φ t x)) (deriv (Φ · x) t) := by
-    apply fderiv_comp_deriv t (by fun_prop) (by fun_prop)
-  _ = _ := by
-    rw [DifferentiableAt.deriv_eq_deriv_zero (by fun_prop)]
+  _ = (fderiv ℝ v (Φ t x)) (deriv (Φ · x) t) :=
+    fderiv_comp_deriv t (by fun_prop) (by fun_prop)
+  _ = _ := by rw [DifferentiableAt.deriv_eq_deriv_zero (by fun_prop)]
diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceLinear.lean b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceLinear.lean
new file mode 100644
index 0000000..0c89341
--- /dev/null
+++ b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceLinear.lean
@@ -0,0 +1,246 @@
+module
+
+public import Mathlib.Analysis.ODE.Basic
+import Mathlib.Analysis.ODE.Gronwall
+import Mathlib.Analysis.ODE.PicardLindelof
+import Mathlib.Analysis.ODE.ExistUnique
+
+import DynamicalSystems.Mathlib.Analysis.ODE.RadialTruncation
+
+/-!
+# Global existence for ODEs with a globally Lipschitz vector field of linear growth
+
+The strategy is:
+
+* `exists_solution_Icc`: for a *bounded* vector field, the Picard-Lindelöf theorem produces a
+  solution on an arbitrarily large compact time interval;
+* `norm_le_gronwallBound_of_linear_growth`: Grönwall's inequality gives an a priori bound on
+  any solution of a vector field with linear growth, on a given compact time interval;
+* `exists_solution_Icc_of_linear_growth`: truncating the vector field outside a large ball
+  (using the `2`-Lipschitz radial retraction `radialTrunc`) reduces the linear growth case to
+  the bounded case, the a priori bound guaranteeing that the solution never sees the
+  truncation;
+* `exists_global_of_exists_solution_Icc`: solutions on larger and larger compact intervals are
+  patched into a single global solution, using uniqueness (Grönwall again).
+-/
+
+open scoped NNReal
+open Metric Set
+
+/-! ## Global existence -/
+
+section GlobalExistence
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+  {f : ℝ → E → E} {C C' : ℝ} {K : ℝ≥0}
+
+/-- Existence on an arbitrarily large compact time interval for a *bounded* vector field,
+from the Picard-Lindelöf theorem. -/
+theorem exists_solution_Icc (h_lip : ∀ t, LipschitzWith K (f t))
+    (h_cont : ∀ x, Continuous (f · x)) (h_bdd : ∀ t x, ‖f t x‖ ≤ C)
+    (t₀ : ℝ) (x₀ : E) (R : ℝ) (hR : 0 ≤ R) :
+    ∃ α : ℝ → E, α t₀ = x₀ ∧ ∀ t ∈ Icc (t₀ - R) (t₀ + R),
+      HasDerivWithinAt α (f t (α t)) (Icc (t₀ - R) (t₀ + R)) t := by
+  have hC : 0 ≤ C := le_trans (norm_nonneg _) (h_bdd 0 0)
+  have ht₀ : t₀ ∈ Icc (t₀ - R) (t₀ + R) := ⟨by linarith, by linarith⟩
+  have hpl : IsPicardLindelof f (tmin := t₀ - R) (tmax := t₀ + R) ⟨t₀, ht₀⟩ x₀
+      ⟨C * R, by positivity⟩ 0 ⟨C, hC⟩ K := by
+    refine ⟨fun t _ ↦ (h_lip t).lipschitzOnWith, fun x _ ↦ (h_cont x).continuousOn,
+      fun t _ x _ ↦ h_bdd t x, ?_⟩
+    change (C : ℝ) * max (t₀ + R - t₀) (t₀ - (t₀ - R)) ≤ (C * R : ℝ) - ((0 : ℝ≥0) : ℝ)
+    rw [show t₀ + R - t₀ = R by ring, show t₀ - (t₀ - R) = R by ring, max_self]
+    simp
+  exact hpl.exists_eq_forall_mem_Icc_hasDerivWithinAt₀
+
+omit [CompleteSpace E] in
+/-- Two solutions with the same initial condition agree on any open interval on which
+they are both defined. -/
+theorem solution_eqOn_Ioo (h_lip : ∀ t, LipschitzWith K (f t))
+    {α β : ℝ → E} {t₀ a b : ℝ} (ht₀ : t₀ ∈ Ioo a b) (hαβ : α t₀ = β t₀)
+    (hα : ∀ t ∈ Ioo a b, HasDerivAt α (f t (α t)) t)
+    (hβ : ∀ t ∈ Ioo a b, HasDerivAt β (f t (β t)) t) :
+    EqOn α β (Ioo a b) :=
+  ODE_solution_unique_of_mem_Ioo (K := K) (s := fun _ ↦ univ)
+    (fun t _ ↦ (h_lip t).lipschitzOnWith) ht₀
+    (fun t ht ↦ ⟨hα t ht, trivial⟩) (fun t ht ↦ ⟨hβ t ht, trivial⟩) hαβ
+
+omit [CompleteSpace E] in
+/-- Solutions on arbitrarily large compact time intervals can be patched into a single global
+solution. -/
+theorem exists_global_of_exists_solution_Icc (h_lip : ∀ t, LipschitzWith K (f t))
+    (H : ∀ (t₀ : ℝ) (x₀ : E) (R : ℝ), 0 ≤ R → ∃ α : ℝ → E, α t₀ = x₀ ∧
+      ∀ t ∈ Icc (t₀ - R) (t₀ + R), HasDerivWithinAt α (f t (α t)) (Icc (t₀ - R) (t₀ + R)) t) :
+    ∃ Φ : ℝ → E → ℝ → E, ∀ t₀ x₀, IsIntegralCurve (Φ t₀ x₀) f ∧ Φ t₀ x₀ t₀ = x₀ := by
+  -- For each initial condition and each `n : ℕ`, a solution on `[t₀ - (n+1), t₀ + (n+1)]`.
+  have H' : ∀ (t₀ : ℝ) (x₀ : E) (n : ℕ), ∃ α : ℝ → E, α t₀ = x₀ ∧
+      ∀ t ∈ Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1)),
+        HasDerivWithinAt α (f t (α t)) (Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1))) t :=
+    fun t₀ x₀ n ↦ H t₀ x₀ ((n : ℝ) + 1) (by positivity)
+  choose α hα0 hα using H'
+  -- At interior times these are genuine solutions.
+  have hderiv : ∀ (t₀ : ℝ) (x₀ : E) (n : ℕ) (t : ℝ), |t - t₀| < (n : ℝ) + 1 →
+      HasDerivAt (α t₀ x₀ n) (f t (α t₀ x₀ n t)) t := by
+    intro t₀ x₀ n t ht
+    rw [abs_lt] at ht
+    obtain ⟨h1, h2⟩ := ht
+    exact (hα t₀ x₀ n t ⟨by linarith, by linarith⟩).hasDerivAt
+      (Icc_mem_nhds (by linarith) (by linarith))
+  -- Solutions for different `n` agree wherever both are defined.
+  have hagree : ∀ (t₀ : ℝ) (x₀ : E) (m n : ℕ), m ≤ n → ∀ t : ℝ, |t - t₀| < (m : ℝ) + 1 →
+      α t₀ x₀ m t = α t₀ x₀ n t := by
+    intro t₀ x₀ m n hmn t ht
+    have hmn' : (m : ℝ) ≤ (n : ℝ) := by exact_mod_cast hmn
+    have hsub : ∀ s ∈ Ioo (t₀ - ((m : ℝ) + 1)) (t₀ + ((m : ℝ) + 1)), |s - t₀| < (m : ℝ) + 1 := by
+      intro s hs
+      rw [abs_lt]
+      exact ⟨by linarith [hs.1], by linarith [hs.2]⟩
+    have hm0 : (0 : ℝ) < (m : ℝ) + 1 := by positivity
+    refine solution_eqOn_Ioo (t₀ := t₀) h_lip (a := t₀ - ((m : ℝ) + 1)) (b := t₀ + ((m : ℝ) + 1))
+      ⟨by linarith, by linarith⟩
+      ((hα0 _ _ _).trans (hα0 _ _ _).symm)
+      (fun s hs ↦ hderiv t₀ x₀ m s (hsub s hs))
+      (fun s hs ↦ hderiv t₀ x₀ n s ((hsub s hs).trans_le (by linarith))) ?_
+    rw [abs_lt] at ht
+    exact ⟨by linarith [ht.1], by linarith [ht.2]⟩
+  refine ⟨fun t₀ x₀ t ↦ α t₀ x₀ ⌈|t - t₀|⌉₊ t, fun t₀ x₀ ↦ ⟨fun t ↦ ?_, by simp [hα0]⟩⟩
+  set N : ℕ := ⌈|t - t₀|⌉₊ with hN
+  have hNle : |t - t₀| ≤ (N : ℝ) := Nat.le_ceil _
+  -- Near `t`, the constructed flow coincides with the single solution of index `N + 1`.
+  have key : ∀ s : ℝ, |s - t| < 1 / 2 → α t₀ x₀ ⌈|s - t₀|⌉₊ s = α t₀ x₀ (N + 1) s := by
+    intro s hs
+    have hst : |s - t₀| ≤ (N : ℝ) + 1 / 2 := by
+      calc |s - t₀| ≤ |s - t| + |t - t₀| := by
+            simpa using abs_sub_le s t t₀
+        _ ≤ (N : ℝ) + 1 / 2 := by linarith
+    refine hagree t₀ x₀ _ (N + 1) ?_ s ?_
+    · refine Nat.ceil_le.mpr ?_
+      push_cast
+      linarith
+    · exact lt_of_le_of_lt (Nat.le_ceil _) (by linarith)
+  have hev : (fun s ↦ α t₀ x₀ ⌈|s - t₀|⌉₊ s) =ᶠ[nhds t] α t₀ x₀ (N + 1) := by
+    have hball : ∀ᶠ s in nhds t, |s - t| < 1 / 2 := by
+      filter_upwards [Metric.ball_mem_nhds t (by norm_num : (0 : ℝ) < 1 / 2)] with s hs
+      simpa [Real.dist_eq] using hs
+    filter_upwards [hball] with s hs using key s hs
+  have hval : α t₀ x₀ N t = α t₀ x₀ (N + 1) t := by
+    simpa using key t (by norm_num)
+  have hd : HasDerivAt (α t₀ x₀ (N + 1)) (f t (α t₀ x₀ (N + 1) t)) t := by
+    refine hderiv t₀ x₀ (N + 1) t ?_
+    push_cast
+    linarith
+  change HasDerivAt (fun s ↦ α t₀ x₀ ⌈|s - t₀|⌉₊ s) (f t (α t₀ x₀ N t)) t
+  rw [hval]
+  exact hd.congr_of_eventuallyEq hev
+
+omit [CompleteSpace E] in
+/-- A priori bound (Grönwall): a solution of a vector field with linear growth
+`‖f t x‖ ≤ C * ‖x‖ + C'` on `[t₀ - T, t₀ + T]` stays in a ball whose radius depends only on
+`‖α t₀‖`, `C`, `C'` and `T`. -/
+theorem norm_le_gronwallBound_of_linear_growth (hC : 0 ≤ C) (hC' : 0 ≤ C')
+    (h_bdd : ∀ t x, ‖f t x‖ ≤ C * ‖x‖ + C') {α : ℝ → E} {t₀ T : ℝ} (hT : 0 ≤ T)
+    (hα : ∀ t ∈ Icc (t₀ - T) (t₀ + T), HasDerivWithinAt α (f t (α t)) (Icc (t₀ - T) (t₀ + T)) t) :
+    ∀ t ∈ Icc (t₀ - T) (t₀ + T), ‖α t‖ ≤ gronwallBound ‖α t₀‖ C C' T := by
+  have hcont : ContinuousOn α (Icc (t₀ - T) (t₀ + T)) := fun t ht ↦ (hα t ht).continuousWithinAt
+  have hint : ∀ t ∈ Ioo (t₀ - T) (t₀ + T), HasDerivAt α (f t (α t)) t := fun t ht ↦
+    (hα t (Ioo_subset_Icc_self ht)).hasDerivAt (Icc_mem_nhds ht.1 ht.2)
+  have hmono : ∀ x ≤ T, gronwallBound ‖α t₀‖ C C' x ≤ gronwallBound ‖α t₀‖ C C' T :=
+    fun x hx ↦ gronwallBound_mono (norm_nonneg _) hC' hC hx
+  -- Forward in time.
+  have hfwd : ∀ t ∈ Icc t₀ (t₀ + T), ‖α t‖ ≤ gronwallBound ‖α t₀‖ C C' (t - t₀) := by
+    refine norm_le_gronwallBound_of_norm_deriv_right_le (f' := fun t ↦ f t (α t))
+      (hcont.mono (fun t ht ↦ ⟨by linarith [ht.1], ht.2⟩)) (fun x hx ↦ ?_) le_rfl
+      (fun x _ ↦ h_bdd x (α x))
+    exact (hint x ⟨by linarith [hx.1, hx.2], hx.2⟩).hasDerivWithinAt
+  -- Backward in time, by reflecting the time variable about `t₀`.
+  have hbwd : ∀ s ∈ Icc t₀ (t₀ + T), ‖α (2 * t₀ - s)‖ ≤ gronwallBound ‖α t₀‖ C C' (s - t₀) := by
+    have hmem : MapsTo (fun s : ℝ ↦ 2 * t₀ - s) (Icc t₀ (t₀ + T)) (Icc (t₀ - T) (t₀ + T)) := by
+      intro s hs
+      exact ⟨by linarith [hs.2], by linarith [hs.1]⟩
+    have hβcont : ContinuousOn (fun s ↦ α (2 * t₀ - s)) (Icc t₀ (t₀ + T)) :=
+      hcont.comp (by fun_prop) hmem
+    refine norm_le_gronwallBound_of_norm_deriv_right_le
+      (f' := fun s ↦ -(f (2 * t₀ - s) (α (2 * t₀ - s)))) hβcont (fun s hs ↦ ?_)
+      (by rw [show 2 * t₀ - t₀ = t₀ by ring]) (fun s _ ↦ by simpa using h_bdd _ _)
+    have h1 : HasDerivAt (fun s : ℝ ↦ 2 * t₀ - s) (-1) s := by
+      simpa using (hasDerivAt_id s).const_sub (2 * t₀)
+    have h2 : HasDerivAt α (f (2 * t₀ - s) (α (2 * t₀ - s))) (2 * t₀ - s) :=
+      hint _ ⟨by linarith [hs.2], by linarith [hs.1, hs.2]⟩
+    have h3 := h2.scomp s h1
+    convert h3.hasDerivWithinAt
+    · simp
+    · simp
+  intro t ht
+  rcases le_or_gt t₀ t with h | h
+  · exact (hfwd t ⟨h, ht.2⟩).trans (hmono _ (by linarith [ht.2]))
+  · have hs : 2 * t₀ - t ∈ Icc t₀ (t₀ + T) := ⟨by linarith, by linarith [ht.1]⟩
+    have hb := hbwd _ hs
+    rw [show 2 * t₀ - (2 * t₀ - t) = t by ring] at hb
+    exact hb.trans (hmono _ (by linarith [ht.1]))
+
+/-- Existence on an arbitrarily large compact time interval for a globally Lipschitz vector
+field with linear growth. -/
+theorem exists_solution_Icc_of_linear_growth (h_lip : ∀ t, LipschitzWith K (f t))
+    (h' : Continuous f.uncurry) (hC' : 0 ≤ C') (h_bdd : ∀ t x, ‖f t x‖ ≤ (K : ℝ) * ‖x‖ + C')
+    (t₀ : ℝ) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) :
+    ∃ α : ℝ → E, α t₀ = x₀ ∧ ∀ t ∈ Icc (t₀ - T) (t₀ + T),
+      HasDerivWithinAt α (f t (α t)) (Icc (t₀ - T) (t₀ + T)) t := by
+  -- Truncate the vector field outside a ball large enough that the a priori bound applies.
+  set R : ℝ := max (gronwallBound ‖x₀‖ (K : ℝ) C' T) 0 with hRdef
+  have hR0 : 0 ≤ R := le_max_right _ _
+  set g : ℝ → E → E := fun t x ↦ f t (radialTrunc R x) with hgdef
+  have hglip : ∀ t, LipschitzWith (K * 2) (g t) := fun t ↦
+    (h_lip t).comp (lipschitzWith_radialTrunc hR0)
+  have hgcont : ∀ x, Continuous (g · x) := fun x ↦ by fun_prop
+  have hgbdd : ∀ t x, ‖g t x‖ ≤ (K : ℝ) * R + C' := by
+    intro t x
+    calc ‖g t x‖ ≤ (K : ℝ) * ‖radialTrunc R x‖ + C' := h_bdd _ _
+      _ ≤ (K : ℝ) * R + C' := by
+          grw [norm_radialTrunc_le hR0]
+  have hggrow : ∀ t x, ‖g t x‖ ≤ (K : ℝ) * ‖x‖ + C' := by
+    intro t x
+    calc ‖g t x‖ ≤ (K : ℝ) * ‖radialTrunc R x‖ + C' := h_bdd _ _
+      _ ≤ (K : ℝ) * ‖x‖ + C' := by
+          grw [norm_radialTrunc_le_self hR0]
+  obtain ⟨α, hα0, hα⟩ := exists_solution_Icc hglip hgcont hgbdd t₀ x₀ T hT
+  have hbound := norm_le_gronwallBound_of_linear_growth (f := g) K.coe_nonneg hC' hggrow hT hα
+  refine ⟨α, hα0, fun t ht ↦ ?_⟩
+  have h1 : ‖α t‖ ≤ R := by
+    have h2 := hbound t ht
+    rw [hα0] at h2
+    grind
+  have h3 : g t (α t) = f t (α t) := by
+    simp [hgdef, radialTrunc_eq_self h1]
+  rw [← h3]
+  exact hα t ht
+
+/-- Global existence of a flow for a globally Lipschitz, jointly continuous vector field of
+linear growth. -/
+public theorem global_existence (h_lip : ∀ t, LipschitzWith K (f t))
+    (ht_bdd : ∀ t, ‖f t 0‖ ≤ C') (h' : Continuous f.uncurry) :
+    ∃ Φ : ℝ → E → ℝ → E, ∀ t₀ x₀, IsIntegralCurve (Φ t₀ x₀) f ∧ Φ t₀ x₀ t₀ = x₀ := by
+  -- Being `K`-Lipschitz, `f t` grows at most like `K * ‖x‖ + ‖f t 0‖`, and `‖f t 0‖ ≤ C'`.
+  have hC' : 0 ≤ C' := by
+    have := ht_bdd 0
+    simpa using (norm_nonneg _).trans this
+  have hgrow : ∀ t x, ‖f t x‖ ≤ (K : ℝ) * ‖x‖ + C' := by
+    intro t x
+    have h0 : ‖f t 0‖ ≤ C' := by simpa using ht_bdd t
+    have hK : ‖f t x - f t 0‖ ≤ (K : ℝ) * ‖x‖ := by
+      have := (h_lip t).dist_le_mul x 0
+      simpa [dist_eq_norm] using this
+    calc ‖f t x‖ = ‖(f t x - f t 0) + f t 0‖ := by rw [sub_add_cancel]
+      _ ≤ ‖f t x - f t 0‖ + ‖f t 0‖ := norm_add_le _ _
+      _ ≤ (K : ℝ) * ‖x‖ + C' := by linarith
+  exact exists_global_of_exists_solution_Icc h_lip
+    (exists_solution_Icc_of_linear_growth h_lip h' hC' hgrow)
+
+attribute [fun_prop] LipschitzWith.continuous
+
+/-- A time-independent globally Lipschitz continuous vector field admits a global fundamental
+solution. -/
+public theorem global_existence_autonomous {f : E → E} (h_lip : LipschitzWith K f) :
+    ∃ Φ : ℝ → E → ℝ → E, ∀ t₀ x₀, IsIntegralCurve (Φ t₀ x₀) (fun _ ↦ f) ∧ Φ t₀ x₀ t₀ = x₀ :=
+  global_existence (fun _ ↦ h_lip) (fun _ ↦ le_refl _) (by fun_prop)
+
+
+end GlobalExistence
diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/RadialTruncation.lean b/DynamicalSystems/Mathlib/Analysis/ODE/RadialTruncation.lean
new file mode 100644
index 0000000..cb069e4
--- /dev/null
+++ b/DynamicalSystems/Mathlib/Analysis/ODE/RadialTruncation.lean
@@ -0,0 +1,115 @@
+module
+
+public import Mathlib.Analysis.ODE.Basic
+
+/-!
+# Radial truncation (radial retraction onto a closed ball)
+
+For `R ≥ 0`, the map `radialTrunc R` is the radial retraction of a normed space onto the
+closed ball of radius `R` centred at the origin: it is the identity on the ball, and it
+sends a point `x` outside the ball to the point `(R / ‖x‖) • x` on the sphere.
+
+The key fact is that this map is Lipschitz with constant `2` in an arbitrary normed space
+(`lipschitzWith_radialTrunc`).  It is used to truncate a vector field of linear growth into
+a bounded one.
+-/
+
+public section
+
+open Metric Set
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+
+/-- The radial retraction onto the closed ball of radius `R` about the origin. -/
+noncomputable def radialTrunc (R : ℝ) (x : E) : E :=
+  if ‖x‖ ≤ R then x else (R / ‖x‖) • x
+
+lemma radialTrunc_eq_self {R : ℝ} {x : E} (hx : ‖x‖ ≤ R) : radialTrunc R x = x :=
+  ite_eq_left hx
+
+lemma norm_radialTrunc_le {R : ℝ} (hR : 0 ≤ R) (x : E) : ‖radialTrunc R x‖ ≤ R := by
+  unfold radialTrunc
+  split_ifs with h
+  · exact h
+  · push Not at h
+    have hx : 0 < ‖x‖ := lt_of_le_of_lt hR h
+    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (by positivity)]
+    rw [div_mul_cancel₀ _ hx.ne']
+
+lemma norm_radialTrunc_le_self {R : ℝ} (hR : 0 ≤ R) (x : E) : ‖radialTrunc R x‖ ≤ ‖x‖ := by
+  unfold radialTrunc
+  split_ifs with h
+  · exact le_rfl
+  · push Not at h
+    have hx : 0 < ‖x‖ := lt_of_le_of_lt hR h
+    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (by positivity),
+      div_mul_cancel₀ _ hx.ne']
+    exact h.le
+
+/-- The radial retraction onto a ball of radius `R ≥ 0` moves points by at most twice their
+distance: it is `2`-Lipschitz. -/
+lemma norm_radialTrunc_sub_radialTrunc_le {R : ℝ} (hR : 0 ≤ R) (x y : E) :
+    ‖radialTrunc R x - radialTrunc R y‖ ≤ 2 * ‖x - y‖ := by
+  wlog hxy : ‖y‖ ≤ ‖x‖ generalizing x y
+  · have h := this y x (le_of_not_ge hxy)
+    rw [norm_sub_rev (radialTrunc R x), norm_sub_rev x]
+    exact h
+  have hd : ‖x‖ - ‖y‖ ≤ ‖x - y‖ := norm_sub_norm_le x y
+  rcases le_or_gt ‖x‖ R with hxR | hxR
+  · rw [radialTrunc_eq_self hxR, radialTrunc_eq_self (hxy.trans hxR)]
+    nlinarith [norm_nonneg (x - y)]
+  · have hx0 : 0 < ‖x‖ := lt_of_le_of_lt hR hxR
+    rw [show radialTrunc R x = (R / ‖x‖) • x from ite_eq_right (not_le.mpr hxR)]
+    set t : ℝ := R / ‖x‖ with ht
+    have ht0 : 0 ≤ t := by positivity
+    have htx : t * ‖x‖ = R := by rw [ht, div_mul_cancel₀ _ hx0.ne']
+    have ht1 : t ≤ 1 := by rw [ht, div_le_one hx0]; linarith
+    rcases le_or_gt ‖y‖ R with hyR | hyR
+    · rw [radialTrunc_eq_self hyR]
+      have hdecomp : t • x - y = t • (x - y) + (t - 1) • y := by module
+      have e1 : ‖t • (x - y)‖ = t * ‖x - y‖ := by
+        rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht0]
+      have e2 : ‖(t - 1) • y‖ = (1 - t) * ‖y‖ := by
+        rw [norm_smul, Real.norm_eq_abs, abs_of_nonpos (by linarith)]
+        ring
+      have h4 : (1 - t) * R ≤ ‖x‖ - R := by nlinarith [sq_nonneg (1 - t)]
+      have h5 : (1 - t) * ‖y‖ ≤ (1 - t) * R :=
+        mul_le_mul_of_nonneg_left hyR (by linarith)
+      have h6 : t * ‖x - y‖ ≤ ‖x - y‖ :=
+        mul_le_of_le_one_left (norm_nonneg _) ht1
+      calc ‖t • x - y‖ = ‖t • (x - y) + (t - 1) • y‖ := by rw [hdecomp]
+        _ ≤ ‖t • (x - y)‖ + ‖(t - 1) • y‖ := norm_add_le _ _
+        _ = t * ‖x - y‖ + (1 - t) * ‖y‖ := by rw [e1, e2]
+        _ ≤ 2 * ‖x - y‖ := by linarith
+    · have hy0 : 0 < ‖y‖ := lt_of_le_of_lt hR hyR
+      rw [show radialTrunc R y = (R / ‖y‖) • y from ite_eq_right (not_le.mpr hyR)]
+      set s : ℝ := R / ‖y‖ with hs
+      have hsy : s * ‖y‖ = R := by rw [hs, div_mul_cancel₀ _ hy0.ne']
+      have hts : t ≤ s := by
+        rw [ht, hs]
+        gcongr
+      have hdecomp : t • x - s • y = t • (x - y) + (t - s) • y := by module
+      have e1 : ‖t • (x - y)‖ = t * ‖x - y‖ := by
+        rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht0]
+      have e2 : ‖(t - s) • y‖ = (s - t) * ‖y‖ := by
+        rw [norm_smul, Real.norm_eq_abs, abs_of_nonpos (by linarith)]
+        ring
+      have h4 : (s - t) * ‖y‖ ≤ ‖x‖ - ‖y‖ := by
+        have hmul : ((s - t) * ‖y‖) * ‖x‖ ≤ (‖x‖ - ‖y‖) * ‖x‖ := by
+          have hexp : ((s - t) * ‖y‖) * ‖x‖ = R * ‖x‖ - R * ‖y‖ := by
+            have : s * ‖y‖ = R := hsy
+            nlinarith [htx, hsy]
+          nlinarith [htx]
+        exact le_of_mul_le_mul_right hmul hx0
+      have h6 : t * ‖x - y‖ ≤ ‖x - y‖ :=
+        mul_le_of_le_one_left (norm_nonneg _) ht1
+      calc ‖t • x - s • y‖ = ‖t • (x - y) + (t - s) • y‖ := by rw [hdecomp]
+        _ ≤ ‖t • (x - y)‖ + ‖(t - s) • y‖ := norm_add_le _ _
+        _ = t * ‖x - y‖ + (s - t) * ‖y‖ := by rw [e1, e2]
+        _ ≤ 2 * ‖x - y‖ := by linarith
+
+lemma lipschitzWith_radialTrunc {R : ℝ} (hR : 0 ≤ R) :
+    LipschitzWith 2 (radialTrunc R : E → E) := by
+  rw [lipschitzWith_iff_dist_le_mul]
+  intro x y
+  simpa [dist_eq_norm] using norm_radialTrunc_sub_radialTrunc_le hR x y
diff --git a/DynamicalSystems/Stability/Linearization.lean b/DynamicalSystems/Stability/Linearization.lean
new file mode 100644
index 0000000..6cd649d
--- /dev/null
+++ b/DynamicalSystems/Stability/Linearization.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+module
+
+public import DynamicalSystems.Stability.Example
+
+import Mathlib.Analysis.InnerProductSpace.Calculus
+import DynamicalSystems.Mathlib.Analysis.Calculus.IsStrictLocalMax
+
+public section
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+
+variable {f : E → E} {Φ : Flow ℝ E} {x₀ : E}
+
+open scoped Topology
+
+theorem exists_isLyapunovOnIn (hf : DifferentiableAt ℝ f x₀) (hx₀ : f x₀ = 0)
+    (h : IsCoercive (innerSL ℝ ∘L (-fderiv ℝ f x₀)))
+    (hΦ : ∀ x₀, IsIntegralCurve (Φ · x₀) (fun _ ↦ f)) :
+    ∃ δ, 0 < δ ∧ IsLyapunovOnIn (fun x ↦ ‖x - x₀‖ ^ 2) Φ { p | ‖p - x₀‖ ^ 2 ≤ δ} (Set.Ici 0) := by
+  obtain ⟨δ, hδ, h⟩ := exists_inner_neg hx₀ h hf
+  use (δ / 2) ^ 2, by positivity
+  have hs : IsOpen { x | ‖x - x₀‖ < δ } := isOpen_lt (by fun_prop) (by fun_prop)
+  apply isLyapunovOnIn_of_fderiv (fun _ ↦ by positivity) hs ?_ ?_ ?_ ?_
+  · intro x hx
+    simp only [Set.mem_ofPred_eq] at hx ⊢
+    rw [sq_le_sq₀ (by positivity) (by positivity)] at hx
+    grw [hx]
+    simpa
+  · simp_rw [← real_inner_self_eq_norm_sq]
+    fun_prop
+  · intro x t
+    apply (hΦ x t).differentiableAt
+  · intro x hx
+    suffices inner ℝ (x - x₀) (f x) ≤ 0 by
+      simp_rw [← real_inner_self_eq_norm_sq]
+      rw [fderiv_inner_apply ℝ (by fun_prop) (by fun_prop), real_inner_comm (x - x₀)]
+      simpa [fderiv_sub_const x₀, (hΦ x 0).deriv]
+    by_cases! h' : x ≠ x₀
+    · apply (h _ _ h').le
+      rwa [mem_ball_iff_norm]
+    · simp [h']
+
+variable [ProperSpace E]
+
+/-- Let `f` be a vector field and `Φ` its fundamental solution.
+A fixed point `x₀` of `Φ` is stable if `inner ℝ y (fderiv ℝ f x₀ y) ≤ -C ‖y‖ ^ 2` for some `C > 0`.
+
+The condition on the derivative is phrased in terms of `IsCoercive`.
+-/
+theorem isStableOn_of_isCoercive_inner_comp_neg_fderiv (hf : DifferentiableAt ℝ f x₀)
+    (hx₀ : f x₀ = 0) (hΦ : ∀ x₀, IsIntegralCurve (Φ · x₀) (fun _ ↦ f))
+    (h : IsCoercive (innerSL ℝ ∘L (-fderiv ℝ f x₀))) :
+    (𝓝 x₀).IsStableOn Φ (Set.Ici 0) := by
+  obtain ⟨δ₀, hδ₀, h_lya⟩ := exists_isLyapunovOnIn hf hx₀ h hΦ
+  apply h_lya.isStableOn_nhds (δ₀ := δ₀) ?_ ?_ ?_ hδ₀
+  · simp
+  · convert isCompact_closedBall x₀ (δ₀ ^ ((1 : ℝ) / 2))
+    ext x
+    simp only [Set.mem_ofPred_eq, one_div, Metric.mem_closedBall]
+    rw [Real.le_rpow_inv_iff_of_pos (by positivity) hδ₀.le (by norm_num), dist_eq_norm]
+    simp
+  · simp [sub_eq_zero]
+  · simp
diff --git a/DynamicalSystems/Stability/Lyapunov.lean b/DynamicalSystems/Stability/Lyapunov.lean
index 43a6b62..fc37c56 100644
--- a/DynamicalSystems/Stability/Lyapunov.lean
+++ b/DynamicalSystems/Stability/Lyapunov.lean
@@ -5,6 +5,7 @@ Authors: Moritz Doll
 -/
 module
 
+public import DynamicalSystems.Basic.Autonomous
 public import DynamicalSystems.Mathlib.Topology.Antitone
 public import DynamicalSystems.Stability.Basic
 public import DynamicalSystems.Mathlib.Analysis.Calculus.Flow
@@ -24,7 +25,7 @@ open scoped Topology
 section Definition
 
 variable [TopologicalSpace E]
-  [Preorder F] [Zero F] [TopologicalSpace F]
+  [Preorder F] [Zero F] [TopologicalSpace F] [Preorder ι]
 
 /-- A Lyapunov function is a continuous non-negative function that is non-increasing with respect
 to a given flow.
@@ -32,7 +33,7 @@ to a given flow.
 Note that we assume that `v` is non-negative and continuous everywhere, but only decreasing on
 `s`. -/
 @[fun_prop]
-structure IsLyapunovOn [Preorder ι] (v : E → F) (Φ : ι → E → E) (s : Set E) : Prop where
+structure IsLyapunovOn (v : E → F) (Φ : ι → E → E) (s : Set E) : Prop where
   /-- A Lyapunov function is non-negative everywhere -/
   pos : ∀ x, 0 ≤ v x
   /-- A Lyapunov function is continuous everywhere -/
@@ -42,10 +43,43 @@ structure IsLyapunovOn [Preorder ι] (v : E → F) (Φ : ι → E → E) (s : Se
   antitone : ∀ ⦃x t₀ t₁⦄ (_ht₀ : Φ t₀ x ∈ s) (_ht₁ : Φ t₁ x ∈ s) (_ht : t₀ ≤ t₁),
     v (Φ t₁ x) ≤ v (Φ t₀ x)
 
+/-- A Lyapunov function is a continuous non-negative function that is non-increasing with respect
+to a given flow.
+
+Note that we assume that `v` is non-negative and continuous everywhere, but only decreasing on
+`s`. -/
+@[fun_prop]
+structure IsLyapunovOn' (v : E → F) (Φ : ι → E → E) (s : Set E) : Prop where
+  /-- A Lyapunov function is non-negative everywhere -/
+  pos : ∀ x, 0 ≤ v x
+  /-- A Lyapunov function is continuous everywhere -/
+  cont : Continuous v
+  /-- A Lyapunov function is monotonically decreasing along the flow for all values `t` such that
+  `Φ t x` is contained in `s`. -/
+  antitone : ∀ ⦃x t₀ t₁⦄ (_hx : x ∈ s) (_ht₀ : Φ t₀ x ∈ s) (_ht₁ : Φ t₁ x ∈ s) (_ht : t₀ ≤ t₁),
+    v (Φ t₁ x) ≤ v (Φ t₀ x)
+
+/-- A Lyapunov function is a continuous non-negative function that is non-increasing with respect
+to a given flow.
+
+Note that we assume that `v` is non-negative and continuous everywhere, but only decreasing on
+`s`. -/
+@[fun_prop]
+structure IsLyapunovOnIn (v : E → F) (Φ : ι → E → E) (s : Set E) (s' : Set ι) : Prop where
+  /-- A Lyapunov function is non-negative everywhere -/
+  pos : ∀ x, 0 ≤ v x
+  /-- A Lyapunov function is continuous everywhere -/
+  cont : Continuous v
+  /-- A Lyapunov function is monotonically decreasing along the flow for all values `t` such that
+  `Φ t x` is contained in `s`. -/
+  antitone : ∀ x ∈ s, ∀ t₀ ∈ s', ∀ t₁ ∈ s', t₀ ≤ t₁ → v (Φ t₁ x) ≤ v (Φ t₀ x)
+  /-- the set `s` is invariant. -/
+  mem : ∀ x ∈ s, ∀ t ∈ s', Φ t x ∈ s
+
 /-- A Lyapunov function is a continuous non-negative function that is non-increasing with respect
 to a given flow. -/
 @[fun_prop]
-structure IsLyapunov [Preorder ι] (v : E → F) (Φ : ι → E → E) : Prop where
+structure IsLyapunov (v : E → F) (Φ : ι → E → E) : Prop where
   /-- A Lyapunov function is non-negative everywhere -/
   pos : ∀ x, 0 ≤ v x
   /-- A Lyapunov function is continuous everywhere -/
@@ -55,7 +89,13 @@ structure IsLyapunov [Preorder ι] (v : E → F) (Φ : ι → E → E) : Prop wh
 
 attribute [fun_prop] IsLyapunov.cont
 
-variable [Preorder ι] {v : E → F} {Φ : ι → E → E} {s : Set E}
+variable {v : E → F} {Φ : ι → E → E} {s : Set E}
+
+@[fun_prop]
+theorem IsLyapunovOn.isLyapunovOn' (h : IsLyapunovOn v Φ s) : IsLyapunovOn' v Φ s where
+  pos := h.pos
+  cont := h.cont
+  antitone _ _ _ _ ht₀ ht₁ ht := h.antitone ht₀ ht₁ ht
 
 @[fun_prop]
 theorem IsLyapunovOn.continuous (h : IsLyapunovOn v Φ s) : Continuous v := h.cont
@@ -64,6 +104,11 @@ theorem IsLyapunovOn.continuous (h : IsLyapunovOn v Φ s) : Continuous v := h.co
 theorem IsLyapunovOn.continuousAt (h : IsLyapunovOn v Φ s) {x : E} : ContinuousAt v x :=
   h.cont.continuousAt
 
+theorem IsLyapunov.isLyapunovOn' (h : IsLyapunov v Φ) (s : Set E) : IsLyapunovOn' v Φ s where
+  pos := h.pos
+  cont := h.cont
+  antitone x _ _ _ _ _ ht := h.antitone x ht
+
 theorem IsLyapunov.isLyapunovOn (h : IsLyapunov v Φ) (s : Set E) : IsLyapunovOn v Φ s where
   pos := h.pos
   cont := h.cont
@@ -76,7 +121,7 @@ open Filter
 
 variable {Φ : ι → E → E} {v : E → F} {x₀ : E} {s : Set E}
 
-section blubb
+section HasBasis
 
 variable [Preorder ι] [IsDirectedOrder ι] [TopologicalSpace E]
 
@@ -87,11 +132,11 @@ variable
 
 /-- The flow composed with a Lyapunov function converges to some point. -/
 theorem IsLyapunovOn.exists_tendsto {x : E} {t₀ : ι} (h_lya : IsLyapunovOn v Φ s)
-    (hx : ∀ t ∈ Set.Ici t₀, Φ t x ∈ s) :
+    (hΦ : ∀ t ∈ Set.Ici t₀, Φ t x ∈ s) :
     ∃ c, Filter.Tendsto (v <| Φ · x) Filter.atTop (𝓝 c) := by
   have h_anti : AntitoneOn (v <| Φ · x) (Set.Ici t₀) := by
     intro t ht t' ht' h
-    exact h_lya.antitone (hx t ht) (hx t' ht') h
+    exact h_lya.antitone (hΦ t ht) (hΦ t' ht') h
   apply h_anti.exists_tendsto ⟨0, ?_⟩
   intro t ht
   exact h_lya.pos _
@@ -100,13 +145,13 @@ variable [Nonempty ι]
 
 /-- The flow composed with a Lyapunov function converges to some point. -/
 theorem IsLyapunovOn.exists_tendsto_of_eventually {x : E} (h_lya : IsLyapunovOn v Φ s)
-    (hx : ∀ᶠ t in atTop, Φ t x ∈ s) :
+    (hΦ : ∀ᶠ t in atTop, Φ t x ∈ s) :
     ∃ c, Filter.Tendsto (v <| Φ · x) Filter.atTop (𝓝 c) := by
-  rw [Filter.eventually_atTop] at hx
-  obtain ⟨t₀, hx⟩ := hx
+  rw [Filter.eventually_atTop] at hΦ
+  obtain ⟨t₀, hΦ⟩ := hΦ
   have h_anti : AntitoneOn (v <| Φ · x) (Set.Ici t₀) := by
     intro t ht t' ht' h
-    exact h_lya.antitone (hx t ht) (hx t' ht') h
+    exact h_lya.antitone (hΦ t ht) (hΦ t' ht') h
   apply h_anti.exists_tendsto ⟨0, ?_⟩
   intro t ht
   exact h_lya.pos _
@@ -222,18 +267,102 @@ theorem hasBasis_setOf_le (h_cont : Continuous v) (h_pos : ∀ x, 0 ≤ v x)
     (𝓝 x₀).HasBasis (0 < ·) ({ p | v p ≤ · }) := by
   simpa using hasBasis_nhdsSet_setOf_le (s' := {x₀}) h_cont h_pos (by simp [hvx₀]) hδ₀ h_cpt
 
-end blubb
+end HasBasis
 
-variable [TopologicalSpace E] [Preorder ι] [FirstCountableTopology E]
+variable [TopologicalSpace E]
 
 variable {v : E → ℝ} {t₀ : ι}
 
-variable {s' : Set E}
+variable {s' : Set E} {x : E}
+
+section ContinuityMethod
+
+variable [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι]
+  [DenselyOrdered ι]
+
+variable [TopologicalSpace α]
+
+theorem continuity_method {γ : ι → α} {p : Set α} {s : Set α} (hs : IsOpen s)
+    (hγ : Continuous γ)
+    (ht₀ : γ t₀ ∈ p) (ht₀' : γ t₀ ∈ s) (h_closed : IsClosed (s ∩ p))
+    (h : ∀ t ∈ Set.Ici t₀, (∀ t' ∈ Set.Icc t₀ t, γ t' ∈ s) → γ t ∈ p)
+    {t : ι} (ht : t₀ ≤ t) :
+    γ t ∈ s ∩ p := by
+  -- Assume there exists `t ≥ t₀` such that `γ t ∉ s ∩ p
+  by_contra hgoal
+  set B : Set ι := {u | u ∈ Set.Icc t₀ t ∧ γ u ∉ s ∩ p} with hB
+  have htB : t ∈ B := by grind
+  have hBne : B.Nonempty := Set.nonempty_of_mem htB
+  have hbdd : BddBelow B := ⟨t₀, fun _ _ ↦ by grind⟩
+  -- Let `τ` denote the inf of all `t` such that `γ t ∉ s ∩ p`
+  set τ := sInf B with hτdef
+  have hτ0 : t₀ ≤ τ := by grind [le_csInf]
+  have hτt : τ ≤ t := by grind [csInf_le]
+  -- forall `t ≤ τ` we have that `γ t ∈ s ∩ p`
+  have hbelow : ∀ t ∈ Set.Ico t₀ τ, γ t ∈ s ∩ p := by
+    intro t ⟨ht₁, ht₂⟩
+    by_contra hc
+    have htB : t ∈ B := by grind
+    grind [csInf_le hbdd htB]
+  -- at time `τ` the path is still in `s ∩ p`, by closedness
+  have hKτ : γ τ ∈ s ∩ p := by
+    rcases eq_or_lt_of_le hτ0 with heq | hlt
+    · grind
+    · have hclosed : IsClosed (γ ⁻¹' (s ∩ p)) := h_closed.preimage hγ
+      have hsub : Set.Ico t₀ τ ⊆ γ ⁻¹' (s ∩ p) := hbelow
+      have hmem : τ ∈ closure (Set.Ico t₀ τ) := by grind [closure_Ico, ne_of_lt]
+      grind [hclosed.closure_eq, closure_mono hsub hmem]
+  have hsτ : ∀ t ∈ Set.Icc t₀ τ, γ t ∈ s := by grind
+  have hBgt : ∀ t ∈ B, τ < t := by grind
+  -- `t₁` satisfies `τ < t₁` and `Set.Ico τ t₁ ⊆ γ ⁻¹' s`
+  obtain ⟨t₁, ht₁, ht₁'⟩ := exists_Ico_subset_of_mem_nhds (hs.preimage hγ |>.mem_nhds hKτ.1)
+    ⟨t, hBgt t htB⟩
+  -- `τ₁` satisfies `τ₁ ∈ B` and `τ₁ < t₁`
+  obtain ⟨τ₁, hτ₁B, hτ₁'⟩ := exists_lt_of_csInf_lt hBne ht₁
+  have : ∀ t' ∈ Set.Icc t₀ τ₁, γ t' ∈ s := by
+    intro t' ⟨ht'₁, ht'₂⟩
+    rcases le_or_gt t' τ with hle | hgt
+    · grind
+    · exact ht₁' ⟨hgt.le, lt_of_le_of_lt ht'₂ hτ₁'⟩
+  grind
+
+theorem continuity_method' {γ : ι → α} {p : Set α} {s : Set α} (hs : IsOpen s) (hp : IsClosed p)
+    (hsp : p ⊆ s) (hγ : Continuous γ) (ht₀ : γ t₀ ∈ p)
+    (h : ∀ t ∈ Set.Ici t₀, (∀ t' ∈ Set.Icc t₀ t, γ t' ∈ s) → γ t ∈ p)
+    {t : ι} (ht : t₀ ≤ t) :
+    γ t ∈ p := by
+  suffices γ t ∈ s ∩ p from Set.mem_of_mem_inter_right this
+  refine continuity_method hs hγ ht₀ (hsp ht₀) ?_ h ht
+  convert hp
+  simp [hsp]
+
+theorem IsLyapunovOn.isInvariantOn {δ : ℝ} (h_lya : IsLyapunovOn v Φ s) (hs : IsOpen s)
+    (hΦ' : ∀ x, Continuous (Φ · x))
+    (hv : IsClosed {p | v p ≤ δ ∧ p ∈ s}) (h_id : ∀ x, Φ t₀ x = x) :
+    IsInvariantOn Φ {p | v p ≤ δ ∧ p ∈ s} (Set.Ici t₀) := by
+  rw [isInvariantOn_iff]
+  intro x ⟨hx₁, hx₂⟩ t (ht : t₀ ≤ t)
+  simp only [Set.mem_ofPred_eq]
+  rw [and_comm]
+  have ht₀ : v (Φ t₀ x) ≤ δ := by rwa [h_id]
+  have ht₀' : Φ t₀ x ∈ s := by rwa [h_id]
+  have h_closed : IsClosed (s ∩ {x | v x ≤ δ}) := by
+    convert hv
+    ext; simp [and_comm]
+  refine continuity_method hs (hΦ' x) ht₀ ht₀' h_closed ?_ ht
+  intro t (ht : t₀ ≤ t) h
+  have := @h_lya.antitone x t₀ t ht₀' (h t (by simp [ht])) ht
+  simp only [Set.mem_ofPred_eq, ge_iff_le]
+  grw [this, ht₀]
+
+end ContinuityMethod
+
+variable [Preorder ι] [FirstCountableTopology E]
 
 /-- Lyapunov stability for time-independent Lyapunov functions.
 
 Version for stability of subsets and local Lyapunov functions. -/
-theorem IsLyapunovOn.isStableOn_nhdsSet (h_lya : IsLyapunovOn v Φ s) (h_cpt : IsCompact s)
+theorem IsLyapunovOn'.isStableOn_nhdsSet (h_lya : IsLyapunovOn' v Φ s) (h_cpt : IsCompact s)
     (hs : ∀ x ∈ s, ∀ t ∈ Set.Ici t₀, Φ t x ∈ s)
     (hvx₀ : ∀ x, v x = 0 ↔ x ∈ s')
     (h_id : ∀ x, Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_subset : { p | v p ≤ δ₀ } ⊆ s) :
@@ -253,13 +382,13 @@ theorem IsLyapunovOn.isStableOn_nhdsSet (h_lya : IsLyapunovOn v Φ s) (h_cpt : I
   simp only [Set.mem_ofPred_eq]
   have hx0 : Φ t₀ x ∈ s := hs _ hx' _ (by simp)
   have hxt : Φ t x ∈ s := hs _ hx' _ ht
-  grw [h_lya.antitone hx0 hxt ht, h_id x, hx]
+  grw [h_lya.antitone hx' hx0 hxt ht, h_id x, hx]
   exact Std.min_le_left
 
 /-- Lyapunov stability for time-independent Lyapunov functions.
 
 Version for stability of points and local Lyapunov functions. -/
-theorem IsLyapunovOn.isStableOn_nhds (h_lya : IsLyapunovOn v Φ s) (h_cpt : IsCompact s)
+theorem IsLyapunovOn'.isStableOn_nhds (h_lya : IsLyapunovOn' v Φ s) (h_cpt : IsCompact s)
     (hs : ∀ x ∈ s, ∀ t ∈ Set.Ici t₀, Φ t x ∈ s)
     (hvx₀ : ∀ x, v x = 0 ↔ x = x₀)
     (h_id : ∀ x, Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_subset : { p | v p ≤ δ₀ } ⊆ s) :
@@ -268,11 +397,45 @@ theorem IsLyapunovOn.isStableOn_nhds (h_lya : IsLyapunovOn v Φ s) (h_cpt : IsCo
 
 /-- Lyapunov stability for time-independent Lyapunov functions.
 
+Version for stability of subsets and local Lyapunov functions. -/
+theorem IsLyapunovOnIn.isStableOn_nhdsSet (h_lya : IsLyapunovOnIn v Φ s (Set.Ici t₀))
+    (h_cpt : IsCompact s) (hvx₀ : ∀ x, v x = 0 ↔ x ∈ s')
+    (h_id : ∀ x, Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_subset : { p | v p ≤ δ₀ } ⊆ s) :
+    (𝓝ˢ s').IsStableOn Φ (Set.Ici t₀) := by
+  have h_cpt' : IsCompact { p | v p ≤ δ₀ } := by
+    apply h_cpt.of_isClosed_subset _ h_subset
+    refine isClosed_le h_lya.cont continuous_const
+  apply (hasBasis_nhdsSet_setOf_le h_lya.cont h_lya.pos hvx₀ hδ₀ h_cpt').isStableOn
+  intro δ hδ
+  use min δ δ₀, lt_min hδ hδ₀
+  intro t (ht : t₀ ≤ t) x (hx : v x ≤ min δ δ₀)
+  have hx' : x ∈ s := by
+    apply h_subset
+    simp only [Set.mem_ofPred_eq]
+    grw [hx]
+    exact Std.min_le_right
+  simp only [Set.mem_ofPred_eq]
+  grw [h_lya.antitone x hx' t₀ (by simp) t (by simp [ht]) ht, h_id x, hx]
+  exact Std.min_le_left
+
+/-- Lyapunov stability for time-independent Lyapunov functions.
+
+Version for stability of points and local Lyapunov functions. -/
+theorem IsLyapunovOnIn.isStableOn_nhds (h_lya : IsLyapunovOnIn v Φ s (Set.Ici t₀))
+    (h_cpt : IsCompact s)
+    (hvx₀ : ∀ x, v x = 0 ↔ x = x₀)
+    (h_id : ∀ x, Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_subset : { p | v p ≤ δ₀ } ⊆ s) :
+    (𝓝 x₀).IsStableOn Φ (Set.Ici t₀) := by
+  simpa using h_lya.isStableOn_nhdsSet (s' := {x₀}) h_cpt (by simp [hvx₀]) h_id hδ₀ h_subset
+
+/-- Lyapunov stability for time-independent Lyapunov functions.
+
 Version for stability of a point and global Lyapunov functions. -/
 theorem IsLyapunov.isStableOn_nhdsSet (h_lya : IsLyapunov v Φ) (hvx₀ : ∀ x, v x = 0 ↔ x ∈ s')
     (h_id : ∀ x, Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_cpt : IsCompact { p | v p ≤ δ₀ }) :
     (𝓝ˢ s').IsStableOn Φ (Set.Ici t₀) := by
-  refine (h_lya.isLyapunovOn { p | v p ≤ δ₀ }).isStableOn_nhdsSet h_cpt ?_ hvx₀ h_id hδ₀ (le_refl _)
+  refine (h_lya.isLyapunovOn' { p | v p ≤ δ₀ }).isStableOn_nhdsSet h_cpt ?_ hvx₀ h_id hδ₀
+    (le_refl _)
   intro x (hx : v x ≤ δ₀) t (ht : t₀ ≤ t)
   simp only [Set.mem_ofPred_eq]
   grw [h_lya.antitone x ht, h_id x, hx]
@@ -283,7 +446,7 @@ Version for stability of a point and global Lyapunov functions. -/
 theorem IsLyapunov.isStableOn_nhds (h_lya : IsLyapunov v Φ) (hvx₀ : ∀ x, v x = 0 ↔ x = x₀)
     (h_id : ∀ x, Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_cpt : IsCompact { p | v p ≤ δ₀ }) :
     (𝓝 x₀).IsStableOn Φ (Set.Ici t₀) := by
-  refine (h_lya.isLyapunovOn { p | v p ≤ δ₀ }).isStableOn_nhds h_cpt ?_ hvx₀ h_id hδ₀ (le_refl _)
+  refine (h_lya.isLyapunovOn' { p | v p ≤ δ₀ }).isStableOn_nhds h_cpt ?_ hvx₀ h_id hδ₀ (le_refl _)
   intro x (hx : v x ≤ δ₀) t (ht : t₀ ≤ t)
   simp only [Set.mem_ofPred_eq]
   grw [h_lya.antitone x ht, h_id x, hx]
@@ -294,7 +457,7 @@ section Continuous
 
 variable [NormedAddCommGroup E]
 
-variable {f : E → E} {Φ : ℝ → E → E} {v : E → ℝ} (s : Set E)
+variable {f : E → E} {Φ : ℝ → E → E} {v : E → ℝ} {s : Set E}
 
 /-- A non-negative differentiable function with decreasing derivative along the flow is a Lyapunov
 function for that flow. -/
@@ -307,47 +470,121 @@ theorem isLyapunov_of_deriv
   cont := h_cont
   antitone := fun x ↦ antitone_of_deriv_nonpos (h_diff x) (h_deriv x)
 
+theorem isLyapunovOn'_of_deriv
+    (hv : ∀ x, 0 ≤ v x)
+    (hv_cont : Continuous v) (h_diff : ∀ x, Differentiable ℝ (v <| Φ · x))
+    (h_deriv : ∀ x ∈ s, deriv (v <| Φ · x) ≤ 0) :
+    IsLyapunovOn' v Φ s where
+  pos := hv
+  cont := hv_cont
+  antitone := by
+    intro x t₀ t₁ hx ht₀ ht₁ ht
+    have : Antitone (v <| Φ · x) := by
+      apply antitone_of_deriv_nonpos (h_diff x)
+      intro t
+      apply h_deriv x hx
+    exact this ht
+
+theorem isLyapunovOnIn_of_deriv {δ₀ : ℝ} (hΦ : ∀ x, Φ 0 x = x)
+    (hv : ∀ x, 0 ≤ v x)
+    (hv_cont : Continuous v) (h_diff : ∀ x, Differentiable ℝ (v <| Φ · x))
+    (h_deriv : ∀ x, v x ≤ δ₀ → deriv (v <| Φ · x) ≤ 0) :
+    IsLyapunovOnIn v Φ { p | v p ≤ δ₀ } (Set.Ici 0) where
+  pos := hv
+  cont := hv_cont
+  antitone := by
+    intro x hx t₀ ht₀ t₁ ht₁ ht
+    have : AntitoneOn (v <| Φ · x) (Set.Ici 0) := by
+      apply antitoneOn_of_deriv_nonpos (convex_Ici 0) (h_diff x).continuous.continuousOn
+        (h_diff x).differentiableOn
+      intro t ht'
+      apply h_deriv x hx
+    exact this ht₀ ht₁ ht
+  mem x hx t ht := by
+    have : Antitone (v <| Φ · x) := by
+      apply antitone_of_deriv_nonpos (h_diff x)
+      intro t
+      apply h_deriv x hx
+    simp only [Set.mem_ofPred_eq, ge_iff_le] at ⊢ hx
+    grw [← hx]
+    nth_rewrite 2 [← hΦ x]
+    apply this ht
+
+/- Need a statement here that says the following: if `s` is open
+(and all of the assumptions of `blubbdieblubb`), for all `x ∈ s` we have that
+`fderiv ℝ v x (f x) ≤ 0`, then `IsLyapunovOn`. -/
+
+
 variable [NormedSpace ℝ E]
 
-/-theorem Flow.isLyapunovOn_of_deriv {Φ : Flow ℝ E} (hΦ : ∀ x, Differentiable ℝ (Φ · x))
-    (hv : ∀ x, 0 ≤ v x)
-    (hv_diff : Differentiable ℝ v)
-    (h_deriv : ∀ x, fderiv ℝ v x (deriv (Φ · x) 0) ≤ 0) :
-    IsLyapunovOn v Φ s where
+private theorem mem_of_fderiv {Φ : Flow ℝ E} {δ₀ : ℝ}
+    (hs : IsOpen s) (hsδ : { p | v p ≤ δ₀ } ⊆ s)
+    (hv_diff : Differentiable ℝ v) (hΦ_diff : ∀ x, Differentiable ℝ (Φ · x))
+    (h_deriv : ∀ x ∈ s, fderiv ℝ v x (deriv (Φ · x) 0) ≤ 0)
+    {x : E} (hx₁ : v x ≤ δ₀) {t : ℝ} (ht : 0 ≤ t) :
+    v (Φ t x) ≤ δ₀ := by
+  have hp_closed : IsClosed { p | v p ≤ δ₀ } := isClosed_le hv_diff.continuous (by fun_prop)
+  have hΦ0 : Φ 0 x ∈ { p | v p ≤ δ₀} := by simpa
+  apply continuity_method' hs hp_closed hsδ (hΦ_diff x).continuous hΦ0 _ ht
+  intro t₀ ht₀ ht₀'
+  suffices AntitoneOn (v <| Φ · x) (Set.Icc 0 t₀) by
+    simp only [Set.mem_ofPred_eq, ge_iff_le] at hΦ0 ⊢
+    grw [← hΦ0]
+    exact this (by grind) (by grind) (by grind)
+  have h_diff : ∀ x, Differentiable ℝ (v <| Φ · x) := by intro; fun_prop
+  apply antitoneOn_of_deriv_nonpos (convex_Icc 0 t₀) (h_diff x).continuous.continuousOn
+    (h_diff x).differentiableOn
+  intro t' ht'
+  rw [deriv_comp_flow hv_diff hΦ_diff]
+  apply h_deriv
+  apply ht₀'
+  simp at ⊢ ht'
+  grind
+
+theorem isLyapunovOnIn_of_fderiv {Φ : Flow ℝ E} {δ₀ : ℝ}
+    (hv : ∀ x, 0 ≤ v x) (hs : IsOpen s) (hsδ : { p | v p ≤ δ₀ } ⊆ s)
+    (hv_diff : Differentiable ℝ v) (hΦ : ∀ x, Differentiable ℝ (Φ · x))
+    (h_deriv : ∀ x ∈ s, fderiv ℝ v x (deriv (Φ · x) 0) ≤ 0) :
+    IsLyapunovOnIn v Φ { p | v p ≤ δ₀ } (Set.Ici 0) where
   pos := hv
   cont := hv_diff.continuous
   antitone := by
-    intro x t₀ t₁ ht₀ ht₁ ht
-    have : AntitoneOn (v <| Φ · x) (Set.Ici 0) := by
-      apply antitoneOn_of_deriv_nonpos (convex_Ici 0)
-      · exact hv_diff.comp (hΦ x) |>.continuous.continuousOn
-      · fun_prop
-      · intro x hx
-        --apply h_deriv
-        sorry
-    --specialize this t₀
-    --apply this
-    sorry-/
+    intro x (hx : v x ≤ δ₀) t₀ ht₀ t₁ ht₁ ht
+    have h_diff : ∀ x, Differentiable ℝ (v <| Φ · x) := by intro; fun_prop
+    suffices AntitoneOn (v <| Φ · x) (Set.Ici 0) from this ht₀ ht₁ ht
+    apply antitoneOn_of_deriv_nonpos (convex_Ici 0) (h_diff x).continuous.continuousOn
+      (h_diff x).differentiableOn
+    intro t ht'
+    simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at ht'
+    rw [deriv_comp_flow hv_diff hΦ]
+    apply h_deriv
+    apply hsδ
+    exact mem_of_fderiv hs hsδ hv_diff hΦ h_deriv hx ht'.le
+  mem x (hx : v x ≤ δ₀) t (ht : 0 ≤ t) := by
+    simp only [Set.mem_ofPred_eq]
+    have : x ∈ s := hsδ hx
+    exact mem_of_fderiv hs hsδ hv_diff hΦ h_deriv hx ht
+
+theorem Flow.isLyapunovOn' {Φ : Flow ℝ E} (hΦ : ∀ x, Differentiable ℝ (Φ · x))
+    (hv : ∀ x, 0 ≤ v x)
+    (hv_diff : Differentiable ℝ v)
+    (h_deriv : ∀ x ∈ s, fderiv ℝ v x (deriv (Φ · x) 0) ≤ 0)
+    (hΦs : ∀ x ∈ s, ∀ t, Φ t x ∈ s) :
+    IsLyapunovOn' v Φ s := by
+  apply isLyapunovOn'_of_deriv hv hv_diff.continuous (fun _ ↦ by fun_prop)
+  intro x hx t
+  rw [deriv_comp_flow hv_diff hΦ]
+  exact h_deriv (Φ t x) (hΦs x hx t)
 
 theorem Flow.isLyapunov {Φ : Flow ℝ E} (hΦ : ∀ x, Differentiable ℝ (Φ · x))
     (hv : ∀ x, 0 ≤ v x) (hv_diff : Differentiable ℝ v)
     (h_deriv : ∀ x, fderiv ℝ v x (deriv (Φ · x) 0) ≤ 0) :
     IsLyapunov v Φ := by
-  refine isLyapunov_of_deriv hv hv_diff.continuous ?_ ?_
-  · intro x
-    fun_prop
-  · intro x t
-    rw [deriv_comp_flow hv_diff hΦ]
-    exact h_deriv (Φ t x)
+  apply isLyapunov_of_deriv hv hv_diff.continuous (fun _ ↦ by fun_prop)
+  intro x t
+  rw [deriv_comp_flow hv_diff hΦ]
+  exact h_deriv (Φ t x)
 
 open scoped NNReal
 
-/-
-/-- Probably not needed anymore. -/
-theorem IsCompleteVectorField.isLyapunov (hf : IsCompleteVectorField (fun _ ↦ f))
-    (hf' : LocallyLipschitz f)
-    (hv : ∀ x, 0 ≤ v x) (hv_diff : Differentiable ℝ v) (h_deriv : ∀ x, fderiv ℝ v x (f x) ≤ 0) :
-    IsLyapunov v (hf.flow hf') :=
-  Flow.isLyapunov (by fun_prop) hv hv_diff (by simpa)-/
-
 end Continuous

From 09675c9680d604fb3d01903e3b1f94172dedcf9d Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Sun, 23 Aug 2026 00:52:03 +1000
Subject: [PATCH 3/8] delete file

---
 .../Analysis/ODE/GlobalExistenceBounded.lean  | 126 ------------------
 1 file changed, 126 deletions(-)
 delete mode 100644 DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceBounded.lean

diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceBounded.lean b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceBounded.lean
deleted file mode 100644
index 263f669..0000000
--- a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceBounded.lean
+++ /dev/null
@@ -1,126 +0,0 @@
-module
-
-public import Mathlib.Analysis.ODE.Basic
-import Mathlib.Analysis.ODE.Gronwall
-import Mathlib.Analysis.ODE.PicardLindelof
-import Mathlib.Analysis.ODE.ExistUnique
-
-/-!
-# Global existence for ODEs with a globally Lipschitz, bounded vector field
-
-We prove that a continuous globally Lipschitz vector field admits a global solution.
-This is a direct consequence of the construction of the Picard iteration.
-
-This file was mainly generated by Aristotle AI.
-
--/
-
-open scoped NNReal
-open Metric Set
-
-/-! ## Global existence -/
-
-section GlobalExistence
-
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
-  {f : ℝ → E → E} {C : ℝ} {K : ℝ≥0}
-
-/-- Local (in fact, on an arbitrarily large compact time interval) existence, from the
-Picard-Lindelöf theorem. -/
-theorem exists_solution_Icc (h_lip : ∀ t, LipschitzWith K (f t))
-    (h_cont : ∀ x, Continuous (f · x)) (h_bdd : ∀ t x, ‖f t x‖ ≤ C)
-    (t₀ : ℝ) (x₀ : E) (R : ℝ) (hR : 0 ≤ R) :
-    ∃ α : ℝ → E, α t₀ = x₀ ∧ ∀ t ∈ Icc (t₀ - R) (t₀ + R),
-      HasDerivWithinAt α (f t (α t)) (Icc (t₀ - R) (t₀ + R)) t := by
-  have hC : 0 ≤ C := le_trans (norm_nonneg _) (h_bdd 0 0)
-  have ht₀ : t₀ ∈ Icc (t₀ - R) (t₀ + R) := ⟨by linarith, by linarith⟩
-  have hpl : IsPicardLindelof f (tmin := t₀ - R) (tmax := t₀ + R) ⟨t₀, ht₀⟩ x₀
-      ⟨C * R, by positivity⟩ 0 ⟨C, hC⟩ K := by
-    refine ⟨fun t _ ↦ (h_lip t).lipschitzOnWith, fun x _ ↦ (h_cont x).continuousOn,
-      fun t _ x _ ↦ h_bdd t x, ?_⟩
-    change (C : ℝ) * max (t₀ + R - t₀) (t₀ - (t₀ - R)) ≤ (C * R : ℝ) - ((0 : ℝ≥0) : ℝ)
-    rw [show t₀ + R - t₀ = R by ring, show t₀ - (t₀ - R) = R by ring, max_self]
-    simp
-  exact hpl.exists_eq_forall_mem_Icc_hasDerivWithinAt₀
-
-omit [CompleteSpace E] in
-/-- Two solutions with the same initial condition agree on any open interval on which
-they are both defined. -/
-public theorem solution_eqOn_Ioo (h_lip : ∀ t, LipschitzWith K (f t))
-    {α β : ℝ → E} {t₀ a b : ℝ} (ht₀ : t₀ ∈ Ioo a b) (hαβ : α t₀ = β t₀)
-    (hα : ∀ t ∈ Ioo a b, HasDerivAt α (f t (α t)) t)
-    (hβ : ∀ t ∈ Ioo a b, HasDerivAt β (f t (β t)) t) :
-    EqOn α β (Ioo a b) :=
-  ODE_solution_unique_of_mem_Ioo (K := K) (s := fun _ ↦ univ)
-    (fun t _ ↦ (h_lip t).lipschitzOnWith) ht₀
-    (fun t ht ↦ ⟨hα t ht, trivial⟩) (fun t ht ↦ ⟨hβ t ht, trivial⟩) hαβ
-
-/-- A continuous vector field that is bounded and Lipschitz in the second variable admits a
-global fundamental solution. -/
-public theorem exists_isIntegralCurve_of_bounded (h_lip : ∀ t, LipschitzWith K (f t))
-    (h_bdd : ∀ t x, ‖f t x‖ ≤ C) (h' : Continuous f.uncurry) :
-    ∃ Φ : ℝ → E → ℝ → E, ∀ t₀ x₀, IsIntegralCurve (Φ t₀ x₀) f ∧ Φ t₀ x₀ t₀ = x₀ := by
-  have h_cont : ∀ x, Continuous (f · x) := fun x ↦
-    h'.comp (continuous_id.prodMk continuous_const)
-  -- For each initial condition and each `n : ℕ`, a solution on `[t₀ - (n+1), t₀ + (n+1)]`.
-  have H : ∀ (t₀ : ℝ) (x₀ : E) (n : ℕ), ∃ α : ℝ → E, α t₀ = x₀ ∧
-      ∀ t ∈ Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1)),
-        HasDerivWithinAt α (f t (α t)) (Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1))) t :=
-    fun t₀ x₀ n ↦ exists_solution_Icc h_lip h_cont h_bdd t₀ x₀ ((n : ℝ) + 1) (by positivity)
-  choose α hα0 hα using H
-  -- At interior times these are genuine solutions.
-  have hderiv : ∀ (t₀ : ℝ) (x₀ : E) (n : ℕ) (t : ℝ), |t - t₀| < (n : ℝ) + 1 →
-      HasDerivAt (α t₀ x₀ n) (f t (α t₀ x₀ n t)) t := by
-    intro t₀ x₀ n t ht
-    rw [abs_lt] at ht
-    obtain ⟨h1, h2⟩ := ht
-    exact (hα t₀ x₀ n t ⟨by linarith, by linarith⟩).hasDerivAt
-      (Icc_mem_nhds (by linarith) (by linarith))
-  -- Solutions for different `n` agree wherever both are defined.
-  have hagree : ∀ (t₀ : ℝ) (x₀ : E) (m n : ℕ), m ≤ n → ∀ t : ℝ, |t - t₀| < (m : ℝ) + 1 →
-      α t₀ x₀ m t = α t₀ x₀ n t := by
-    intro t₀ x₀ m n hmn t ht
-    have hmn' : (m : ℝ) ≤ (n : ℝ) := by exact_mod_cast hmn
-    have hsub : ∀ s ∈ Ioo (t₀ - ((m : ℝ) + 1)) (t₀ + ((m : ℝ) + 1)), |s - t₀| < (m : ℝ) + 1 := by
-      intro s hs
-      rw [abs_lt]
-      exact ⟨by linarith [hs.1], by linarith [hs.2]⟩
-    have hm0 : (0 : ℝ) < (m : ℝ) + 1 := by positivity
-    refine solution_eqOn_Ioo (t₀ := t₀) h_lip (a := t₀ - ((m : ℝ) + 1)) (b := t₀ + ((m : ℝ) + 1))
-      ⟨by linarith, by linarith⟩
-      ((hα0 _ _ _).trans (hα0 _ _ _).symm)
-      (fun s hs ↦ hderiv t₀ x₀ m s (hsub s hs))
-      (fun s hs ↦ hderiv t₀ x₀ n s ((hsub s hs).trans_le (by linarith))) ?_
-    rw [abs_lt] at ht
-    exact ⟨by linarith [ht.1], by linarith [ht.2]⟩
-  refine ⟨fun t₀ x₀ t ↦ α t₀ x₀ ⌈|t - t₀|⌉₊ t, fun t₀ x₀ ↦ ⟨fun t ↦ ?_, by simp [hα0]⟩⟩
-  set N : ℕ := ⌈|t - t₀|⌉₊ with hN
-  have hNle : |t - t₀| ≤ (N : ℝ) := Nat.le_ceil _
-  -- Near `t`, the constructed flow coincides with the single solution of index `N + 1`.
-  have key : ∀ s : ℝ, |s - t| < 1 / 2 → α t₀ x₀ ⌈|s - t₀|⌉₊ s = α t₀ x₀ (N + 1) s := by
-    intro s hs
-    have hst : |s - t₀| ≤ (N : ℝ) + 1 / 2 := by
-      calc |s - t₀| ≤ |s - t| + |t - t₀| := by
-            simpa using abs_sub_le s t t₀
-        _ ≤ (N : ℝ) + 1 / 2 := by linarith
-    refine hagree t₀ x₀ _ (N + 1) ?_ s ?_
-    · refine Nat.ceil_le.mpr ?_
-      push_cast
-      linarith
-    · exact lt_of_le_of_lt (Nat.le_ceil _) (by linarith)
-  have hev : (fun s ↦ α t₀ x₀ ⌈|s - t₀|⌉₊ s) =ᶠ[nhds t] α t₀ x₀ (N + 1) := by
-    have hball : ∀ᶠ s in nhds t, |s - t| < 1 / 2 := by
-      filter_upwards [Metric.ball_mem_nhds t (by norm_num : (0 : ℝ) < 1 / 2)] with s hs
-      simpa [Real.dist_eq] using hs
-    filter_upwards [hball] with s hs using key s hs
-  have hval : α t₀ x₀ N t = α t₀ x₀ (N + 1) t := by
-    simpa using key t (by norm_num)
-  have hd : HasDerivAt (α t₀ x₀ (N + 1)) (f t (α t₀ x₀ (N + 1) t)) t := by
-    refine hderiv t₀ x₀ (N + 1) t ?_
-    push_cast
-    linarith
-  change HasDerivAt (fun s ↦ α t₀ x₀ ⌈|s - t₀|⌉₊ s) (f t (α t₀ x₀ N t)) t
-  rw [hval]
-  exact hd.congr_of_eventuallyEq hev
-
-end GlobalExistence

From 6b062533207018c76be6c41a154e68d26555951c Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Sun, 23 Aug 2026 00:54:19 +1000
Subject: [PATCH 4/8] update main file

---
 DynamicalSystems.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/DynamicalSystems.lean b/DynamicalSystems.lean
index 3e47419..f118b5b 100644
--- a/DynamicalSystems.lean
+++ b/DynamicalSystems.lean
@@ -11,7 +11,8 @@ import DynamicalSystems.Mathlib.Analysis.Calculus
 import DynamicalSystems.Mathlib.Analysis.ODE.Caratheodory
 import DynamicalSystems.Mathlib.Analysis.ODE.ExistUnique
 import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistence
-import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistenceBounded
+import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistenceLinear
+import DynamicalSystems.Mathlib.Analysis.ODE.RadialTruncation
 import DynamicalSystems.Mathlib.Analysis.ODE.UniformlyLocallyLipschitz
 import DynamicalSystems.Mathlib.Dynamics.Basic
 import DynamicalSystems.Mathlib.Topology.Antitone
@@ -20,5 +21,6 @@ import DynamicalSystems.Stability.Basic
 import DynamicalSystems.Stability.Hamiltonian
 import DynamicalSystems.Stability.Example
 import DynamicalSystems.Stability.LaSalle
+import DynamicalSystems.Stability.Linearization
 import DynamicalSystems.Stability.Lyapunov
 import DynamicalSystems.Stability.RLCCircuit

From 9a0ed66c12b702fb2e7c31bce99242415f0522d9 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Sun, 23 Aug 2026 01:22:33 +1000
Subject: [PATCH 5/8] updates

---
 .../Analysis/Calculus/IsStrictLocalMax.lean   | 92 +++++++++++++++++++
 DynamicalSystems/Stability/Linearization.lean |  6 ++
 2 files changed, 98 insertions(+)
 create mode 100644 DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean

diff --git a/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean b/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean
new file mode 100644
index 0000000..5a1f156
--- /dev/null
+++ b/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean
@@ -0,0 +1,92 @@
+module
+
+public import Mathlib.Analysis.Calculus.TaylorIntegral
+
+/-! # Existence -/
+
+variable {E F : Type*}
+
+open scoped NNReal Nat
+
+variable {a b : ℝ≥0}
+
+theorem NNReal.exists_pos_mul_lt (hb : b ≠ 0) : ∃ c > 0, c * a < b := by
+  by_cases! h : a ≠ 0
+  · use b / (2 * a), by positivity
+    field_simp
+    exact one_lt_two
+  · simp only [gt_iff_lt, h, mul_zero, exists_and_right]
+    exact ⟨⟨1, zero_lt_one⟩, hb.pos⟩
+
+theorem Real.exists_pos_mul_lt {a b : ℝ} (hb : 0 < b) : ∃ c > 0, c * a < b := by
+  obtain ⟨c, hc, h⟩ := NNReal.exists_pos_mul_lt (a := a.toNNReal) (b := b.toNNReal) (by simp [hb])
+  use c, hc
+  rw [← toNNReal_lt_toNNReal_iff hb]
+  convert h
+  rw [toNNReal_mul (by norm_cast; exact hc.le)]
+  simp
+
+section NormedSpace
+
+variable [NormedAddCommGroup E] [NormedAddCommGroup F]
+
+variable [NormedSpace ℝ E] [NormedSpace ℝ F]
+
+variable {f : E → F} {x₀ x y : E} {n : ℕ}
+
+variable [CompleteSpace F]
+
+/-- *Taylor's theorem with remainder in integral form*. -/
+theorem map_eq_sum_add_integral_iteratedFDeriv (hf : ∀ (t : ℝ) (_ht : t ∈ Set.Icc 0 1),
+    ContDiffAt ℝ (n + 1) f (x₀ + t • (x - x₀))) :
+    f x = ∑ k ∈ Finset.range (n + 1), (k ! : ℝ)⁻¹ • (iteratedFDeriv ℝ k f x₀ (fun _ ↦ x - x₀)) +
+    (n ! : ℝ)⁻¹ • ∫ t in 0..1, (1 - t) ^ n •
+      iteratedFDeriv ℝ (n + 1) f (x₀ + t • (x - x₀)) (fun _ ↦ x - x₀) := by
+  convert map_add_eq_sum_add_integral_iteratedFDeriv hf
+  module
+
+end NormedSpace
+
+section InnerProductSpace
+
+variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+
+open scoped Topology
+
+variable {f : E → E} {x₀ x y : E} {n : ℕ} {δ₀ : ℝ}
+
+/-- If `-fderiv ℝ f x₀` is coercive, then there exists a neighborhood of `x₀` such that
+`inner ℝ (x - x₀) (f x) < 0` for all `x ≠ x₀` in that neighborhood. -/
+public theorem eventually_inner_neg (hf : f x₀ = 0)
+    (h : IsCoercive ((innerSL ℝ) ∘L (-fderiv ℝ f x₀))) (hdiff : DifferentiableAt ℝ f x₀) :
+    ∀ᶠ x in 𝓝 x₀, x ≠ x₀ → inner ℝ (x - x₀) (f x) < 0 := by
+  obtain ⟨C, hC, hcoer⟩ := h
+  have hev := hdiff.hasFDerivAt.isLittleO.def (c := C / 2) (by positivity)
+  filter_upwards [hev] with x hx hxx₀
+  set u : E := x - x₀ with hu
+  have hupos : 0 < ‖u‖ := by simpa [hu, sub_eq_zero] using hxx₀
+  have hlin : inner ℝ u ((fderiv ℝ f x₀) u) ≤ -(C * ‖u‖ * ‖u‖) := by
+    have key : C * ‖u‖ * ‖u‖ ≤ -inner ℝ ((fderiv ℝ f x₀) u) u := by
+      simpa [innerSL_apply_apply ℝ] using hcoer u
+    grind [real_inner_comm]
+  have hrem : inner ℝ u (f x - f x₀ - (fderiv ℝ f x₀) u) ≤ C / 2 * ‖u‖ * ‖u‖ := by
+    calc inner ℝ u (f x - f x₀ - (fderiv ℝ f x₀) u)
+        ≤ ‖u‖ * ‖f x - f x₀ - (fderiv ℝ f x₀) u‖ := real_inner_le_norm _ _
+      _ ≤ ‖u‖ * (C / 2 * ‖u‖) := by gcongr
+      _ = C / 2 * ‖u‖ * ‖u‖ := by ring
+  have hsplit : inner ℝ u (f x) =
+      inner ℝ u ((fderiv ℝ f x₀) u) + inner ℝ u (f x - f x₀ - (fderiv ℝ f x₀) u) := by
+    rw [← inner_add_right]
+    congr 1
+    grind
+  have hpos : 0 < C / 2 * ‖u‖ * ‖u‖ := by positivity
+  grind
+
+/-- If `-fderiv ℝ f x₀` is coercive, then there exists a neighborhood of `x₀` such that
+`inner ℝ (x - x₀) (f x) < 0` for all `x ≠ x₀` in that neighborhood. -/
+public theorem exists_inner_neg (hf : f x₀ = 0) (h : IsCoercive ((innerSL ℝ) ∘L (-fderiv ℝ f x₀)))
+    (hdiff : DifferentiableAt ℝ f x₀) :
+    ∃ δ, 0 < δ ∧ ∀ x ∈ Metric.ball x₀ δ, x ≠ x₀ → inner ℝ (x - x₀) (f x) < 0 :=
+  Metric.eventually_nhds_iff.mp (eventually_inner_neg hf h hdiff)
+
+end InnerProductSpace
diff --git a/DynamicalSystems/Stability/Linearization.lean b/DynamicalSystems/Stability/Linearization.lean
index 6cd649d..443e8ca 100644
--- a/DynamicalSystems/Stability/Linearization.lean
+++ b/DynamicalSystems/Stability/Linearization.lean
@@ -10,6 +10,12 @@ public import DynamicalSystems.Stability.Example
 import Mathlib.Analysis.InnerProductSpace.Calculus
 import DynamicalSystems.Mathlib.Analysis.Calculus.IsStrictLocalMax
 
+/-! # Stability of fixed points by linearization
+
+This file proves that a fixed point `x₀` of an autonomous ODE is stable if the `-fderiv ℝ f x₀` is
+coercive, in the sense that `innerSL ℝ ∘L (-fderiv ℝ f x₀)` is a coercive bilinear form.
+-/
+
 public section
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

From 3ed214a7065c0268747103584a0c428462ce4d06 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Sun, 23 Aug 2026 01:24:17 +1000
Subject: [PATCH 6/8] updates

---
 DynamicalSystems.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/DynamicalSystems.lean b/DynamicalSystems.lean
index f118b5b..45c656b 100644
--- a/DynamicalSystems.lean
+++ b/DynamicalSystems.lean
@@ -7,7 +7,8 @@ import DynamicalSystems.InputOutput.ClosedLoop
 import DynamicalSystems.InputOutput.Dissipative
 import DynamicalSystems.InputOutput.Example
 import DynamicalSystems.InputOutput.Stability
-import DynamicalSystems.Mathlib.Analysis.Calculus
+import DynamicalSystems.Mathlib.Analysis.Calculus.Flow
+import DynamicalSystems.Mathlib.Analysis.Calculus.IsStrictLocalMax
 import DynamicalSystems.Mathlib.Analysis.ODE.Caratheodory
 import DynamicalSystems.Mathlib.Analysis.ODE.ExistUnique
 import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistence

From 2f47098fdbf998a5e7abd08fc6ce621a58388638 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Sun, 23 Aug 2026 01:26:10 +1000
Subject: [PATCH 7/8] copyright

---
 .../Mathlib/Analysis/Calculus/IsStrictLocalMax.lean          | 5 +++++
 .../Mathlib/Analysis/ODE/GlobalExistenceLinear.lean          | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean b/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean
index 5a1f156..23c29c9 100644
--- a/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean
+++ b/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
 module
 
 public import Mathlib.Analysis.Calculus.TaylorIntegral
diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceLinear.lean b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceLinear.lean
index 0c89341..f08f432 100644
--- a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceLinear.lean
+++ b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistenceLinear.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
 module
 
 public import Mathlib.Analysis.ODE.Basic

From a6635399d20b71dcacfc585c0611c2f202577797 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Mon, 24 Aug 2026 10:48:53 +1000
Subject: [PATCH 8/8] fixes

---
 .../Analysis/Calculus/IsStrictLocalMax.lean   | 26 +++++++++----------
 DynamicalSystems/Stability/Lyapunov.lean      | 20 ++++++++++++++
 2 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean b/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean
index 23c29c9..9a8d6cf 100644
--- a/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean
+++ b/DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean
@@ -69,23 +69,23 @@ public theorem eventually_inner_neg (hf : f x₀ = 0)
   have hev := hdiff.hasFDerivAt.isLittleO.def (c := C / 2) (by positivity)
   filter_upwards [hev] with x hx hxx₀
   set u : E := x - x₀ with hu
-  have hupos : 0 < ‖u‖ := by simpa [hu, sub_eq_zero] using hxx₀
-  have hlin : inner ℝ u ((fderiv ℝ f x₀) u) ≤ -(C * ‖u‖ * ‖u‖) := by
-    have key : C * ‖u‖ * ‖u‖ ≤ -inner ℝ ((fderiv ℝ f x₀) u) u := by
-      simpa [innerSL_apply_apply ℝ] using hcoer u
-    grind [real_inner_comm]
-  have hrem : inner ℝ u (f x - f x₀ - (fderiv ℝ f x₀) u) ≤ C / 2 * ‖u‖ * ‖u‖ := by
+  have hle : inner ℝ u (f x - f x₀ - (fderiv ℝ f x₀) u) ≤ C / 2 * ‖u‖ * ‖u‖ := by
     calc inner ℝ u (f x - f x₀ - (fderiv ℝ f x₀) u)
         ≤ ‖u‖ * ‖f x - f x₀ - (fderiv ℝ f x₀) u‖ := real_inner_le_norm _ _
       _ ≤ ‖u‖ * (C / 2 * ‖u‖) := by gcongr
       _ = C / 2 * ‖u‖ * ‖u‖ := by ring
-  have hsplit : inner ℝ u (f x) =
-      inner ℝ u ((fderiv ℝ f x₀) u) + inner ℝ u (f x - f x₀ - (fderiv ℝ f x₀) u) := by
-    rw [← inner_add_right]
-    congr 1
-    grind
-  have hpos : 0 < C / 2 * ‖u‖ * ‖u‖ := by positivity
-  grind
+  calc
+    _ = inner ℝ u ((fderiv ℝ f x₀) u) + inner ℝ u (f x - f x₀ - (fderiv ℝ f x₀) u) := by
+      simp [← inner_add_right, hf]
+    _ ≤ -(C * ‖u‖ * ‖u‖) + C / 2 * ‖u‖ * ‖u‖ := by
+      gcongr
+      suffices C * ‖u‖ * ‖u‖ ≤ -inner ℝ ((fderiv ℝ f x₀) u) u by grind [real_inner_comm]
+      simpa [innerSL_apply_apply ℝ] using hcoer u
+    _ = - C / 2 * ‖u‖ * ‖u‖ := by grind
+    _ < _ := by
+      suffices 0 < C / 2 * ‖u‖ * ‖u‖ by grind
+      have : 0 < ‖u‖ := by simpa [hu, sub_eq_zero] using hxx₀
+      positivity
 
 /-- If `-fderiv ℝ f x₀` is coercive, then there exists a neighborhood of `x₀` such that
 `inner ℝ (x - x₀) (f x) < 0` for all `x ≠ x₀` in that neighborhood. -/
diff --git a/DynamicalSystems/Stability/Lyapunov.lean b/DynamicalSystems/Stability/Lyapunov.lean
index fc37c56..a754136 100644
--- a/DynamicalSystems/Stability/Lyapunov.lean
+++ b/DynamicalSystems/Stability/Lyapunov.lean
@@ -397,6 +397,26 @@ theorem IsLyapunovOn'.isStableOn_nhds (h_lya : IsLyapunovOn' v Φ s) (h_cpt : Is
 
 /-- Lyapunov stability for time-independent Lyapunov functions.
 
+Version for stability of subsets and local Lyapunov functions. -/
+theorem IsLyapunovOn.isStableOn_nhdsSet (h_lya : IsLyapunovOn v Φ s) (h_cpt : IsCompact s)
+    (hs : ∀ x ∈ s, ∀ t ∈ Set.Ici t₀, Φ t x ∈ s)
+    (hvx₀ : ∀ x, v x = 0 ↔ x ∈ s')
+    (h_id : ∀ x, Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_subset : { p | v p ≤ δ₀ } ⊆ s) :
+    (𝓝ˢ s').IsStableOn Φ (Set.Ici t₀) :=
+  h_lya.isLyapunovOn'.isStableOn_nhdsSet h_cpt hs hvx₀ h_id hδ₀ h_subset
+
+/-- Lyapunov stability for time-independent Lyapunov functions.
+
+Version for stability of points and local Lyapunov functions. -/
+theorem IsLyapunovOn.isStableOn_nhds (h_lya : IsLyapunovOn v Φ s) (h_cpt : IsCompact s)
+    (hs : ∀ x ∈ s, ∀ t ∈ Set.Ici t₀, Φ t x ∈ s)
+    (hvx₀ : ∀ x, v x = 0 ↔ x = x₀)
+    (h_id : ∀ x, Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_subset : { p | v p ≤ δ₀ } ⊆ s) :
+    (𝓝 x₀).IsStableOn Φ (Set.Ici t₀) := by
+  simpa using h_lya.isStableOn_nhdsSet (s' := {x₀}) h_cpt hs (by simp [hvx₀]) h_id hδ₀ h_subset
+
+/-- Lyapunov stability for time-independent Lyapunov functions.
+
 Version for stability of subsets and local Lyapunov functions. -/
 theorem IsLyapunovOnIn.isStableOn_nhdsSet (h_lya : IsLyapunovOnIn v Φ s (Set.Ici t₀))
     (h_cpt : IsCompact s) (hvx₀ : ∀ x, v x = 0 ↔ x ∈ s')