OAI/Geometry/IsometricImmersion/Calculus/ExtremumHessian.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.ExtremumCalculus.second_deriv_nonneg_of_localMin line 16
  2. theorem OAI.SmoothLocal.Geometry.ExtremumCalculus.second_deriv_nonpos_of_localMax line 29
  3. def OAI.SmoothLocal.Geometry.ordinaryHessian line 44
  4. theorem OAI.SmoothLocal.Geometry.second_deriv_along_line line 49
  5. theorem OAI.SmoothLocal.Geometry.secondFDeriv_nonneg_of_localMin line 75
  6. theorem OAI.SmoothLocal.Geometry.secondFDeriv_nonpos_of_localMax line 88
  7. theorem OAI.SmoothLocal.Geometry.secondFDeriv_basis_quadratic line 101
  8. theorem OAI.SmoothLocal.Geometry.ordinaryHessian_det_nonneg_of_localMin line 118
  9. theorem OAI.SmoothLocal.Geometry.ordinaryHessian_det_nonneg_of_localMax line 133
  10. theorem OAI.SmoothLocal.Geometry.ordinaryHessian_det_nonneg_of_localExtr line 148
  11. theorem OAI.SmoothLocal.Geometry.covHessian_eq_ordinaryHessian_of_localExtr line 154
  12. theorem OAI.SmoothLocal.Geometry.covHessian_at_localExtr line 160