Conditional upper bound on B₂ via a radical lower bound (Erdős #367)

We formalize the "Langevin route" for the general-k upper bound in Erdős #367, taking the deep unproven ingredient — a radical lower bound for products of consecutive integers — as an explicit hypothesis (RadLB).

Definitions

• rad m — the radical (squarefree kernel) of m: product of its distinct prime factors.
• B2 m — the powerful (2-full) part of m: ∏_{p : v_p(m) ≥ 2} p^{v_p(m)}.
• F k n — the product of k consecutive integers starting at n.

Main results

• lemma_star (unconditional): rad m ^ 2 * B2 m ≤ m ^ 2.
• B2_upper_bound (conditional on RadLB): for every ε > 0 there is C' > 0 with B2 (F k n) ≤ C' * n ^ (2 + ε) for all n ≥ 1.

Definitions

def GeneralK.rad (m : ℕ) : ℕ

The radical of m: product of its distinct prime factors. rad(0) = rad(1) = 1 by convention.

Equations

• GeneralK.rad m = ∏ p ∈ m.factorization.support, p

def GeneralK.B2 (m : ℕ) : ℕ

The 2-full (powerful) part of m: product of p^{a_p} over primes with a_p ≥ 2.

Equations

• GeneralK.B2 m = ∏ p ∈ m.factorization.support with 2 ≤ m.factorization p, p ^ m.factorization p

def GeneralK.F (k n : ℕ) : ℕ

Product of k consecutive integers starting at n.

Equations

• GeneralK.F k n = ∏ i ∈ Finset.range k, (n + i)

Auxiliary lemmas

theorem GeneralK.prime_of_mem_factorization_support {m p : ℕ} (hp : p ∈ m.factorization.support) : Nat.Prime p

Every element of the factorization support is a prime.

theorem GeneralK.rad_pos (m : ℕ) : 1 ≤ rad m

theorem GeneralK.F_pos {k n : ℕ} (hn : 1 ≤ n) : 1 ≤ F k n

theorem GeneralK.F_ne_zero {k n : ℕ} (hn : 1 ≤ n) : F k n ≠ 0

theorem GeneralK.factor_le_mul {k n i : ℕ} (_hk : 1 ≤ k) (hn : 1 ≤ n) (hi : i < k) : n + i ≤ k * n

theorem GeneralK.F_le_pow {k n : ℕ} (hk : 1 ≤ k) (hn : 1 ≤ n) : F k n ≤ (k * n) ^ k

LEMMA STAR

theorem GeneralK.lemma_star (m : ℕ) (hm : m ≠ 0) : rad m ^ 2 * B2 m ≤ m ^ 2

Bridge to ℝ

theorem GeneralK.B2_le_sq_div_rad_sq (m : ℕ) (hm : m ≠ 0) : ↑(B2 m) ≤ ↑m ^ 2 / ↑(rad m) ^ 2

theorem GeneralK.rad_cast_pos (m : ℕ) : 0 < ↑(rad m)

RadLB hypothesis and conditional theorem

def GeneralK.RadLB (k : ℕ) : Prop

The "Langevin route" radical lower bound, taken as a hypothesis. For every ε > 0 there is C > 0 such that rad(F(k,n)) ≥ C · n^{k-1-ε} for all n ≥ 1.

Equations

• GeneralK.RadLB k = ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ↑(GeneralK.rad (GeneralK.F k n)) ≥ C * ↑n ^ (↑k - 1 - ε)

theorem GeneralK.B2_upper_bound (k : ℕ) (hk : 1 ≤ k) (hRadLB : RadLB k) (ε : ℝ) : 0 < ε → ∃ (C' : ℝ), 0 < C' ∧ ∀ (n : ℕ), 1 ≤ n → ↑(B2 (F k n)) ≤ C' * ↑n ^ (2 + ε)