OAI/NumberTheory/DirichletL/Detector/LocalSummation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeEuler.hasSum_geometric_tail line 12
2. lemma OAI.SevenEighths.ProbeEuler.tsum_two_of_rest_zero line 21
3. def OAI.SevenEighths.ProbeEuler.principalInner line 33
4. lemma OAI.SevenEighths.ProbeEuler.squarefree_boundary_hasSum line 38
5. lemma OAI.SevenEighths.ProbeEuler.even_kone_hasSum line 51
6. lemma OAI.SevenEighths.ProbeEuler.even_bulk_hasSum line 65
7. lemma OAI.SevenEighths.ProbeEuler.squarefree_bulk_hasSum line 76
8. lemma OAI.SevenEighths.ProbeEuler.principalInner_two line 87
9. lemma OAI.SevenEighths.ProbeEuler.principalInner_squarefree line 95
10. lemma OAI.SevenEighths.ProbeEuler.principalInner_even line 103
11. lemma OAI.SevenEighths.ProbeEuler.principalInner_odd line 113
12. lemma OAI.SevenEighths.ProbeEuler.principalInner_zero line 118
13. lemma OAI.SevenEighths.ProbeEuler.principalInner_squarefree_hasSum line 122
14. lemma OAI.SevenEighths.ProbeEuler.principalInner_even_hasSum line 139
15. def OAI.SevenEighths.ProbeEuler.principalMarkedSeries line 163
16. theorem OAI.SevenEighths.ProbeEuler.principalMarkedSeries_eq line 166