Runs of multiples: the lower bound

For every large n there is an n-element set S of positive integers with ∑ a ∈ S, kVal S a ≥ c n log n log log n.

Route (see docs/runs-of-multiples.pdf, §2):

• Sm X y is the set of y-smooth numbers in [1, X]. If a ∈ Sm X y then j * a ∈ Sm (X * y) y for all 1 ≤ j ≤ y.
• Rankin's trick (via Mathlib's Euler product over smooth numbers) with σ = 1 / log y gives |Sm (y ^ K) y| ≤ exp (K + C₀ y / log y).
• Pigeonhole over X_i = y ^ i, i ≤ K = ⌈y / log y⌉, gives a block B = Sm (y ^ (i+1)) y with |B| ≤ exp (C₂ y / log y) containing G = Sm (y ^ i) y, |G| ≥ δ |B|, all of whose first y multiples lie in B.
• ⌊n / |B|⌋ scaled copies M ^ j • B plus padding give the set for every large n.

Elementary analytic estimates

theorem RunsOfMultiples.inv_one_sub_exp_neg_le {u : ℝ} (hu : 0 < u) : (1 - Real.exp (-u))⁻¹ ≤ Real.exp (1 / u)

Smooth numbers and Rankin's bound

def RunsOfMultiples.Sm (X y : ℕ) : Finset ℕ

The y-smooth numbers in [1, X].

Equations

• RunsOfMultiples.Sm X y = X.smoothNumbersUpTo (y + 1)

theorem RunsOfMultiples.pos_of_mem_Sm {X y m : ℕ} (hm : m ∈ Sm X y) : 0 < m

theorem RunsOfMultiples.one_mem_Sm {X y : ℕ} (hX : 1 ≤ X) : 1 ∈ Sm X y

theorem RunsOfMultiples.Sm_mono {X X' y : ℕ} (h : X ≤ X') : Sm X y ⊆ Sm X' y

theorem RunsOfMultiples.mul_mem_Sm {X y a j : ℕ} (ha : a ∈ Sm X y) (hj1 : 1 ≤ j) (hjy : j ≤ y) : j * a ∈ Sm (X * y) y

noncomputable def RunsOfMultiples.rpowHom (σ : ℝ) : ℕ →* ℝ

The completely multiplicative function m ↦ m ^ (-σ).

Equations

• RunsOfMultiples.rpowHom σ = { toFun := fun (n : ℕ) => ↑n ^ (-σ), map_one' := ⋯, map_mul' := ⋯ }

theorem RunsOfMultiples.rankin_sum (σ : ℝ) (hσ : 0 < σ) (y X : ℕ) : ∑ m ∈ Sm X y, ↑m ^ (-σ) ≤ ∏ p ∈ (y + 1).primesBelow, (1 - ↑p ^ (-σ))⁻¹

theorem RunsOfMultiples.rankin_card (σ : ℝ) (hσ : 0 < σ) (y X : ℕ) (hX : 0 < X) : ↑(Sm X y).card ≤ ↑X ^ σ * ∏ p ∈ (y + 1).primesBelow, (1 - ↑p ^ (-σ))⁻¹

Rankin's trick: |Sm X y| ≤ X ^ σ ∏_{p ≤ y} (1 - p ^ (-σ))⁻¹.

theorem RunsOfMultiples.factor_le {y p : ℕ} (hy : 2 ≤ y) (hp : 2 ≤ p) : (1 - ↑p ^ (-(1 / Real.log ↑y)))⁻¹ ≤ Real.exp (Real.log ↑y / Real.log ↑p)

Each Euler factor with σ = 1 / log y is at most exp (log y / log p).

theorem RunsOfMultiples.sum_log_div_le (y : ℕ) (hy : 2 ≤ y) : ∑ p ∈ (y + 1).primesBelow, Real.log ↑y / Real.log ↑p ≤ 2 * ↑(y + 1).primesBelow.card + ↑y.sqrt * (Real.log ↑y / Real.log 2)

Splitting the primes at √y.

noncomputable def RunsOfMultiples.C₀ : ℝ

The constant in the Rankin bound.

Equations

• RunsOfMultiples.C₀ = 2 * (2 * Real.log 4 + 2) + 16 / Real.log 2

theorem RunsOfMultiples.C₀_pos : 0 < C₀

theorem RunsOfMultiples.sum_log_div_le' (y : ℕ) (hy : 2 ≤ y) : ∑ p ∈ (y + 1).primesBelow, Real.log ↑y / Real.log ↑p ≤ C₀ * (↑y / Real.log ↑y)

theorem RunsOfMultiples.card_Sm_le (y K : ℕ) (hy : 2 ≤ y) : ↑(Sm (y ^ K) y).card ≤ Real.exp (↑K + C₀ * (↑y / Real.log ↑y))

|Sm (y ^ K) y| ≤ exp (K + C₀ y / log y).

Pigeonhole: a block with many elements having long runs

theorem RunsOfMultiples.pigeon (f : ℕ → ℝ) (r : ℝ) (h0 : 1 ≤ f 0) (hr : 0 ≤ r) (K : ℕ) (hK : f K < r ^ K) : ∃ i < K, f (i + 1) < r * f i

theorem RunsOfMultiples.block : ∃ (δ : ℝ), 0 < δ ∧ ∃ (C₂ : ℝ), 0 < C₂ ∧ ∀ (y : ℕ), 2 ≤ y → ∃ (B : Finset ℕ) (G : Finset ℕ), (∀ a ∈ B, 0 < a) ∧ G ⊆ B ∧ (∀ a ∈ G, ∀ (j : ℕ), 1 ≤ j → j ≤ y → j * a ∈ B) ∧ 0 < B.card ∧ δ * ↑B.card ≤ ↑G.card ∧ ↑B.card ≤ Real.exp (C₂ * (↑y / Real.log ↑y))

The block: for every y ≥ 2 there are G ⊆ B, |G| ≥ δ |B|, |B| ≤ exp (C₂ y / log y), such that the first y multiples of every a ∈ G lie in B.

The lower bound

theorem RunsOfMultiples.lower_bound : ∃ (c : ℝ), 0 < c ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (S : Finset ℕ), (∀ a ∈ S, 0 < a) ∧ S.card = n ∧ c * ↑n * Real.log ↑n * Real.log (Real.log ↑n) ≤ ↑(∑ a ∈ S, kVal S a)