Erdős problem 239 · problems.science

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?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

239.lean

Retained formal statement1 of 1

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].

FormalConjectures/ErdosProblems/239.leanErdos239.erdos_2394 linesExact file

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

SolvedStatement only, no proof

Sources

Search problems.science