OAI/Geometry/IsometricImmersion/Curvature/DiskCurvatureProfiles.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.roundRadiusSq_contDiff line 12
  2. def OAI.SmoothLocal.Geometry.negativeDiskProfile line 16
  3. theorem OAI.SmoothLocal.Geometry.negativeDiskProfile_contDiff line 19
  4. theorem OAI.SmoothLocal.Geometry.negativeDiskProfile_nonpos line 23
  5. theorem OAI.SmoothLocal.Geometry.negativeDiskProfile_neg_inside line 26
  6. theorem OAI.SmoothLocal.Geometry.negativeDiskProfile_zero_outside line 30
  7. theorem OAI.SmoothLocal.Geometry.negativeDiskProfile_support line 35
  8. theorem OAI.SmoothLocal.Geometry.negativeDiskProfile_tsupport_subset line 45
  9. theorem OAI.SmoothLocal.Geometry.negativeDiskProfile_hasCompactSupport line 51
  10. theorem OAI.SmoothLocal.Geometry.negativeDiskProfile_frontier_zero line 56
  11. def OAI.SmoothLocal.Geometry.accumulatingDiskProfile line 62
  12. theorem OAI.SmoothLocal.Geometry.accumulatingDiskProfile_contDiff line 65
  13. theorem OAI.SmoothLocal.Geometry.accumulatingDiskProfile_tsupport_subset line 68
  14. theorem OAI.SmoothLocal.Geometry.accumulatingDiskProfile_hasCompactSupport line 72
  15. theorem OAI.SmoothLocal.Geometry.accumulatingDiskProfile_neg_interior line 76
  16. theorem OAI.SmoothLocal.Geometry.accumulatingDiskProfile_frontier_zero line 82