Products of primes in an interval

The explicit affine disperser works over 𝔽_{2 ^ n} for n a product of distinct primes from an interval (L, 4 L], kept below a target T by a greedy walk through the primes in increasing order (Cslib.selectBelow). The walk either takes every prime or ends within a factor 4 L of T (Cslib.prod_le_or_lt_mul_prod_selectBelow), and Chebyshev's bounds show that the product of all primes in (L, 4 L] is at least 4 ^ L up to a factor (4 L + 1) ^ (4 √L + 5) (Cslib.four_pow_le_mul_prod_primesIoc): the lower bound θ (4 L) ≥ 4 L log 2 - O(√L log L) beats the upper bound θ L ≤ 2 L log 2 by 2 L log 2.

Main definitions

• Cslib.primesIoc: the primes in (a, b], in increasing order.
• Cslib.selectBelow: the greedy choice of primes with product at most T.

Main results

• Cslib.prod_selectBelow_le: the chosen product is at most T.
• Cslib.prod_le_or_lt_mul_prod_selectBelow: either every prime is chosen or the product exceeds T / B, for B a bound on the primes.
• Cslib.four_pow_le_mul_prod_primesIoc: 4 ^ L is at most (4 L + 1) ^ (4 ⌊√L⌋ + 5) times the product of the primes in (L, 4 L].

References

• P. L. Chebyshev, Mémoire sur les nombres premiers

def Cslib.primesIoc (a b : ℕ) : List ℕ

The primes p with a < p ≤ b, in increasing order.

theorem Cslib.mem_primesIoc {a b p : ℕ} : p ∈ primesIoc a b ↔ a < p ∧ p ≤ b ∧ Nat.Prime p

p is in primesIoc a b exactly when p is a prime with a < p ≤ b.

theorem Cslib.nodup_primesIoc (a b : ℕ) : (primesIoc a b).Nodup

primesIoc a b has no duplicates.

def Cslib.selectBelow : ℕ → List ℕ → List ℕ

The greedy choice from a list ps of primes with product at most T: walk through ps, keeping each prime that fits into the remaining budget.

theorem Cslib.selectBelow_sublist (T : ℕ) (ps : List ℕ) : (selectBelow T ps).Sublist ps

The greedy choice is a sublist of ps.

theorem Cslib.prod_selectBelow_le {T : ℕ} (hT : 1 ≤ T) (ps : List ℕ) : (selectBelow T ps).prod ≤ T

The greedy choice has product at most the budget T ≥ 1.

theorem Cslib.prod_le_or_lt_mul_prod_selectBelow {B : ℕ} (T : ℕ) {ps : List ℕ} (hps : ∀ p ∈ ps, 0 < p ∧ p ≤ B) : ps.prod ≤ (selectBelow T ps).prod ∨ T < B * (selectBelow T ps).prod

The greedy choice is large: if every element of ps is positive and at most B, either every element is chosen (the product of ps is at most the chosen product) or the chosen product exceeds T / B.

theorem Cslib.prod_primesIoc (a b : ℕ) : (primesIoc a b).prod = ∏ p ∈ Finset.Ico (a + 1) (b + 1) with Nat.Prime p, p

The product of primesIoc a b is the product of the primes in the interval [a + 1, b].

theorem Cslib.four_pow_le_mul_prod_primesIoc (L : ℕ) : 4 ^ L ≤ (4 * L + 1) ^ (4 * L.sqrt + 5) * (primesIoc L (4 * L)).prod

Chebyshev's bounds on primes in (L, 4 L]: 4 ^ L ≤ (4 L + 1) ^ (4 ⌊√L⌋ + 5) times their product.