Radical bound and double counting (Lemma 3 and equation (7))

For a finite set T of positive integers that is closed under divisors (DivClosed) and under replacing a prime factor by a smaller prime (ShiftClosed), we show

∑_{a ∈ T} L T a = O(n log n log log n), n = |T|.

• Lemma 3: for b ∈ T with m distinct prime factors, 2 ^ m ≤ n, and every product ∏_{p ∣ b} g p with g p ≤ p prime lies in T. Each such product has at most m ^ m preimages g, so ∏_{p ∣ b} π(p) ≤ n m ^ m. With log p ≤ 2 log π(p) + C this gives ∑_{p ∣ b} log p = O(log n log log n). (docs/first-missing-multiple.pdf uses m! preimages; m ^ m suffices.)
• Equation (7): ∑_{a ∈ T} θ(L T a) ≤ ∑_{b ∈ T} ∑_{p ∣ b} log p, via (a, p) ↦ (p a, p).

theorem RunsOfMultiples.box_mem {T : Finset ℕ} (hshift : ShiftClosed T) (g : ℕ → ℕ) (s : Finset ℕ) (hs : ∀ p ∈ s, Nat.Prime p ∧ Nat.Prime (g p) ∧ g p ≤ p) (c : ℕ) : c * ∏ p ∈ s, p ∈ T → c * ∏ p ∈ s, g p ∈ T

Replacing the prime factors p ∈ s of c * ∏ s by smaller primes g p stays inside a shift-closed set.

theorem RunsOfMultiples.prod_primeFactors_mem {T : Finset ℕ} (hdiv : DivClosed T) {b : ℕ} (hb : b ∈ T) {s : Finset ℕ} (hs : s ⊆ b.primeFactors) : ∏ p ∈ s, p ∈ T

Products of prime factors of b ∈ T lie in a divisor-closed T.

theorem RunsOfMultiples.two_pow_card_primeFactors_le {T : Finset ℕ} (hdiv : DivClosed T) {b : ℕ} (hb : b ∈ T) : 2 ^ b.primeFactors.card ≤ T.card

(5): the squarefree divisors of b are distinct elements of T, so 2 ^ m ≤ |T|.

theorem RunsOfMultiples.prod_card_primesUpTo_le {T : Finset ℕ} (hdiv : DivClosed T) (hshift : ShiftClosed T) {b : ℕ} (hb : b ∈ T) : ∏ p ∈ b.primeFactors, (primesUpTo p).card ≤ T.card * b.primeFactors.card ^ b.primeFactors.card

(6), with m ^ m in place of m!: the box of index tuples has at most |T| m ^ m elements.

theorem RunsOfMultiples.log_le_two_log_card_primesUpTo : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : ℕ), Nat.Prime p → Real.log ↑p ≤ 2 * Real.log ↑(primesUpTo p).card + C

log p ≤ 2 log π(p) + C for all primes p, from π(4q) - π(q) ≥ q^(3/4) for large q (this is π(x) ≥ √x for large x, up to constants).

theorem RunsOfMultiples.sum_log_primeFactors_le {C : ℝ} (hC : ∀ (p : ℕ), Nat.Prime p → Real.log ↑p ≤ 2 * Real.log ↑(primesUpTo p).card + C) {T : Finset ℕ} (hdiv : DivClosed T) (hshift : ShiftClosed T) {b : ℕ} (hb : b ∈ T) : ∑ p ∈ b.primeFactors, Real.log ↑p ≤ 2 * Real.log ↑T.card + 2 * (↑b.primeFactors.card * Real.log ↑b.primeFactors.card) + C * ↑b.primeFactors.card

Lemma 3, explicit form: ∑_{p ∣ b} log p ≤ 2 log n + 2 m log m + C m.

theorem RunsOfMultiples.radical_bound : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (T : Finset ℕ), DivClosed T → ShiftClosed T → 1 ≤ Real.log (Real.log ↑T.card) → ∀ b ∈ T, ∑ p ∈ b.primeFactors, Real.log ↑p ≤ K * Real.log ↑T.card * Real.log (Real.log ↑T.card)

Lemma 3. ∑_{p ∣ b} log p = O(log n log log n) for b ∈ T, once log log n ≥ 1.

theorem RunsOfMultiples.sum_theta_L_le (T : Finset ℕ) (hpos : ∀ a ∈ T, 0 < a) : ∑ a ∈ T, ∑ p ∈ primesUpTo (L T a), Real.log ↑p ≤ ∑ b ∈ T, ∑ p ∈ b.primeFactors, Real.log ↑p

Double counting (7). ∑_{a ∈ T} θ(L T a) ≤ ∑_{b ∈ T} ∑_{p ∣ b} log p, via the injection (a, p) ↦ (p a, p): if p ≤ L T a then p a ∈ T.

theorem RunsOfMultiples.sum_L_le_of_closed : ∃ (C : ℝ) (N : ℕ), ∀ (T : Finset ℕ), (∀ a ∈ T, 0 < a) → DivClosed T → ShiftClosed T → N ≤ T.card → ∑ a ∈ T, ↑(L T a) ≤ C * ↑T.card * Real.log ↑T.card * Real.log (Real.log ↑T.card)

Upper bound for closed sets. If T is closed under divisors and prime shifts, then ∑_{a ∈ T} L T a = O(n log n log log n) with n = |T|.