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].
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/516.lean∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (n : ℕ), a n ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → Erdos516.OfFiniteOrder f → Filter.limsup (fun r => Erdos516.ratio r f) Filter.atTop = 1SolvedStatement only, no proof