UniformSupportedHeatBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Decrement constants chosen before the harmonic coordinates and mass

theorem OAI.RegularPointCoordinates.exists_uniform_supported_heat_bound 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_uniform_supported_heat_bound (m : ℕ) (hg : HasCoordinateHeatBounds μ ker)
    {Vlo Vhi η lambda : ℝ}
    (hVlo : 0 < Vlo) (hVhi : 0 < Vhi) (hη : 0 ≤ η) (hlambda : 0 < lambda) :
    ∃ C : ℝ, 0 < C ∧
      ∀ (R : ℝ) (hR : 0 < R), R ≤ 1 → ∀ (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),
        0 < ρ → ρ < r → 0 ≤ κ → 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda →
        (∀ y ∈ ball p (R / 4), (χ.weight : X → ℝ) y = 1) →
        (∀ y ∉ ball p R, (χ.weight : X → ℝ) y = 0) →
…

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