OAI/Geometry/WeakHessian/Transport/MapEvalReal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsTestPlan.map_evalReal_le line 18
2. lemma OAI.WeakHessian.IsTestPlan.lintegral_abs_eval_le line 36
3. lemma OAI.WeakHessian.IsTestPlan.lintegral_abs_action_le line 57
4. lemma OAI.WeakHessian.IsTestPlan.endpoint_mean_le_add line 96
5. lemma OAI.WeakHessian.IsTestPlan.action_le_add line 138
6. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.of_l2_tendsto line 163