Erdős Problem #520

Prime entries are random variables. -/ measurable_of_prime p : p.Prime → Measurable (f p) /-- Prime entries are independent. -/ iIndepFun_primes : iIndepFun (fun p : Primes ↦ f p) ℙ /-- Primes entries are uniformly distributed on `{-1, 1}`. -/ prob_of_prime p : p.Prime → ℙ {ω | f p ω = 1} = 1 / 2 ∧ ℙ {ω | f p ω = -1} = 1 / 2 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 /-- 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? \] The answer is no: Høystad [Hø26] (with GPT-5.6 Pro and Claude) proved, following the Halász–Lau–Tenenbaum–Wu–Caich martingale approach with Harper's low-moment estimates [Ha13], that almost surely \(\sum_{m \le N} f(m) \ll \sqrt{N} (\log \log N)^{1/4 + \eta}\) for every \(\eta > 0\), so the \(\limsup\) is \(0\) almost surely. The linked formal proof works with the concrete model `ℕ → Bool` with the product of fair coins, whose squarefree-supported Rademacher function is `IsRademacherMultiplicative`; this refutes the statement b