OAI/NumberTheory/PrimePackets/SieveConvolution.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.Sieve.convolution_prime line 32
  2. lemma OAI.PrimeDegreePackets.Sieve.convolution_pow_prime line 38
  3. lemma OAI.PrimeDegreePackets.Sieve.nFoldDivisor_prime line 53
  4. lemma OAI.PrimeDegreePackets.Sieve.mul_le_of_prime_power_le line 59
  5. def OAI.PrimeDegreePackets.Sieve.coefficientPenalty line 74
  6. lemma OAI.PrimeDegreePackets.Sieve.coefficientPenalty_bounds line 77
  7. lemma OAI.PrimeDegreePackets.Sieve.coefficientPenalty_prime line 88
  8. lemma OAI.PrimeDegreePackets.Sieve.convolution_ge_left line 94
  9. theorem OAI.PrimeDegreePackets.Sieve.divisor_bounded_majorant line 103
  10. lemma OAI.PrimeDegreePackets.Sieve.nFoldDivisor_real line 142
  11. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_pow_le_divisor line 151
  12. lemma OAI.PrimeDegreePackets.Sieve.convolution_sum_interval line 167
  13. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_pow_initial_le line 187
  14. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_pow_interval_trivial line 193
  15. lemma OAI.PrimeDegreePackets.Sieve.divided_interval_estimates line 223
  16. def OAI.PrimeDegreePackets.Sieve.intervalConstant line 275
  17. lemma OAI.PrimeDegreePackets.Sieve.intervalConstant_nonneg line 278
  18. def OAI.PrimeDegreePackets.Sieve.primeExponential line 280
  19. lemma OAI.PrimeDegreePackets.Sieve.primeExponential_one_le line 283
  20. lemma OAI.PrimeDegreePackets.Sieve.primeExponential_mono line 288
  21. theorem OAI.PrimeDegreePackets.Sieve.corrected_interval_finite line 298
  22. lemma OAI.PrimeDegreePackets.Sieve.log_power_error_vanishes line 387
  23. lemma OAI.PrimeDegreePackets.Sieve.eventual_tail_threshold line 397
  24. lemma OAI.PrimeDegreePackets.Sieve.reciprocal_cutoff_bound line 407
  25. lemma OAI.PrimeDegreePackets.Sieve.tail_absorbed line 417
  26. lemma OAI.PrimeDegreePackets.Sieve.sqrt_fourth_bound line 441