VolumeDensity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The small-scale Hausdorff-volume upper bound

The CD-derived Hausdorff ball estimate has an exponential factor tending to one. It supplies the exact small-scale density input for every nonnegative comparison curvature parameter.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.normalized_ball_volume_upper line 24
Source documentation
The normalized Hausdorff volume has the explicit CD exponential upper bound, with its exact Euclidean normalization.
```
theorem NoncollapsedRCD.normalized_ball_volume_upper {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : X) {r : ℝ} (hr : 0 < r) :
    (hausdorff n X).real (ball p r) ≤
      (euclideanUnitVolume n *
        Real.exp (2*r*Real.sqrt (|K|/((n:ℝ)-1))) ^ n) * r ^ n := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.euclideanUnitVolume
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.smallScaleVolumeUpper line 48
Source documentation
The CD Hausdorff estimate implies the exact small-scale volume upper bound for every nonnegative comparison curvature parameter.
```
theorem NoncollapsedRCD.smallScaleVolumeUpper {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) {a : ℝ} (ha : 0 ≤ a) (p : X) :
    SmallScaleVolumeUpper (hausdorff n X) (comparisonModelVolume (n-1) a)
      p (euclideanUnitVolume n) := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SmallScaleVolumeUpper, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.euclideanUnitVolume