Erdős Problem 933

References:

• erdosproblems.com/933
• [Er76d] Erdős, P, Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44.

def Erdos933.k (n : ℕ) : ℕ

The 2-adic valuation of $n(n+1)$.

Equations

• Erdos933.k n = padicValNat 2 (n * (n + 1))

def Erdos933.l (n : ℕ) : ℕ

The 3-adic valuation of $n(n+1)$.

Equations

• Erdos933.l n = padicValNat 3 (n * (n + 1))

theorem Erdos933.erdos_933 : sorry ↔ Filter.limsup (fun (n : ℕ) => ↑↑(2 ^ k n * 3 ^ l n) / (↑↑n * ↑(Real.log ↑n))) Filter.atTop = ⊤

If $n(n+1)=2^k3^lm$, where $(m,6)=1$, then is it true that $\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty$?

theorem Erdos933.erdos_933.variants.mahler : ∃ (c : ℕ → ℝ), c =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(2 ^ k n * 3 ^ l n) < ↑n ^ (1 + c n)

Mahler proved (a more general result that implies in particular) that $2^k3^l<n^{1+o(1)}$.

theorem Erdos933.erdos_933.variants.lower_bound : {n : ℕ | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infinite

Erdős [Er76d] wrote 'it is easy to see' that for infinitely many $n$, $2^k 3^l > n\log n$.

Steinerberger has noted a simple proof of this fact follows from taking $n=2^{3^r}$ for any integer $r\geq 1$, when $k=3^r$ and $l=r+1$.