OAI/MathematicalPhysics/Transonic/Shooting/AxisFamilyDisk.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SepticProfile.AxisFamily.exists_continuous_remainder_disk line 15

   Source documentation

   The nonresonant sonic remainder is constructed continuously on the entire closed shooting chart, with one positive complex radius.

   theorem exists_continuous_remainder_disk :
       ∃ r : ℝ, 0<r ∧ ∃ f : Parameter → analyticDisk, Continuous f ∧
         (∀ a, f a ∈ realDisk) ∧
         (∀ a, extend (f a : DiskMap) 0=0) ∧
         ∀ a z, z ∈ ball (0:ℂ) 1 →
           denominator a ((r:ℂ)*z,extend (f a:DiskMap) z) ≠ 0 ∧
           z*deriv (extend (f a:DiskMap)) z+(2:ℂ)*extend (f a:DiskMap) z=
             (r:ℂ)*z*H a ((r:ℂ)*z,extend (f a:DiskMap) z) := by
   …

   Mentions: OAI.SepticProfile.AxisFamily.denominator, OAI.SepticProfile.AxisFamily.H