OAI/Geometry/RCD/Sobolev/FiniteScaleCutoffBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.dyadicDirectionConstant line 15
2. theorem OAI.RegularPointCoordinates.dyadicDirectionConstant_nonneg line 18
3. theorem OAI.RegularPointCoordinates.dyadic_power_volume line 23
4. theorem OAI.RegularPointCoordinates.finite_scale_cutoff_budget line 35

   Source documentation

   The same original harmonic column supplies small directional error on all controlled scales and a fixed raw bound outside them. The cutoff therefore has a small finite prefix and a Gaussian-summable tail.

   theorem finite_scale_cutoff_budget {K : ℝ} (m : ℕ) (hX : NoncollapsedRCD K (m + 1) X)
       {a : ℝ} (ha : 0 ≤ a)
       (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
       (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
       (p : X) {r ε : ℝ} (hr : 0 < r) (hε : 0 ≤ ε)
       (hsmall : ((m + 1 : ℕ) : ℝ) ^ 2 * (normalizationVolumeRatio m * ε) ≤ 1 / 2)
       (A : Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
       (hA : IsExactMeanNormalization (hausdorff (m + 1) X) hX.quadratic
         (sobolevColumnMap (hausdorff (m + 1) X) hX.quadratic u) (ball p r) measurableSet_ball A)
       (k : ℕ) (hscale : ∀ j ≤ k, a * (3 * (2 ^ j * r)) ≤ 1)
       (hnormal : ∀ j ≤ k, ∃ (S : Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
         (w : X → Euclidean (m + 1)),
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizationVolumeRatio, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap