OAI/NumberTheory/JointDickman/Arithmetic/AdditionSieveDensity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The combined normalizer and sieve density for an addition product

  1. def OAI.JointDickman.quarterOdds line 12
  2. def OAI.JointDickman.additionSieveTheta line 14
  3. def OAI.JointDickman.additionSieveDensity line 16
  4. theorem OAI.JointDickman.quarterOdds_bounds line 19
  5. theorem OAI.JointDickman.additionSieveTheta_bounds line 28
  6. theorem OAI.JointDickman.additionSieve_local_bound line 35
  7. theorem OAI.JointDickman.additionSieve_normalizer_bound line 63
  8. theorem OAI.JointDickman.prime_roughness_product_log_bound line 102
  9. theorem OAI.JointDickman.additionSieve_density_log_bound line 132
  10. theorem OAI.JointDickman.additionSieveDensity_nonneg line 145
  11. theorem OAI.JointDickman.quarterNormalizer_le_prefix line 153