OAI/NumberTheory/JointDickman/Amplification/RegularityChernoffFactors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Chernoff factors with the actual truncated sieve prime sets

  1. def OAI.JointDickman.prefixUpperFactor line 13
  2. def OAI.JointDickman.prefixLowerFactor line 17
  3. theorem OAI.JointDickman.actual_prefix_chernoff_decay line 21
  4. def OAI.JointDickman.tailChernoffFactor line 55
  5. theorem OAI.JointDickman.actual_tail_chernoff_sum line 61
  6. theorem OAI.JointDickman.tail_endpoint_index_lt line 86