OAI/Geometry/RCD/Heat/HeatHalfVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform volume comparison between a heat time and its half

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_half_volume_comparison line 15

    Source documentation

    The single scale comparison needed when splitting the heat semigroup.

    theorem NoncollapsedRCD.heat_half_volume_comparison {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
    ∃ D : ℝ, 1 ≤ D ∧ ∀ (t : ℝ), 0 < t → t ≤ 1 → ∀ z : X,
      (hausdorff n X).real (ball z (Real.sqrt t)) ≤
        D*(hausdorff n X).real (ball z (Real.sqrt (t/2))) := by
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff