OAI/Geometry/RCD/Metric/RescalingVolumeDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absolute ball-volume profiles at every shrinking scale

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.rescaling_volume_density line 14
  2. theorem OAI.RegularPointCoordinates.rescaling_volume_convergence_of_density line 35

    Source documentation

    Euclidean density convergence gives absolute volume convergence at every rescaled radius.

    theorem rescaling_volume_convergence_of_density {n : ℕ} {p : X}
    (hdensity : ∀ s : ℕ → ℝ, (∀ k, 0 < s k) → Tendsto s atTop (𝓝 0) →
      Tendsto (fun k => (hausdorff n X).real (ball p (s k))/(s k)^n)
        atTop (𝓝 (euclideanUnitVolume n))) :
    EuclideanRescalingVolumeConvergence (hausdorff n X) n p (euclideanUnitVolume n) := by
…

    Mentions: OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.euclideanUnitVolume, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence