OAI/Analysis/BiholderTransport/Calculus/HopfGradient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.cost_divided_triangle_two_times line 19
2. lemma OAI.WeakMTWTransport.mdifferentiableAt_of_chart_differentiable line 37
3. lemma OAI.WeakMTWTransport.WeakMTW.mdifferentiable_hopfLax line 48
4. lemma OAI.WeakMTWTransport.hopfLax_derivative_of_minimizer line 57
5. def OAI.WeakMTWTransport.riemannianGradient line 115
6. lemma OAI.WeakMTWTransport.riemannianGradient_eq_of_derivative line 125
7. lemma OAI.WeakMTWTransport.WeakMTW.hopfLax_backward_flow line 134