OAI/NumberTheory/PrimePackets/MangoldtBounds.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.vonMangoldt_floor_identity line 37
  2. lemma OAI.PrimeDegreePackets.nat_floor_quotient_half line 44
  3. theorem OAI.PrimeDegreePackets.vonMangoldt_reciprocal_sum line 55
  4. lemma OAI.PrimeDegreePackets.finite_euler_lower line 86
  5. lemma OAI.PrimeDegreePackets.log_one_add_lower_quadratic line 106
  6. lemma OAI.PrimeDegreePackets.prime_exp_le_euler line 113
  7. lemma OAI.PrimeDegreePackets.realDirichletTerm_multiplicative line 134
  8. lemma OAI.PrimeDegreePackets.realDirichletTerm_nonneg line 142
  9. lemma OAI.PrimeDegreePackets.realDirichletTerm_le_div line 146
  10. lemma OAI.PrimeDegreePackets.prime_quadratic_sum_le line 158
  11. lemma OAI.PrimeDegreePackets.reciprocal_dirichlet_difference line 178
  12. lemma OAI.PrimeDegreePackets.prime_reciprocal_log_sum line 189
  13. lemma OAI.PrimeDegreePackets.shifted_prime_sum_le line 202
  14. theorem OAI.PrimeDegreePackets.prime_exponential_le_dirichlet line 236
  15. lemma OAI.PrimeDegreePackets.idealCoefficientReal_prime_le line 271
  16. theorem OAI.PrimeDegreePackets.ideal_prime_exponential_le_zeta line 278
  17. def OAI.PrimeDegreePackets.coprimeIdealCoefficient line 300
  18. lemma OAI.PrimeDegreePackets.coprimeIdealCoefficient_multiplicative line 304
  19. lemma OAI.PrimeDegreePackets.coprimeIdealCoefficient_bounds line 312
  20. lemma OAI.PrimeDegreePackets.coprimeIdealCoefficient_le line 323
  21. theorem OAI.PrimeDegreePackets.coprime_ideal_relative_interval line 332
  22. def OAI.PrimeDegreePackets.localEulerTailConstant line 381
  23. lemma OAI.PrimeDegreePackets.multichoose_succ_eq line 384
  24. lemma OAI.PrimeDegreePackets.summable_multichoose_geometric line 390
  25. lemma OAI.PrimeDegreePackets.summable_localEulerTailConstant line 396
  26. lemma OAI.PrimeDegreePackets.localEulerTailConstant_nonneg line 406
  27. def OAI.PrimeDegreePackets.idealPrimeEuler line 413
  28. lemma OAI.PrimeDegreePackets.idealPrimeEuler_summable line 416
  29. lemma OAI.PrimeDegreePackets.idealPrimeEuler_one_le line 433
  30. lemma OAI.PrimeDegreePackets.idealPrimeEuler_le line 441
  31. lemma OAI.PrimeDegreePackets.log_idealPrimeEuler_le line 476
  32. def OAI.PrimeDegreePackets.badPrimeEuler line 485
  33. lemma OAI.PrimeDegreePackets.badPrimeEuler_pos line 487
  34. lemma OAI.PrimeDegreePackets.log_badPrimeEuler_le line 493