OAI/MathematicalPhysics/Transonic/Shooting/AxisFamilyC1.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.NormalizedAxis.A line 13
  2. def OAI.SepticProfile.NormalizedAxis.A1 line 14
  3. def OAI.SepticProfile.NormalizedAxis.R line 15
  4. theorem OAI.SepticProfile.NormalizedAxis.axis_identity line 18
  5. def OAI.SepticProfile.NormalizedAxis.H line 25
  6. theorem OAI.SepticProfile.NormalizedAxis.H_analytic line 30
  7. theorem OAI.SepticProfile.NormalizedAxis.H_real line 41
  8. def OAI.SepticProfile.AxisFamily.numerator line 55
  9. def OAI.SepticProfile.AxisFamily.denominator line 60
  10. def OAI.SepticProfile.AxisFamily.H line 63
  11. def OAI.SepticProfile.AxisFamily.numeratorC1 line 65
  12. def OAI.SepticProfile.AxisFamily.denominatorC1 line 76
  13. lemma OAI.SepticProfile.AxisFamily.denominator_zero_ne line 87
  14. lemma OAI.SepticProfile.AxisFamily.H_normalizedAxis line 90
  15. theorem OAI.SepticProfile.AxisFamily.uniform_bounds line 94