Erdős Problem 520

Reference: erdosproblems.com/520

structure IsRademacherMultiplicative {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (f : ℕ → Ω → ℝ) : Prop

A random function $f$ is Rademacher multiplicative if $f(1) = 1$, for each prime $p$, we independently choose $f(p) \in \{-1, 1\}$ uniformly at random, for each square-free integer $n = p_1 \cdots p_r$, $f(n) = f(p_1) \cdots f(p_r)$, and for each non-squarefree integer $n$, $f(n) = 0$.

• iIndepFun_primes : ProbabilityTheory.iIndepFun (fun (p : Nat.Primes) => f ↑p) MeasureTheory.volume

  Prime entries are independent.

• prob_of_prime (p : ℕ) : Nat.Prime p → MeasureTheory.volume {ω : Ω | f p ω = 1} = 1 / 2 ∧ MeasureTheory.volume {ω : Ω | f p ω = -1} = 1 / 2

  Primes entries are uniformly distributed on {-1, 1}.

• map_one (ω : Ω) : f 1 ω = 1
• map_mul_of_coprime (a b : ℕ) (ω : Ω) : a.Coprime b → f (a * b) ω = f a ω * f b ω
• map_of_not_squarefree (n : ℕ) (ω : Ω) : ¬Squarefree n → f n ω = 0

theorem erdos_520 {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] : sorry ↔ ∃ c > 0, ∀ (f : ℕ → Ω → ℝ), IsRademacherMultiplicative f → ∀ᵐ (ω : Ω), Filter.limsup (fun (N : ℕ) => ∑ m ∈ Finset.Iic N, f m ω / √(↑N * Real.log (Real.log ↑N))) Filter.atTop = c

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