HeatBallPowerVolume.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial lower bounds for kernel normalization balls

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_ball_volume_lower line 17

Source documentation

Every small normalization ball with center in twice the working ball retains a dimensional polynomial fraction of the working volume.

theorem NoncollapsedRCD.heat_ball_volume_lower {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : X) {R t : ℝ}
    (hR : 0 < R) (hcurv : -1 ≤ K*R^2) (ht : 0 < t) (htR : t ≤ R^2)
    (z : X) (hz : dist z p ≤ 2*R) :
    (Real.sqrt t/(4*Real.exp 8*R))^n*(hausdorff n X).real (ball p R) ≤
      (hausdorff n X).real (ball z (Real.sqrt t)) := by
…

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