OAI/Analysis/BiholderTransport/Volume/Measurable.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.ConvexProximal.exists_subgradient line 27
2. lemma OAI.WeakMTWTransport.ConvexProximal.prox_surjective line 59
3. lemma OAI.WeakMTWTransport.ConvexProximal.ae_exists_regular_proximal_inverse line 65
4. lemma OAI.WeakMTWTransport.ConvexProximal.subgradient_line_deriv line 99
5. lemma OAI.WeakMTWTransport.ConvexProximal.quadraticExpansion_of_subgradient_differential line 115
6. lemma OAI.WeakMTWTransport.ConvexProximal.symmetrized_quadratic line 182
7. lemma OAI.WeakMTWTransport.ConvexProximal.ae_quadraticExpansion_lipschitz_convex line 197
8. lemma OAI.WeakMTWTransport.ConvexProximal.quadraticExpansion_congr_nhds line 228
9. lemma OAI.WeakMTWTransport.ConvexProximal.ae_quadraticExpansion_convex_open line 242
10. lemma OAI.WeakMTWTransport.ConvexProximal.quadraticExpansion_sub_quadratic line 269
11. lemma OAI.WeakMTWTransport.ConvexProximal.ae_quadraticExpansion_semiconvex_open line 289