OAI/MathematicalPhysics/Transonic/Shooting/FamilyC1.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SepticProfile.FamilyC1.V line 11
  2. structure OAI.SepticProfile.FamilyC1.Data line 16

    Source documentation

    Continuous dependence of a polynomial family and its complex differential. This is used only to obtain the uniform nonlinear bounds in the source sonic contraction, not as a replacement for construction of the shooting family.

    structure Data (h : A → V → ℂ) where
…

    Mentions: OAI.SepticProfile.FamilyC1.V

  3. def OAI.SepticProfile.FamilyC1.Data.const line 25
  4. def OAI.SepticProfile.FamilyC1.Data.fst line 31
  5. def OAI.SepticProfile.FamilyC1.Data.snd line 37
  6. def OAI.SepticProfile.FamilyC1.Data.add line 43
  7. def OAI.SepticProfile.FamilyC1.Data.neg line 49
  8. def OAI.SepticProfile.FamilyC1.Data.sub line 55
  9. def OAI.SepticProfile.FamilyC1.Data.mul line 61
  10. def OAI.SepticProfile.FamilyC1.Data.pow line 67
  11. lemma OAI.SepticProfile.FamilyC1.exists_uniform_den_radius line 77

    Source documentation

    The denominator cannot vanish in a uniform tube about the compact family of origin points. No global zero-free condition is assumed.

    lemma exists_uniform_den_radius [CompactSpace A] {d : A → V → ℂ}
    (hd : Continuous (fun p : A × V => d p.1 p.2)) (hn : ∀ a, d a 0 ≠ 0) :
    ∃ R : ℝ, 0 < R ∧ ∀ a v, v ∈ closedBall 0 R → d a v ≠ 0 := by
…

    Mentions: OAI.SepticProfile.FamilyC1.V