OAI/Analysis/MassAction/ODEGlobal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.exists_global_of_compatible_curves line 17

   Source documentation

   A compatible sequence of curves on intervals with unbounded right endpoints has a global extension. Agreement on left half-lines preserves the germ at zero.

   theorem exists_global_of_compatible_curves
       {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
       {f : E → E} {a : ℝ} (b : ℕ → ℝ) (hb : Monotone b)
       (hunbounded : ∀ t : ℝ, ∃ n : ℕ, t < b n)
       (x : ℕ → ℝ → E)
       (hcompat : ∀ n, EqOn (x (n + 1)) (x n) (Iic (b n)))
       (hderiv : ∀ n, ∀ t ∈ Icc a (b n), HasDerivAt (x n) (f (x n t)) t) :
       ∃ g : ℝ → E, (∀ n, EqOn g (x n) (Iic (b n))) ∧
         ∀ t, a ≤ t → HasDerivAt g (f (g t)) t := by
   …

2. theorem OAI.Problem326.exists_global_solution_of_compact_trapping line 53

   Source documentation

   Compact trapping turns local existence into a global forward solution. Only trapping of finite, closed-interval solutions is assumed.

   theorem exists_global_solution_of_compact_trapping
       {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
       {f : E → E} (hf : ContDiff ℝ 1 f) {K : Set E} (hK : IsCompact K)
       (htrap : ∀ z ∈ K, ∀ S : ℝ, 0 ≤ S → ∀ x : ℝ → E,
         x 0 = z →
         (∀ t ∈ Icc (0 : ℝ) S, HasDerivAt x (f (x t)) t) →
         ∀ t ∈ Icc (0 : ℝ) S, x t ∈ K)
       {z : E} (hz : z ∈ K) :
       ∃ g : ℝ → E, g 0 = z ∧
         (∀ t : ℝ, 0 ≤ t → HasDerivAt g (f (g t)) t) ∧
         ∀ t : ℝ, 0 ≤ t → g t ∈ K := by
   …