GaussianVolumeTail.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform small-time cutoff errors from local volume lower bounds

theorem OAI.RegularPointCoordinates.sqrt_power_inverse line 16

theorem OAI.RegularPointCoordinates.HasCoordinateHeatBounds.off_diagonal_small line 29

Source documentation

Quantitative Gaussian bounds and a local Euclidean volume lower bound force uniform decay on any two positively separated sets.

theorem HasCoordinateHeatBounds.off_diagonal_small
    (hg : HasCoordinateHeatBounds μ k)
    (hnonneg : ∀ t, 0 < t → ∀ x y, 0 ≤ k t x y)
    (n : ℕ) (P S : Set X) {d D V : ℝ} (hd : 0 < d) (hD : 0 < D) (hV : 0 < V)
    (hsep : ∀ x ∈ P, ∀ y ∈ S, d ≤ dist x y)
    (hvol : ∀ y ∈ S, ∀ s, 0 < s → s ≤ D → V * s ^ n ≤ μ.real (ball y s))
    {η : ℝ} (hη : 0 < η) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ t, 0 < t → t < δ → ∀ x ∈ P, ∀ y ∈ S, |k t x y| ≤ η := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds

theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.heat_error_uniformly_small line 64

Source documentation

The actual product-rule cutoff error tends to zero uniformly at interior poles. Only local volume lower bounds on its annulus are used.

theorem GoodLaplacianCutoff.heat_error_uniformly_small
    (hg : HasCoordinateHeatBounds μ k) {p : X} {ρ C D V : ℝ}
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρ : 0 < ρ) (hD : 0 < D) (hV : 0 < V)
    (n : ℕ) (hvol : ∀ y, ρ ≤ dist p y → dist p y ≤ 2 * ρ →
      ∀ s, 0 < s → s ≤ D → V * s ^ n ≤ μ.real (ball y s))
    (g : SobolevSpace μ hQ) {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ t, 0 < t → t < δ → ∀ x ∈ ball p (ρ / 2),
      |∫ z, k t x z * cutoffSourceDensity μ hQ g χ.sobolev χ.laplacian z ∂μ| < ε := by
…

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