OAI/Geometry/RCD/Transport/MidpointLengthApproximation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact midpoint distortion as the limit of finite length bins

  1. def OAI.RegularPointCoordinates.upperLength line 13
  2. theorem OAI.RegularPointCoordinates.upperLength_pos line 15
  3. theorem OAI.RegularPointCoordinates.le_upperLength line 19
  4. theorem OAI.RegularPointCoordinates.upperLength_le_add line 22
  5. theorem OAI.RegularPointCoordinates.upperLength_tendsto line 27
  6. theorem OAI.RegularPointCoordinates.sigma_nonpos_midpoint_eq line 35
  7. theorem OAI.RegularPointCoordinates.sigma_nonpos_midpoint_ne_zero line 43
  8. theorem OAI.RegularPointCoordinates.sigma_nonpos_midpoint_ne_top line 48
  9. theorem OAI.RegularPointCoordinates.midpoint_upperLength_tendsto line 53