Erdős Problem 517

References:

• erdosproblems.com/517
• [Bi28] Biernacki, Miécislas, Sur les équations algébriques contenant des paramétres arbitraires. (1928), 145.

theorem Erdos517.erdos_517.fabry : sorry ↔ ∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (z : ℂ), HasSum (fun (k : ℕ) => a k * z ^ n k) (f z)) → ∀ (z : ℂ), {x : ℂ | f x = z}.Infinite

If f(z) = ∑ aₖzⁿₖ is an entire function such that nₖ / k → ∞, is it true that f assumes every value infinitely often?

theorem Erdos517.erdos_517.fejer {f : ℂ → ℂ} {n : ℕ → ℕ} (hn : HasFejerGaps n) {a : ℕ → ℂ} (hf : ∀ (z : ℂ), HasSum (fun (k : ℕ) => a k * z ^ n k) (f z)) (z : ℂ) : {x : ℂ | f x = z}.Infinite

If f(z) = ∑ aₖzⁿₖ is an entire function such that ∑ 1 / nₖ < ∞, then f assumes every value infinitely often. This theorem is proved in [Bi28].