Erdős problem 239
Let be a multiplicative function. Is it true that 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.leanTrue ↔ ∀ (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