OAI/Geometry/WeakHessian/Transport/BoundedHopfMapLipschitz.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.boundedHopfMap_lipschitz line 50
2. lemma OAI.WeakHessianTransport.integrable_bounded_pairing line 61
3. lemma OAI.WeakHessianTransport.norm_integral_bounded_pairing line 66
4. lemma OAI.WeakHessianTransport.integral_bounded_pairing_sub_left line 76
5. lemma OAI.WeakHessianTransport.integral_bounded_pairing_sub_right line 83
6. lemma OAI.WeakHessianTransport.integral_bounded_pairing_evolution line 90
7. lemma OAI.WeakHessianTransport.boundedHopfMap_L1_increment line 99
8. lemma OAI.WeakHessianTransport.tendsto_bounded_pairing_L1 line 116
9. lemma OAI.WeakHessianTransport.hopf_L1_upper_slope line 136