OAI/Geometry/WeakMTW/Variations/BranchHessian.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.WeakMTWGlobalSupport.WeakMTW.cost_coord_eq_inverse_arbitrary_chartline 23 - def
OAI.WeakMTWGlobalSupport.WeakMTW.branchHessianDiagline 82 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.branchHessianDiag_continuousline 90 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.actionHessian_eq_branchline 121