OAI/Analysis/BiholderTransport/Regularity/LipschitzSubAeDeriv.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.lipschitzOn_sub_le_of_ae_deriv_le line 13
2. lemma OAI.WeakMTWTransport.lipschitzOn_barrier line 25
3. lemma OAI.WeakMTWTransport.norm_deficit_advance line 60
4. lemma OAI.WeakMTWTransport.norm_surplus_advance line 70