OAI/Geometry/WeakHessian/Transport/OptimalPlansShort.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.halfTime_one line 52
  2. lemma OAI.WeakHessian.rightTime_zero line 54
  3. lemma OAI.WeakHessian.IsGeodesic.half_length line 57
  4. lemma OAI.WeakHessian.IsGeodesic.right_length line 64
  5. lemma OAI.WeakHessian.IsGeodesic.halfCurve line 71
  6. lemma OAI.WeakHessian.IsGeodesic.rightCurve line 80
  7. lemma OAI.WeakHessian.interpolation_map_half line 91
  8. lemma OAI.WeakHessian.interpolation_map_right line 95
  9. lemma OAI.WeakHessian.integrable_plan_energy_half line 101
  10. lemma OAI.WeakHessian.integrable_plan_energy_right line 113
  11. lemma OAI.WeakHessian.planEnergy_half line 125
  12. lemma OAI.WeakHessian.planEnergy_right line 135
  13. def OAI.WeakHessian.OptimalPlansShort line 144
  14. lemma OAI.WeakHessian.optimalPlansShort_of_ball line 149
  15. lemma OAI.WeakHessian.optimalPlan_energy_le line 162
  16. theorem OAI.WeakHessian.OptimalPlansShort.halves line 176
  17. lemma OAI.WeakHessian.OptimalPlansShort.subplan line 235