Erdős Problem 513

Reference:

• erdosproblems.com/513
• [ClHa64] Clunie, J. and Hayman, W. K., The maximum term of a power series. J. Analyse Math. (1964), 143-186.

noncomputable def Erdos513.ratio (r : ℝ) (f : ℂ → ℂ) : ℝ

Equations

• Erdos513.ratio r f = (⨆ (n : ℕ), ‖iteratedDeriv n f 0 * ↑(↑n.factorial)⁻¹ * ↑r ^ n‖) / ⨆ (z : { z : ℂ // ‖z‖ = r }), ‖f ↑z‖

theorem Erdos513.erdos_513.sup : sorry = ⨆ (f : { f : ℂ → ℂ // Transcendental (Polynomial ℂ) f ∧ Differentiable ℂ f }), Filter.liminf (fun (r : ℝ) => ratio r ↑f) Filter.atTop

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

theorem Erdos513.erdos_513.upper_bound : ∃ c > 0, ⨆ (f : { f : ℂ → ℂ // Transcendental (Polynomial ℂ) f ∧ Differentiable ℂ f }), Filter.liminf (fun (r : ℝ) => ratio r ↑f) Filter.atTop ≤ 2 / Real.pi - c

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

theorem Erdos513.erdos_513.lower_bound : ⨆ (f : { f : ℂ → ℂ // Transcendental (Polynomial ℂ) f ∧ Differentiable ℂ f }), Filter.liminf (fun (r : ℝ) => ratio r ↑f) Filter.atTop > 1 / 2

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