OAI/Geometry/WeakHessian/Transport/BoundedHopfMap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.boundedContinuous_bounds line 40
2. def OAI.WeakHessianTransport.boundedHopfMap line 46
3. lemma OAI.WeakHessianTransport.boundedHopfMap_zero line 59
4. lemma OAI.WeakHessianTransport.boundedHopfMap_apply_pos line 62
5. lemma OAI.WeakHessianTransport.boundedHopfMap_time_lipschitz line 66
6. lemma OAI.WeakHessianTransport.boundedHopfMap_dist_initial line 78
7. lemma OAI.WeakHessianTransport.continuousOn_boundedHopfMap line 90
8. def OAI.WeakHessianTransport.boundedHopfLp line 107
9. lemma OAI.WeakHessianTransport.continuousOn_boundedHopfLp line 109
10. lemma OAI.WeakHessianTransport.boundedHopfLp_coe_ae line 113
11. lemma OAI.WeakHessianTransport.boundedHopfLp_energy_bound line 117