OAI/Geometry/RCD/Coordinates/RegularSharpProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_sharp_projection_constants line 19

   Source documentation

   The actual two-center projection has a uniform sharp bound on the same regular neighborhood, under the explicitly separated metric and source tolerances.

   theorem regular_sharp_projection_constants {K : ℝ} (m : ℕ)
       (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
       (hgradient : LocalHarmonicL2GradientInput hX) (hmean : LocalHarmonicL2MeanValueInput hX)
       (hmeasured : LocalMeasuredCoordinateInput hX)
       (hhessian : LocalPoissonHessianActionInput hX)
       (hproduct : LocalPoissonGradientProductInput hX)
       (hpoincare : LocalMeanPoincareInput hX)
       (hcompact : LocalPoissonHarmonicCompactnessInput hX)
       {κ B J C A Cχ epsilon D : ℝ}
       (hκ : 0 ≤ κ) (hK : -κ ≤ K) (hB : 0 ≤ B) (hJ : 0 ≤ J) (hCχ : 0 ≤ Cχ) (hA : 0 ≤ A)
       (hepsilon : 0 ≤ epsilon)
       (hsmall : ((m + 2 : ℕ) : ℝ) ^ 2 *
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.LocalMeanPoincareInput, OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput