OAI/Geometry/RCD/Coordinates/GoodSplittingSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One compact good set for every smaller splitting scale

The original harmonic functions and their representatives are retained. Only their finite Gram defect enters the maximal estimate.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.good_splitting_set line 18