GlobalGaussianShell.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Global Gaussian shell bounds from Bishop--Gromov

theorem OAI.RegularPointCoordinates.dyadic_volume_polynomial_bound line 17
Source documentation
The polynomial cost of moving the volume center and then integrating one shell has a fixed geometric rate.
```
theorem dyadic_volume_polynomial_bound (n j : ℕ) {r : ℝ} (hr : 0 < r) :
    ((r + 2 ^ j * r) / r) ^ n * ((2 ^ j * r) / r) ^ n ≤
      (2 : ℝ) ^ n * ((2 : ℝ) ^ (2 * n)) ^ j := by
…
```
def OAI.RegularPointCoordinates.globalGaussianShellBound line 39
Source documentation
The pole volume normalizes a kernel bound on any dyadic shell, even outside an almost Euclidean region.
```
def globalGaussianShellBound (m : ℕ) (a C B D r : ℝ) (p : X) (j : ℕ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.global_gaussian_shell_bound line 45

theorem OAI.RegularPointCoordinates.global_gaussian_shell_volume_bound line 69

Source documentation

Integrating the shell bound cancels the pole volume. The remaining majorant is uniform for all reference radii at most one.

theorem global_gaussian_shell_volume_bound (m : ℕ) {a C B D r : ℝ}
    (ha : 0 ≤ a) (hC : 0 ≤ C) (hB : 0 ≤ B) (hr : 0 < r) (hr1 : r ≤ 1)
    (hBG : BallVolumeComparison μ (comparisonModelVolume m a))
    (p : X) (hp : 0 < μ.real (ball p r)) (j : ℕ) :
    globalGaussianShellBound μ m a C B D r p j * μ.real (ball p (2 ^ j * r)) ≤
      (C * Real.exp (B + (m : ℝ) * a) * (2 : ℝ) ^ (m + 1)) *
        (((2 : ℝ) ^ (2 * (m + 1))) ^ j *
          Real.exp ((2 * (m : ℝ) * a) * 2 ^ j) * gaussianShellFactor D⁻¹ j) := by
…

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