Erdős problem 520

Let $f$ be a Rademacher multiplicative function. Does there exist some constant $c > 0$ such that, almost surely, $\limsup_{N \to \infty} \frac{\sum_{m \leq N} f(m)}{\sqrt{N \log \log N}} = c?$

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

520.lean

Retained formal statement1 of 1

Let $f$ be a Rademacher multiplicative function. Does there exist some constant $c > 0$ such that, almost surely, $\limsup_{N \to \infty} \frac{\sum_{m \leq N} f(m)}{\sqrt{N \log \log N}} = c?$

FormalConjectures/ErdosProblems/520.leanErdos520.erdos_5206 linesExact file

1True ↔2  ∃ c > 0,3    ∀ (Ω : Type) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]4      (f : ℕ → Ω → ℝ),5      Erdos520.IsRademacherMultiplicative f →6        ∀ᵐ (ω : Ω), Filter.limsup (fun N => ∑ m ∈ Finset.Iic N, f m ω / √(↑N * Real.log (Real.log ↑N))) Filter.atTop = c

OpenStatement only, no proof