OAI/Analysis/BiholderTransport/Contact/SubgradientDifferential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.quadraticTaylor_increment line 20
2. lemma OAI.WeakMTWTransport.subgradient_directional_bound line 29
3. lemma OAI.WeakMTWTransport.subgradient_norm_bound line 73
4. lemma OAI.WeakMTWTransport.subgradient_zero_of_quadraticExpansion line 95
5. lemma OAI.WeakMTWTransport.subgradient_uniform_differential line 126
6. def OAI.WeakMTWTransport.IsSemiconvexSubgradientOn line 172
7. lemma OAI.WeakMTWTransport.semiconvex_subgradient_iff line 176
8. lemma OAI.WeakMTWTransport.quadraticExpansion_add_quadratic line 193
9. lemma OAI.WeakMTWTransport.semiconvex_subgradient_uniform_differential line 211