A fixed multiplicative prime window has enough product to avoid every integer of prescribed logarithmic height, and only O(L/log L) primes. These are the arithmetic inputs to the residue-class cover.

noncomputable def CCDN.congruencePrimeWindow (L : ℝ) : Finset ℕ

The primes p with L < p ≤ c L, where c is scalingPrimeRatio.

Equations

• CCDN.congruencePrimeWindow L = Finset.filter Nat.Prime (Finset.Ioc 0 ⌊CCDN.scalingPrimeRatio * L⌋₊) \ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊L⌋₊)

theorem CCDN.mem_congruencePrimeWindow {L : ℝ} (hL : 1 ≤ L) {p : ℕ} : p ∈ congruencePrimeWindow L ↔ Nat.Prime p ∧ L < ↑p ∧ ↑p ≤ scalingPrimeRatio * L

For L ≥ 1, a natural number lies in congruencePrimeWindow L exactly when it is a prime p with L < p ≤ c L, where c is scalingPrimeRatio.

theorem CCDN.congruencePrimeWindow_log_upper {L : ℝ} (hL : 1 ≤ L) : ∑ p ∈ congruencePrimeWindow L, Real.log ↑p ≤ (Real.log 4 + 4) * scalingPrimeRatio * L

For L ≥ 1, the sum of log p over the primes of congruencePrimeWindow L is at most (log 4 + 4) c L, where c is scalingPrimeRatio.

theorem CCDN.congruencePrimeWindow_card_log_bound {L : ℝ} (hL : 1 ≤ L) : ↑(congruencePrimeWindow L).card * Real.log L ≤ (Real.log 4 + 4) * scalingPrimeRatio * L

For L ≥ 1, the number of primes in congruencePrimeWindow L, multiplied by log L, is at most (log 4 + 4) c L, where c is scalingPrimeRatio.

theorem CCDN.congruencePrimeWindow_avoiding_product {L : ℝ} (hL : 1 ≤ L) {D : ℤ} (hD : D ≠ 0) (hheight : Real.log |↑D| ≤ L) : Real.exp L ≤ ∏ p ∈ congruencePrimeWindow L with ¬↑p ∣ D, ↑p

For L ≥ 1 and a nonzero integer D with log |D| ≤ L, the product of the primes of congruencePrimeWindow L not dividing D is at least exp L.