UniformHeatCumulative.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform cumulative heat estimates from actual splitting data

theorem OAI.RegularPointCoordinates.uniform_heat_cumulative_of_splitting line 25

Source documentation

All smallness is chosen before the harmonic map, its Bochner measure, and the working radius. From actual splitting, cutoff and volume data the heat comparison, slow growth, small mass and both decrement bounds imply the cumulative comparison. No cumulative conclusion is an input.

theorem uniform_heat_cumulative_of_splitting {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison (hausdorff (m + 2) X) (comparisonModelVolume (m + 1) a))
    {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff (m + 2) X) hX.quadratic ker)
    (hg : HasCoordinateHeatBounds (hausdorff (m + 2) X) ker)
    {L B Vlo Vhi C η lambda : ℝ} (hL : 0 ≤ L) (hB : 0 ≤ B)
    (hVlo : 0 < Vlo) (hVhi : 0 < Vhi) (hC : 0 ≤ C) (hη : 0 ≤ η) (hlambda : 0 < lambda) :
    ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧
      ∀ (R : ℝ) (hR : 0 < R), R ≤ 1 → a * (3 * R) ≤ 1 →
      ∀ (u : Fin (m + 2) → SobolevSpace (hausdorff (m + 2) X) hX.quadratic)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.SobolevSpace