OAI/NumberTheory/JointDickman/Arithmetic/BrunUpperSieve.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An unconditional proof of the required upper sieve

Even inclusion-exclusion truncations on disjoint logarithmic prime blocks have coefficients of absolute value one. Their orders grow with the block index, so their errors are summable while every supported prime product stays below z. This proves the finite-event consequence of Ford's Theorem 2.4 used here.

  1. def OAI.JointDickman.brunSieveConstant line 18
  2. theorem OAI.JointDickman.brunPrimeBlocks_survival line 21
  3. theorem OAI.JointDickman.brunPrimeBlocks_mean_bound line 38
  4. theorem OAI.JointDickman.fordUpperSieveInput line 63