OAI/Geometry/WeakHessian/LocalBounds/BoundedEndpointTube.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.boundedEndpointTube line 49
  2. lemma OAI.WeakHessian.isClosed_boundedEndpointTube line 53
  3. lemma OAI.WeakHessian.boundedEndpointTube_length_le line 59
  4. lemma OAI.WeakHessian.boundedEndpointTube_range line 66
  5. lemma OAI.WeakHessian.isCompact_boundedEndpointTube line 80
  6. lemma OAI.WeakHessian.isCompact_probability_supported line 92
  7. lemma OAI.WeakHessian.isCompact_midpoint_constraints line 104
  8. def OAI.WeakHessian.clippedEndpointCost line 131
  9. lemma OAI.WeakHessian.clippedEndpointCost_nonneg line 145
  10. lemma OAI.WeakHessian.clippedEndpointCost_eq line 149
  11. lemma OAI.WeakHessian.endpointCost_eq_clipped_integral line 158
  12. def OAI.WeakHessian.optimalTimeLaws line 173
  13. lemma OAI.WeakHessian.optimalPlan_supported_tube line 180
  14. theorem OAI.WeakHessian.isCompact_optimalTimeLaws line 203