The upper bound

The main argument, with the two prime-number inputs (a Chebyshev lower bound for θ and a lower bound for the number of primes in (q, K q]) taken as the hypothesis PrimeInput. These are discharged from Mathlib's Chebyshev file in Primes.lean.

theorem RunsOfMultiples.card_le_sup (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) : S.card ≤ S.sup id

theorem RunsOfMultiples.card_mul_log_le {T S : Finset ℕ} (hTS : T ⊆ S) : ↑T.card * Real.log ↑T.card ≤ ↑T.card * Real.log ↑S.card

theorem RunsOfMultiples.fibre_bound (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {K : ℕ} (hK : 1 ≤ K) {q₀ : ℕ} (hgap : ∀ (q : ℕ), q₀ ≤ q → ↑q ^ (3 / 4) ≤ ↑(Finset.filter Nat.Prime (Finset.Ioc q (K * q))).card) {Q₀ : ℝ} (hQ₀1 : 1 ≤ Q₀) (hQ₀q₀ : ↑q₀ ≤ Q₀) (hQ₀ : ∀ (q : ℕ), Q₀ ≤ ↑q → Real.log ↑q * Real.log ↑S.card ≤ ↑q ^ (1 / 4)) {q : ℕ} (hq : Nat.Prime q) (c : ℕ →₀ ℕ) : Real.log ↑q * ↑{m ∈ A S (K * q) | key q m = c}.card ≤ (Real.log Q₀ + 2 / Real.log 2) * ↑{m ∈ A S q | key q m = c}.card + 4 * ent ({m ∈ S | key q m = c}) fun (m : ℕ) => m.factorization q

The per-fibre estimate: weight log q on the pairs (a, q) with a ∈ A (K q).

theorem RunsOfMultiples.prime_bound (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {K : ℕ} (hK : 1 ≤ K) {q₀ : ℕ} (hgap : ∀ (q : ℕ), q₀ ≤ q → ↑q ^ (3 / 4) ≤ ↑(Finset.filter Nat.Prime (Finset.Ioc q (K * q))).card) {Q₀ : ℝ} (hQ₀1 : 1 ≤ Q₀) (hQ₀q₀ : ↑q₀ ≤ Q₀) (hQ₀ : ∀ (q : ℕ), Q₀ ≤ ↑q → Real.log ↑q * Real.log ↑S.card ≤ ↑q ^ (1 / 4)) {q : ℕ} (hq : Nat.Prime q) : Real.log ↑q * ↑(A S (K * q)).card ≤ (Real.log Q₀ + 2 / Real.log 2) * ↑(A S q).card + 4 * D S q

Summing the fibre estimate over the fibres of the q-smooth part.

theorem RunsOfMultiples.double_count (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {K : ℕ} (hK : 0 < K) : ∑ q ∈ Finset.range (S.sup id + 1) with Nat.Prime q, Real.log ↑q * ↑(A S (K * q)).card = ∑ a ∈ S, ∑ p ∈ primesUpTo (L S a / K), Real.log ↑p

Double counting: ∑_q log q |A (K q)| = ∑_a θ(L a / K).

theorem RunsOfMultiples.upper_core (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {K q₀ : ℕ} {c₁ C₁ : ℝ} (hPI : PrimeInput K c₁ C₁ q₀) {Q₀ : ℝ} (hQ₀1 : 1 ≤ Q₀) (hQ₀q₀ : ↑q₀ ≤ Q₀) (hQ₀ : ∀ (q : ℕ), Q₀ ≤ ↑q → Real.log ↑q * Real.log ↑S.card ≤ ↑q ^ (1 / 4)) : c₁ / ↑K * ∑ a ∈ S, ↑(L S a) ≤ (Real.log Q₀ + 2 / Real.log 2) * (2 / Real.log 2) * (↑S.card * Real.log ↑S.card) + 4 * (↑S.card * Real.log ↑S.card) + (c₁ + C₁) * ↑S.card

The explicit form of the upper bound.

theorem RunsOfMultiples.upper_of_primeInput {K q₀ : ℕ} {c₁ C₁ : ℝ} (hPI : PrimeInput K c₁ C₁ q₀) : ∃ (C : ℝ) (N : ℕ), ∀ (S : Finset ℕ), (∀ a ∈ S, 0 < a) → N ≤ S.card → ↑(∑ a ∈ S, kVal S a) ≤ C * ↑S.card * Real.log ↑S.card * Real.log (Real.log ↑S.card)

The upper bound in asymptotic form, given the prime-number input.