Erdős Problem 700

Reference: erdosproblems.com/700

A problem of Erdős and Szekeres [ErSz78].

References:

• [ErSz78] Erdős, P. and Szekeres, G., Some number theoretic problems on binomial coefficients, Austral. Math. Soc. Gaz. (1978), 97-99.
• OEIS A091963
• Guy, R. K., Unsolved Problems in Number Theory, B31, B33.

noncomputable def Erdos700.f (n : ℕ) : ℕ

f n = min_{1 < k ≤ n/2} gcd(n, C(n,k)). (The infimum is 0 when the range is empty, i.e. n < 4.)

Equations

• Erdos700.f n = sInf {m : ℕ | ∃ (k : ℕ), 1 < k ∧ k ≤ n / 2 ∧ m = n.gcd (n.choose k)}

noncomputable def Erdos700.P (n : ℕ) : ℕ

P n is the largest prime factor of n (and 0 if n ≤ 1).

Equations

• Erdos700.P n = n.primeFactors.sup id

def Erdos700.fSet (n : ℕ) : Set ℕ

The set whose infimum defines f.

Equations

• Erdos700.fSet n = {m : ℕ | ∃ (k : ℕ), 1 < k ∧ k ≤ n / 2 ∧ m = n.gcd (n.choose k)}

theorem Erdos700.f_eq (n : ℕ) : f n = sInf (fSet n)

f n unfolds to the infimum of fSet n.

theorem Erdos700.f_mem (n k : ℕ) (h1 : 1 < k) (h2 : k ≤ n / 2) : n.gcd (n.choose k) ∈ fSet n

Each gcd(n, C(n,k)) with 1 < k ≤ n/2 belongs to fSet n.

theorem Erdos700.f_le (n k : ℕ) (h1 : 1 < k) (h2 : k ≤ n / 2) : f n ≤ n.gcd (n.choose k)

f n is a lower bound: f n ≤ gcd(n, C(n,k)) for every 1 < k ≤ n/2.

theorem Erdos700.erdos_700.parts.i (n : ℕ) (hn : ¬Nat.Prime n) (hn1 : 1 < n) : f n = n / P n ↔ sorry

Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$ and let $P(n)$ be the largest prime dividing $n$.

(a) Characterise those composite $n$ such that $f(n) = n/P(n)$.

Erdős–Szekeres [ErSz78] note that $f(n) = n/P(n)$ when $n$ is a product of two primes (erdos_700.variants.prime_mul), with $n = 30$ a further example. The characterisation itself is open; we state it as the (unknown) predicate that is equivalent to being such an n.

theorem Erdos700.erdos_700.parts.ii : sorry ↔ {n : ℕ | ¬Nat.Prime n ∧ 1 < n ∧ f n ^ 2 > n}.Infinite

Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$.

(b) Are there infinitely many composite $n$ such that $f(n) > n^{1/2}$?

Erdős–Szekeres [ErSz78] could not prove this. (Since $f(n) \ge p(n)$, the least prime factor of $n$, there are infinitely many $n$ — those of the form $p^2$ — with $f(n) \ge n^{1/2}$; the question asks for the strict inequality.) Here $f(n) > n^{1/2}$ is written as (f n) ^ 2 > n.

theorem Erdos700.erdos_700.parts.iii : sorry ↔ ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), ¬Nat.Prime n → 1 < n → ↑(f n) ≤ C * ↑n / Real.log ↑n ^ A

Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$.

(c) Is it true that, for every composite $n$, $f(n) \ll_A n/(\log n)^A$ for every $A > 0$?

Erdős–Szekeres [ErSz78] prove the weaker bound $f(n) \le (1 + o(1)) n/\log n$ (the case $A = 1$). Here $f(n) \ll_A n/(\log n)^A$ is spelled out as: for every A > 0 there is a constant C (depending on A) with f(n) ≤ C · n/(log n)^A for every composite n.

theorem Erdos700.prime_dvd_of_not_dvd_choose (P n k : ℕ) (hP : Nat.Prime P) (hPn : P ∣ n) (h : ¬P ∣ n.choose k) : P ∣ k

Lucas (one step): for prime P ∣ n, if P ∤ C(n,k) then P ∣ k.

theorem Erdos700.erdos_700.variants.prime_pow (p a : ℕ) (hp : Nat.Prime p) (ha : 2 ≤ a) : f (p ^ a) = p

f(p^a) = p for a prime p and a ≥ 2 (recorded by Erdős–Szekeres [ErSz78]). In particular, since (p^a) / P(p^a) = p^{a-1}, the prime power p^a is a "hit" (f(n) = n / P(n)) if and only if a = 2.

theorem Erdos700.erdos_700.variants.prime_mul (p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p < q) : f (p * q) = p

f(pq) = p for distinct primes p < q (recorded by Erdős–Szekeres [ErSz78]); in particular pq is always a "hit" (f(pq) = pq / P(pq) = p). Proof via Lucas' theorem: p ∤ C(pq,k) ⟹ p ∣ k (and the same for q), so any k with gcd(pq, C(pq,k)) = 1 must be a multiple of pq, of which there are none in (1, pq/2]; the witness k = q gives gcd(pq, C(pq,q)) = p.