OAI/Geometry/RCD/Harmonic/AveragedEndpointPairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pairing the exact derivative of the averaged potential

On the inner ball the cutoff is one, so its L2 derivative has precisely the normalized endpoint pairing appearing in the energy estimate.

  1. theorem OAI.RegularPointCoordinates.averaged_endpoint_pairing line 18