Zeros of the entire function 1 + Σ (z/n)ⁿ

DefinitionThe entire function \(1+\sum_{n\ge 1}(z/n)^n\)#✓fully proved

This is the function \(F:\mathbb{C}\to\mathbb{C}\) given by

\[F(z)=1+\sum_{n=1}^{\infty}\left(\frac{z}{n}\right)^{n}.\]

noncomputable def F : ℂ → ℂ :=
  fun z => 1 + ∑' n : ℕ, (z / (n + 1 : ℂ)) ^ (n + 1)

Used by 1

Used byZeros of \(1+\sum_{n\ge 1}(z/n)^n\) in a disc

TheoremZeros of \(1+\sum_{n\ge 1}(z/n)^n\) in a disc#●ready to prove

Let \(F\) be the entire function

\[F(z)=1+\sum_{n=1}^{\infty}\left(\frac{z}{n}\right)^{n}.\]

For every real \(R>0\), \(F\) has only finitely many zeros in the open disc \(\{z\in\mathbb{C} : |z|\lt R\}\), and the number of these zeros counted with multiplicity is at most \(4R\).

public theorem_wanted exists_finset_zeros_sum_analyticOrderNatAt_le
  (R : ℝ)
  (hR : 0 < R) :
  ∃ s : Finset ℂ,
    (∀ z : ℂ, z ∈ s ↔ ‖z‖ < R ∧ F z = 0) ∧
    ((∑ z ∈ s, analyticOrderNatAt F z) : ℝ) ≤ 4 * R

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Entire and meromorphic functions of one complex variable, and related topics), problem ma_proofbench_l2_91.

Uses 1

Statement usesThe entire function \(1+\sum_{n\ge 1}(z/n)^n\)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.