AnnularVolume.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A definite annulus in the almost-Euclidean volume regime

theorem OAI.RegularPointCoordinates.relative_volume_annulus line 14

Source documentation

The relative quarter-error gives positive volume and a definite exterior annulus in every dimension at least two.

theorem relative_volume_annulus {n : ℕ} (hn : 2 ≤ n) {r omega V W : ℝ}
    (hr : 0 < r) (homega : 0 < omega)
    (hV : |V / (omega * r ^ n) - 1| ≤ 1 / 4)
    (hW : |W / (omega * (2 * r) ^ n) - 1| ≤ 1 / 4) :
    0 < V ∧ 2 * V ≤ W := by
…

theorem OAI.RegularPointCoordinates.curvature_bound_sixtyfour line 43
Source documentation
An explicit radius cap for every curvature test on a 64-fold ball.
```
theorem curvature_bound_sixtyfour {K r : ℝ} (hr : 0 ≤ r)
    (hcap : r ≤ 1 / (64 * (|K| + 1))) : -1 ≤ K * (64 * r) ^ 2 := by
…
```