ComparisonModel.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Uniformly flat negative-curvature comparison volumes

The dimension is m + 1. The radial factor for curvature -m * a ^ 2 is written as the primitive of cosh (a * t), which also covers a = 0 without a removable singularity. Its volume is normalized by the volume of the Euclidean unit ball. The bounds below are uniform down to radius zero, as required before applying almost-volume rigidity.

def OAI.RegularPointCoordinates.radialComparison line 21
def OAI.RegularPointCoordinates.comparisonModelVolume line 24
theorem OAI.RegularPointCoordinates.continuous_radialComparison line 27
theorem OAI.RegularPointCoordinates.continuous_comparisonModelVolume line 31
theorem OAI.RegularPointCoordinates.radialComparison_zero line 36
theorem OAI.RegularPointCoordinates.radialComparison_eq_sinh line 39
theorem OAI.RegularPointCoordinates.radialComparison_bounds line 50
theorem OAI.RegularPointCoordinates.comparisonModelVolume_zero line 68
theorem OAI.RegularPointCoordinates.comparisonModelVolume_bounds line 75
theorem OAI.RegularPointCoordinates.comparisonModelVolume_pos line 107
theorem OAI.RegularPointCoordinates.comparisonModelVolume_relative_error line 113
Source documentation
A single model error at the outer radius controls every smaller positive radius. There is no positive lower cutoff on the radius.
```
theorem comparisonModelVolume_relative_error (m : ℕ) {a r R : ℝ}
    (ha : 0 ≤ a) (hr : 0 < r) (hrR : r ≤ R) :
    0 ≤ comparisonModelVolume m a r / r ^ (m + 1) - 1 ∧
      comparisonModelVolume m a r / r ^ (m + 1) - 1 ≤ Real.cosh (a * R) ^ m - 1 := by
…
```
Mentions: OAI.RegularPointCoordinates.comparisonModelVolume
theorem OAI.RegularPointCoordinates.comparisonModelVolume_uniformly_flat line 132
theorem OAI.RegularPointCoordinates.comparisonModelVolume_density line 148
Source documentation
For a fixed curvature parameter the normalized model volumes tend to one at small radii, with no division at radius zero.
```
theorem comparisonModelVolume_density (m : ℕ) {a : ℝ} (ha : 0 ≤ a)
    {r : ℕ → ℝ} (hr : ∀ i, 0 < r i) (hrzero : Tendsto r atTop (𝓝 0)) :
    Tendsto (fun i => comparisonModelVolume m a (r i) / r i ^ (m + 1))
      atTop (𝓝 1) := by
…
```
Mentions: OAI.RegularPointCoordinates.comparisonModelVolume