OAI/Geometry/RCD/Sobolev/PoissonFamilyGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform interior gradient bounds for the actual Poisson family

  1. theorem OAI.RegularPointCoordinates.poisson_family_gradient line 16

    Source documentation

    A single gradient constant works for every center and actual replacement, including interior balls centered near the source center.

    theorem poisson_family_gradient {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (hgradient : LocalPoissonGradientInput hX) {κ B : ℝ} (hκ : 0 ≤ κ) :
    letI : IsLocallyFiniteMeasure (hausdorff n X) :=
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonGradientInput, OAI.RegularPointCoordinates.hausdorff