Erdős Problem 126

Reference: erdosproblems.com/126

def IsMaximalAddFactorsCard (f : ℕ → ℕ) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem erdos_126 : (∀ (f : ℕ → ℕ), IsMaximalAddFactorsCard f → Filter.Tendsto (fun (n : ℕ) => ↑(f n) / Real.log ↑n) Filter.atTop Filter.atTop) ↔ sorry

Let $f(n)$ be maximal such that if $A\subseteq\mathbb{N}$ has $|A| = n$ then $\prod_{a\neq b\in A}(a + b)$ has at least $f(n)$ distinct prime factors. Is it true that $\frac{f(n)}{\log n} \to\infty$?

theorem erdos_126.variants.IsBigO (f : ℕ → ℕ) (hf : IsMaximalAddFactorsCard f) : ((fun (n : ℕ) => Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => ↑(f n)) ∧ (fun (n : ℕ) => ↑(f n)) =O[Filter.atTop] fun (n : ℕ) => ↑n / Real.log ↑n

Erdős and Turán proved [ErTu34] in their first joint paper that $$ \log n \ll f(n) \ll \frac{n}{\log n} $$

[ErTu34] Erdős, Paul and Turan, Paul, On a Problem in the Elementary Theory of Numbers. Amer. Math. Monthly (1934), 608-611.

theorem erdos_126.variants.isLittleO (f : ℕ → ℕ) (hf : IsMaximalAddFactorsCard f) : (fun (n : ℕ) => ↑(f n)) =o[Filter.atTop] fun (n : ℕ) => ↑n / Real.log ↑n

Erdős says that $f(n) = o(\frac{n}{\log n})$ has never been proved.