OAI/Geometry/WeakHessian/Transport/IntegrableEvalBounded.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsTestPlan.integrable_eval_bounded line 49
2. lemma OAI.WeakHessian.BoundedTracks.integrable_lipschitz_eval line 57
3. lemma OAI.WeakHessian.IsTestPlan.integrable_gradient_energy line 75
4. lemma OAI.WeakHessian.IsTestPlan.integrable_gamma_eval line 87
5. lemma OAI.WeakHessian.IsTestPlan.perturbation_energy line 98
6. lemma OAI.WeakHessian.IsTestPlan.contact_gradient_energy_le line 115
7. lemma OAI.WeakHessianTransport.tendsto_of_quadratic_variations line 134