OAI/Geometry/RCD/Heat/HeatBlockVolumes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.heat_block_volume_bounds line 18

   Source documentation

   The common almost-Euclidean volume regime supplies the upper and lower Gaussian denominators throughout an entire dyadic time block.

   theorem heat_block_volume_bounds (μ : Measure X) (n : ℕ) (z : X)
       {omega ε D s t : ℝ} (homega : 0 < omega) (hε : ε < 1)
       (hs : 0 < s) (hsD : s ≤ D) (ht : t ∈ Icc (s ^ 2 / 4) (s ^ 2))
       (hvolume : ∀ r, 0 < r → r ≤ D →
         |μ.real (ball z r) / (omega * r ^ n) - 1| ≤ ε) :
       0 < μ.real (ball z (Real.sqrt t)) ∧
         ((1 - ε) * omega / 2 ^ n) * s ^ n ≤ μ.real (ball z (Real.sqrt t)) ∧
         μ.real (ball z (Real.sqrt t)) ≤ ((1 + ε) * omega) * s ^ n := by
   …

2. theorem OAI.RegularPointCoordinates.dyadic_heat_bounds_of_volume_regime line 65

   Source documentation

   A single almost-Euclidean volume regime supplies all volume hypotheses of the uniform decrement theorem.

   theorem dyadic_heat_bounds_of_volume_regime (hg : HasCoordinateHeatBounds μ ker)
       (m : ℕ) (hn : n = m + 2) (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
       {R omega ε η lambda : ℝ} (hR : 0 < R) (hR1 : R ≤ 1)
       (homega : 0 < omega) (hε : 0 ≤ ε) (hε1 : ε < 1)
       (hη : 0 ≤ η) (hlambda : 0 < lambda)
       (hreg : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda)
       (hχone : ∀ y ∈ ball p R, (χ.weight : X → ℝ) y = 1)
       (herror : ∀ t, 0 < t → t ≤ R ^ 2 → ‖harmonicHeatError μ hQ (k := ker) G χ t p‖ ≤ η)
   …

   Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.harmonicHeatError