erdős #516
Let be an entire function of finite order such that . Let and . Is it true that
Worked, still open.
analysis · solved · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 30 · solved (literature)
theorem erdos_516 {f : ℂ → ℂ} {n : ℕ → ℕ}
(hn : HasFabryGaps n) {a : ℕ → ℂ} (ha : ∀ n, a n ≠ 0)
(hfn : ∀ z, HasSum (fun k => a k * z ^ n k) (f z)) (hf : OfFiniteOrder f) :
limsup (fun r => ratio r f) atTop = 1formal-conjectures/516.lean ↗status
solved