UniformDyadicHeatBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform two-sided decrement bound for the actual heat family

theorem OAI.RegularPointCoordinates.uniform_dyadic_heat_bounds line 26

Source documentation

The published Gaussian bound, volume bounds and the actual annular error estimate imply both decrement bounds with one constant. In particular, the envelope and the lower mass are constructed from the same full measure.

theorem uniform_dyadic_heat_bounds (hg : HasCoordinateHeatBounds μ ker)
    (m : ℕ) (hn : n = m + 2) (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {R Vlo Vhi η lambda : ℝ} (hR : 0 < R) (hR1 : R ≤ 1)
    (hVlo : 0 < Vlo) (hVhi : 0 < Vhi) (hη : 0 ≤ η) (hlambda : 0 < lambda)
    (hreg : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda)
    (hχone : ∀ y ∈ ball p R, (χ.weight : X → ℝ) y = 1)
    (herror : ∀ t, 0 < t → t ≤ R ^ 2 → ‖harmonicHeatError μ hQ (k := ker) G χ t p‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.harmonicHeatError