Erdős Problem 1063

References:

• erdosproblems.com/1063
• [ErSe83] Erdos, P. and Selfridge, J. L., Problem 6447. Amer. Math. Monthly (1983), 710.
• [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), Problem B31.
• [Mo85] Monier (1985). No reference found.

noncomputable def Erdos1063.n (k : ℕ) : ℕ

Let $n_k$ be the least $n \ge 2k$ such that all but one of the integers $n - i$ with $0 \le i < k$ divide $\binom{n}{k}$.

Equations

• Erdos1063.n k = sInf {m : ℕ | 2 * k ≤ m ∧ ∃ i0 < k, ¬m - i0 ∣ m.choose k ∧ ∀ i < k, i ≠ i0 → m - i ∣ m.choose k}

theorem Erdos1063.erdos_1063.variants.exists_exception {n k : ℕ} (hk : 2 ≤ k) (h : 2 * k ≤ n) : ∃ i < k, ¬n - i ∣ n.choose k

Erdős and Selfridge noted that, for $n \ge 2k$ with $k \ge 2$, at least one of the numbers $n - i$ for $0 \le i < k$ fails to divide $\binom{n}{k}$ ([ErSe83]).

theorem Erdos1063.erdos_1063.variants.small_values : n 2 = 4 ∧ n 3 = 6 ∧ n 4 = 9 ∧ n 5 = 12

The initial values satisfy $n_2 = 4$, $n_3 = 6$, $n_4 = 9$, and $n_5 = 12$ ([Gu04], Problem B31).

theorem Erdos1063.erdos_1063.variants.monier_upper_bound {k : ℕ} (hk : 3 ≤ k) : n k ≤ k.factorial

Monier observed that $n_k \le k!$ for $k \ge 3$ ([Mo85]). TODO: Find reference

theorem Erdos1063.erdos_1063.variants.cambie_upper_bound {k : ℕ} (hk : 3 ≤ k) : n k ≤ k * (Finset.Icc 1 (k - 1)).lcm id

Cambie observed the improved bound $n_k \le k \cdot \operatorname{lcm}(1, \dotsc, k - 1)$.

theorem Erdos1063.erdos_1063.variants.exp_upper_bound : ∃ (f : ℕ → ℝ), Filter.Tendsto f Filter.atTop (nhds 0) ∧ ∀ (k : ℕ), ↑(n k) ≤ Real.exp ((1 + f k) * ↑k)

The least common multiple bound implies $n_k \le \exp((1 + o(1))k)$.

theorem Erdos1063.erdos_1063.better_upper : have upper_bound := sorry; (fun (k : ℕ) => ↑(n k)) =O[Filter.atTop] upper_bound ∧ upper_bound =o[Filter.atTop] fun (k : ℕ) => ↑k * (Finset.Icc 1 (k - 1)).lcm fun (n : ℕ) => ↑n

Estimate $n_k$ by finding a better upper bound.