OAI/Geometry/RCD/Harmonic/RadialMixedLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual radial mixed-gradient convergence with the original physical measures

The compact recoveries below are constructed from the RCD data. Their finite initial shifts depend on the chosen test, and are removed before stating the limit for the original, fixed harmonic sequence.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.radial_mixed_limit line 19