RescaledBallVolume.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform nearby-ball volume ratios at bounded rescaled curvature

Only the existing CD condition is used. Nonnegative curvature uses the Euclidean ratio, and negative curvature uses the exponential distortion bound. The resulting constant is chosen before the center and radius.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.rescaled_ball_volume_lower line 21

Source documentation

The exact polynomial lower bound behind the scale-uniform volume factor.

theorem NoncollapsedRCD.rescaled_ball_volume_lower {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) {a δ : ℝ}
    (ha : 0 ≤ a) (hδ : 0 < δ) (hδ1 : δ ≤ 1)
    (p : X) (R : ℝ) (hR : 0 < R) (hcurv : -a ≤ K*R^2)
    (y : X) (hy : dist y p ≤ R) :
    (δ/(2*Real.exp (4*Real.sqrt a)))^n*(hausdorff n X).real (ball p R) ≤
      (hausdorff n X).real (ball y (δ*R)) := by
…

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

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.rescaled_ball_volume_factor line 92