OAI/NumberTheory/DirichletL/PrimeCounting/IdealPrimeMass.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.PNT.IdealPrimeMass.primeClassCoeff line 14
2. def OAI.SevenEighths.PNT.IdealPrimeMass.higherClassCoeff line 17
3. theorem OAI.SevenEighths.PNT.IdealPrimeMass.value_prime line 20
4. theorem OAI.SevenEighths.PNT.IdealPrimeMass.prime_of_isPrimePow_of_norm_prime line 23
5. theorem OAI.SevenEighths.PNT.IdealPrimeMass.value_eq_zero_of_nonprime_of_norm_prime line 30
6. theorem OAI.SevenEighths.PNT.IdealPrimeMass.primeClassCoeff_eq_sum_log line 35
7. theorem OAI.SevenEighths.PNT.IdealPrimeMass.primeClassCoeff_nonneg line 46
8. theorem OAI.SevenEighths.PNT.IdealPrimeMass.higherClassCoeff_nonneg line 49
9. theorem OAI.SevenEighths.PNT.IdealPrimeMass.classCoeff_eq_prime_add_higher line 52
10. theorem OAI.SevenEighths.PNT.IdealPrimeMass.higherClassCoeff_zero line 60
11. theorem OAI.SevenEighths.PNT.IdealPrimeMass.primeClassCoeff_zero line 63
12. theorem OAI.SevenEighths.PNT.IdealPrimeMass.higherClassCoeff_eq_zero_of_prime line 66
13. theorem OAI.SevenEighths.PNT.IdealPrimeMass.higherClassCoeff_le_nonprime_vonMangoldt line 76
14. theorem OAI.SevenEighths.PNT.IdealPrimeMass.summable_nonprime_vonMangoldt_div line 83
15. theorem OAI.SevenEighths.PNT.IdealPrimeMass.higherClassCoeff_summable_div line 89
16. theorem OAI.SevenEighths.PNT.IdealPrimeMass.higherClassCoeff_ratio_tendsto_zero line 99
17. theorem OAI.SevenEighths.PNT.IdealPrimeMass.primeClassCoeff_ratio_tendsto line 104
18. def OAI.SevenEighths.PNT.IdealPrimeMass.primeIdealsBelow line 119
19. theorem OAI.SevenEighths.PNT.IdealPrimeMass.mem_primeIdealsBelow line 123
20. theorem OAI.SevenEighths.PNT.IdealPrimeMass.zero_not_mem_primeIdealsBelow line 128
21. def OAI.SevenEighths.PNT.IdealPrimeMass.primeLogMass line 133
22. theorem OAI.SevenEighths.PNT.IdealPrimeMass.primeLogMass_eq_cumsum line 136
23. theorem OAI.SevenEighths.PNT.IdealPrimeMass.primeLogMass_ratio_tendsto line 157