HeatPoleIncrements.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Heat increments with a fixed cutoff center and a variable pole

theorem OAI.RegularPointCoordinates.harmonic_heat_increment_lower_mass_at line 23

Source documentation

The cutoff and energy are fixed; the pole is an independent point.

theorem harmonic_heat_increment_lower_mass_at (x : X) (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    (S : Set X) (hS : MeasurableSet S) (hχone : ∀ y ∈ S, (χ.weight : X → ℝ) y = 1)
    {s t c η lambda : ℝ} (hs : 0 < s) (hst : s ≤ t) (hlambda0 : 0 ≤ lambda)
    (hlambda : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda)
    (herror : ∀ u ∈ Icc s t, ‖harmonicHeatError μ hQ (k := ker) G χ u x‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError

theorem OAI.RegularPointCoordinates.dyadic_heat_increment_upper_bound_at line 65

Source documentation

The upper increment also uses an independent heat pole.

theorem dyadic_heat_increment_upper_bound_at (x : X) (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {s E η lambda : ℝ} (hs : 0 < s) (hlambda0 : 0 ≤ lambda)
    (hlambda : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda)
    (herror : ∀ t ∈ Icc (s ^ 2 / 4) (s ^ 2), ‖harmonicHeatError μ hQ (k := ker) G χ t x‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError