GaussianUpperHeatIncrement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian kernel bounds give the actual upper heat decrement

theorem OAI.RegularPointCoordinates.shell_bound_of_displacement line 18

Source documentation

A scale-displacement Gaussian majorant gives the exact shell factor.

theorem shell_bound_of_displacement (p : X) {r C D : ℝ} (hr : 0 < r) (f : X → ℝ)
    (hbound : ∀ q : ℝ, 0 ≤ q → ∀ z, q * r ≤ dist p z →
      f z ≤ C * Real.exp (-q ^ 2 / D)) (j : ℕ) {z : X} (hz : z ∈ dyadicShell p r j) :
    f z ≤ C * gaussianShellFactor D⁻¹ j := by
…

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

theorem OAI.RegularPointCoordinates.gaussian_dyadic_heat_increment_upper line 41

Source documentation

The Gaussian shell convolution controls the actual upper decrement. The only exterior term is the explicitly decaying Gaussian times total mass.

theorem gaussian_dyadic_heat_increment_upper (m : ℕ)
    (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {s A D η lambda : ℝ} (hs : 0 < s) (hA : 0 ≤ A) (hD : 0 < D)
    (hlambda0 : 0 ≤ lambda) (hlambda : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda)
    (herror : ∀ t ∈ Icc (s ^ 2 / 4) (s ^ 2), ‖harmonicHeatError μ hQ (k := ker) G χ t p‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError