OAI/Geometry/CylinderCovering/Rational/Potential.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SlopeRational.radius_radial_coordinate line 11
  2. theorem OAI.SlopeRational.potential_contDiffAt line 15
  3. theorem OAI.SlopeRational.potential_contDiffOn line 22
  4. theorem OAI.SlopeRational.potential_radial_deriv_Y line 29
  5. theorem OAI.SlopeRational.potential_radial_hasDerivAt_r line 34
  6. theorem OAI.SlopeRational.potential_radial_hasDerivAt_YY line 43
  7. theorem OAI.SlopeRational.potential_radial_hasDerivAt_Yr line 49
  8. theorem OAI.SlopeRational.potential_radial_hasDerivAt_rY line 58
  9. theorem OAI.SlopeRational.potential_radial_hasDerivAt_rr line 71
  10. theorem OAI.SlopeRational.potential_radial_hessian_det line 91
  11. theorem OAI.SlopeRational.potential_zero_homogeneous line 104
  12. theorem OAI.SlopeRational.field_zero_ratio line 114