Erdős Problem 516

References:

• erdosproblems.com/516
• [Fu63] Fuchs, W. H. J., Proof of a conjecture of G. Pólya concerning gap series. Illinois J. Math. (1963), 661--667.
• [Ko65] Kövari, Thomas, A gap-theorem for entire functions of infinite order. Michigan Math. J. (1965), 133--140.

def OfFiniteOrder {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : E → F) : Prop

An entire function f is said to be of finite order if there exist numbers c, a ≥ 0 such that for all z, ‖f z‖ ≤ c * rexp (‖z‖ ^ a).

Equations

• OfFiniteOrder f = (Differentiable ℂ f ∧ ∃ c ≥ 0, ∃ a ≥ 0, ∀ (z : E), ‖f z‖ ≤ c * Real.exp (‖z‖ ^ a))

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

Equations

• Erdos516.ratio r f = Real.log (⨅ (z : { z : ℂ // ‖z‖ = r }), ‖f ↑z‖) / Real.log (⨆ (z : { z : ℂ // ‖z‖ = r }), ‖f ↑z‖)

theorem Erdos516.erdos_516.limsup_ratio_eq_one_of_hasFabryGaps_ofFiniteOrder {f : ℂ → ℂ} {n : ℕ → ℕ} (hn : HasFabryGaps n) {a : ℕ → ℂ} (hfn : ∀ (z : ℂ), HasSum (fun (k : ℕ) => a k * z ^ n k) (f z)) (hf : OfFiniteOrder f) : Filter.limsup (fun (r : ℝ) => ratio r f) Filter.atTop = 1

Let f = ∑ aₖzⁿₖ be an entire function of finite order such that nₖ / k → ∞. Then limsup (fun r => ratio r f) atTop = 1. This is proved in [Fu63].

theorem Erdos516.erdos_516.limsup_ratio_eq_one {f : ℂ → ℂ} {n : ℕ → ℕ} (hn : ∃ c > 0, ∀ (k : ℕ), ↑(n k) > ↑k * Real.log ↑k ^ (2 + c)) {a : ℕ → ℂ} (hfn : ∀ (z : ℂ), HasSum (fun (k : ℕ) => a k * z ^ n k) (f z)) : Filter.limsup (fun (r : ℝ) => ratio r f) Filter.atTop = 1

Let f = ∑ aₖzⁿₖ be an entire function such that nₖ > k (log k) ^ (2 + c). Then limsup (fun r => ratio r f) atTop = 1. This is proved in [Ko65].

theorem Erdos516.erdos_516.limsup_ratio_eq_one_of_hasFejerGaps : sorry ↔ ∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFejerGaps n → ∀ {a : ℕ → ℂ}, (∀ (z : ℂ), HasSum (fun (k : ℕ) => a k * z ^ n k) (f z)) → Filter.limsup (fun (r : ℝ) => ratio r f) Filter.atTop = 1

Is it true that for all entire functions f = ∑ aₖzⁿₖ such that ∑' 1 / nₖ < ∞, limsup (fun r => ratio r f) atTop = 1?