GaussianTimeBlock.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian shell bounds uniform over a dyadic time block

theorem OAI.RegularPointCoordinates.gaussian_time_displacement_upper line 18

Source documentation

On times t≤r², the same spatial Gaussian at scale r bounds every kernel in the block once the time-dependent volume has a uniform lower bound.

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

theorem OAI.RegularPointCoordinates.gaussian_time_shell_upper line 48

Source documentation

A single coefficient bounds a full spatial shell at every time in the block. Its Gaussian tail has no dependence on the selected time.

theorem gaussian_time_shell_upper (n : ℕ) {t r C V D B : ℝ}
    (ht : 0 < t) (htr : t ≤ r ^ 2) (hr : 0 < r)
    (hC : 0 ≤ C) (hV : 0 < V) (hD : 0 < D) (hB : 0 ≤ B)
    (p : X) (j : ℕ) {z : X} (hz : z ∈ dyadicShell p r j)
    (hupper : ker t p z ≤ (C / μ.real (ball z (Real.sqrt t))) *
      Real.exp (-(dist p z) ^ 2 / (D * t) + B * t))
    (hvol : V * r ^ n ≤ μ.real (ball z (Real.sqrt t))) :
    ker t p z ≤ (C / (V * r ^ n)) * Real.exp (B * r ^ 2) * gaussianShellFactor D⁻¹ j := by
…

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