SharpProjectionGradient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior gradient control from the sharp projection estimate

theorem OAI.RegularPointCoordinates.SharpProjectionFamily.uniform_gradient_bound line 17

Source documentation

The uniform sharp L2 projection bound yields the interior gradient estimate in natural radius units. The constants precede every configuration.

theorem SharpProjectionFamily.uniform_gradient_bound {K : ℝ} {n : ℕ}
    {hX : NoncollapsedRCD K n X} {I : Type*} {S ρ : ℝ}
    (d : SharpProjectionFamily hX I S ρ)
    (hcompact : LocalPoissonHarmonicCompactnessInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
    (hS : 0 < S) (hρ : 0 < ρ) (hρS : ρ < S) :
    ∃ G : ℝ, 0 < G ∧ ∃ δ : ℝ, 0 < δ ∧ ∀ i, d.error i < δ →
      ∀ᵐ x ∂(hausdorff n X).restrict (ball (d.center i) (ρ / 2 * d.radius i)),
        d.radius i ^ 2 * localGamma (hausdorff n X) hX.quadratic
          (d.residual i) (d.residual i) x ≤ G ^ 2 * d.source i ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SharpProjectionFamily, OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.localGamma