OAI/NumberTheory/DirichletL/Hecke/DetectorDyadicSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeDetectorDyadicBridge.fourierSet line 14
2. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.fourierSet_nonzero line 16
3. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.pairSet_subset_fourier line 20
4. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.annular_covered line 29
5. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.inverse_annular_covered line 41
6. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.scales_le_eight_terminal line 48
7. theorem OAI.SevenEighths.HeckeDetectorDyadicBridge.dyadicBlock_eq_fourier_rectangle line 57