Erdős problem 516
Let f = ∑ aₖzⁿₖ be an entire function of finite order such that nₖ / k → ∞. Then limsup (fun r => ratio r f) atTop = 1. This is proved in [Fu63].
Sources
FormalConjectures/ErdosProblems/
516.lean
Retained formal statement
Is it true that for all entire functions f = ∑ aₖzⁿₖ such that ∑' 1 / nₖ < ∞, limsup (fun r => ratio r f) atTop = 1?
True ↔ ∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFejerGaps n → ∀ {a : ℕ → ℂ}, (∀ (n : ℕ), a n ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → Filter.limsup (fun r => Erdos516.ratio r f) Filter.atTop = 1OpenStatement only, no proof