erdos_126.variants.IsBigO

Specification

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.

Prize

$250

Paul Erdős

Lean 4 Statement

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

ID: ErdosProblems__126__erdos_126.variants.IsBigO

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof