OAI/Geometry/RCD/Harmonic/RadialTimeReplacement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Replacing a radial-time region while retaining its source capacity

The replacement preserves both endpoint marginals. The one-sided CD support estimate holds at the chosen time and survives endpoint concentration.

  1. theorem OAI.RegularPointCoordinates.FullCD.replace_time_region line 19