OAI/Geometry/RCD/Harmonic/CurvatureHarmonicVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The variational lower bound for actual harmonic perturbations

The test is in the original Dirichlet space. Its compact support makes the mixed source energy vanish on any containing interior ball.

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