CutoffErrorEstimates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Annular support and heat bounds for the cutoff error

theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.error_zero_off_annulus line 19
Source documentation
The product-rule error lives only in the transition annulus.
```
theorem GoodLaplacianCutoff.error_zero_off_annulus {p : X} {r C : ℝ}
    (χ : GoodLaplacianCutoff μ hQ p r C) (g : SobolevSpace μ hQ) :
    ∀ᵐ z ∂μ, z ∉ {z | r ≤ dist p z ∧ dist p z ≤ 2 * r} →
      cutoffSourceDensity μ hQ g χ.sobolev χ.laplacian z = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.cutoffSourceDensity

theorem OAI.RegularPointCoordinates.abs_integral_mul_le_of_bound_on line 40

Source documentation

A kernel bound is needed only where the integrable error is supported.

theorem abs_integral_mul_le_of_bound_on {f k : X → ℝ} (hf : Integrable f μ)
    {S : Set X} {A : ℝ} (_hA : 0 ≤ A)
    (hzero : ∀ᵐ z ∂μ, z ∉ S → f z = 0) (hk : ∀ z ∈ S, |k z| ≤ A) :
    |∫ z, k z * f z ∂μ| ≤ A * ∫ z, |f z| ∂μ := by
…

theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.heat_error_le line 55

Source documentation

The cutoff error is controlled by a heat-kernel estimate on its annulus and its finite L1 mass.

theorem GoodLaplacianCutoff.heat_error_le {p : X} {r C : ℝ}
    (χ : GoodLaplacianCutoff μ hQ p r C) (g : SobolevSpace μ hQ)
    (k : X → ℝ) {A : ℝ} (hA : 0 ≤ A)
    (hk : ∀ z, r ≤ dist p z → dist p z ≤ 2 * r → |k z| ≤ A) :
    |∫ z, k z * cutoffSourceDensity μ hQ g χ.sobolev χ.laplacian z ∂μ| ≤
      A * ∫ z, |cutoffSourceDensity μ hQ g χ.sobolev χ.laplacian z| ∂μ :=
…

Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.cutoffSourceDensity

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.heatGram_le line 71

Source documentation

Unit heat mass and the local gradient bound give a uniform upper bound on the actual cutoff Gram, at every positive time.

theorem LocalHarmonicEnergy.heatGram_le
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχ : ∀ z, 0 ≤ χ z ∧ χ z ≤ 1)
    (hχs : HasCompactSupport (χ : X → ℝ))
    (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    {t : ℝ} (ht : 0 < t) (x : X) :
    ⟪v, cutoffHeatGram μ hQ hk χ.continuous hχs U ht x 0 v⟫_ℝ ≤
      (L : ℝ) ^ 2 * ‖v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.cutoffHeatGram