Erdős Problem 239

References:

• erdosproblems.com/239
• [Ha68] Halász, G., Über die Mittelwerte multiplikativer zahlentheoretischer Funktionen. Acta Math. Acad. Sci. Hungar. (1968), 365-403.
• [Wi67] Wirsing, E., Das asymptotische Verhalten von Summen über multiplikative Funk­tionen. Acta Math. Acad. Sei. Hung. (1967), 411-467.

theorem Erdos239.erdos_239 : True ↔ ∀ (f : ℕ → ℝ), (∀ n ≥ 1, f n = 1 ∨ f n = -1) ∧ (∀ (m n : ℕ), m.Coprime n → f (m * n) = f m * f n) ∧ f 1 = 1 → ∃ (L : ℝ), Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.Icc 1 N, f n) / ↑N) Filter.atTop (nhds L)

Let $f:\mathbb{N}\to \{-1,1\}$ be a multiplicative function. Is it true that [ \lim_{N\to \infty}\frac{1}{N}\sum_{n\leq N}f(n)] always exists?

The answer is yes, as proved by Wirsing [Wi67], and generalised by Halász [Ha68].