OAI/Geometry/RCD/Heat/HeatMassIncrement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.gaussian_lower_on_time_block line 22

   Source documentation

   One Gaussian lower constant works on the entire dyadic time block, including when the reference measure has global negative-curvature growth.

   theorem gaussian_lower_on_time_block (hg : HasGaussianHeatBounds μ ker)
       (n : ℕ) {r V A : ℝ} (hr : 0 < r) (hV : 0 < V) (hA : 0 ≤ A)
       (x : X) (S : Set X)
       (hvolume : ∀ t, r ^ 2 / 4 ≤ t → t ≤ r ^ 2 → ∀ y ∈ S,
         0 < μ.real (ball y (Real.sqrt t)) ∧
           μ.real (ball y (Real.sqrt t)) ≤ V * r ^ n)
       (hdist : ∀ y ∈ S, (dist x y) ^ 2 ≤ A * r ^ 2) :
       ∃ c : ℝ, 0 < c ∧ ∀ t, r ^ 2 / 4 ≤ t → t ≤ r ^ 2 → ∀ y ∈ S, c ≤ ker t x y := by
   …

   Mentions: OAI.RegularPointCoordinates.HasGaussianHeatBounds

2. theorem OAI.RegularPointCoordinates.harmonic_heat_increment_lower_mass line 57

   Source documentation

   Integrating the canonical lower heat derivative controls the full Bochner mass on any set where the cutoff is one. No density for the mass measure is required.

   theorem harmonic_heat_increment_lower_mass (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
       (S : Set X) (hS : MeasurableSet S) (hχone : ∀ y ∈ S, (χ.weight : X → ℝ) y = 1)
       {s t c η lambda : ℝ} (hs : 0 < s) (hst : s ≤ t) (hlambda0 : 0 ≤ lambda)
       (hlambda : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda)
       (herror : ∀ u ∈ Icc s t, ‖harmonicHeatError μ hQ (k := ker) G χ u p‖ ≤ η)
   …

   Mentions: OAI.RegularPointCoordinates.harmonicHeatError