GaussianCutoffError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From local directional errors to actual cutoff heat errors

theorem OAI.RegularPointCoordinates.weighted_direction_error_integrable line 22

Source documentation

A bounded integrable nonnegative weight makes the directional Gram error integrable, even when the reference measure is infinite.

theorem weighted_direction_error_integrable (u : SobolevSpace μ hQ) (c : ℝ)
    {w : X → ℝ} (hw : AEStronglyMeasurable w μ) {C : ℝ≥0}
    (hb : ∀ᵐ x ∂μ, ‖w x‖ ≤ (C : ℝ)) (hi : Integrable w μ)
    (hpos : ∀ᵐ x ∂μ, 0 ≤ w x) :
    Integrable (fun x => w x * |localGamma μ hQ u u x - c|) μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.cutoff_heat_direction_error_le_series line 39

Source documentation

A ball error budget is integrated using the actual heat kernel. The Gaussian bound is used only where the cutoff is nonzero.

theorem cutoff_heat_direction_error_le_series (u : SobolevSpace μ hQ) (c : ℝ)
    (n : ℕ) (p : X) {r C V D B : ℝ} (hr : 0 < r)
    (hC : 0 ≤ C) (hV : 0 < V) (hD : 0 < D)
    (hχrange : ∀ y, 0 ≤ χ y ∧ χ y ≤ 1)
    (hupper : ∀ y, k (r ^ 2) p y ≤ (C / μ.real (ball y r)) *
      Real.exp (-(dist p y) ^ 2 / (D * r ^ 2) + B * r ^ 2))
    (hvol : ∀ y, χ y ≠ 0 → V * r ^ n ≤ μ.real (ball y r))
    {e : ℕ → ℝ}
    (he : ∀ j, (∫ y in ball p (2 ^ j * r),
      χ y * |localGamma μ hQ u u y - c| ∂μ) ≤ e j)
    (hsum : Summable (fun j => gaussianShellFactor D⁻¹ j * e j)) :
    (∫ y, (χ y * k (r ^ 2) p y) * |localGamma μ hQ u u y - c| ∂μ) ≤
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.gaussianShellFactor