OAI/NumberTheory/DirichletL/Detector/LocalSeries.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeEuler.principalMarkedTerm line 15
2. lemma OAI.SevenEighths.ProbeEuler.localGamma_conjugate_three_sq line 23
3. lemma OAI.SevenEighths.ProbeEuler.firstGauss_ne_zero line 34
4. lemma OAI.SevenEighths.ProbeEuler.primeNorm_ne_zero line 51
5. theorem OAI.SevenEighths.ProbeEuler.markedTerm_zero_index line 57
6. lemma OAI.SevenEighths.ProbeEuler.markedTerm_higher_outer line 62
7. lemma OAI.SevenEighths.ProbeEuler.markedTerm_odd line 69
8. lemma OAI.SevenEighths.ProbeEuler.markedTerm_squarefree_boundary line 76
9. lemma OAI.SevenEighths.ProbeEuler.markedTerm_squarefree_boundary_off line 86
10. lemma OAI.SevenEighths.ProbeEuler.markedTerm_even_bulk line 92
11. lemma OAI.SevenEighths.ProbeEuler.markedTerm_even_bulk_off line 103
12. lemma OAI.SevenEighths.ProbeEuler.markedTerm_even_kone line 109
13. lemma OAI.SevenEighths.ProbeEuler.markedTerm_even_kone_off line 119
14. lemma OAI.SevenEighths.ProbeEuler.markedTerm_squarefree_bulk line 125
15. lemma OAI.SevenEighths.ProbeEuler.markedTerm_squarefree_bulk_off line 136