OAI/MathematicalPhysics/Transonic/Profile/Equations.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Relativistic self-similar profile equations

The sonic change of variables and compatibility conditions for the septic wave profile, following the relativistic profile construction of Buckmaster and Chen.

  1. def OAI.SepticProfile.velocityToU line 24
  2. def OAI.SepticProfile.profileDenom line 26
  3. def OAI.SepticProfile.profileNumer line 29
  4. def OAI.SepticProfile.sonicDenom line 32
  5. def OAI.SepticProfile.sonicNumer line 34
  6. theorem OAI.SepticProfile.hasDerivAt_velocityToU line 37
  7. theorem OAI.SepticProfile.transformed_profile_equation line 45
  8. theorem OAI.SepticProfile.sonicDenom_at_sonic line 56
  9. theorem OAI.SepticProfile.sonicNumer_at_sonic line 60
  10. theorem OAI.SepticProfile.sonic_radius_necessary line 66
  11. theorem OAI.SepticProfile.sonic_no_slope_off_selected_radius line 77
  12. theorem OAI.SepticProfile.no_rhs_on_sonic_neighborhood line 85
  13. theorem OAI.SepticProfile.hasDerivAt_sonicDenom line 100
  14. theorem OAI.SepticProfile.hasDerivAt_sonicNumer line 109
  15. theorem OAI.SepticProfile.sonic_crossing_slope_equation line 124
  16. theorem OAI.SepticProfile.transformed_equation_of_source line 144
  17. theorem OAI.SepticProfile.no_finite_sonic_rhs_limit line 153
  18. theorem OAI.SepticProfile.not_continuousAt_sonic_quotient line 180
  19. theorem OAI.SepticProfile.axis_slope_necessary line 205
  20. theorem OAI.SepticProfile.radial_velocity_contDiff line 236
  21. theorem OAI.SepticProfile.source_axis_slope line 241
  22. def OAI.SepticProfile.ell line 256
  23. def OAI.SepticProfile.sonicSpeed line 257
  24. def OAI.SepticProfile.sonicRadius line 258
  25. theorem OAI.SepticProfile.source_parameter_bounds line 260
  26. theorem OAI.SepticProfile.source_no_rhs_on_sonic_neighborhood line 302
  27. def OAI.SepticProfile.q line 313
  28. def OAI.SepticProfile.slopeA line 315
  29. def OAI.SepticProfile.slopeB line 318
  30. def OAI.SepticProfile.slopeC line 321
  31. def OAI.SepticProfile.resonancePolynomial line 323
  32. lemma OAI.SepticProfile.sonicSpeed_sq line 326
  33. lemma OAI.SepticProfile.sonicRadius_eq line 334
  34. lemma OAI.SepticProfile.source_beta_lt_two line 338
  35. lemma OAI.SepticProfile.slope_coefficients line 347
  36. lemma OAI.SepticProfile.source_coefficients_positive line 365
  37. lemma OAI.SepticProfile.source_slope_separation line 387
  38. def OAI.SepticProfile.sigma line 402
  39. def OAI.SepticProfile.kappa line 403
  40. def OAI.SepticProfile.normalizedDenom line 405
  41. def OAI.SepticProfile.normalizedNumer line 408
  42. lemma OAI.SepticProfile.normalized_denominator line 411
  43. lemma OAI.SepticProfile.normalized_numerator line 420
  44. lemma OAI.SepticProfile.normalized_equation_iff line 430
  45. def OAI.SepticProfile.jetA line 443
  46. def OAI.SepticProfile.jetB line 444
  47. def OAI.SepticProfile.jetC line 445
  48. def OAI.SepticProfile.jetLinear line 447
  49. lemma OAI.SepticProfile.sigma_eq_radius_sq line 450
  50. lemma OAI.SepticProfile.jet_coefficients_positive line 458
  51. lemma OAI.SepticProfile.jet_resonance_identity line 479
  52. lemma OAI.SepticProfile.exists_admissible_ratio73 line 488
  53. lemma OAI.SepticProfile.exists_zero_jet_linear73 line 511