OAI/MathematicalPhysics/Transonic/Shooting/SourceFamilyDisk.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SepticProfile.SourceFamily.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 (J : FamilyJet) :
       ∃ 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 J a ((r:ℂ)*z,extend (f a:DiskMap) z) ≠ 0 ∧
           z*deriv (extend (f a:DiskMap)) z+((76-rho a:ℝ):ℂ)*extend (f a:DiskMap) z=
             (r:ℂ)*z*H J a ((r:ℂ)*z,extend (f a:DiskMap) z) := by
   …

   Mentions: OAI.SepticProfile.SourceFamily.FamilyJet, OAI.SepticProfile.SourceFamily.Parameter, OAI.SepticProfile.SourceFamily.denominator, OAI.SepticProfile.SourceFamily.rho, OAI.SepticProfile.SourceFamily.H