OAI/Geometry/RCD/Harmonic/RadialFirstVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

First variation for a family of radial contractions

The family may use a different optimal plan at each contraction scale. Uniform compression and shrinking length suffice for the signed limit.

  1. theorem OAI.RegularPointCoordinates.radial_first_variation_eventually_gt line 20