OAI/Geometry/IsometricImmersion/Calculus/AffineHessian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.matrix_column_basis_expansion line 13
  2. def OAI.SmoothLocal.Geometry.bilinearMatrix line 20
  3. theorem OAI.SmoothLocal.Geometry.bilinear_matrix_congruence line 23
  4. theorem OAI.SmoothLocal.Geometry.second_coordPartial_affine_comp line 33
  5. theorem OAI.SmoothLocal.Geometry.fderiv_affine_comp_eq_zero line 63
  6. theorem OAI.SmoothLocal.Geometry.covHessian_eq_secondFDeriv_at_critical line 73
  7. theorem OAI.SmoothLocal.Geometry.covHessian_affinePullback_at_critical line 83
  8. theorem OAI.SmoothLocal.Geometry.covHessian_affinePullback_at_zero line 101