Erdős problem 520 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

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

Sources

Search problems.science