Erdős Problem 942

Reference: erdosproblems.com/942

def Erdos942.erdos_942.h (n : ℕ) : ℕ

Let $h(n)$ count the number of powerful integers in $[n^2, (n + 1)^2)$.

Equations

• Erdos942.erdos_942.h n = (Finset.filter Nat.Powerful (Finset.Ico (n ^ 2) ((n + 1) ^ 2))).card

theorem Erdos942.erdos_942 : (∃ c > 0, ∃ (o : ℕ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ (n : ℕ), ↑(erdos_942.h n) < Real.log ↑n ^ (c + o n) ∧ {n : ℕ | ↑(erdos_942.h n) > Real.log ↑n ^ (c - o n)}.Infinite) ↔ sorry

Is there some constant $c > 0$ such that $h(n) < (\log n)^{c + o(1)}$ and, for infinitely many $n$, $h(n) > (\log n)^{c - o(1)}$.

theorem Erdos942.erdos_942.variants.limsup : Filter.limsup ((fun (n : ℕ) => ↑n) ∘ h) Filter.atTop = ⊤

It is not hard to prove that $\limsup h(n) = \infty$.

theorem Erdos942.erdos_942.variants.density : ∃ (δ : ℕ → ℝ), ∀ (l : ℕ), {n : ℕ | h n = l}.HasDensity (δ l) ∧ ∑' (l : ℕ), δ l = 1

It is not hard to prove that the density $δ_l$ of integers for which $h(n) = l$ exists and satisfies $$\sum_l δ_l = 1$$.