Runs of multiples: the lower bound via the "matching construction"

This file formalises §3 ("A matching construction") of docs/first-missing-multiple.pdf.

For y ≥ 2 let

• small y = primes p ≤ √y (encoded as p * p ≤ y), q = #small y;
• large y = primes in (√y, y] (encoded as y < p * p, p ≤ y), m = #large y;
• L = ⌊log₂ y⌋ = Nat.log 2 y, H = 2 q L.

S_y is the set of integers ∏_{p ≤ √y} p ^ u_p * ∏_{√y < p ≤ y} p ^ v_p with 0 ≤ u_p ≤ H and ∑ v_p ≤ m. We represent exponent vectors as finsupps ℕ →₀ ℕ and the number as f.prod (· ^ ·). The small-prime part ranges over smallExp y H (Finset.finsupp), the large-prime part over largeExp y m: finsupps supported on insert 1 (large y) with total sum exactly m, the coordinate at 1 being a slack variable (1 ^ v = 1), so that these give exactly the products with ∑ v_p ≤ m (stars and bars with a slack variable; Finset.card_finsuppAntidiag_nat_eq_choose).

The good elements (u_p ≤ H - L, ∑ v_p ≤ m - 1) have all first y multiples in S_y, at least a quarter of S_y is good, and |S_y| ≤ (H + 1) ^ q * C(2m, m) ≤ exp (C y / log y). The padding step is the same as in RunsOfMultiples.Replication (replicate).

def RunsOfMultiples.Alt.small (y : ℕ) : Finset ℕ

Primes p with p ≤ √y, i.e. p * p ≤ y.

Equations

• RunsOfMultiples.Alt.small y = {p ∈ (y + 1).primesBelow | p * p ≤ y}

def RunsOfMultiples.Alt.large (y : ℕ) : Finset ℕ

Primes p with √y < p ≤ y.

Equations

• RunsOfMultiples.Alt.large y = {p ∈ (y + 1).primesBelow | y < p * p}

def RunsOfMultiples.Alt.qq (y : ℕ) : ℕ

q = π(√y).

Equations

• RunsOfMultiples.Alt.qq y = (RunsOfMultiples.Alt.small y).card

def RunsOfMultiples.Alt.mm (y : ℕ) : ℕ

m = π(y) - π(√y).

Equations

• RunsOfMultiples.Alt.mm y = (RunsOfMultiples.Alt.large y).card

def RunsOfMultiples.Alt.LL (y : ℕ) : ℕ

L = ⌊log₂ y⌋.

Equations

• RunsOfMultiples.Alt.LL y = Nat.log 2 y

def RunsOfMultiples.Alt.HH (y : ℕ) : ℕ

H = 2 q L.

Equations

• RunsOfMultiples.Alt.HH y = 2 * RunsOfMultiples.Alt.qq y * RunsOfMultiples.Alt.LL y

def RunsOfMultiples.Alt.slack (y : ℕ) : Finset ℕ

Index set for the large-prime exponents, with a slack coordinate at 1.

Equations

• RunsOfMultiples.Alt.slack y = insert 1 (RunsOfMultiples.Alt.large y)

noncomputable def RunsOfMultiples.Alt.pw (f : ℕ →₀ ℕ) : ℕ

The number with exponent vector f.

Equations

• RunsOfMultiples.Alt.pw f = f.prod fun (x1 x2 : ℕ) => x1 ^ x2

noncomputable def RunsOfMultiples.Alt.smallExp (y e : ℕ) : Finset (ℕ →₀ ℕ)

Small-prime exponent vectors with all entries ≤ e.

Equations

• RunsOfMultiples.Alt.smallExp y e = (RunsOfMultiples.Alt.small y).finsupp fun (x : ℕ) => Finset.range (e + 1)

noncomputable def RunsOfMultiples.Alt.largeExp (y k : ℕ) : Finset (ℕ →₀ ℕ)

Large-prime exponent vectors (plus slack at 1) with total sum k.

Equations

• RunsOfMultiples.Alt.largeExp y k = (RunsOfMultiples.Alt.slack y).finsuppAntidiag k

noncomputable def RunsOfMultiples.Alt.smallPart (y e : ℕ) : Finset ℕ

Small parts ∏_{p ≤ √y} p ^ u_p, u_p ≤ e.

Equations

• RunsOfMultiples.Alt.smallPart y e = Finset.image RunsOfMultiples.Alt.pw (RunsOfMultiples.Alt.smallExp y e)

noncomputable def RunsOfMultiples.Alt.largePart (y k : ℕ) : Finset ℕ

Large parts ∏_{√y < p ≤ y} p ^ v_p, ∑ v_p ≤ k.

Equations

• RunsOfMultiples.Alt.largePart y k = Finset.image RunsOfMultiples.Alt.pw (RunsOfMultiples.Alt.largeExp y k)

