OAI/Analysis/BiholderTransport/Convexity/ModifiedEnvelopeRegularity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.differentiableAt_of_const_mul line 18
2. lemma OAI.WeakMTWTransport.C11_const_mul_cancel line 24
3. lemma OAI.WeakMTWTransport.HasSecondTaylor.hasQuadraticExpansion line 45
4. lemma OAI.WeakMTWTransport.ae_secondTaylor_of_C11 line 58