OAI/NumberTheory/PrimePackets/PowerfulIdeals.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.isPowerful_mul_iff line 27
  2. lemma OAI.PrimeDegreePackets.isPowerful_prime_pow line 62
  3. lemma OAI.PrimeDegreePackets.powerfulCorrection_one line 69
  4. def OAI.PrimeDegreePackets.powerfulFunction line 74
  5. lemma OAI.PrimeDegreePackets.powerfulFunction_apply line 77
  6. lemma OAI.PrimeDegreePackets.powerfulFunction_multiplicative line 79
  7. lemma OAI.PrimeDegreePackets.Sieve.sum_moebius_div_indicator line 95
  8. lemma OAI.PrimeDegreePackets.Sieve.sum_moebius_interval line 106
  9. def OAI.PrimeDegreePackets.Sieve.multipleMobius line 114
  10. lemma OAI.PrimeDegreePackets.Sieve.sum_multipleMobius line 117
  11. def OAI.PrimeDegreePackets.Sieve.sieveDenominator line 135
  12. def OAI.PrimeDegreePackets.Sieve.optimalY line 138
  13. def OAI.PrimeDegreePackets.Sieve.optimalWeight line 141
  14. lemma OAI.PrimeDegreePackets.Sieve.sieveDenominator_pos line 144
  15. lemma OAI.PrimeDegreePackets.Sieve.nu_mul_optimalWeight line 156
  16. lemma OAI.PrimeDegreePackets.Sieve.optimalWeight_transform line 160
  17. lemma OAI.PrimeDegreePackets.Sieve.optimalWeight_one line 168
  18. lemma OAI.PrimeDegreePackets.Sieve.optimalWeight_mainSum line 190
  19. lemma OAI.PrimeDegreePackets.Sieve.optimalWeight_eq_zero_of_lt line 215
  20. lemma OAI.PrimeDegreePackets.Sieve.abs_optimalWeight_le line 227
  21. lemma OAI.PrimeDegreePackets.Sieve.sum_divisors_lambdaSquared line 261
  22. lemma OAI.PrimeDegreePackets.Sieve.abs_lambdaSquared_le line 288
  23. lemma OAI.PrimeDegreePackets.Sieve.errSum_lambdaSquared_le line 299
  24. lemma OAI.PrimeDegreePackets.Sieve.optimalWeight_errSum_le line 313
  25. theorem OAI.PrimeDegreePackets.Sieve.optimized_sieve_bound line 328
  26. def OAI.PrimeDegreePackets.Sieve.radical line 343
  27. lemma OAI.PrimeDegreePackets.Sieve.radical_dvd line 345
  28. lemma OAI.PrimeDegreePackets.Sieve.radical_pos line 347
  29. lemma OAI.PrimeDegreePackets.Sieve.primeFactors_radical line 350
  30. lemma OAI.PrimeDegreePackets.Sieve.div_radical_factored line 353
  31. lemma OAI.PrimeDegreePackets.Sieve.reciprocal_factored_hasSum line 361
  32. lemma OAI.PrimeDegreePackets.Sieve.reciprocal_radical_class_bound line 385
  33. theorem OAI.PrimeDegreePackets.Sieve.harmonic_le_inverse_totient_sum line 416