noncomputable def RunsOfMultiples.Alt.Sy (y : ℕ) : Finset ℕ

The block S_y.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RunsOfMultiples.Alt.Gy (y : ℕ) : Finset ℕ

The good elements of S_y: u_p ≤ H - L, ∑ v_p ≤ m - 1.

Equations

• One or more equations did not get rendered due to their size.

Basic facts

theorem RunsOfMultiples.Alt.pw_add (f g : ℕ →₀ ℕ) : pw (f + g) = pw f * pw g

theorem RunsOfMultiples.Alt.pw_single (a k : ℕ) : pw (Finsupp.single a k) = a ^ k

theorem RunsOfMultiples.Alt.pw_pos (f : ℕ →₀ ℕ) (hf : ∀ p ∈ f.support, 0 < p) : 0 < pw f

theorem RunsOfMultiples.Alt.mem_small {y p : ℕ} : p ∈ small y ↔ Nat.Prime p ∧ p ≤ y ∧ p * p ≤ y

theorem RunsOfMultiples.Alt.mem_large {y p : ℕ} : p ∈ large y ↔ Nat.Prime p ∧ p ≤ y ∧ y < p * p

theorem RunsOfMultiples.Alt.one_notMem_large (y : ℕ) : 1 ∉ large y

theorem RunsOfMultiples.Alt.card_largeExp (y k : ℕ) : (largeExp y k).card = (mm y + k).choose k

theorem RunsOfMultiples.Alt.card_smallExp (y e : ℕ) : (smallExp y e).card = (e + 1) ^ qq y

theorem RunsOfMultiples.Alt.pw_injOn_smallExp (y e : ℕ) : Set.InjOn pw ↑(smallExp y e)

theorem RunsOfMultiples.Alt.pw_erase_one (f : ℕ →₀ ℕ) : pw f = pw (Finsupp.erase 1 f)

theorem RunsOfMultiples.Alt.pw_injOn_largeExp (y k : ℕ) : Set.InjOn pw ↑(largeExp y k)

Unique factorisation: the parts and their product are injective

theorem RunsOfMultiples.Alt.prime_dvd_pw {f : ℕ →₀ ℕ} {p : ℕ} (hp : Nat.Prime p) (h : p ∣ pw f) : ∃ r ∈ f.support, p ∣ r

theorem RunsOfMultiples.Alt.prime_dvd_smallPart {y e a p : ℕ} (ha : a ∈ smallPart y e) (hp : Nat.Prime p) (h : p ∣ a) : p ∈ small y

theorem RunsOfMultiples.Alt.prime_dvd_largePart {y k a p : ℕ} (ha : a ∈ largePart y k) (hp : Nat.Prime p) (h : p ∣ a) : p ∈ large y

theorem RunsOfMultiples.Alt.coprime_parts {y e k a b : ℕ} (ha : a ∈ smallPart y e) (hb : b ∈ largePart y k) : a.Coprime b

theorem RunsOfMultiples.Alt.smallPart_pos {y e a : ℕ} (ha : a ∈ smallPart y e) : 0 < a

theorem RunsOfMultiples.Alt.largePart_pos {y k b : ℕ} (hb : b ∈ largePart y k) : 0 < b

theorem RunsOfMultiples.Alt.mul_injOn_parts (y e k : ℕ) : Set.InjOn (fun (x : ℕ × ℕ) => x.1 * x.2) ↑(smallPart y e ×ˢ largePart y k)

theorem RunsOfMultiples.Alt.card_smallPart (y e : ℕ) : (smallPart y e).card = (e + 1) ^ qq y

theorem RunsOfMultiples.Alt.card_largePart (y k : ℕ) : (largePart y k).card = (mm y + k).choose k

theorem RunsOfMultiples.Alt.card_Sy (y : ℕ) : (Sy y).card = (HH y + 1) ^ qq y * (mm y + mm y).choose (mm y)

|S_y| = (H + 1) ^ q * C(2m, m) (equation (9)).

theorem RunsOfMultiples.Alt.card_Gy (y : ℕ) : (Gy y).card = (HH y - LL y + 1) ^ qq y * (mm y + (mm y - 1)).choose (mm y - 1)

At least a quarter of S_y is good

theorem RunsOfMultiples.Alt.bernoulli_aux (q L : ℕ) : (2 * q * L + 1) ^ q ≤ 2 * (2 * q * L - L + 1) ^ q

Bernoulli: (H + 1) ^ q ≤ 2 (H - L + 1) ^ q for H = 2 q L.

theorem RunsOfMultiples.Alt.choose_le_two_mul (m : ℕ) : (m + m).choose m ≤ 2 * (m + (m - 1)).choose (m - 1)

C(2m, m) = 2 C(2m - 1, m - 1) (for m ≥ 1; for m = 0 both sides are 1).

theorem RunsOfMultiples.Alt.card_Sy_le (y : ℕ) : (Sy y).card ≤ 4 * (Gy y).card

