DyadicNormalizedError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform directional errors in a fixed dyadic normalizing frame

theorem OAI.RegularPointCoordinates.dyadic_normalized_mean_bound line 18

Source documentation

Outward mean comparisons become a norm estimate in the initial exact frame.

theorem dyadic_normalized_mean_bound {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

theorem OAI.RegularPointCoordinates.dyadic_error_coefficient_le line 52

Source documentation

The coefficient in the directional estimate grows at most like 2^k, while retaining the original splitting error.

theorem dyadic_error_coefficient_le {n C ε : ℝ} (hC : 0 ≤ C)
    (hε : 0 ≤ ε) (hsmall : n ^ 2 * (C * ε) ≤ 1 / 2) (k : ℕ) :
    (n ^ 2 * ε) * (1 + 2 * (n ^ 2 * (C * ε)) * (2 ^ k - 1)) +
      2 * (n ^ 2 * (C * ε)) * (2 ^ k - 1) ≤
      (n ^ 2 + 2 * (n ^ 2 * C)) * ε * 2 ^ k := by
…

theorem OAI.RegularPointCoordinates.dyadic_normalized_directional_error line 69

Source documentation

Every finite outward dyadic ball has a directional L1 error bounded by the initial splitting tolerance times an explicit geometric factor.

theorem dyadic_normalized_directional_error {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)),
…