OAI/Geometry/RCD/Metric/UniformVolumeRatio.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.normalizationVolumeRatio line 14
2. theorem OAI.RegularPointCoordinates.normalizationVolumeRatio_ge_one line 16
3. theorem OAI.RegularPointCoordinates.nearby_normalization_volume_ratio line 25

   Source documentation

   Bishop--Gromov supplies the volume loss used to localize splitting maps; the constant depends only on the dimension when curvature times radius is bounded.

   theorem nearby_normalization_volume_ratio {X : Type*} [MetricSpace X]
       [MeasurableSpace X] [BorelSpace X] {K : ℝ} (m : ℕ)
       (hX : NoncollapsedRCD K (m + 1) X) {a : ℝ} (ha : 0 ≤ a)
       (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
       {p q : X} {R : ℝ} (hR : 0 < R) (hcurv : a * (3 * R) ≤ 1)
       (hq : q ∈ ball p (R / 4)) :
       (hausdorff (m + 1) X).real (ball p (2 * R)) ≤
         normalizationVolumeRatio m * (hausdorff (m + 1) X).real (ball q (R / 2)) := by
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.normalizationVolumeRatio