OAI/Geometry/WeakHessian/Transport/HopfMap.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.hopf_forward_increment line 35
2. lemma OAI.WeakHessianTransport.continuousMap_bounds line 65
3. def OAI.WeakHessianTransport.hopfMap line 71
4. lemma OAI.WeakHessianTransport.hopfMap_zero line 78
5. lemma OAI.WeakHessianTransport.hopfMap_apply_pos line 81
6. lemma OAI.WeakHessianTransport.hopfMap_time_lipschitz line 85
7. lemma OAI.WeakHessianTransport.hopfMap_dist_initial line 97
8. lemma OAI.WeakHessianTransport.continuousOn_hopfMap line 109
9. def OAI.WeakHessianTransport.hopfLp line 126
10. lemma OAI.WeakHessianTransport.continuousOn_hopfLp line 128
11. lemma OAI.WeakHessianTransport.hopfLp_coe_ae line 132
12. lemma OAI.WeakHessianTransport.integrable_localSlope_sq line 138
13. lemma OAI.WeakHessianTransport.cheegerEnergy_le_integral_localSlope line 148
14. lemma OAI.WeakHessianTransport.hopfLp_energy_bound line 165