OAI/Geometry/IsometricImmersion/Curvature/PatchCurvatureProfiles.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.openPatchBox line 15
  2. theorem OAI.SmoothLocal.Geometry.mem_openPatchBox_iff_norm_lt line 17
  3. theorem OAI.SmoothLocal.Geometry.openPatchBox_subset_closedPatchBox line 22
  4. def OAI.SmoothLocal.Geometry.patchAxisCutoff line 26
  5. theorem OAI.SmoothLocal.Geometry.patchAxisCutoff_contDiff line 30
  6. theorem OAI.SmoothLocal.Geometry.patchAxisCutoff_one line 33
  7. theorem OAI.SmoothLocal.Geometry.patchAxisCutoff_zero_left line 40
  8. theorem OAI.SmoothLocal.Geometry.patchAxisCutoff_zero_right line 45
  9. theorem OAI.SmoothLocal.Geometry.patchAxisCutoff_support_bound line 50
  10. def OAI.SmoothLocal.Geometry.patchBoxCutoff line 59
  11. theorem OAI.SmoothLocal.Geometry.patchBoxCutoff_contDiff line 61
  12. theorem OAI.SmoothLocal.Geometry.patchBoxCutoff_one line 65
  13. theorem OAI.SmoothLocal.Geometry.patchBoxCutoff_support_bound line 70
  14. def OAI.SmoothLocal.Geometry.localPatchProfile line 81
  15. theorem OAI.SmoothLocal.Geometry.localPatchProfile_contDiff line 83
  16. theorem OAI.SmoothLocal.Geometry.localPatchProfile_eq_model line 86
  17. theorem OAI.SmoothLocal.Geometry.localPatchProfile_tsupport_bound line 90
  18. theorem OAI.SmoothLocal.Geometry.localPatchProfile_hasCompactSupport line 98
  19. theorem OAI.SmoothLocal.Geometry.localPatchProfile_tsupport_strictly_inside line 102
  20. def OAI.SmoothLocal.Geometry.affinePatchProfile line 109
  21. theorem OAI.SmoothLocal.Geometry.affinePatchProfile_contDiff line 112
  22. theorem OAI.SmoothLocal.Geometry.affinePatchProfile_support line 116
  23. theorem OAI.SmoothLocal.Geometry.affinePatchProfile_tsupport line 128
  24. theorem OAI.SmoothLocal.Geometry.affinePatchProfile_hasCompactSupport line 135
  25. theorem OAI.SmoothLocal.Geometry.affinePatchProfile_tsupport_strictly_inside line 142
  26. def OAI.SmoothLocal.Geometry.patchModelNeighborhood line 148
  27. theorem OAI.SmoothLocal.Geometry.patchModelNeighborhood_isOpen line 151
  28. theorem OAI.SmoothLocal.Geometry.patchModelNeighborhood_contains_innerSquare line 155
  29. theorem OAI.SmoothLocal.Geometry.affinePatchProfile_eq_model_on_neighborhood line 169
  30. def OAI.SmoothLocal.Geometry.orientedPatchProfile line 180
  31. theorem OAI.SmoothLocal.Geometry.orientedPatchProfile_contDiff line 183
  32. theorem OAI.SmoothLocal.Geometry.orientedPatchProfile_hasCompactSupport line 186
  33. theorem OAI.SmoothLocal.Geometry.orientedPatchProfile_tsupport_subset_patch line 190
  34. theorem OAI.SmoothLocal.Geometry.orientedPatchProfile_tsupport_subset_layer line 195