HarmonicRadialBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Radial derivatives of harmonic residuals on an interior ball

theorem OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput.radial_derivative_bound line 19

Source documentation

The published harmonic gradient estimate controls the actual radial derivative on the inner ball by the outer value norm. No normalization of the function or division by that norm is used.

theorem LocalHarmonicL2GradientInput.radial_derivative_bound
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hinput : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
    {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (R : ℝ), 0 < R → -κ ≤ K * R ^ 2 →
      ∀ (f w : SobolevSpace (hausdorff n X) hX.quadratic) (B : ℝ), 0 ≤ B →
      ∀ hf : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (R / 2)),
        localGamma (hausdorff n X) hX.quadratic f f x ≤ B ^ 2,
      IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p R) w →
      ‖normalizeLocalL2 (hausdorff n X) (ball p (R / 2))
        (ne_of_lt (hX.finiteOnBounded _ isBounded_ball))
        (localRadialDerivative (hausdorff n X) hX.quadratic (ball p (R / 2)) f hf w)‖ ≤
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.localRadialDerivative