OAI/Geometry/NodalSets/Charts/ChartHessianLemmas.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Geometry.quadraticChart_fderiv_apply_hasFDerivAt line 15
  2. lemma OAI.Yau.Geometry.scalar_chart_first line 22
  3. theorem OAI.Yau.Geometry.scalar_chart_hessian line 30
  4. theorem OAI.Yau.Geometry.equal_gradient_chart_hessian_difference line 54
  5. def OAI.Yau.Geometry.christoffelCovector line 69
  6. lemma OAI.Yau.Geometry.christoffelCovector_apply line 74
  7. def OAI.Yau.Geometry.christoffelTensor line 79
  8. lemma OAI.Yau.Geometry.christoffelTensor_pair line 84
  9. lemma OAI.Yau.Geometry.christoffelTensor_symmetric line 90
  10. lemma OAI.Yau.Geometry.christoffelTensor_cancel line 98