OAI/Geometry/RCD/Coordinates/OutwardCovectorGrowth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.dyadic_covector_norm_reverse_growth line 18

   Source documentation

   The other half of the same adjacent mean comparison bounds smaller scale covectors by the original one. Together with shrinking radii this makes the center values of the actual affine fits tend to zero.

   theorem dyadic_covector_norm_reverse_growth {K : ℝ} (m : ℕ)
       (hX : NoncollapsedRCD K (m + 1) X) {a R ε : ℝ} (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) (hR : 0 < R) (hscale : a * (3 * R) ≤ 1) (hε : 0 ≤ ε)
       (hsmall : ((m + 1 : ℕ) : ℝ) ^ 2 * (normalizationVolumeRatio m * ε) ≤ 1 / 64)
       (S : ℕ → Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
       (hexact : ∀ i, IsExactMeanNormalization (hausdorff (m + 1) X) hX.quadratic
         (sobolevColumnMap (hausdorff (m + 1) X) hX.quadratic u)
         (ball p (R / 2 ^ i)) measurableSet_ball (S i))
       (hfirst : ∀ i, ∃ w : X → Euclidean (m + 1),
         FirstOrderSplittingOn (hausdorff (m + 1) X) hX.quadratic p (R / 2 ^ i) ε
   …

   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, OAI.RegularPointCoordinates.FirstOrderSplittingOn