Entire and meromorphic functions

Growth and value distribution of entire and meromorphic functions: Wiman–Valiron theory and maximum term, Hayman admissibility, Weierstrass factorization, Mittag-Leffler, Liouville-type rigidity, preimages and zeros/ones on lines.

• Countable dense sets as preimages under entire functions
• Hayman admissibility
• Liouville-type theorems
• Mittag-Leffler theorem
• Rényi–Vincze characterization of the exponential
• Spherical area and valence of meromorphic functions
• Turán's three-value problem
• Wiman–Valiron theory
• Growth of entire functions along continua
• Zeros and ones of entire functions on lines
• Zeros of the entire function 1 + Σ (z/n)ⁿ

TheoremA \(1\)-periodic entire function bounded by \(C e^{|\operatorname{Im} s|}\) is constant#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) be entire with \(f(s + 1) = f(s)\) for all \(s \in \mathbb{C}\), and suppose there is a real constant \(C\) such that \(|f(s)| \le C e^{|\operatorname{Im} s|}\) for every \(s\) with \(0 \le \operatorname{Re} s \le 1\). Then \(f\) is constant.

The two-sided bound cannot be weakened to the one-sided \(|f(s)| = O(e^{\operatorname{Im} s})\) as \(\operatorname{Im} s \to \infty\): the function \(f(s) = e^{2 \pi i s}\) is entire and \(1\)-periodic, satisfies \(|f(s)| = e^{-2 \pi \operatorname{Im} s} \le e^{\operatorname{Im} s}\) for \(\operatorname{Im} s \ge 0\), and is not constant.

theorem eq_const_of_periodic_one_of_norm_le_exp_abs_im
    (f : ℂ → ℂ)
    (hf_diff : Differentiable ℂ f)
    (hf_per : Periodic f (1 : ℂ))
    (hf_growth : ∃ C : ℝ, ∀ s : ℂ, 0 ≤ s.re → s.re ≤ 1 →
      ‖f s‖ ≤ C * Real.exp |s.im|) :
    ∃ c : ℂ, f = Function.const ℂ c

Sources

• ATLAS NumberTheoryI, Lemma 17.14, corrected; the book prints the one-sided bound, under which the lemma is false.

TheoremA nonzero entire power series with infinitely many zeros#●ready to prove

There is a sequence \((a_k)_{k \ge 0}\) of complex numbers, not all zero, such that the power series \(\sum_{k=0}^{\infty} a_k z^k\) converges absolutely for every \(z \in \mathbb{C}\) and its sum vanishes at infinitely many points \(z \in \mathbb{C}\).

public theorem_wanted exists_entire_powerSeries_infinite_zeros : ∃ a : ℕ → ℂ,
      (∀ z : ℂ, Summable (fun k : ℕ => a k * z ^ k)) ∧
      Set.Infinite {z : ℂ | (∑' k : ℕ, a k * z ^ k) = 0} ∧
      (∃ k : ℕ, a k ≠ 0)

Sources

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

TheoremEntire solutions of the Fermat cubic are constant#●ready to prove

Let \(f\) and \(g\) be entire functions with \(f(z)^3 + g(z)^3 = 1\) for every \(z \in \mathbb{C}\). Then \(f\) and \(g\) are constant.

public theorem_wanted entire_cube_add_cube_eq_one_const
    (f g : ℂ → ℂ)
    (hf_entire : Differentiable ℂ f)
    (hg_entire : Differentiable ℂ g)
    (hfg : ∀ z : ℂ, f z ^ (3 : ℕ) + g z ^ (3 : ℕ) = 1) :
    ∃ a b : ℂ, (∀ z : ℂ, f z = a) ∧ (∀ z : ℂ, g z = b)

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_61.

TheoremInjective entire functions are affine#●ready to prove

If \(f : \mathbb{C} \to \mathbb{C}\) is entire and injective, then there are \(a, b \in \mathbb{C}\) with \(a \ne 0\) such that \(f(z) = az + b\) for all \(z \in \mathbb{C}\).

public theorem_wanted exists_affine_of_differentiable_injective
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (hinj : Function.Injective f) :
    ∃ a b : ℂ, a ≠ 0 ∧ ∀ z : ℂ, f z = a * z + b

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l1_37.

TheoremWeierstrass theorem on prescribed simple zeros#✓fully proved

Let \(S \subseteq \mathbb{C}\) be a closed set all of whose points are isolated: for each \(z \in S\) there is \(\varepsilon > 0\) such that no point \(w \ne z\) of \(S\) satisfies \(|w - z| < \varepsilon\). Then there is an entire function \(f\) whose zeros are exactly the points of \(S\), all of them simple: \(f'(z) \ne 0\) for every \(z \in S\).

theorem weierstrass_factorization
    (S : Set ℂ) (hS_closed : IsClosed S)
    (hS_discrete : ∀ z ∈ S, ∃ ε > 0, (Metric.ball z ε \ {z}) ∩ S = ∅) :
    ∃ f : ℂ → ℂ, Differentiable ℂ f ∧
      (∀ z : ℂ, f z = 0 ↔ z ∈ S) ∧
      (∀ z ∈ S, deriv f z ≠ 0)

Sources

• Weierstrass factorization theorem 1876; see Rudin; Lean is simple-zero corollary with closed discrete prescribed zero set S and entire f with exact zeros S and nonvanishing derivative on S.

2 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.