Skip to content

Erdős problem 239

Start work

Let f:N→{−1,1}f:\mathbb{N}\to \{-1,1\} be a multiplicative function. Is it true that lim⁡N→∞1N∑n≤Nf(n) \lim_{N\to \infty}\frac{1}{N}\sum_{n\leq N}f(n) always exists?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

239.lean

Retained formal statement1 of 1

Let f:N→{−1,1}f:\mathbb{N}\to \{-1,1\} be a multiplicative function. Is it true that lim⁡N→∞1N∑n≤Nf(n) \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
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)
SolvedStatement only, no proof