OAI/Geometry/WeakMTW/Variations/ActionHessian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWGlobalSupport.WeakMTW.initialCost line 23
2. def OAI.WeakMTWGlobalSupport.WeakMTW.tangentChartLinear line 25
3. theorem OAI.WeakMTWGlobalSupport.WeakMTW.tangentChartLinear_eq line 31
4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.initialCost_geometry line 38
5. def OAI.WeakMTWGlobalSupport.WeakMTW.actionHessian line 78
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.actionHessian_symmetric line 83
7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.actionHessian_radial line 92
8. theorem OAI.WeakMTWGlobalSupport.WeakMTW.actionHessian_diag line 99