OAI/NumberTheory/DirichletL/Hecke/DetectorDyadicProfiles.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeDetectorDyadicProfiles.section_deriv_smooth line 11
2. theorem OAI.SevenEighths.HeckeDetectorDyadicProfiles.section_iteratedDeriv_smooth line 20
3. theorem OAI.SevenEighths.HeckeDetectorDyadicProfiles.compact_family_deriv_integrable line 29
4. theorem OAI.SevenEighths.HeckeDetectorDyadicProfiles.compact_family_deriv_L1_bound line 40
5. theorem OAI.SevenEighths.HeckeDetectorDyadicProfiles.compact_family_fourier_power_bound line 68
6. theorem OAI.SevenEighths.HeckeDetectorDyadicProfiles.compact_family_fourier_weighted_bound line 98
7. def OAI.SevenEighths.HeckeDetectorDyadicProfiles.ratioProfile line 123
8. def OAI.SevenEighths.HeckeDetectorDyadicProfiles.logFamily line 125
9. lemma OAI.SevenEighths.HeckeDetectorDyadicProfiles.logFamily_smooth line 128
10. lemma OAI.SevenEighths.HeckeDetectorDyadicProfiles.ratioProfile_support line 138
11. lemma OAI.SevenEighths.HeckeDetectorDyadicProfiles.logFamily_support line 143
12. theorem OAI.SevenEighths.HeckeDetectorDyadicProfiles.ratioProfile_mellin_bound line 149
13. lemma OAI.SevenEighths.HeckeDetectorDyadicProfiles.inverseProfile_eq_ratio line 177
14. theorem OAI.SevenEighths.HeckeDetectorDyadicProfiles.exists_profile_bounds line 184