OAI/Geometry/RCD/Sobolev/PoissonGradientInput.lean

interior gradient input for the Poisson replacements

Jiang, Cheeger-harmonic functions in metric measure spaces revisited, J. Funct. Anal. 266 (2014), 1373--1394, Theorem 3.1 (arXiv:1307.1334v2, printed p.7), bounds the gradient by the local supremum of the function and the bounded right-hand side. The following is only its constant-source interior-ball consequence on RCD spaces at bounded rescaled curvature. The half-radius conclusion follows by covering with the theorem's one-eighth-radius balls. RCD supplies the uniform local doubling, Poincare and heat-semigroup curvature constants.