OAI/NumberTheory/DirichletL/Hecke/DetectorTail.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.HeckeDetectorTail.exponential_cubic_bound line 13
2. lemma OAI.SevenEighths.HeckeDetectorTail.divisor_count line 29
3. theorem OAI.SevenEighths.HeckeDetectorTail.cutoffCoefficient_bound line 40
4. lemma OAI.SevenEighths.HeckeDetectorTail.norm_weight_two line 63
5. lemma OAI.SevenEighths.HeckeDetectorTail.weighted_norm_le_one line 69
6. theorem OAI.SevenEighths.HeckeDetectorTail.exponentialTerm_bound line 87
7. theorem OAI.SevenEighths.HeckeDetectorTail.exponentialTerm_summable line 112
8. lemma OAI.SevenEighths.HeckeDetectorTail.cutoff_defect_bound line 118
9. def OAI.SevenEighths.HeckeDetectorTail.terminalRemainder line 122
10. lemma OAI.SevenEighths.HeckeDetectorTail.exponentialTerm_half line 126
11. theorem OAI.SevenEighths.HeckeDetectorTail.terminalRemainder_bound line 137
12. theorem OAI.SevenEighths.HeckeDetectorTail.terminalRemainder_summable line 172
13. theorem OAI.SevenEighths.HeckeDetectorTail.terminalRemainder_tsum_bound line 182
14. theorem OAI.SevenEighths.HeckeDetectorTail.terminalRemainder_uniform_small line 197
15. theorem OAI.SevenEighths.HeckeDetectorTail.exponential_sum_tail_unconditional line 232
16. def OAI.SevenEighths.HeckeDetectorTail.terminalTerm line 242
17. lemma OAI.SevenEighths.HeckeDetectorTail.summable_mul_bounded line 246
18. theorem OAI.SevenEighths.HeckeDetectorTail.terminal_sum_identity line 253
19. theorem OAI.SevenEighths.HeckeDetectorTail.terminal_sum_finite line 276