ScaledHeatAtBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Scale-invariant decrement constants for one fixed cutoff

theorem OAI.RegularPointCoordinates.exists_scaled_supported_heat_bound_at line 23

Source documentation

With fixed cutoff support, Gaussian constants give a common two-sided decrement constant before choosing the harmonic column, its full Bochner measure, the pole or the cutoff. This order permits subsequent mass absorption.

theorem exists_scaled_supported_heat_bound_at (m : ℕ) (hg : HasCoordinateHeatBounds μ ker)
    {Vlo Vhi Lambda : ℝ}
    (hVlo : 0 < Vlo) (hVhi : 0 < Vhi) (hLambda : 0 ≤ Lambda) :
    ∃ C : ℝ, 0 < C ∧
      ∀ (R : ℝ) (hR : 0 < R), R ≤ 1 → ∀ (lambda η : ℝ) (hlambda : 0 < lambda),
        0 ≤ η → (lambda + η) * R ^ 2 ≤ Lambda → ∀ (p : X) (r κ : ℝ) (L : ℝ≥0)
        (U : Euclidean (m + 2) →L[ℝ] SobolevSpace μ hQ)
        (M : PositiveBilinearMeasure X (Euclidean (m + 2)))
        (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v)
        (ρ Ccut : ℝ) (χ : GoodLaplacianCutoff μ hQ p ρ Ccut) (x : X),
        0 < ρ → ρ < r → 0 ≤ κ → 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda →
        (∀ y ∈ ball x (R / 4), (χ.weight : X → ℝ) y = 1) →
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.GoodLaplacianCutoff