OAI/Analysis/MassAction/ODEConcatenation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.hasDerivAt_join line 16

   Source documentation

   Two differentiable curves with the same value and derivative at a joining time can be glued there without losing differentiability.

   theorem hasDerivAt_join
       {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
       {x y : ℝ → E} {c : ℝ} {v : E}
       (hx : HasDerivAt x v c) (hy : HasDerivAt y v c) (hxy : x c = y c) :
       HasDerivAt (fun t => if t ≤ c then x t else y t) v c := by
   …

2. theorem OAI.Problem326.hasDerivAt_join_on_Icc line 31

   Source documentation

   Concatenation of autonomous ODE solutions. Ordinary derivatives at the end points avoid a separate endpoint extension argument.

   theorem hasDerivAt_join_on_Icc
       {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
       {f : E → E} {x y : ℝ → E} {a c b : ℝ}
       (hx : ∀ t ∈ Icc a c, HasDerivAt x (f (x t)) t)
       (hy : ∀ t ∈ Icc c b, HasDerivAt y (f (y t)) t)
       (hxy : x c = y c) :
       ∀ t ∈ Icc a b,
         HasDerivAt (fun s => if s ≤ c then x s else y s)
           (f (if t ≤ c then x t else y t)) t := by
   …

3. theorem OAI.Problem326.exists_extend_solution_on_Icc line 60

   Source documentation

   A uniform local existence statement extends a finite solution by one fixed step whenever its endpoint remains in the allowed set.

   theorem exists_extend_solution_on_Icc
       {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
       {f : E → E} {K : Set E} {T a c : ℝ} {x : ℝ → E}
       (hlocal : ∀ z ∈ K, ∃ y : ℝ → E, y 0 = z ∧
         ∀ t ∈ Icc (0 : ℝ) T, HasDerivAt y (f (y t)) t)
       (hx : ∀ t ∈ Icc a c, HasDerivAt x (f (x t)) t)
       (hxc : x c ∈ K) :
       ∃ x' : ℝ → E, EqOn x' x (Iic c) ∧
         ∀ t ∈ Icc a (c + T), HasDerivAt x' (f (x' t)) t := by
   …