Skip to content

Erdős problem 513

Start work

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 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
∃ c > 0, ⨆ f, Filter.liminf (fun r => Erdos513.ratio r ↑f) Filter.atTop ≤ 2 / Real.pi - c
SolvedStatement only, no proof