OAI/MathematicalPhysics/Transonic/Shooting/ExteriorGermEntry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SepticProfile.SourceFamily.UniformGerm.jet_data line 13
2. lemma OAI.SepticProfile.SourceFamily.UniformGerm.exists_exterior_entry line 31

   Source documentation

   A finite Taylor sign certificate supplies a genuine positive entry point for continuation. No unverified Taylor-tail estimate is assumed.

   lemma UniformGerm.exists_exterior_entry (G : UniformGerm) (p : Parameter)
       {d w : ℝ} (hd : 0<d) (hw : 0<w)
       (hp : 0<coeff 74 (SonicJet.jet (G.realFunction p))) :
       ∃ a : ℝ, 0<a ∧ a<1 ∧ d/256*a<w ∧ d/256*a<G.radius ∧
         (lowerPoly (SonicJet.jet (G.realFunction p)) d).eval a<G.realFunction p (d/256*a) ∧
         G.realFunction p (d/256*a)<Real.sqrt (5/3) := by
   …

   Mentions: OAI.SepticProfile.SourceFamily.UniformGerm, OAI.SepticProfile.SourceFamily.Parameter, OAI.SepticProfile.SonicJet.jet