Skip to content

Erdős problem 239

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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/239.lean

Formal Conjectures

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

Continue