OAI/Geometry/RCD/Transport/MetricLimitMidpointContraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local midpoint contraction for the actual weak metric-law limit

The proof passes the normalized CD inequality from the original spaces. Open source balls and a closed enlarged target avoid a boundary assumption.

  1. theorem OAI.RegularPointCoordinates.normalizedBallPushforward_preimage_ne_zero line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.metric_limit_midpoint_enlarged line 33