RegularHeatCutoff.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniformly negligible cutoff heat errors near a regular point

The volume lower bound needed for the Gaussian tail estimate is supplied by the already proved regular-point volume neighborhood, rather than by an additional analytic assumption.

theorem OAI.RegularPointCoordinates.regular_uniform_heat_cutoff_errors line 29

Source documentation

At a regular point a single volume neighborhood gives uniform small-time cutoff-error estimates for every smaller supported cutoff.

theorem regular_uniform_heat_cutoff_errors
    (m : ℕ) {a ω R : ℝ} {p : X} (ha : 0 ≤ a) (hω : 0 < ω) (hR : 0 < R)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular (m + 1) p)
    (hvolume : EuclideanRescalingVolumeConvergence μ (m + 1) p ω)
    (hBG : BallVolumeComparison μ (comparisonModelVolume m a))
    (hdensity : ∀ y, SmallScaleVolumeUpper μ (comparisonModelVolume m a) y ω)
    (hfinite : ∀ y r, μ (ball y r) ≠ ∞) (hg : HasCoordinateHeatBounds μ k) :
    ∃ D : ℝ, 0 < D ∧ D ≤ R ∧ ∀ ρ, 0 < ρ → 2 * ρ ≤ D →
      ∀ C (χ : GoodLaplacianCutoff μ hQ p ρ C) (g : SobolevSpace μ hQ),
        ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
          ∀ t, 0 < t → t < δ → ∀ x ∈ ball p (ρ / 2),
            |∫ z, k t x z * cutoffSourceDensity μ hQ g χ.sobolev χ.laplacian z ∂μ| < ε := by
…