OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/MassPowerBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinarySparseTerminal.mass_power_bound line 25
2. lemma OAI.OrdinarySparseTerminal.remainder_normalize line 38
3. lemma OAI.OrdinarySparseTerminal.remainder_at_power line 46
4. theorem OAI.OrdinarySparseTerminal.terminal_raw_bound line 98
5. lemma OAI.OrdinarySparseTerminal.sparse_error_compare line 150
6. lemma OAI.OrdinarySparseTerminal.terminal_density_facts line 163
7. theorem OAI.OrdinarySparseTerminal.terminal_grid_bound line 195
8. theorem OAI.OrdinarySparseTerminal.sparse_terminal_small line 247