OAI/MathematicalPhysics/Transonic/Exterior/Conv.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.ExteriorJet.relative line 10
  2. def OAI.SepticProfile.ExteriorJet.pairValue line 11
  3. def OAI.SepticProfile.ExteriorJet.squareRatio line 12
  4. def OAI.SepticProfile.ExteriorJet.powerRatio line 14
  5. def OAI.SepticProfile.ExteriorJet.squareRRatio line 15
  6. lemma OAI.SepticProfile.ExteriorJet.pairValue_eq line 18
  7. lemma OAI.SepticProfile.ExteriorJet.relative_self line 25
  8. lemma OAI.SepticProfile.ExteriorJet.relative_step line 28
  9. lemma OAI.SepticProfile.ExteriorJet.squareRatio_sum line 33
  10. lemma OAI.SepticProfile.ExteriorJet.powerRatio_square line 41
  11. lemma OAI.SepticProfile.ExteriorJet.powerRatio_cube line 46
  12. lemma OAI.SepticProfile.ExteriorJet.powerRatio_fourth line 61
  13. lemma OAI.SepticProfile.ExteriorJet.squareRRatio_sum line 78
  14. lemma OAI.SepticProfile.ExteriorJet.powerRatio_low line 87
  15. def OAI.SepticProfile.ExteriorJet.ratioStep line 97

    Source documentation

    The normalized scalar recurrence used for the exterior jet enclosure. Unlike unnormalized coefficient arithmetic it cancels the largest jet scale.

    def ratioStep (sigma kappa c : ℝ) (n : ℕ) (sq cu qu : ℕ → ℝ) (sr : ℝ) : ℝ :=
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa

  16. lemma OAI.SepticProfile.ExteriorJet.normalized_recurrence line 106