Erdős problem 516 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

516.lean

Retained formal statement1 of 3

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].

FormalConjectures/ErdosProblems/516.leanErdos516.erdos_5166 linesExact file

1∀ {f : ℂ → ℂ} {n : ℕ → ℕ},2  HasFabryGaps n →3    ∀ {a : ℕ → ℂ},4      (∀ (n : ℕ), a n ≠ 0) →5        (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) →6          Erdos516.OfFiniteOrder f → Filter.limsup (fun r => Erdos516.ratio r f) Filter.atTop = 1

SolvedStatement only, no proof

Sources

Search problems.science