OAI/Geometry/WeakHessian/Curvature/Nonbranching.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.CurvatureDimension.contact_first_variation line 49
  2. def OAI.WeakHessian.Nonbranching line 72
  3. theorem OAI.WeakHessian.clampTime_coe line 77
  4. theorem OAI.WeakHessian.evalReal_zero line 80
  5. theorem OAI.WeakHessian.evalReal_one line 83
  6. theorem OAI.WeakHessian.IsGeodesic.lipschitzWith line 86
  7. theorem OAI.WeakHessian.IsGeodesic.evalReal_lipschitzWith line 92
  8. theorem OAI.WeakHessian.isGeodesic_of_dist_le line 98
  9. theorem OAI.WeakHessian.lipschitzWith_if_le line 119
  10. theorem OAI.WeakHessian.IsGeodesic.stretch_lipschitzWith line 153
  11. def OAI.WeakHessian.splicedFunction line 169
  12. theorem OAI.WeakHessian.splicedFunction_lipschitzWith line 174
  13. theorem OAI.WeakHessian.Nonbranching.unique_strict_subsegment line 195
  14. theorem OAI.WeakHessian.isCompact_curve_family line 241
  15. lemma OAI.WeakHessian.isClosed_isGeodesic line 262
  16. def OAI.WeakHessian.endpointTube line 271
  17. lemma OAI.WeakHessian.isClosed_endpointTube line 274
  18. lemma OAI.WeakHessian.endpointTube_length_le line 279
  19. lemma OAI.WeakHessian.endpointTube_range line 286
  20. theorem OAI.WeakHessian.isCompact_endpointTube line 298
  21. theorem OAI.WeakHessian.unique_geodesic_endpoint_stability line 309
  22. theorem OAI.WeakHessian.integral_tendsto_of_endpoint_concentration line 348