OAI/NumberTheory/JointDickman/Counting/TiltedCoefficient.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exponential prime-count tilts of the actual coefficient

  1. def OAI.JointDickman.primeDivisorCount line 12
  2. def OAI.JointDickman.tiltedPrimeWeight line 15
  3. def OAI.JointDickman.tiltedCoefficientWeight line 18
  4. def OAI.JointDickman.tiltedSieveTheta line 21
  5. theorem OAI.JointDickman.coefficient_prefix_count line 24
  6. theorem OAI.JointDickman.coefficient_tail_count line 30
  7. theorem OAI.JointDickman.coefficientWeight_zero line 40
  8. theorem OAI.JointDickman.tiltedPrimeWeight_bounds line 43
  9. theorem OAI.JointDickman.tiltedSieveTheta_bounds line 48
  10. theorem OAI.JointDickman.tilted_prime_product line 55
  11. theorem OAI.JointDickman.tiltedCoefficientWeight_nonneg line 67
  12. theorem OAI.JointDickman.tiltedCoefficientWeight_le_sieved line 71