OAI/Geometry/RCD/Transport/NearbySegment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Controlled segments with endpoints near prescribed points

Only a dimensional constant and the explicit endpoint radius loss occur. The estimate uses the original Hausdorff measure and permits every real K.

  1. def OAI.RegularPointCoordinates.segmentCost line 16
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.nearby_defect_segment line 18