OAI/MathematicalPhysics/Transonic/Phase/Profile.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SepticProfile.GlobalProfile line 14
  2. lemma OAI.SepticProfile.globalProfile_of_exists line 31
  3. def OAI.SepticProfile.GlobalProfile.b line 35
  4. def OAI.SepticProfile.GlobalProfile.velocity line 36
  5. def OAI.SepticProfile.GlobalProfile.integrand line 37
  6. def OAI.SepticProfile.GlobalProfile.primitive line 39
  7. def OAI.SepticProfile.GlobalProfile.H line 42
  8. lemma OAI.SepticProfile.GlobalProfile.b_pos line 45
  9. lemma OAI.SepticProfile.GlobalProfile.velocity_zero line 46
  10. lemma OAI.SepticProfile.GlobalProfile.velocity_neg line 47
  11. lemma OAI.SepticProfile.GlobalProfile.velocity_smooth line 50
  12. lemma OAI.SepticProfile.GlobalProfile.pole_pos line 56
  13. lemma OAI.SepticProfile.GlobalProfile.velocity_range line 66
  14. lemma OAI.SepticProfile.GlobalProfile.integrand_smooth line 72
  15. lemma OAI.SepticProfile.GlobalProfile.primitive_derivative line 76
  16. lemma OAI.SepticProfile.GlobalProfile.primitive_smooth line 82
  17. lemma OAI.SepticProfile.GlobalProfile.H_pos line 89
  18. lemma OAI.SepticProfile.GlobalProfile.H_smooth line 91
  19. lemma OAI.SepticProfile.GlobalProfile.H_derivative line 93
  20. def OAI.SepticProfile.GlobalProfile.A line 98
  21. def OAI.SepticProfile.GlobalProfile.B line 99
  22. def OAI.SepticProfile.GlobalProfile.M0 line 100
  23. lemma OAI.SepticProfile.GlobalProfile.A_eq line 102
  24. lemma OAI.SepticProfile.GlobalProfile.B_eq line 107
  25. lemma OAI.SepticProfile.GlobalProfile.A_pos line 110
  26. lemma OAI.SepticProfile.GlobalProfile.M0_eq line 113
  27. lemma OAI.SepticProfile.GlobalProfile.M0_pos line 117