OAI/NumberTheory/PrimePackets/IntervalSieve.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.Sieve.reciprocalDensity line 32
  2. lemma OAI.PrimeDegreePackets.Sieve.reciprocalDensity_multiplicative line 34
  3. def OAI.PrimeDegreePackets.Sieve.intervalSieve line 41
  4. lemma OAI.PrimeDegreePackets.Sieve.interval_divisibility_card line 57
  5. lemma OAI.PrimeDegreePackets.Sieve.interval_multSum line 76
  6. lemma OAI.PrimeDegreePackets.Sieve.real_div_lt_nat_div_add_one line 84
  7. lemma OAI.PrimeDegreePackets.Sieve.interval_rem_abs_le_one line 89
  8. lemma OAI.PrimeDegreePackets.Sieve.interval_selbergTerms line 101
  9. theorem OAI.PrimeDegreePackets.Sieve.sifted_interval_bound line 113
  10. def OAI.PrimeDegreePackets.Sieve.truncatedTotientSum line 169
  11. lemma OAI.PrimeDegreePackets.Sieve.sum_divisors_coprime line 172
  12. lemma OAI.PrimeDegreePackets.Sieve.truncatedTotientSum_mul_le line 179
  13. lemma OAI.PrimeDegreePackets.Sieve.fullTotientSum_pos line 199
  14. lemma OAI.PrimeDegreePackets.Sieve.harmonic_le_truncatedTotientSum_mul line 206
  15. theorem OAI.PrimeDegreePackets.Sieve.sifted_interval_complement_bound line 215
  16. lemma OAI.PrimeDegreePackets.Sieve.squarefree_prime_product line 280
  17. lemma OAI.PrimeDegreePackets.Sieve.fullTotientSum_mul line 287
  18. lemma OAI.PrimeDegreePackets.Sieve.fullTotientSum_prime_product line 301
  19. def OAI.PrimeDegreePackets.Sieve.mixtureMass line 319
  20. def OAI.PrimeDegreePackets.Sieve.softWeight line 322
  21. lemma OAI.PrimeDegreePackets.Sieve.mixtureMass_nonneg line 325
  22. lemma OAI.PrimeDegreePackets.Sieve.sum_mixtureMass line 330
  23. lemma OAI.PrimeDegreePackets.Sieve.coprime_prime_product_indicator line 336
  24. lemma OAI.PrimeDegreePackets.Sieve.softWeight_eq_mixture line 341
  25. lemma OAI.PrimeDegreePackets.Sieve.sum_softWeight_eq_mixture line 350
  26. lemma OAI.PrimeDegreePackets.Sieve.sum_mixture_complementEuler line 362
  27. theorem OAI.PrimeDegreePackets.Sieve.soft_interval_bound line 382
  28. def OAI.PrimeDegreePackets.Sieve.primePenalty line 432
  29. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_apply line 435
  30. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_multiplicative line 439
  31. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_one line 448
  32. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_prime_pow line 451
  33. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_nonneg line 456
  34. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_le_one line 463
  35. def OAI.PrimeDegreePackets.Sieve.logWeight line 472
  36. lemma OAI.PrimeDegreePackets.Sieve.logWeight_apply line 475
  37. lemma OAI.PrimeDegreePackets.Sieve.logWeight_mul line 478
  38. def OAI.PrimeDegreePackets.Sieve.coefficientLogDerivation line 496
  39. lemma OAI.PrimeDegreePackets.Sieve.logWeight_pow line 507
  40. lemma OAI.PrimeDegreePackets.Sieve.convolution_nonneg line 514
  41. lemma OAI.PrimeDegreePackets.Sieve.convolution_pow_nonneg line 520
  42. def OAI.PrimeDegreePackets.Sieve.reciprocalCoefficients line 529
  43. lemma OAI.PrimeDegreePackets.Sieve.reciprocalCoefficients_apply line 532
  44. lemma OAI.PrimeDegreePackets.Sieve.reciprocalCoefficients_multiplicative line 535
  45. def OAI.PrimeDegreePackets.Sieve.divisorReciprocal line 545
  46. lemma OAI.PrimeDegreePackets.Sieve.divisorReciprocal_apply line 548
  47. lemma OAI.PrimeDegreePackets.Sieve.divisorReciprocal_multiplicative line 553
  48. lemma OAI.PrimeDegreePackets.Sieve.divisorReciprocal_nonneg line 558
  49. lemma OAI.PrimeDegreePackets.Sieve.geometric_partial_sum_le line 563
  50. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_divisorReciprocal_pow line 568
  51. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_divisorReciprocal_pow_le line 580
  52. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_divisorReciprocal_le line 596
  53. lemma OAI.PrimeDegreePackets.Sieve.reciprocalCoefficients_mul line 612
  54. lemma OAI.PrimeDegreePackets.Sieve.divisorReciprocal_mono_divisor line 624
  55. lemma OAI.PrimeDegreePackets.Sieve.divisorReciprocal_mul_le line 631
  56. lemma OAI.PrimeDegreePackets.Sieve.divisorReciprocal_one line 647
  57. lemma OAI.PrimeDegreePackets.Sieve.divisorReciprocal_pow_le line 655
  58. lemma OAI.PrimeDegreePackets.Sieve.sum_reciprocal_le_divisorReciprocal_factorial line 665
  59. theorem OAI.PrimeDegreePackets.Sieve.sum_primePenalty_pow_reciprocal_le line 677
  60. def OAI.PrimeDegreePackets.Sieve.largeFactorConvolution line 702
  61. lemma OAI.PrimeDegreePackets.Sieve.largeFactorConvolution_nonneg line 705
  62. lemma OAI.PrimeDegreePackets.Sieve.convolution_pow_le_largeFactor line 712
  63. lemma OAI.PrimeDegreePackets.Sieve.sum_divisor_large_interval line 761
  64. lemma OAI.PrimeDegreePackets.Sieve.sum_largeFactorConvolution_le line 819