OAI/NumberTheory/DirichletL/Hecke/DetectorProfiles.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeDetectorProfiles.expNeg line 9
2. lemma OAI.SevenEighths.HeckeDetectorProfiles.expNeg_smooth line 11
3. lemma OAI.SevenEighths.HeckeDetectorProfiles.expNeg_hasDerivAt line 14
4. lemma OAI.SevenEighths.HeckeDetectorProfiles.iteratedDeriv_expNeg line 18
5. lemma OAI.SevenEighths.HeckeDetectorProfiles.expNeg_derivative_norm line 28
6. lemma OAI.SevenEighths.HeckeDetectorProfiles.expNeg_derivative_decay line 33
7. def OAI.SevenEighths.HeckeDetectorProfiles.productProfile line 45
8. def OAI.SevenEighths.HeckeDetectorProfiles.inverseProfile line 48
9. def OAI.SevenEighths.HeckeDetectorProfiles.logSourceFun line 50
10. lemma OAI.SevenEighths.HeckeDetectorProfiles.logSource_smooth line 53
11. lemma OAI.SevenEighths.HeckeDetectorProfiles.logSource_compact line 60
12. def OAI.SevenEighths.HeckeDetectorProfiles.logSource line 64
13. lemma OAI.SevenEighths.HeckeDetectorProfiles.logSource_apply line 69