OAI/NumberTheory/PrimePackets/DivisorBounds.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.sum_divisors_initial line 27
  2. def OAI.PrimeDegreePackets.nFoldDivisor line 69
  3. lemma OAI.PrimeDegreePackets.nFoldDivisor_succ line 71
  4. lemma OAI.PrimeDegreePackets.nFoldDivisor_one line 75
  5. lemma OAI.PrimeDegreePackets.nFoldDivisor_sum_succ line 80
  6. lemma OAI.PrimeDegreePackets.harmonic_real_eq_sum line 87
  7. lemma OAI.PrimeDegreePackets.harmonic_real_nonneg line 91
  8. lemma OAI.PrimeDegreePackets.harmonic_real_mono line 95
  9. lemma OAI.PrimeDegreePackets.nFoldDivisor_reciprocal_sum line 103
  10. theorem OAI.PrimeDegreePackets.nFoldDivisor_summatory_le line 144
  11. theorem OAI.PrimeDegreePackets.nFoldDivisor_summatory_real line 168
  12. theorem OAI.PrimeDegreePackets.nFoldDivisor_prime_pow line 184
  13. theorem OAI.PrimeDegreePackets.nFoldDivisor_prime_pow_le line 194
  14. lemma OAI.PrimeDegreePackets.choose_mul_geometric_le line 203
  15. lemma OAI.PrimeDegreePackets.nFoldDivisor_prime_pow_rpow line 212
  16. theorem OAI.PrimeDegreePackets.nFoldDivisor_subpolynomial line 239
  17. def OAI.PrimeDegreePackets.IsPowerful line 304
  18. lemma OAI.PrimeDegreePackets.powerful_square_cube line 306
  19. def OAI.PrimeDegreePackets.powerfulCorrection line 336
  20. lemma OAI.PrimeDegreePackets.powerfulCorrection_nonneg line 340
  21. lemma OAI.PrimeDegreePackets.powerfulCorrection_zero line 344
  22. def OAI.PrimeDegreePackets.powerfulRepresentation line 347
  23. lemma OAI.PrimeDegreePackets.powerfulRepresentation_spec line 351
  24. lemma OAI.PrimeDegreePackets.powerfulRepresentation_injective line 356
  25. lemma OAI.PrimeDegreePackets.powerful_rpow_summable line 369
  26. theorem OAI.PrimeDegreePackets.powerfulCorrection_summable line 386
  27. def OAI.PrimeDegreePackets.powerfulMoment line 407
  28. lemma OAI.PrimeDegreePackets.powerfulMoment_nonneg line 410
  29. lemma OAI.PrimeDegreePackets.powerfulCorrection_moment_sum_le line 413
  30. lemma OAI.PrimeDegreePackets.powerfulCorrection_reciprocal_sum_le line 424
  31. lemma OAI.PrimeDegreePackets.powerfulCorrection_reciprocal_identity line 435
  32. theorem OAI.PrimeDegreePackets.powerfulCorrection_reciprocal_tail line 444