OAI/Geometry/HyperbolicGroups/StationaryInterpolation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A midpoint-stationary short polygon interpolates to an actual constant-speed local geodesic, rather than merely to a combinatorial chain.

  1. abbrev OAI.HyperbolicObstruction.IsGeodesic.segment line 16
  2. lemma OAI.HyperbolicObstruction.IsGeodesic.segment_spec line 17
  3. lemma OAI.HyperbolicObstruction.UniformLocalCATZero.segment_unique line 20
  4. abbrev OAI.HyperbolicObstruction.StationaryInterpolation.edge line 49
  5. lemma OAI.HyperbolicObstruction.StationaryInterpolation.edge_spec line 50
  6. lemma OAI.HyperbolicObstruction.StationaryInterpolation.edge_length_eq line 53
  7. lemma OAI.HyperbolicObstruction.StationaryInterpolation.double_eq line 66
  8. lemma OAI.HyperbolicObstruction.StationaryInterpolation.curve_local_dist line 105
  9. lemma OAI.HyperbolicObstruction.StationaryInterpolation.isLocalSegment line 161