OAI/NumberTheory/DirichletL/Hecke/DetectorProfilesCutoffs.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.HeckeDetectorProfiles.cutoff line 9
2. lemma OAI.SevenEighths.HeckeDetectorProfiles.cutoff_one line 11
3. lemma OAI.SevenEighths.HeckeDetectorProfiles.cutoff_zero line 15
4. lemma OAI.SevenEighths.HeckeDetectorProfiles.cutoff_norm_le line 23
5. lemma OAI.SevenEighths.HeckeDetectorProfiles.annular_log_bound line 28
6. theorem OAI.SevenEighths.HeckeDetectorProfiles.exists_product_log_cutoff line 39