OAI/Geometry/RCD/Harmonic/RadialVariationBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite radial first-variation inequality

The exact quadratic decrement and cost replace a Kantorovich potential. The error depends only on the short-plan pullback modulus, uniformly in the chosen transport plan.

  1. theorem OAI.RegularPointCoordinates.radial_variation_lower_bound line 22