OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ExplicitDensityCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinarySparseShell.explicit_density_cost line 24
2. theorem OAI.OrdinarySparseShell.polynomial_sparse_shell line 39
3. lemma OAI.OrdinarySparseShell.all_lengths_of_shell line 88
4. theorem OAI.OrdinarySparseShell.polynomial_sparse_all_lengths line 142
5. lemma OAI.OrdinarySparseShell.polynomial_exponent_bound line 155