OAI/NumberTheory/DirichletL/IdealMangoldt.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.IdealMangoldt.primeBase line 13
  2. theorem OAI.SevenEighths.IdealMangoldt.primeBase_spec line 15
  3. theorem OAI.SevenEighths.IdealMangoldt.primeBase_pow line 21
  4. def OAI.SevenEighths.IdealMangoldt.value line 29
  5. theorem OAI.SevenEighths.IdealMangoldt.value_zero line 32
  6. theorem OAI.SevenEighths.IdealMangoldt.value_one line 35
  7. theorem OAI.SevenEighths.IdealMangoldt.value_pow line 38
  8. theorem OAI.SevenEighths.IdealMangoldt.value_nonneg line 43
  9. theorem OAI.SevenEighths.IdealMangoldt.isPrimePow_absNorm line 50
  10. theorem OAI.SevenEighths.IdealMangoldt.value_eq_zero_of_norm_not_primePow line 58
  11. theorem OAI.SevenEighths.IdealMangoldt.prime_mem_primesOver_of_dvd_norm line 62
  12. theorem OAI.SevenEighths.IdealMangoldt.primeBase_mem_primesOver line 71
  13. theorem OAI.SevenEighths.IdealMangoldt.primeBase_injective_on_norm line 82
  14. def OAI.SevenEighths.IdealMangoldt.normFiber line 97
  15. theorem OAI.SevenEighths.IdealMangoldt.mem_normFiber line 100
  16. def OAI.SevenEighths.IdealMangoldt.coeff line 103
  17. theorem OAI.SevenEighths.IdealMangoldt.coeff_nonneg line 105
  18. theorem OAI.SevenEighths.IdealMangoldt.coeff_le_unweighted line 109
  19. theorem OAI.SevenEighths.IdealMangoldt.coeff_eq_sum_primePowers line 115
  20. theorem OAI.SevenEighths.IdealMangoldt.coeff_eq_zero_of_not_primePow line 120
  21. def OAI.SevenEighths.IdealMangoldt.primesOver line 127
  22. theorem OAI.SevenEighths.IdealMangoldt.mem_primesOver line 130
  23. theorem OAI.SevenEighths.IdealMangoldt.primesOver_card line 134
  24. theorem OAI.SevenEighths.IdealMangoldt.primesOver_log_sum_le line 138
  25. theorem OAI.SevenEighths.IdealMangoldt.coeff_prime_pow_le line 181
  26. theorem OAI.SevenEighths.IdealMangoldt.coeff_le_two_vonMangoldt line 207
  27. theorem OAI.SevenEighths.IdealMangoldt.coeff_chebyshev line 216
  28. theorem OAI.SevenEighths.IdealMangoldt.coeff_summable_nterm line 233
  29. theorem OAI.SevenEighths.IdealMangoldt.coeff_LSeriesSummable line 251
  30. def OAI.SevenEighths.IdealMangoldt.classCoeff line 257
  31. theorem OAI.SevenEighths.IdealMangoldt.classCoeff_nonneg line 260
  32. theorem OAI.SevenEighths.IdealMangoldt.classCoeff_le_two_vonMangoldt line 263
  33. theorem OAI.SevenEighths.IdealMangoldt.classCoeff_chebyshev line 267
  34. theorem OAI.SevenEighths.IdealMangoldt.classCoeff_summable_nterm line 272