OAI/Geometry/RCD/Metric/DistanceEikonal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The distance eikonal identity from actual RCD transport

Restrict normalized volume to any positive-measure set on which the relaxed slope is less than one. The constructed compressed radial plan realizes the full distance speed, contradicting the weak upper gradient inequality.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.inward_minimalSlope_eq_one line 24
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.inwardSobolev_eikonal line 100