OAI/Geometry/WeakMTW/Potentials/IntermediateGradient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWGlobalSupport.WeakMTW.normalGradient line 26
2. theorem OAI.WeakMTWGlobalSupport.WeakMTW.normalGradient_of_upper_support line 30
3. theorem OAI.WeakMTWGlobalSupport.WeakMTW.backward_vector_minimizing line 63
4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.intermediate_gradient_state line 76
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.intermediate_pole_flow line 101