A scaling prime from the first Mertens estimate. If every prime in a fixed multiplicative interval divides a nonzero integer, that integer has large logarithmic height.

theorem CCDN.prime_interval_weight_lower {L T : ℝ} (hL : 1 ≤ L) (hLT : L ≤ T) : Real.log T - Real.log L - 2 * mertensError ≤ ∑ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊T⌋₊) \ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊L⌋₊), Real.log ↑p / ↑p

Lower bound from the first Mertens estimate: for 1 ≤ L ≤ T, the sum of log p / p over the primes p with L < p ≤ T is at least log T - log L - 2 mertensError.

noncomputable def CCDN.scalingPrimeRatio : ℝ

The absolute constant A = exp (2 mertensError + 2) such that a prime in the interval (B / A, B] can be found avoiding the prime divisors of any nonzero integer D with log |D| < B / A.

Equations

• CCDN.scalingPrimeRatio = Real.exp (2 * CCDN.mertensError + 2)

theorem CCDN.scalingPrimeRatio_one_le : 1 ≤ scalingPrimeRatio

The scaling-prime ratio is at least one.

theorem CCDN.exists_scaling_prime {B : ℝ} (hB : scalingPrimeRatio ≤ B) {D : ℤ} (hD : D ≠ 0) (hheight : Real.log |↑D| < B / scalingPrimeRatio) : ∃ (p : ℕ), Nat.Prime p ∧ B / scalingPrimeRatio < ↑p ∧ ↑p ≤ B ∧ ¬↑p ∣ D

A prime of size comparable to B avoids D when log |D| < B/A, where A=exp(2*mertensError+2) is an absolute constant.