OAI/Geometry/RCD/Sobolev/HarmonicEnergyGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Energy-gradient control from the finite-span calculus

Appending two zero harmonic functions permits the already stated Poisson Hessian and gradient-product inputs to be applied to a harmonic column. The auxiliary full measure is bounded with an actual larger cutoff.

  1. theorem OAI.RegularPointCoordinates.harmonic_energy_gradient_le line 22