OAI/Geometry/RCD/Harmonic/CurvatureHarmonicLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weak Euclidean equation under the original curvature-scale bound

Sharp recovered test energies and harmonic orthogonality force the compact Euclidean gradient pairing to vanish. No energy convergence is assumed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_value_limit_weak_of_curvature line 21