VolumeRegime.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Volume convergence and the all-center volume regime

The volume-convergence hypothesis is the fixed-space rescaling specialization of De Philippis--Gigli (2018), Theorems 1.2 and 1.3. It concerns ball volumes in a Euclidean pointed limit. Bishop--Gromov comparison and the density upper bound then control all smaller balls around every nearby center.

def OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence line 29
Source documentation
Volume convergence for the normalized Hausdorff measure of an n-dimensional noncollapsed RCD space. omega is the Euclidean unit-ball volume. The source metric is unchanged: a rescaled radius R is s i * R in the original metric.
```
def EuclideanRescalingVolumeConvergence (μ : Measure X) (n : ℕ) (p : X)
    (omega : ℝ) : Prop :=
…
```
theorem OAI.RegularPointCoordinates.regular_rescaling_volume_converges line 36

theorem OAI.RegularPointCoordinates.regular_small_scale_volume line 48

Source documentation

The volume conclusion holds at every sufficiently small scale; there is no preselected favorable sequence of scales.

theorem regular_small_scale_volume {μ : Measure X} {n : ℕ} {p : X}
    {omega : ℝ} (hcompact : PointedRescalingPrecompactness p)
    (hregular : IsRegular n p)
    (hvolume : EuclideanRescalingVolumeConvergence μ n p omega)
    {epsilon : ℝ} (hepsilon : 0 < epsilon) :
    ∃ delta : ℝ, 0 < delta ∧ ∀ r : ℝ, 0 < r → r < delta →
      |μ.real (ball p r) / r ^ n - omega| < epsilon := by
…

Mentions: OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence

theorem OAI.RegularPointCoordinates.uniform_volume_error_of_outer_ball line 76

Source documentation

One large-ball lower bound and the density upper bound give two-sided Euclidean volume bounds at every smaller radius and center. All measures and distances here are in the original metric.

theorem uniform_volume_error_of_outer_ball
    {μ : Measure X} (m : ℕ) {a omega epsilon R D : ℝ} {p : X}
    (ha : 0 ≤ a) (homega : 0 < omega) (hepsilon1 : epsilon ≤ 1)
    (hRD : 0 < R + D)
    (hcomparison : BallVolumeComparison μ (comparisonModelVolume m a))
    (hdensity : ∀ y, SmallScaleVolumeUpper μ (comparisonModelVolume m a) y omega)
    (hfinite : ∀ y, μ (ball y (R + D)) ≠ ∞)
    (hlarge : ((1 - epsilon) * omega) * comparisonModelVolume m a (R + D) ≤
      μ.real (ball p R))
    (hmodel : Real.cosh (a * D) ^ m ≤ 1 + epsilon) :
    ∀ y, dist p y ≤ D → ∀ r, 0 < r → r ≤ D → r ≤ R + D →
      |μ.real (ball y r) / (omega * r ^ (m + 1)) - 1| ≤ epsilon := by
…

Mentions: OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SmallScaleVolumeUpper

theorem OAI.RegularPointCoordinates.exists_uniform_volume_neighborhood line 120

Source documentation

A regular point has a neighborhood on which every smaller ball has almost Euclidean volume. This constructs a single neighborhood working for all centers and all positive smaller radii simultaneously.

theorem exists_uniform_volume_neighborhood
    {μ : Measure X} (m : ℕ) {a omega epsilon rho : ℝ} {p : X}
    (ha : 0 ≤ a) (homega : 0 < omega) (hepsilon : 0 < epsilon)
    (hepsilon1 : epsilon ≤ 1) (hrho : 0 < rho)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular (m + 1) p)
    (hvolume : EuclideanRescalingVolumeConvergence μ (m + 1) p omega)
    (hcomparison : BallVolumeComparison μ (comparisonModelVolume m a))
    (hdensity : ∀ y, SmallScaleVolumeUpper μ (comparisonModelVolume m a) y omega)
    (hfinite : ∀ y r, μ (ball y r) ≠ ∞) :
    ∃ D : ℝ, 0 < D ∧ D ≤ rho ∧ ∀ y, dist p y ≤ D →
      ∀ r, 0 < r → r ≤ D →
        |μ.real (ball y r) / (omega * r ^ (m + 1)) - 1| ≤ epsilon := by
…

Mentions: OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SmallScaleVolumeUpper