HarmonicGradientFromPoisson.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The harmonic L² gradient input from the existing Poisson and mean inputs

A fixed small ball around each interior point has uniformly comparable volume. The harmonic mean estimate bounds its values, and the constant-zero case of the Poisson gradient estimate bounds its gradient. A countable open subcover combines the local almost-everywhere estimates.

theorem OAI.RegularPointCoordinates.curvature_mul_scale line 24
theorem OAI.RegularPointCoordinates.curvature_unit_scale line 33
theorem OAI.RegularPointCoordinates.harmonicTargetNorm_le_of_volume line 45
theorem OAI.RegularPointCoordinates.harmonicGradientInput_of_poisson_and_mean line 75
Source documentation
The harmonic L² gradient estimate is redundant once the Poisson gradient and harmonic mean-value estimates have been supplied.
```
theorem harmonicGradientInput_of_poisson_and_mean {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X)
    (hpoisson : LocalPoissonGradientInput hX) (hmean : LocalHarmonicL2MeanValueInput hX) :
    LocalHarmonicL2GradientInput hX := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonGradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput