OAI/Geometry/RCD/Harmonic/SmoothHarmonicModelCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual Euclidean harmonic models under the original curvature-scale bound

The normalized harmonic model, finite affine moments and smooth value pairings are constructed without any restriction on the limiting radii.

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