UniformHeatMassIncrement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform dyadic heat lower bounds with the correct mass scaling

theorem OAI.RegularPointCoordinates.uniform_gaussian_lower_time_block line 19

Source documentation

Gaussian lower constants are fixed before choosing the scale or pole. Only the stated local volume upper bounds are needed on the testing set.

theorem uniform_gaussian_lower_time_block (μ : Measure X) {ker : ℝ → X → X → ℝ}
    (hg : HasCoordinateHeatBounds μ ker) (n : ℕ)
    {V A : ℝ} (hV : 0 < V) (hA : 0 ≤ A) :
    ∃ c : ℝ, 0 < c ∧ ∀ r, 0 < r → r ≤ 1 → ∀ (x : X) (S : Set X),
      (∀ t, r ^ 2 / 4 ≤ t → t ≤ r ^ 2 → ∀ y ∈ S,
        0 < μ.real (ball y (Real.sqrt t)) ∧ μ.real (ball y (Real.sqrt t)) ≤ V * r ^ n) →
      (∀ y ∈ S, (dist x y) ^ 2 ≤ A * r ^ 2) →
      ∀ t, r ^ 2 / 4 ≤ t → t ≤ r ^ 2 → ∀ y ∈ S, c / r ^ n ≤ ker t x y := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds

theorem OAI.RegularPointCoordinates.dyadic_heat_increment_lower_mass line 51

Source documentation

On a dyadic time block the actual heat decrement dominates the local mass with its dimensionless factor r²/rⁿ. The mass is the full measure.

theorem dyadic_heat_increment_lower_mass (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    (S : Set X) (hS : MeasurableSet S) (hχone : ∀ y ∈ S, (χ.weight : X → ℝ) y = 1)
    {s c η 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 p‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError