OAI/NumberTheory/DirichletL/Hecke/DetectorFourierSeparation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeDetectorFourier.phasePolynomial line 10
2. lemma OAI.SevenEighths.HeckeDetectorFourier.phasePolynomial_continuous line 13
3. lemma OAI.SevenEighths.HeckeDetectorFourier.phasePolynomial_norm line 19
4. lemma OAI.SevenEighths.HeckeDetectorFourier.separated_pair_integrable line 25
5. lemma OAI.SevenEighths.HeckeDetectorFourier.schwartz_product_inversion line 36
6. theorem OAI.SevenEighths.HeckeDetectorFourier.finite_pair_separation line 51