OAI/Geometry/RCD/Transport/QuadraticMidpointError.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Recovering the full midpoint law from interior time intervals

  1. theorem OAI.RegularPointCoordinates.quadratic_midpoint_error_bound line 11
  2. abbrev OAI.RegularPointCoordinates.quadraticMidpointTime line 36
  3. theorem OAI.RegularPointCoordinates.squared_distance_along_geodesic line 38
  4. def OAI.RegularPointCoordinates.fullMidpointDefect line 67
  5. theorem OAI.RegularPointCoordinates.fullMidpointDefect_le_interior line 71