OAI/Geometry/WeakMTW/Variations/MTWConcavity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakMTWGlobalSupport.ParameterCalculus.slice_deriv_smooth line 16
2. theorem OAI.WeakMTWGlobalSupport.ParameterCalculus.slice_second_smooth line 25
3. def OAI.WeakMTWGlobalSupport.WeakMTW.actionHessianDiag line 41
4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.cost_exp_parameter_smooth line 44
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.actionHessianDiag_smooth line 59
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.mtw_eq_hessian_diag line 66
7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.mtw_on_line_eq line 72
8. theorem OAI.WeakMTWGlobalSupport.WeakMTW.transverse_action_concave line 86