OAI/Geometry/RCD/Sobolev/DistancePoissonGradient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform gradient bounds for the constructed distance Poisson sequence

  1. theorem OAI.RegularPointCoordinates.DistancePoissonFamily.value_bound line 15
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.distance_poisson_family_gradient line 42

    Source documentation

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

    theorem NoncollapsedRCD.distance_poisson_family_gradient {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    [(hausdorff n X).Regular] (hK : K≤0) (p₀ : X) {κ B : ℝ} (hκ : 0≤κ) :
    letI : IsLocallyFiniteMeasure (hausdorff n X) :=
…

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