DyadicCovectorGrowth.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Slow growth of covectors in the same exact dyadic frames

theorem OAI.RegularPointCoordinates.dyadic_covector_norm_growth line 17

Source documentation

Exact normalization converts the adjacent mean comparison directly into slow growth of the covector norm used by the radial fit recurrence.

theorem dyadic_covector_norm_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