GaussianShellKernel.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative Gaussian bounds on the actual dyadic shells

def OAI.RegularPointCoordinates.gaussianShellFactor line 15
Source documentation
The first shell contains the pole; subsequent shells have a Gaussian factor at their inner radius.
```
def gaussianShellFactor (c : ℝ) : ℕ → ℝ
  | 0 => 1
  | j + 1 => Real.exp (-c * 4 ^ j)
```
theorem OAI.RegularPointCoordinates.gaussianShellFactor_nonneg line 19
theorem OAI.RegularPointCoordinates.summable_gaussianShellFactor line 22

theorem OAI.RegularPointCoordinates.gaussian_upper_scaled_distance line 33

Source documentation

Cancel the reference radius from a Gaussian exponent and retain the actual volume normalization.

theorem gaussian_upper_scaled_distance (n : ℕ) {r q C V D B : ℝ}
    (hr : 0 < r) (hq : 0 ≤ q) (hC : 0 ≤ C) (hV : 0 < V) (hD : 0 < D)
    (p y : X)
    (hupper : k (r ^ 2) p y ≤ (C / μ.real (ball y r)) *
      Real.exp (-(dist p y) ^ 2 / (D * r ^ 2) + B * r ^ 2))
    (hvol : V * r ^ n ≤ μ.real (ball y r)) (hsep : q * r ≤ dist p y) :
    k (r ^ 2) p y ≤ (C / (V * r ^ n)) * Real.exp (B * r ^ 2) *
      Real.exp (-(q ^ 2) / D) := by
…

theorem OAI.RegularPointCoordinates.gaussian_shell_upper line 59

Source documentation

A Gaussian kernel bound on one actual dyadic shell.

theorem gaussian_shell_upper (n : ℕ) {r C V D B : ℝ}
    (hr : 0 < r) (hC : 0 ≤ C) (hV : 0 < V) (hD : 0 < D)
    (p : X) (j : ℕ) {y : X} (hy : y ∈ dyadicShell p r j)
    (hupper : k (r ^ 2) p y ≤ (C / μ.real (ball y r)) *
      Real.exp (-(dist p y) ^ 2 / (D * r ^ 2) + B * r ^ 2))
    (hvol : V * r ^ n ≤ μ.real (ball y r)) :
    k (r ^ 2) p y ≤ (C / (V * r ^ n)) * Real.exp (B * r ^ 2) *
      gaussianShellFactor D⁻¹ j := by
…

Mentions: OAI.RegularPointCoordinates.dyadicShell, OAI.RegularPointCoordinates.gaussianShellFactor

theorem OAI.RegularPointCoordinates.gaussian_cutoff_shell_upper line 85

Source documentation

The JLZ bound gives one explicit shell majorant for a cutoff kernel. Only the centers where the cutoff is nonzero need the volume lower bound.

theorem gaussian_cutoff_shell_upper (n : ℕ) {r C V D B : ℝ}
    (hr : 0 < r) (hC : 0 ≤ C) (hV : 0 < V) (hD : 0 < D)
    (p : X) {χ : X → ℝ} (hχ : ∀ y, 0 ≤ χ y ∧ χ y ≤ 1)
    (hk : ∀ y, 0 ≤ k (r ^ 2) p y)
    (hupper : ∀ y, k (r ^ 2) p y ≤ (C / μ.real (ball y r)) *
      Real.exp (-(dist p y) ^ 2 / (D * r ^ 2) + B * r ^ 2))
    (hvol : ∀ y, χ y ≠ 0 → V * r ^ n ≤ μ.real (ball y r))
    (j : ℕ) {y : X} (hy : y ∈ dyadicShell p r j) :
    χ y * k (r ^ 2) p y ≤ (C / (V * r ^ n)) * Real.exp (B * r ^ 2) *
      gaussianShellFactor D⁻¹ j := by
…

Mentions: OAI.RegularPointCoordinates.dyadicShell, OAI.RegularPointCoordinates.gaussianShellFactor