OAI/Analysis/BiholderTransport/Contact/Subgradient.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.IsSubgradientOn line 16
2. def OAI.WeakMTWTransport.quadraticTaylor line 19
3. def OAI.WeakMTWTransport.HasQuadraticExpansion line 22
4. lemma OAI.WeakMTWTransport.convex_lipschitz_extension line 27
5. lemma OAI.WeakMTWTransport.ae_of_locally_ae line 93
6. def OAI.WeakMTWTransport.ConvexProximal.energy line 117
7. lemma OAI.WeakMTWTransport.ConvexProximal.norm_sq_add_real line 119
8. lemma OAI.WeakMTWTransport.ConvexProximal.energy_increment line 125
9. lemma OAI.WeakMTWTransport.ConvexProximal.subgradient_iff_minimizer line 134
10. lemma OAI.WeakMTWTransport.ConvexProximal.subgradient_strong_min line 172
11. lemma OAI.WeakMTWTransport.ConvexProximal.subgradient_monotone line 184
12. lemma OAI.WeakMTWTransport.ConvexProximal.minimizer_unique line 193
13. lemma OAI.WeakMTWTransport.ConvexProximal.exists_minimizer line 204
14. def OAI.WeakMTWTransport.ConvexProximal.prox line 231
15. lemma OAI.WeakMTWTransport.ConvexProximal.prox_minimizes line 234
16. lemma OAI.WeakMTWTransport.ConvexProximal.prox_subgradient line 238
17. lemma OAI.WeakMTWTransport.ConvexProximal.prox_of_subgradient line 243
18. lemma OAI.WeakMTWTransport.ConvexProximal.prox_firm line 250
19. lemma OAI.WeakMTWTransport.ConvexProximal.prox_lipschitz line 261
20. lemma OAI.WeakMTWTransport.ConvexProximal.subgradient_norm_le line 272
21. lemma OAI.WeakMTWTransport.ConvexProximal.gradient_subgradient line 281
22. lemma OAI.WeakMTWTransport.ConvexProximal.subgradient_eq_gradient line 309
23. lemma OAI.WeakMTWTransport.ConvexProximal.isClosed_subgradient_projection line 329
24. lemma OAI.WeakMTWTransport.ConvexProximal.subgradient_continuity_at_singleton line 348
25. lemma OAI.WeakMTWTransport.ConvexProximal.subgradient_continuity_of_differentiable line 371
26. lemma OAI.WeakMTWTransport.ConvexProximal.uniform_subgradient_differential_of_regular_prox line 378