OAI/NumberTheory/DirichletL/Hecke/DyadicLossBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeDyadic.central_squared_exponents line 8
2. theorem OAI.SevenEighths.HeckeDyadic.exists_central_loss_parameters line 19
3. theorem OAI.SevenEighths.HeckeDyadic.indexed_height_bound line 37
4. theorem OAI.SevenEighths.HeckeDyadic.min_plain_bound line 47
5. theorem OAI.SevenEighths.HeckeDyadic.squared_bound_of_central_and_error line 54