OAI/Geometry/RCD/Transport/MetricLocalMidpointVolume.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local midpoint volume control throughout the approximation ball

The endpoints can be near any interior target point. The radius condition only keeps their short connecting geodesics inside the working region.

  1. theorem OAI.RegularPointCoordinates.pointed_local_geodesic_radius line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.metric_local_midpoint_volume line 44