FiniteScaleHeatError.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Heat error from a finite normalization range and a Gaussian tail

theorem OAI.RegularPointCoordinates.finite_scale_heat_direction_error line 22

Source documentation

Finite-scale errors and the raw tail bound integrate with the same Gaussian series. The radius cancels exactly against the kernel volume.

theorem finite_scale_heat_direction_error (u : SobolevSpace μ hQ) (c : ℝ)
    (n N : ℕ) (p : X) {r C V D B F b ε : ℝ} (hr : 0 < r)
    (hC : 0 ≤ C) (hV : 0 < V) (hD : 0 < D) (hF : 0 ≤ F) (hb : 0 ≤ b) (hε : 0 ≤ ε)
    (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))
    (hbudget : ∀ j, (∫ y in ball p (2 ^ j * r), χ y * |localGamma μ hQ u u y - c| ∂μ) ≤
      F * r ^ n * splitSeriesTerm (fun i => b ^ i) ε N j) :
    (∫ y, (χ y * k (r ^ 2) p y) * |localGamma μ hQ u u y - c| ∂μ) ≤
      (F * C / V) * Real.exp (B * r ^ 2) *
        (ε * (∑' j, b ^ j * gaussianShellFactor D⁻¹ j) +
…

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