OAI/Geometry/RCD/Transport/RadialPlanSlope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering slope one from a compressed radial plan

An actual radial plan realizes the full metric speed of the distance function. The weak-upper-gradient inequality then forces slope one at its initial marginal. This isolates the analytic step from constructing the radial plan by concentration of its final endpoint.

  1. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.integral_speed_le_of_radial_plan line 23
  2. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.eq_one_of_radial_plan line 57