Erdős problem 517
If f(z) = ∑ aₖzⁿₖ is an entire function (with aₖ ≠ 0 for all k) such that nₖ / k → ∞, is it true that f assumes every value infinitely often?
Sources
FormalConjectures/ErdosProblems/
517.lean
Retained formal statement
If f(z) = ∑ aₖzⁿₖ is an entire function (with aₖ ≠ 0 for all k) such that ∑ 1 / nₖ < ∞, then f assumes every value infinitely often. This theorem is proved in [Bi28].
∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFejerGaps n → ∀ {a : ℕ → ℂ}, (∀ (k : ℕ), a k ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → ∀ (z : ℂ), {x | f x = z}.InfiniteSolvedStatement only, no proof