OAI/Geometry/RCD/Harmonic/PinchingTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Inward square-root tails are controlled by the summable envelope

Only the defect itself needs to be summable. Its square root need not be. The extra decay from the radii controls the inward tail of affine constants.

  1. theorem OAI.RegularPointCoordinates.geometric_sqrt_tail_le line 16