DyadicInteriorBalls.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Expanding interior balls and their volume factors

theorem OAI.RegularPointCoordinates.expanding_radii line 14

Source documentation

Expanding radii have a dyadic gap available for a local mean estimate.

theorem expanding_radii {R : ℝ} (hR : 0 < R) (i : ℕ) :
    0 < R/(4*2^i) ∧ R/(4*2^i) ≤ R ∧
    0 < R-R/(2*2^i) ∧ R-R/(2*2^i) < R ∧
    (R-R/(2*2^i))+R/(4*2^i) = R-R/(2*2^(i+1)) := by
…

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.expanding_volume_factor line 33

Source documentation

The reciprocal volume cost grows by a fixed geometric factor.

theorem NoncollapsedRCD.expanding_volume_factor {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : X) (R : ℝ)
    (hR : 0 < R) (hcurv : -1 ≤ K*R^2) (i : ℕ) (q : X) (hq : dist q p ≤ R) :
    (hausdorff n X).real (ball p R) ≤
      ((8*Real.exp 4)^n*(2^n:ℝ)^i)*(hausdorff n X).real (ball q (R/(4*2^i))) := by
…

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