Problem

erdos:520

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

Open Current State

Declared status: open
Formalization: formalized
Subjects: number theoryprobability
OEIS: N/A
Sources: source:erdos-problemssource:formal-conjectures
Statement: www.erdosproblems.com

Matching claims

0

No direct claims

This problem has no directly related claim record.

Browse this Repository’s Claims