OAI/Analysis/BiholderTransport/Regularity/OuterVelocityFactorNonneg.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.outerVelocity_factor_nonneg line 12
2. lemma OAI.WeakMTWTransport.outerVelocity_nonneg line 23
3. lemma OAI.WeakMTWTransport.outerVelocity_le_factor line 30
4. lemma OAI.WeakMTWTransport.outerVelocity_le line 40
5. lemma OAI.WeakMTWTransport.outerVelocity_le_L line 54
6. lemma OAI.WeakMTWTransport.hasDerivAt_outerPrimitive line 64
7. lemma OAI.WeakMTWTransport.outerPrimitive_smooth line 70
8. lemma OAI.WeakMTWTransport.outerTemplate_smooth line 81
9. lemma OAI.WeakMTWTransport.outerPrimitive_monotone line 86
10. lemma OAI.WeakMTWTransport.outerPrimitive_sub line 93
11. lemma OAI.WeakMTWTransport.outerPrimitive_flat_left line 102
12. lemma OAI.WeakMTWTransport.outerPrimitive_flat_right line 115
13. lemma OAI.WeakMTWTransport.outerPrimitive_bounds line 129