OAI/Geometry/RCD/Coordinates/HeatNormalizationVolume.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Volume factors at the Gaussian localization scale

These estimates use the actual CD volume comparison already proved for the space. There is no model-volume or Gaussian premise.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.ball_volume_ratio_exp line 23
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.gaussian_normalization_volume line 46