HarmonicGradientInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The harmonic L² interior gradient specialization

Jiang (2014), JFA266, Theorem 1.1 (arXiv:1307.1334v2, printed p.3), with eigenvalue zero, gives an interior gradient bound by the local L¹ mean. Cauchy--Schwarz replaces that mean by the L² mean. Covering a fixed inner fraction and Bishop--Gromov comparison (Sturm2006II, Theorem2.3) give the following fixed-fraction specialization. Constants are chosen before the ball and function and depend only on the stated curvature bound and ratio.

def OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput line 25
Source documentation
The normalized L² interior gradient bound for harmonic functions. This is a analytic input, not an affine approximation premise.
```
def LocalHarmonicL2GradientInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD