VolumeProfileRegularity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Absolute continuity of the Euclidean-normalized volume profile

Bishop--Gromov and a positive Lipschitz comparison model make ball volume Lipschitz on every compact interval of positive radii. Multiplication by the smooth Euclidean normalization then gives the absolute continuity needed by the radial source budget.

theorem OAI.RegularPointCoordinates.volume_profile_lipschitzOn line 22
theorem OAI.RegularPointCoordinates.contDiff_one_comparisonModelVolume line 63
Source documentation
The fixed negative-curvature comparison volume is continuously differentiable.
```
theorem contDiff_one_comparisonModelVolume (m : ℕ) (c : ℝ) :
    ContDiff ℝ 1 (comparisonModelVolume m c) := by
…
```
Mentions: OAI.RegularPointCoordinates.comparisonModelVolume
theorem OAI.RegularPointCoordinates.ball_volume_absolutelyContinuous line 83
Source documentation
Ball volume is absolutely continuous away from radius zero under the published Bishop--Gromov comparison with the explicit model.
```
theorem ball_volume_absolutelyContinuous {μ : Measure X} (m : ℕ) {c : ℝ} (hc : 0 ≤ c)
    (hBG : BallVolumeComparison μ (comparisonModelVolume m c)) (x : X)
    {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hfin : μ (ball x b) ≠ ∞) :
    AbsolutelyContinuousOnInterval (fun t => μ.real (ball x t)) a b := by
…
```
Mentions: OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume
theorem OAI.RegularPointCoordinates.normalized_ball_volume_absolutelyContinuous line 110
Source documentation
Euclidean-normalized volume retains absolute continuity on positive radius intervals; this does not assume monotonicity of that normalization.
```
theorem normalized_ball_volume_absolutelyContinuous {μ : Measure X} (m : ℕ) {c : ℝ} (hc : 0 ≤ c)
    (hBG : BallVolumeComparison μ (comparisonModelVolume m c)) (x : X)
    {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hfin : μ (ball x b) ≠ ∞) :
    AbsolutelyContinuousOnInterval (fun t => μ.real (ball x t) / t ^ (m + 1)) a b := by
…
```
Mentions: OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume
theorem OAI.RegularPointCoordinates.sphere_measure_zero_of_comparison line 129
Source documentation
Bishop--Gromov with a positive continuous model excludes mass on every positive-radius sphere, not merely almost every sphere.
```
theorem sphere_measure_zero_of_comparison {model : ℝ → ℝ}
    (hBG : BallVolumeComparison μ model) (hcont : Continuous model)
    (x : X) {r : ℝ} (hr : 0 < r) (hmodel : 0 < model r) : μ (sphere x r) = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.BallVolumeComparison