Erdős problem 513

Let `f` be a transcendental entire function. What is the greatest possible value of `liminf (fun r : ℝ => ratio r f) atTop`?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

513.lean

Retained formal statement1 of 3

Let f be a transcendental entire function. What is the greatest possible value of liminf (fun r : ℝ => ratio r f) atTop?

FormalConjectures/ErdosProblems/513.leanErdos513.erdos_5131 lineExact file

1sorry = ⨆ f, Filter.liminf (fun r => Erdos513.ratio r ↑f) Filter.atTop

OpenStatement only, no proof