OAI/Analysis/BiholderTransport/Regularity/InteriorMaximum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.boundedModifiedDatum line 14
2. lemma OAI.WeakMTWTransport.continuous_boundedModifiedDatum line 21
3. lemma OAI.WeakMTWTransport.continuous_cTransform_family line 25
4. lemma OAI.WeakMTWTransport.continuous_hopfLax_family line 31
5. lemma OAI.WeakMTWTransport.continuous_regularizedComparison line 39
6. lemma OAI.WeakMTWTransport.regularizedComparison_error line 53
7. lemma OAI.WeakMTWTransport.regularized_interior_maximum line 70