OAI/MathematicalPhysics/Transonic/Profile/FiniteSourceProfile.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.SonicShooting.MatchedPair.beta line 13
  2. def OAI.SepticProfile.SonicShooting.MatchedPair.radius line 14
  3. def OAI.SepticProfile.SonicShooting.MatchedPair.sonicU line 15
  4. def OAI.SepticProfile.SonicShooting.MatchedPair.velocity line 16
  5. lemma OAI.SepticProfile.SonicShooting.MatchedPair.beta_bounds line 18
  6. lemma OAI.SepticProfile.SonicShooting.MatchedPair.radius_bounds line 20
  7. lemma OAI.SepticProfile.SonicShooting.sonicSpeed_bounds line 23
  8. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_zero line 28
  9. lemma OAI.SepticProfile.SonicShooting.MatchedPair.sonicU_smooth line 33
  10. lemma OAI.SepticProfile.SonicShooting.MatchedPair.sonicU_derivative line 37
  11. lemma OAI.SepticProfile.SonicShooting.MatchedPair.sonicU_equation line 49
  12. lemma OAI.SepticProfile.SonicShooting.MatchedPair.sonicU_zero line 67
  13. lemma OAI.SepticProfile.SonicShooting.MatchedPair.sonicU_at_radius line 69
  14. lemma OAI.SepticProfile.SonicShooting.MatchedPair.exists_physical_width line 72
  15. structure OAI.SepticProfile.SonicShooting.PhysicalWidth line 105
  16. lemma OAI.SepticProfile.SonicShooting.MatchedPair.exists_physicalWidth line 112
  17. def OAI.SepticProfile.SonicShooting.PhysicalWidth.endpoint line 116
  18. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.endpoint_bounds line 118
  19. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.rescale line 124
  20. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.rescale_full line 128
  21. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.y_abs line 131
  22. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.U_abs line 135
  23. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.chart_pos line 137
  24. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.velocity_smooth line 144
  25. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.velocity_equation line 150
  26. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.velocity_abs line 159
  27. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_positive line 163
  28. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.velocity_below line 172
  29. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.recover_U line 181
  30. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.unique_sonic line 188
  31. lemma OAI.SepticProfile.SonicShooting.PhysicalWidth.sonic_slope line 202