OAI/NumberTheory/DirichletL/Hecke/DetectorFourierWitness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.HeckeDetectorFourier.frequency_interval_compl line 10
2. lemma OAI.SevenEighths.HeckeDetectorFourier.exists_interval_norm_product line 16
3. theorem OAI.SevenEighths.HeckeDetectorFourier.exists_interval_frequency line 37
4. theorem OAI.SevenEighths.HeckeDetectorFourier.integral_sub_interval_norm_le line 55
5. theorem OAI.SevenEighths.HeckeDetectorFourier.separated_pair_norm_le line 75
6. theorem OAI.SevenEighths.HeckeDetectorFourier.schwartz_tail_le line 84
7. theorem OAI.SevenEighths.HeckeDetectorFourier.separated_pair_tail_of_bound line 92
8. theorem OAI.SevenEighths.HeckeDetectorFourier.separated_pair_tail line 113
9. theorem OAI.SevenEighths.HeckeDetectorFourier.exists_bounded_frequency line 126