OAI/MathematicalPhysics/Transonic/Shooting/ODEGlue.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.ODEGlue.join line 12
2. lemma OAI.SepticProfile.ODEGlue.join_left line 14
3. lemma OAI.SepticProfile.ODEGlue.join_right line 18
4. theorem OAI.SepticProfile.ODEGlue.hasDerivWithinAt_join line 28

   Source documentation

   Joining ODE arcs at the same value gives an ODE arc, including the joining point. No uniqueness or a missing continuation is assumed.

   theorem hasDerivWithinAt_join {a c b : ℝ} (hac : a≤c) (hcb : c≤b)
       {f : ℝ → ℝ → ℝ} {u v : ℝ → ℝ}
       (hu : ∀ t ∈ Icc a c, HasDerivWithinAt u (f t (u t)) (Icc a c) t)
       (hv : ∀ t ∈ Icc c b, HasDerivWithinAt v (f t (v t)) (Icc c b) t)
       (h : u c=v c) (t : ℝ) (ht : t ∈ Icc a b) :
       HasDerivWithinAt (join c u v) (f t (join c u v t)) (Icc a b) t := by
   …

   Mentions: OAI.SepticProfile.ODEGlue.join

5. theorem OAI.SepticProfile.ODEGlue.smooth_arc line 67

   Source documentation

   Smoothness of an arc follows from its actual nonsingular smooth field.

   theorem smooth_arc {a b : ℝ} {f : ℝ → ℝ → ℝ} {u : ℝ → ℝ} {s : Set ℝ}
       (hf : ContDiffOn ℝ ∞ (Function.uncurry f) (Icc a b ×ˢ s))
       (hu : ∀ t ∈ Icc a b, HasDerivWithinAt u (f t (u t)) (Icc a b) t)
       (hr : MapsTo u (Icc a b) s) : ContDiffOn ℝ ∞ u (Icc a b) :=
   …