OAI/MathematicalPhysics/Transonic/Exterior/TaylorEntry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SepticProfile.ExteriorPolynomial.taylor_jet_littleO line 11
2. lemma OAI.SepticProfile.ExteriorPolynomial.enters_above_trunc73 line 36

   Source documentation

   The nonresonant positive 74th source coefficient supplies the entry above P73. This is not an assumed Taylor-tail sign.

   lemma enters_above_trunc73 (f : ℝ → ℝ) (hf : ContDiffAt ℝ 74 f 0)
       (hp : 0<PowerSeries.coeff 74 (SonicJet.jet f)) :
       ∀ᶠ x in 𝓝 (0:ℝ), 0<x → (PowerSeries.trunc 74 (SonicJet.jet f)).eval x<f x := by
   …

   Mentions: OAI.SepticProfile.SonicJet.jet