GaussianVolumeMoment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Local volume integration of Gaussian source bounds

def OAI.RegularPointCoordinates.gaussianVolumeMomentConstant line 16
Source documentation
The local Gaussian volume sum has finite total mass in every fixed dimension. It will control bounded-density curvature sources.
```
def gaussianVolumeMomentConstant (n : ℕ) (c : ℝ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.gaussianVolumeMomentConstant_nonneg line 19

theorem OAI.RegularPointCoordinates.integral_gaussian_shell_le_volume line 27

Source documentation

Integrating a supported Gaussian only needs upper ball volumes at the finitely many scales inside its support.

theorem integral_gaussian_shell_le_volume (ν : Measure X) [IsFiniteMeasure ν]
    (n : ℕ) (x : X) {s C c V : ℝ} (hs : 0 < s) (hC : 0 ≤ C) (hc : 0 < c) (hV : 0 ≤ V)
    (N : ℕ) {f : X → ℝ} (hf : Integrable f ν)
    (hlocal : ∀ j ≤ N, ∀ z ∈ dyadicShell x s j,
      f z ≤ C / s ^ n * gaussianShellFactor c j)
    (hzero : ∀ z ∉ ball x (2 ^ N * s), f z = 0)
    (hvolume : ∀ j ≤ N, ν.real (ball x (2 ^ j * s)) ≤ V * (2 ^ j * s) ^ n) :
    (∫ z, f z ∂ν) ≤ C * V * gaussianVolumeMomentConstant n c := by
…

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