OAI/Geometry/TranslativeCovering/LocalizationRates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LocalizationRates.Space line 19
2. def OAI.LocalizationRates.β line 20
3. def OAI.LocalizationRates.W line 21
4. def OAI.LocalizationRates.rround line 22
5. lemma OAI.LocalizationRates.n_eta_limit line 23
6. lemma OAI.LocalizationRates.rminus_limit line 30
7. lemma OAI.LocalizationRates.ball_scale line 33
8. lemma OAI.LocalizationRates.outer_rate line 40
9. lemma OAI.LocalizationRates.inner_rate line 59
10. lemma OAI.LocalizationRates.dimension line 83