OAI/NumberTheory/DirichletL/Hecke/DetectorProfilesBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeDetectorProfiles.scaled_derivatives_of_decay line 9
2. theorem OAI.SevenEighths.HeckeDetectorProfiles.scaled_schwartz_derivatives line 37
3. theorem OAI.SevenEighths.HeckeDetectorProfiles.scaled_expNeg_derivatives line 47
4. lemma OAI.SevenEighths.HeckeDetectorProfiles.const_one_derivative_norm line 55
5. lemma OAI.SevenEighths.HeckeDetectorProfiles.complement_derivative_bound line 60
6. lemma OAI.SevenEighths.HeckeDetectorProfiles.product_derivative_bound line 68