UniformHeatMassTail.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform heat mass tails on spaces with Bishop--Gromov comparison

def OAI.RegularPointCoordinates.gaussianMassEnvelope line 15
theorem OAI.RegularPointCoordinates.gaussianMassEnvelope_nonneg line 19
theorem OAI.RegularPointCoordinates.summable_gaussianMassEnvelope line 25

theorem OAI.RegularPointCoordinates.exists_uniform_heat_mass_tail line 35

Source documentation

The tail bound is uniform in the pole and in all reference radii at most one. No global Euclidean volume hypothesis is used.

theorem exists_uniform_heat_mass_tail (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) :
    ∃ C : ℝ, 0 < C ∧ ∀ p r, 0 < r → r ≤ 1 → ∀ N : ℕ,
      (∫ y in (ball p (2 ^ N * r))ᶜ, ker (r ^ 2) p y ∂μ) ≤
        C * ∑' j, gaussianMassEnvelope m a (j + (N + 1)) := by
…

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