VolumeComparison.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Transferring volume information between centers and scales

The comparison hypothesis is the cross-multiplied ball-volume inequality from Bishop--Gromov. Its model function remains explicit, so the argument applies to the negative-curvature models before taking the flat limit.

def OAI.RegularPointCoordinates.BallVolumeComparison line 24
Source documentation
The ball comparison in Sturm (2006), Theorem 2.3, equation (2.5), written without divisions. For the application the model is the radial volume of the constant negative-curvature comparison space.
```
def BallVolumeComparison (μ : Measure X) (model : ℝ → ℝ) : Prop :=
…
```

theorem OAI.RegularPointCoordinates.volume_lower_at_nearby_center line 30

Source documentation

A central large ball lies in a slightly enlarged ball about every nearby center, so its volume gives a lower bound at every smaller scale.

theorem volume_lower_at_nearby_center
    {μ : Measure X} {model : ℝ → ℝ} (hcomparison : BallVolumeComparison μ model)
    {p y : X} {R D r a : ℝ} (hy : dist p y ≤ D) (hr : 0 < r)
    (hrR : r ≤ R + D) (hmodelr : 0 ≤ model r) (hmodelR : 0 < model (R + D))
    (hfinite : μ (ball y (R + D)) ≠ ∞)
    (hlarge : a * model (R + D) ≤ μ.real (ball p R)) :
    a * model r ≤ μ.real (ball y r) := by
…

Mentions: OAI.RegularPointCoordinates.BallVolumeComparison

theorem OAI.RegularPointCoordinates.uniform_volume_lower_on_ball line 52

Source documentation

Uniform large-scale information is inherited by every center and every positive smaller radius, without a lower cutoff on that radius.

theorem uniform_volume_lower_on_ball
    {μ : Measure X} {model : ℝ → ℝ} (hcomparison : BallVolumeComparison μ model)
    {p : X} {R D a : ℝ} (hmodel : ∀ r, 0 < r → 0 < model r)
    (hRD : 0 < R + D)
    (hfinite : ∀ y, μ (ball y (R + D)) ≠ ∞)
    (hlarge : a * model (R + D) ≤ μ.real (ball p R)) :
    ∀ y, dist p y ≤ D → ∀ r, 0 < r → r ≤ R + D →
      a * model r ≤ μ.real (ball y r) := by
…

Mentions: OAI.RegularPointCoordinates.BallVolumeComparison

def OAI.RegularPointCoordinates.SmallScaleVolumeUpper line 66
Source documentation
A weak form of an upper density bound: arbitrarily small radii approach the given upper bound. Bishop--Gromov propagates it to all radii.
```
def SmallScaleVolumeUpper (μ : Measure X) (model : ℝ → ℝ) (y : X) (a : ℝ) : Prop :=
…
```
theorem OAI.RegularPointCoordinates.volume_upper_of_small_scale_upper line 70