OAI/Geometry/RCD/Harmonic/InnerHarmonicLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A classical limit for the actual inner-ball harmonic candidates

Both the measured maps and the normalizing bound on the smaller ball are derived from the original outer approximation and global L2 bound.

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