GlobalVolumeGrowth.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Global volume ratios for the Gaussian tail estimate

theorem OAI.RegularPointCoordinates.comparisonModelVolume_le_exp line 14
Source documentation
The hyperbolic comparison factor has at most exponential growth.
```
theorem comparisonModelVolume_le_exp (m : ℕ) {a R : ℝ} (ha : 0 ≤ a) (hR : 0 ≤ R) :
    comparisonModelVolume m a R ≤ Real.exp ((m : ℝ) * a * R) * R ^ (m + 1) := by
…
```
Mentions: OAI.RegularPointCoordinates.comparisonModelVolume

theorem OAI.RegularPointCoordinates.volume_ratio_le_exp line 32

Source documentation

Bishop--Gromov compares arbitrary radii with a polynomial and the explicit hyperbolic exponential factor.

theorem volume_ratio_le_exp (μ : Measure X) (m : ℕ) {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison μ (comparisonModelVolume m a))
    (p : X) {r R : ℝ} (hr : 0 < r) (hrR : r ≤ R) :
    μ.real (ball p R) ≤ Real.exp ((m : ℝ) * a * R) * (R / r) ^ (m + 1) *
      μ.real (ball p r) := by
…

Mentions: OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume

theorem OAI.RegularPointCoordinates.inverse_volume_at_distant_center_le line 52

Source documentation

A ball about the pole sits in a larger ball about any distant point. The inverse small-ball volume in the Gaussian upper bound therefore has an explicit estimate in terms of the pole's ball volume.

theorem inverse_volume_at_distant_center_le (μ : Measure X) (m : ℕ) {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison μ (comparisonModelVolume m a))
    (hfinite : ∀ x s, μ (ball x s) ≠ ⊤)
    (p y : X) {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R) (hpy : dist p y ≤ R)
    (hp : 0 < μ.real (ball p r)) :
    0 < μ.real (ball y r) ∧
      (μ.real (ball y r))⁻¹ ≤
        (Real.exp ((m : ℝ) * a * (r + R)) * ((r + R) / r) ^ (m + 1)) /
          μ.real (ball p r) := by
…

Mentions: OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume