OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ShellGridScales.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinarySparseShell.shell_grid_scales line 24
2. lemma OAI.OrdinarySparseShell.shell_height line 38
3. lemma OAI.OrdinarySparseShell.shell_small_errors line 47
4. lemma OAI.OrdinarySparseShell.shell_remainder line 96
5. theorem OAI.OrdinarySparseShell.shell_raw_bound line 123
6. theorem OAI.OrdinarySparseShell.shell_grid_bound line 178
7. theorem OAI.OrdinarySparseShell.sparse_shell_small line 237
8. theorem OAI.OrdinarySparseShell.sparse_cofactor_all_lengths line 268