feat: linearization and global existence for linearly bounded vector fields

DynamicalSystems.lean

@@ -7,10 +7,13 @@ 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
+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
@@ -19,5 +22,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

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 :=

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)]

DynamicalSystems/Mathlib/Analysis/Calculus/IsStrictLocalMax.lean

@@ -0,0 +1,97 @@
+/-
+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
+
+/-! # 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 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
+  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. -/
+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

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