LowerCurvatureVolume.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Scale-uniform volume comparison from nonnegative curvature

The existing CD support-volume argument gives Euclidean ball-ratio comparison when K is nonnegative. This removes dependence on |K| at large radii from the local estimates used to discharge the harmonic gradient input.

theorem OAI.RegularPointCoordinates.time_le_sigma_of_nonneg_curvature line 18
theorem OAI.RegularPointCoordinates.time_le_tau_of_nonneg_curvature line 41
theorem OAI.RegularPointCoordinates.tau_zero_curvature line 62
theorem OAI.RegularPointCoordinates.FullCD.zero_of_nonneg_curvature line 77
Source documentation
The nonnegative-curvature CD condition also supplies its zero-curvature specialization. This keeps the compression constants uniform when the original positive curvature is arbitrarily large.
```
theorem FullCD.zero_of_nonneg_curvature {μ : Measure X} {K : ℝ} {n : ℕ}
    (hcd : FullCD μ K n) (hn : 2 ≤ n) (hK : 0 ≤ K) : FullCD μ 0 n := by
…
```
Mentions: OAI.RegularPointCoordinates.FullCD
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.zero_of_nonneg_curvature line 95
Source documentation
Preserve the metric measure structure while lowering a nonnegative curvature bound to zero.
```
theorem NoncollapsedRCD.zero_of_nonneg_curvature {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (hK : 0 ≤ K) :
    NoncollapsedRCD 0 n X where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
theorem OAI.RegularPointCoordinates.FullCD.nonneg_ball_ratio_at_time line 106
theorem OAI.RegularPointCoordinates.FullCD.nonneg_ball_ratio line 162