Skip to content

Erdős problem 516

Start work

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

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

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
∀ {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 = 1
SolvedStatement only, no proof