Skip to content

Erdős problem 520

Let ff be a Rademacher multiplicative function. Does there exist some constant c>0c > 0 such that, almost surely, lim sup⁡N→∞∑m≤Nf(m)Nlog⁡log⁡N=c? \limsup_{N \to \infty} \frac{\sum_{m \leq N} f(m)}{\sqrt{N \log \log N}} = c?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/520.lean

Formal Conjectures

FormalConjectures/ErdosProblems/520.leanErdos520.erdos_5206 linesExact file
True ↔  ∃ c > 0,    ∀ (Ω : Type) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]      (f : ℕ → Ω → ℝ),      Erdos520.IsRademacherMultiplicative f →        ∀ᵐ (ω : Ω), Filter.limsup (fun N => ∑ m ∈ Finset.Iic N, f m ω / √(↑N * Real.log (Real.log ↑N))) Filter.atTop = c
OpenStatement only, no proof

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page