OAI/Analysis/BiholderTransport/Regularity/Alignment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.hopfLax_derivative_of_scaled_minimizer line 18
2. lemma OAI.WeakMTWTransport.hopfLax_backward_minimizer line 76
3. lemma OAI.WeakMTWTransport.gradients_cancel_at_local_max line 100
4. lemma OAI.WeakMTWTransport.WeakMTW.hopf_maximum_aligned line 120