OAI/MathematicalPhysics/Transonic/Shooting/SourceFamilyJets.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SepticProfile.SourceFamily.Parameter line 11
  2. lemma OAI.SepticProfile.SourceFamily.continuous_a line 13
  3. lemma OAI.SepticProfile.SourceFamily.continuous_e line 14
  4. lemma OAI.SepticProfile.SourceFamily.continuous_d line 15
  5. lemma OAI.SepticProfile.SourceFamily.continuous_k line 16
  6. lemma OAI.SepticProfile.SourceFamily.continuous_sigma line 18
  7. lemma OAI.SepticProfile.SourceFamily.continuous_kappa line 24
  8. lemma OAI.SepticProfile.SourceFamily.continuous_slope line 30
  9. lemma OAI.SepticProfile.SourceFamily.continuous_ratio line 34
  10. def OAI.SepticProfile.SourceFamily.sig line 37
  11. def OAI.SepticProfile.SourceFamily.kap line 38
  12. def OAI.SepticProfile.SourceFamily.slp line 39
  13. def OAI.SepticProfile.SourceFamily.rho line 40
  14. def OAI.SepticProfile.SourceFamily.cst line 41
  15. structure OAI.SepticProfile.SourceFamily.FamilyJet line 43
  16. theorem OAI.SepticProfile.SourceFamily.exists_familyJet line 58

    Source documentation

    One continuous finite jet of order76 works on the whole chart. In particular this is not a separate choice of polynomial at every parameter.

    theorem exists_familyJet : Nonempty FamilyJet := by
…

    Mentions: OAI.SepticProfile.SourceFamily.FamilyJet

  17. lemma OAI.SepticProfile.SourceFamily.indicial_shift line 65
  18. lemma OAI.SepticProfile.SourceFamily.specialize_prefP line 71
  19. lemma OAI.SepticProfile.SourceFamily.specialize_denQuotP line 74
  20. lemma OAI.SepticProfile.SourceFamily.specialize_transP line 80
  21. lemma OAI.SepticProfile.SourceFamily.specialize_linP line 84