OAI/Geometry/WeakHessian/Entropy/EntropyContact.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsTestPlan.restrict_reference_of_tracks line 19
2. lemma OAI.WeakHessian.IsTestPlan.ball_localization line 32
3. lemma OAI.WeakHessian.IsTestPlan.integrable_eval line 40
4. lemma OAI.WeakHessian.IsTestPlan.integrable_eval_local line 47
5. lemma OAI.WeakHessian.IsTestPlan.continuous_integral_eval_local line 54
6. lemma OAI.WeakHessian.LocallyL2.integrable_eval line 64
7. lemma OAI.WeakHessian.LocallyL2.integrable_sq_eval line 74
8. lemma OAI.WeakHessian.LocallyL2.continuous_integral_sq_eval line 79
9. lemma OAI.WeakHessian.LocallyL2.integrable_sq_prod_eval line 85
10. lemma OAI.WeakHessian.IsTestPlan.continuous_local_gradient_energy line 96
11. lemma OAI.WeakHessian.IsTestPlan.tendsto_average_local_gradient_energy line 102
12. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.geodesic_young_local line 122
13. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.geodesic_young_time_local line 180
14. lemma OAI.WeakHessian.IsTestPlan.integrable_local_gamma_eval line 214
15. lemma OAI.WeakHessian.IsTestPlan.local_perturbation_energy line 221
16. lemma OAI.WeakHessian.IsTestPlan.contact_first_variation_local line 236
17. def OAI.WeakHessianTransport.lowerLipExtension line 305
18. lemma OAI.WeakHessianTransport.lowerLipExtension_bdd line 308
19. lemma OAI.WeakHessianTransport.lowerLipExtension_eq line 319
20. lemma OAI.WeakHessianTransport.lowerLipExtension_lipschitz line 331
21. lemma OAI.WeakHessianTransport.quadratic_cost_two_point_lower line 343
22. lemma OAI.WeakHessianTransport.lowerLipExtension_dual line 362
23. lemma OAI.WeakHessianTransport.quadraticTransportCost_map_subtype line 380
24. lemma OAI.WeakHessianTransport.compact_quadraticCost_eq line 390
25. lemma OAI.WeakHessianTransport.compact_kantorovich_potentials_of_optimal line 405
26. lemma OAI.WeakHessianTransport.bounded_support_kantorovich_potentials line 461