Erdős Problem 392 #
Reference: erdosproblems.com/392
theorem
Erdos392.erdos_392
(A : ℕ → ℕ)
(h :
∀ n > 0,
IsLeast
{x : ℕ | ∃ (t : ℕ) (_ : ∃ (a : Fin (t + 1) → ℕ), n.factorial = ∏ i : Fin (t + 1), a i ∧ Monotone a ∧ a ↑t ≤ n ^ 2),
t + 1 = x}
(A n))
:
Let $A(n)$ denote the least value of $t$ such that $$ n! = a_1 \cdots a_t $$ with $a_1 \leq \cdots \leq a_t\leq n^2$. Then $$ A(n) = \frac{n}{2} - \frac{n}{2\log n} + o\left(\frac{n}{\log n}\right). $$
theorem
Erdos392.erdos_392.variants.lower
(A : ℕ → ℕ)
(hA :
∀ n > 0,
IsLeast
{x : ℕ | ∃ (t : ℕ) (_ : ∃ (a : Fin (t + 1) → ℕ), n.factorial = ∏ i : Fin (t + 1), a i ∧ Monotone a ∧ a ↑t ≤ n),
t + 1 = x}
(A n))
:
If we change the condition to $a_t \leq n$ it can be shown that $$ A(n) = n - \frac{n}{log n} + o\left(\frac{n}{\log n}\right) $$
theorem
Erdos392.erdos_392.variants.implication
(h :
∀ (A : ℕ → ℕ),
(∀ n > 0,
IsLeast
{x : ℕ | ∃ (t : ℕ) (_ : ∃ (a : Fin (t + 1) → ℕ), n.factorial = ∏ i : Fin (t + 1), a i ∧ Monotone a ∧ a ↑t ≤ n ^ 2),
t + 1 = x}
(A n)) →
(fun (n : ℕ) => ↑(A n) - ↑n / 2 + ↑n / (2 * Real.log ↑n)) =o[Filter.atTop] fun (n : ℕ) => ↑n / Real.log ↑n)
(A : ℕ → ℕ)
(hA :
∀ n > 0,
IsLeast
{x : ℕ | ∃ (t : ℕ) (_ : ∃ (a : Fin (t + 1) → ℕ), n.factorial = ∏ i : Fin (t + 1), a i ∧ Monotone a ∧ a ↑t ≤ n),
t + 1 = x}
(A n))
:
Cambie has observed that a positive answer follows from the result above with $a_t \leq n$, simply by pairing variables together, e.g. taking $a'_i = a_{2i-1}a_{2i}$ (and the lower bound follows from Stirling's approximation).