OAI/Geometry/WeakHessian/Transport/PlanEnergy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.integrable_squared_distance_of_cost line 61
  2. lemma OAI.WeakHessian.quadraticTransportCost_eq_integral line 68
  3. lemma OAI.WeakHessian.cost_ne_top_of_bounded line 76
  4. lemma OAI.WeakHessian.quadratic_triangle_rigidity line 86
  5. lemma OAI.WeakHessian.joinCurve_isGeodesic line 121
  6. def OAI.WeakHessian.planEnergy line 153
  7. lemma OAI.WeakHessian.plan_energy_measurable line 156
  8. lemma OAI.WeakHessian.planEnergy_nonneg line 160
  9. lemma OAI.WeakHessian.planCost_eq_ofReal_energy line 163
  10. lemma OAI.WeakHessian.integrable_plan_energy line 172
  11. lemma OAI.WeakHessian.exists_joinable_gluing line 179
  12. def OAI.WeakHessian.halfCurve line 203
  13. def OAI.WeakHessian.rightCurve line 204
  14. lemma OAI.WeakHessian.continuous_halfCurve line 206
  15. lemma OAI.WeakHessian.continuous_rightCurve line 208
  16. lemma OAI.WeakHessian.halfCurve_joinCurve line 211
  17. lemma OAI.WeakHessian.rightCurve_joinCurve line 215
  18. theorem OAI.WeakHessian.exists_optimal_geodesic_join line 219