OAI/Geometry/RCD/Sobolev/DyadicTailBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dyadic_tail_bound line 19

   Source documentation

   An absolute-value truncation turns the dyadic support estimate into faster-than-quadratic decay of the level-set measures.

   theorem NoncollapsedRCD.dyadic_tail_bound {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
       ∃ C D : ℝ, 0 < C ∧ 2 ≤ D ∧ ∀ (p : X) (R : ℝ), 0 < R → -1 ≤ K*R^2 →
         ∀ w : SobolevSpace.dirichlet (hausdorff n X) hX.quadratic (ball p R),
         ∀ (t : ℝ), 0 < t → ∀ k : ℕ,
         2*D^(k+1)*‖SobolevSpace.toLp (hausdorff n X) hX.quadratic w.val‖^2 ≤
           (hausdorff n X).real (ball p R)*t^2 →
         t^2 * (hausdorff n X).real (ball p R ∩
           {x | 2*t < |SobolevSpace.toLp (hausdorff n X) hX.quadratic w.val x|}) ≤
           C*(R/2^k)^2 * energyForm (hausdorff n X) hX.quadratic w.val w.val := by
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm