OAI/NumberTheory/DirichletL/Detector/LiftedFourier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.ProbePrimePower.primePowerGauss_lift_add line 11
2. theorem OAI.SevenEighths.ProbePrimePower.primePowerGauss_add_period line 26
3. theorem OAI.SevenEighths.ProbePrimePower.gauss_exactQuotient_lift line 39
4. theorem OAI.SevenEighths.ProbePrimePower.positiveScalar_full_lift line 55
5. lemma OAI.SevenEighths.ProbePrimePower.quotientTrace_split_frequency line 75
6. def OAI.SevenEighths.ProbePrimePower.quotientFourier line 84
7. lemma OAI.SevenEighths.ProbePrimePower.quotientFourier_congr line 89
8. lemma OAI.SevenEighths.ProbePrimePower.primePowerGauss_eq_quotientFourier line 95