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 statement2 of 3

Let f = ∑ aₖzⁿₖ be an entire function such that nₖ > k (log k) ^ (2 + c). Then limsup (fun r => ratio r f) atTop = 1. This is proved in [Ko65].

FormalConjectures/ErdosProblems/516.leanErdos516.erdos_516.variants.limsup_ratio_eq_one6 linesExact file

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

SolvedStatement only, no proof

Sources

Search problems.science