OAI/Geometry/RCD/Sobolev/HarmonicCutoffErrorIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_harmonic_cutoff_error_integral_bound line 26

   Source documentation

   Both error time integrals exist, and their sum vanishes with the averaging radius. The uniform constant uses only finitely many source masses.

   theorem exists_harmonic_cutoff_error_integral_bound (hg : HasCoordinateHeatBounds μ ker)
       (hdiff : HasGaussianHeatDifferenceBounds μ ker) (hρ : 0 < ρ) (hρr : ρ < r₀)
       {A V δ : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hδ : 0 < δ) :
       ∃ C : ℝ, 0 < C ∧ ∀ (R r : ℝ) (x q : X),
         0 < R → R ≤ 1 → 0 < r → r ≤ R →
         μ (ball q r) ≠ ∞ → V * r ^ n ≤ μ.real (ball q r) → dist x q ≤ A * r →
         (∀ z, ρ ≤ dist p z → dist p z ≤ 2 * ρ → δ ≤ dist x z) →
         (∀ t, 0 < t → t ≤ R ^ 2 → ∀ z, ρ ≤ dist p z → dist p z ≤ 2 * ρ →
           V * (Real.sqrt t) ^ n ≤ μ.real (ball z (Real.sqrt t))) →
         ∀ v : Euclidean n,
         IntervalIntegrable (fun t => ∫ z, kernelAverage μ ker t (ball q r) z *
           cutoffSourceDensity μ hQ (G v).energy χ.sobolev χ.laplacian z ∂μ) volume 0 (r ^ 2) ∧
   …

   Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.cutoffSourceDensity