At least a quarter of S_y is good.

Good elements have their first y multiples in S_y

theorem RunsOfMultiples.Alt.factorization_mem_smallExp {y j : ℕ} (hj1 : 1 ≤ j) (hjy : j ≤ y) (h : ∀ (p : ℕ), Nat.Prime p → p ∣ j → p * p ≤ y) : j.factorization ∈ smallExp y (LL y)

If 1 ≤ j ≤ y has no prime factor > √y, its exponent vector lies in smallExp y L: each small-prime exponent of j is at most L = ⌊log₂ y⌋.

theorem RunsOfMultiples.Alt.decomp {y j : ℕ} (hj1 : 1 ≤ j) (hjy : j ≤ y) : ∃ (js : ℕ) (jl : ℕ), j = js * jl ∧ js.factorization ∈ smallExp y (LL y) ∧ 1 ≤ js ∧ jl ∈ slack y

Every 1 ≤ j ≤ y is js * jl with js having small-prime exponents ≤ L and jl ∈ {1} ∪ (√y, y] (at most one prime factor > √y, counted with multiplicity).

theorem RunsOfMultiples.Alt.add_mem_smallExp {y : ℕ} {g e : ℕ →₀ ℕ} (hg : g ∈ smallExp y (LL y)) (he : e ∈ smallExp y (HH y - LL y)) : g + e ∈ smallExp y (HH y)

theorem RunsOfMultiples.Alt.add_single_mem_largeExp {y k x c : ℕ} {f : ℕ →₀ ℕ} (hf : f ∈ largeExp y k) (hx : x ∈ slack y) : f + Finsupp.single x c ∈ largeExp y (k + c)

theorem RunsOfMultiples.Alt.mem_largePart_iff {y k b : ℕ} : b ∈ largePart y k ↔ ∃ (v : ℕ →₀ ℕ), v.support ⊆ large y ∧ ∑ p ∈ large y, v p ≤ k ∧ pw v = b

Sanity check of the slack encoding: largePart y k is exactly the set of ∏_{√y < p ≤ y} p ^ v_p with ∑ v_p ≤ k, as in (8).

theorem RunsOfMultiples.Alt.mul_mem_Sy {y a j : ℕ} (ha : a ∈ Gy y) (hj1 : 1 ≤ j) (hjy : j ≤ y) : j * a ∈ Sy y

If a is good and 1 ≤ j ≤ y, then j a ∈ S_y.

theorem RunsOfMultiples.Alt.Gy_subset_Sy {y : ℕ} (hy : 1 ≤ y) : Gy y ⊆ Sy y

theorem RunsOfMultiples.Alt.pos_of_mem_Sy {y a : ℕ} (ha : a ∈ Sy y) : 0 < a

theorem RunsOfMultiples.Alt.card_Sy_pos (y : ℕ) : 0 < (Sy y).card

Size of S_y: log |S_y| = O(y / log y) (upper half of (12))

theorem RunsOfMultiples.Alt.qq_le_sqrt (y : ℕ) : qq y ≤ y.sqrt

theorem RunsOfMultiples.Alt.mm_le (y : ℕ) : mm y ≤ (y + 1).primesBelow.card

theorem RunsOfMultiples.Alt.HH_add_one_le {y : ℕ} (hy : 2 ≤ y) : HH y + 1 ≤ y ^ 4

noncomputable def RunsOfMultiples.Alt.C₃ : ℝ

The constant in |S_y| ≤ exp (C₃ y / log y).

Equations

• RunsOfMultiples.Alt.C₃ = 64 + Real.log 4 * (2 * Real.log 4 + 2)

theorem RunsOfMultiples.Alt.C₃_pos : 0 < C₃

theorem RunsOfMultiples.Alt.card_Sy_le_exp {y : ℕ} (hy : 2 ≤ y) : ↑(Sy y).card ≤ Real.exp (C₃ * (↑y / Real.log ↑y))

|S_y| ≤ (H + 1) ^ q * 4 ^ m ≤ exp (C₃ y / log y), using q ≤ √y, H + 1 ≤ y ^ 4 and Chebyshev's bound for m ≤ π(y).

theorem RunsOfMultiples.Alt.block_alt : ∃ (δ : ℝ), 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 of §3: B = S_y, G = good elements, |G| ≥ |B| / 4, |B| ≤ exp (C₃ y / log y). Same shape as RunsOfMultiples.block.

Padding to every n (end of §3)

y = ⌊ε log n log log n⌋ with ε = 1 / (2 C₂), so |S_y| ≤ exp (L / 2) ≤ n / 2; take ⌊n / |S_y|⌋ disjoint dilates M ^ i • S_y and pad (replicate from RunsOfMultiples.Replication). The argument below is the one of lower_bound, applied to the block block_alt of §3.

theorem RunsOfMultiples.lower_bound_alt : ∃ (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)

Lower bound (alternative construction, §3).