MissingHeatMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniformly small heat mass lost by an interior cutoff

theorem OAI.RegularPointCoordinates.cutoff_heat_mass_error_le_outside line 22

Source documentation

A cutoff equal to one on a ball loses no more mass than the heat kernel places outside that ball.

theorem cutoff_heat_mass_error_le_outside {χ : X → ℝ}
    (hχ : Continuous χ) (hsχ : HasCompactSupport χ)
    (hχrange : ∀ y, 0 ≤ χ y ∧ χ y ≤ 1) (p : X) {t R : ℝ} (ht : 0 < t)
    (hχone : ∀ y ∈ ball p R, χ y = 1) :
    |(∫ y, χ y * ker t p y ∂μ) - 1| ≤ ∫ y in (ball p R)ᶜ, ker t p y ∂μ := by
…

theorem OAI.RegularPointCoordinates.missing_heat_mass_uniformly_small line 56

Source documentation

The missing mass tends uniformly to zero when the cutoff has more and more dyadic room around its pole.

theorem missing_heat_mass_uniformly_small (m : ℕ) {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison μ (comparisonModelVolume m a))
    (hfinite : ∀ x r, μ (ball x r) ≠ ∞)
    (hpos : ∀ x r, 0 < r → 0 < μ.real (ball x r))
    (hg : HasCoordinateHeatBounds μ ker) {η : ℝ} (hη : 0 < η) :
    ∃ N : ℕ, ∀ M, N ≤ M → ∀ p r R, 0 < r → r ≤ 1 → 2 ^ M * r ≤ R →
      ∀ χ : X → ℝ, Continuous χ → HasCompactSupport χ →
        (∀ y, 0 ≤ χ y ∧ χ y ≤ 1) → (∀ y ∈ ball p R, χ y = 1) →
          |(∫ y, χ y * ker (r ^ 2) p y ∂μ) - 1| < η := by
…

Mentions: OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.HasCoordinateHeatBounds