HarmonicMeanValueInput.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The published harmonic mean-value estimate used for affine evaluation

Jiang, Cheeger-harmonic functions in metric measure spaces revisited, JFA 266 (2014), Lemma 4.1 (printed pp.14–15), with lambda=0 and exponent 2. Only the half-ball L-infinity consequence under bounded rescaled curvature is retained. Full support and continuity give pointwise evaluation below.

def OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput line 21
Source documentation
The fixed-ratio, harmonic L²-to-L∞ specialization of Jiang Lemma 4.1.
```
def LocalHarmonicL2MeanValueInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD

theorem OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput.center_bound line 30

Source documentation

The a.e. estimate applies at the center to every continuous representative.

theorem LocalHarmonicL2MeanValueInput.center_bound {K : ℝ} {n : ℕ}
    {hX : NoncollapsedRCD K n X} (hmean : LocalHarmonicL2MeanValueInput hX)
    (hn : 2 ≤ n) {a : ℝ} (ha : 0 ≤ a) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (r : ℝ), 0 < r → -a ≤ K * r ^ 2 →
    ∀ (w : SobolevSpace (hausdorff n X) hX.quadratic) (v : X → ℝ),
      IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p r) w →
      ContinuousOn v (ball p r) →
      (SobolevSpace.toLp (hausdorff n X) hX.quadratic w =ᵐ[
        (hausdorff n X).restrict (ball p r)] v) →
      |v p| ≤ C * harmonicTargetNorm hX p r w := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.harmonicTargetNorm