HarmonicCutoffErrorBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for every direction of the actual annular error

theorem OAI.RegularPointCoordinates.abs_quadratic_le_norm line 15

theorem OAI.RegularPointCoordinates.exists_harmonic_cutoff_error_bound line 34

Source documentation

Finitely many genuine L1 error masses control every direction, uniformly in the averaging scale and center subject to the stated volume/separation bounds.

theorem exists_harmonic_cutoff_error_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 t : ℝ) (x q : X),
      0 < r → r ≤ 1 → 0 < t → t ≤ 1 →
      μ (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) →
      (∀ z, ρ ≤ dist p z → dist p z ≤ 2 * ρ →
        V * (Real.sqrt t) ^ n ≤ μ.real (ball z (Real.sqrt t))) →
      ∀ v : Euclidean n,
      (t ≤ r ^ 2 → |∫ z, kernelAverage μ ker t (ball q r) z *
        cutoffSourceDensity μ hQ (G v).energy χ.sobolev χ.laplacian z ∂μ| ≤ C * ‖v‖ ^ 2) ∧
…

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