OAI/Geometry/WeakMTW/Variations/DiscreteVariationalCalculus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakMTWGlobalSupport.DiscreteVariational.scalar_second_nonneg line 13
2. theorem OAI.WeakMTWGlobalSupport.DiscreteVariational.hessian_apply line 30
3. theorem OAI.WeakMTWGlobalSupport.DiscreteVariational.line_second line 36
4. theorem OAI.WeakMTWGlobalSupport.DiscreteVariational.hessian_nonneg line 58