GaussianDyadicShells.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shell integration and Gaussian summability

theorem OAI.RegularPointCoordinates.summable_dyadic_gaussian line 18
Source documentation
A geometric volume or normalization loss is summable against the Gaussian decay on dyadic annuli.
```
theorem summable_dyadic_gaussian {b c d : ℝ} (hb : 0 ≤ b) (hc : 0 < c) (hd : 1 < d) :
    Summable (fun j : ℕ => b ^ j * Real.exp (-c * d ^ j)) := by
…
```
def OAI.RegularPointCoordinates.dyadicShell line 47
Source documentation
Disjoint dyadic balls, including the initial ball at index zero.
```
def dyadicShell (p : X) (r : ℝ) (j : ℕ) : Set X :=
…
```
theorem OAI.RegularPointCoordinates.dyadicShell_subset_ball line 50
theorem OAI.RegularPointCoordinates.iUnion_dyadicShell line 54
theorem OAI.RegularPointCoordinates.dyadicShell_separation line 62
theorem OAI.RegularPointCoordinates.measurableSet_dyadicShell line 75

theorem OAI.RegularPointCoordinates.integral_le_dyadic_shell_sum_of_product line 81

Source documentation

A weighted integral is bounded by a series of ball error budgets. The kernel bound is only needed on each disjoint shell.

theorem integral_le_dyadic_shell_sum_of_product (μ : Measure X) (p : X) {r : ℝ} (hr : 0 < r)
    {f w : X → ℝ} {W e : ℕ → ℝ}
    (hi : Integrable (fun x => w x * f x) μ)
    (hfi : ∀ j, IntegrableOn f (ball p (2 ^ j * r)) μ)
    (hf : ∀ᵐ x ∂μ, 0 ≤ f x) (hW : ∀ j, 0 ≤ W j)
    (hw : ∀ j, ∀ᵐ x ∂μ.restrict (dyadicShell p r j), w x * f x ≤ W j * f x)
    (he : ∀ j, (∫ x in ball p (2 ^ j * r), f x ∂μ) ≤ e j)
    (hsum : Summable (fun j => W j * e j)) :
    (∫ x, w x * f x ∂μ) ≤ ∑' j : ℕ, W j * e j := by
…

Mentions: OAI.RegularPointCoordinates.dyadicShell