Erdős problem 513 · problems.science

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

Sources

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

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

513.lean

Retained formal statement2 of 3

For all transcendental entire function f, liminf (fun r : ℝ => ratio r f) atTop > 1 / 2.

FormalConjectures/ErdosProblems/513.leanErdos513.erdos_513.variants.lower_bound1 lineExact file

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

SolvedStatement only, no proof