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

For all transcendental entire function f, liminf (fun r : ℝ => ratio r f) atTop ≤ 2 / π - c for some c > 0. This is proved in [ClHa64].

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

1∃ c > 0, ⨆ f, Filter.liminf (fun r => Erdos513.ratio r ↑f) Filter.atTop ≤ 2 / Real.pi - c

SolvedStatement only, no proof