OAI/Geometry/IsometricImmersion/Immersions/OrientedHeightPullback.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.orientedCovHessian line 16
  2. theorem OAI.SmoothLocal.Geometry.orientedCovHessian_contDiffOn line 20
  3. theorem OAI.SmoothLocal.Geometry.exists_open_oriented_height_neighborhood line 33
  4. theorem OAI.SmoothLocal.Geometry.rank_one_height_has_oriented_neighborhood line 62
  5. theorem OAI.SmoothLocal.Geometry.scaled_matrix_congruence line 90
  6. theorem OAI.SmoothLocal.Geometry.affinePullbackMetric_scaled line 97
  7. theorem OAI.SmoothLocal.Geometry.covHessian_affinePullback_scaled line 103
  8. theorem OAI.SmoothLocal.Geometry.heightEnergy_affinePullback_scaled line 113
  9. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_affinePullback_scaled line 123
  10. theorem OAI.SmoothLocal.Geometry.modelSquare_subset_closedPatchBox line 131
  11. theorem OAI.SmoothLocal.Geometry.oriented_patch_height_admissible_of_subset line 137