OAI/Geometry/RCD/Harmonic/HarmonicValueAffineCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual normalized harmonic value limits and every finite affine moment

The limit is constructed on the entire open ball from the original RCD sequence. This theorem does not assert Euclidean harmonicity or convergence of gradient pairings; those remain the analytic identification step.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_value_affine_compactness line 20