DyadicVolumeLower.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Dyadic lower volumes at every nearby center

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.rescaled_dyadic_volume_lower line 17

Source documentation

Iterating one scale-uniform doubling factor gives lower volumes at all dyadic radii, with the same factor for every nearby center.

theorem NoncollapsedRCD.rescaled_dyadic_volume_lower {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
    ∃ D : ℝ, 2 ≤ D ∧ ∀ (p : X) (R : ℝ), 0 < R → -1 ≤ K*R^2 →
      ∀ q : X, dist q p ≤ R → ∀ k : ℕ,
        (hausdorff n X).real (ball p R) ≤
          D^(k+1) * (hausdorff n X).real (ball q (R/2^k)) := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff