Prime-counting hypotheses for runs of multiples

Separating the numerical prime input lets the entropy and Chebyshev arguments compile independently.

def RunsOfMultiples.primesUpTo (m : ℕ) : Finset ℕ

The primes ≤ m.

Equations

• RunsOfMultiples.primesUpTo m = Finset.filter Nat.Prime (Finset.range (m + 1))

structure RunsOfMultiples.PrimeInput (K : ℕ) (c₁ C₁ : ℝ) (q₀ : ℕ) : Prop

Prime-number input for the upper bound.

• K_pos : 0 < K
• c₁_pos : 0 < c₁
• C₁_nonneg : 0 ≤ C₁
• theta (m : ℕ) : c₁ * ↑m - C₁ ≤ ∑ p ∈ primesUpTo m, Real.log ↑p
• gap (q : ℕ) : q₀ ≤ q → ↑q ^ (3 / 4) ≤ ↑(Finset.filter Nat.Prime (Finset.Ioc q (K * q))).card