OAI/NumberTheory/DirichletL/Hecke/DetectorDyadicBridge.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.norm_phase line 13
2. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.normalization line 32
3. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.polynomial_eq_finite line 38
4. theorem OAI.SevenEighths.HeckeDetectorDyadicBridge.phase_sum_eq_polynomial line 69
5. def OAI.SevenEighths.HeckeDetectorDyadicBridge.inverseProfile line 89
6. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.inverseProfile_at_norm line 92
7. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.weighted_eq line 98
8. theorem OAI.SevenEighths.HeckeDetectorDyadicBridge.plain_phase_eq line 103
9. theorem OAI.SevenEighths.HeckeDetectorDyadicBridge.inverse_phase_eq line 116
10. lemma OAI.SevenEighths.HeckeDetectorDyadicBridge.normalization_norm line 131
11. theorem OAI.SevenEighths.HeckeDetectorDyadicBridge.pair_phase_norm line 137