OAI/Geometry/RCD/Sobolev/FixedCutoffNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_fixed_cutoff_neighborhood line 22

   Source documentation

   The same actual cutoff works at every center in a smaller ball. Its annular error has one dyadic starting index for all those centers.

   theorem exists_fixed_cutoff_neighborhood {n : ℕ} {K R omega C : ℝ} {p : X}
       {U : Euclidean n →L[ℝ] SobolevSpace μ hQ}
       {M : PositiveBilinearMeasure X (Euclidean n)} {L : ℝ≥0}
       (G : ∀ v, LocalHarmonicEnergy μ hQ U M |K| p (4 * R) L v)
       (hg : HasCoordinateHeatBounds μ ker) (hR : 0 < R) (homega : 0 < omega)
       (hcurv : |K| * (16 * R) ^ 2 ≤ 1)
       (hvolume : ∀ y, dist p y ≤ 16 * R → ∀ s, 0 < s → s ≤ 32 * R →
         |μ.real (ball y s) / (omega * s ^ n) - 1| ≤ 1 / 2)
       (hcut : ∀ s, 0 < s → -1 ≤ K * s ^ 2 →
         Nonempty (GoodLaplacianCutoff μ hQ p s C)) :
       ∃ χ : GoodLaplacianCutoff μ hQ p (3 * R / 8) C, ∃ J : ℕ,
         ∀ q ∈ ball p (R / 32),
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.GoodLaplacianCutoff