OAI/Geometry/WeakHessian/Geodesics/TwoLegEstimate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.integral_lipschitz_deviation line 17
2. lemma OAI.WeakHessian.integral_dist_le_of_ae_ball line 36
3. lemma OAI.WeakHessian.backward_action_coarse line 44
4. lemma OAI.WeakHessian.weighted_coupling_entropy_bound line 69