OAI/NumberTheory/Ostmann/Construction/BalancedCellScale.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.cellPrimeCutoff line 13
2. lemma OAI.Ostmann.Construction.cellPrimeCutoff_pos line 15
3. lemma OAI.Ostmann.Construction.cellPrimeCutoff_tendsto line 18
4. lemma OAI.Ostmann.Construction.cellPrimeCutoff_log_lower line 21
5. lemma OAI.Ostmann.Construction.cellPrimeCutoff_loglog_upper line 25
6. def OAI.Ostmann.Construction.BalancedCellAfterTwo line 40
7. theorem OAI.Ostmann.Construction.balancedCellAfterTwo_eventually line 44
8. theorem OAI.Ostmann.Construction.badLogCellCenters_linear_bound line 74