OAI/NumberTheory/SiegelZeros/EntireFunctions/ZeroShellBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W04.summable_dyadic_shell_majorant line 16
2. theorem OAI.SiegelZeros.WeightedTorusJets.W04.summable_inv_norm_sq_of_dyadic_count line 26
3. theorem OAI.SiegelZeros.WeightedTorusJets.W04.summable_inv_norm_sq_of_nonzero_dyadic_count line 95
4. theorem OAI.SiegelZeros.WeightedTorusJets.W48.exists_dyadic_bound line 118
5. def OAI.SiegelZeros.WeightedTorusJets.W48.dyadicShellIndex line 126
6. theorem OAI.SiegelZeros.WeightedTorusJets.W48.dyadicShell_upper line 129
7. theorem OAI.SiegelZeros.WeightedTorusJets.W48.dyadicShell_lower line 133
8. theorem OAI.SiegelZeros.WeightedTorusJets.W48.finite_count_le line 145
9. theorem OAI.SiegelZeros.WeightedTorusJets.W48.finite_shell_reciprocal_le line 157
10. theorem OAI.SiegelZeros.WeightedTorusJets.W48.finite_shell_inverse_square_le line 176
11. theorem OAI.SiegelZeros.WeightedTorusJets.W48.dyadic_tail_majorant_hasSum line 196
12. theorem OAI.SiegelZeros.WeightedTorusJets.W48.finite_tail_inverse_square_le line 214
13. theorem OAI.SiegelZeros.WeightedTorusJets.W48.tail_inverse_square_le line 246
14. theorem OAI.SiegelZeros.WeightedTorusJets.W48.finite_near_reciprocal_le line 263
15. theorem OAI.SiegelZeros.WeightedTorusJets.W48.tail_inverse_square_le_of_threshold line 326
16. theorem OAI.SiegelZeros.WeightedTorusJets.W48.dyadic_log_index line 344