OAI/Geometry/RCD/Harmonic/RadialVolumeProfile.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A continuous radial comparison profile directly from CD

Continuity of the radial profile gives null spheres directly from the curvature-dimension condition, before using integrated volume comparison.

  1. theorem OAI.RegularPointCoordinates.FullCD.hyperbolic_radial_ballVolumeComparison line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.sphere_null line 63

    Source documentation

    Every positive-radius sphere is null, without assuming model Bishop--Gromov in advance.

    theorem NoncollapsedRCD.sphere_null {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : X) {r : ℝ} (hr : 0 < r) :
    hausdorff n X (sphere p r) = 0 := by
…

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

  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.closedBall_measure_eq_ball line 82