OAI/Geometry/RCD/Sobolev/CutoffErrorL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.error_L1_le line 19

   Source documentation

   The source is estimated on its actual support. Young's inequality uses only the energy-gradient integral on the enclosing ball.

   theorem GoodLaplacianCutoff.error_L1_le {p : X} {ρ C R B : ℝ}
       (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρ : 0 < ρ) (hC : 0 ≤ C)
       (hroom : 2 * ρ < R) (g : SobolevSpace μ hQ)
       (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x| ≤ B) :
       (∫ x, |cutoffSourceDensity μ hQ g χ.sobolev χ.laplacian x| ∂μ) ≤
         (B * (C / ρ ^ 2) + (C / ρ) ^ 2) * μ.real (ball p R) +
           ∫ x in ball p R, localGamma μ hQ g g x ∂μ := by
   …

   Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.cutoffSourceDensity, OAI.RegularPointCoordinates.localGamma