OAI/Geometry/IsometricImmersion/Calculus/AffineCovariantHessian.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.ordinaryCoordinateHessian line 10
  2. def OAI.SmoothLocal.Geometry.connectionHessianCorrection line 13
  3. theorem OAI.SmoothLocal.Geometry.covHessian_eq_ordinary_sub_correction line 17
  4. theorem OAI.SmoothLocal.Geometry.ordinaryCoordinateHessian_affine_comp line 20
  5. theorem OAI.SmoothLocal.Geometry.connectionHessianCorrection_affine_comp line 36
  6. theorem OAI.SmoothLocal.Geometry.covHessian_affinePullback line 65
  7. def OAI.SmoothLocal.Geometry.coordinateCovector line 77
  8. theorem OAI.SmoothLocal.Geometry.coordinateCovector_affine_comp line 79
  9. theorem OAI.SmoothLocal.Geometry.covectorNormSq_eq_dotProduct line 87
  10. theorem OAI.SmoothLocal.Geometry.inverseMetric_affinePullback line 93
  11. theorem OAI.SmoothLocal.Geometry.covectorNormSq_affinePullback line 100
  12. theorem OAI.SmoothLocal.Geometry.heightEnergy_affinePullback line 117
  13. theorem OAI.SmoothLocal.Geometry.heightEnergy_affinePullback_pos_iff line 126