Liouville-type theorems

TheoremBounded holomorphic functions on the punctured plane are constant#●ready to prove

Let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on \(\mathbb{C} \setminus \{0\}\), and suppose that there is a real number \(C\) with \(|f(z)| \le C\) for every \(z \ne 0\). Then there is a constant \(c \in \mathbb{C}\) with \(f(z) = c\) for every \(z \ne 0\).

public theorem_wanted eqOn_const_of_differentiableOn_compl_zero_of_bounded
    (f : ℂ → ℂ) (hHol : DifferentiableOn ℂ f ({0}ᶜ))
    (hBdd : ∃ C : ℝ, ∀ z : ℂ, z ≠ 0 → ‖f z‖ ≤ C) :
    ∃ c : ℂ, Set.EqOn f (fun _ => c) ({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_84.

TheoremAn entire function with a polynomial derivative is a polynomial#●ready to prove

Let \(k\) be a positive integer and let \(f : \mathbb{C} \to \mathbb{C}\) be an entire function. If there is a complex polynomial \(p\) such that the \(k\)th derivative of \(f\) satisfies \(f^{(k)}(z) = p(z)\) for all \(z \in \mathbb{C}\), then there is a complex polynomial \(q\) such that \(f(z) = q(z)\) for all \(z \in \mathbb{C}\).

public theorem_wanted exists_polynomial_of_iteratedDeriv_eq_polynomial
    {k : ℕ} (hk : 0 < k) {f : ℂ → ℂ}
    (hf : Differentiable ℂ f)
    (hpoly : ∃ p : Polynomial ℂ, iteratedDeriv k f = fun z => p.eval z) :
    ∃ q : Polynomial ℂ, f = fun z => q.eval z
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_90.

TheoremAn entire function of sublinear growth is constant#●ready to prove

Let \(f : \mathbb{C} \to \mathbb{C}\) be an entire function such that \(f(z)/z \to 0\) as \(|z| \to \infty\). Then \(f\) is constant: there is \(c \in \mathbb{C}\) with \(f(z) = c\) for all \(z \in \mathbb{C}\).

public theorem_wanted exists_const_of_differentiable_of_tendsto_div_self_zero
    {f : ℂ → ℂ} (hf : Differentiable ℂ f)
  (hlim : Tendsto (fun z : ℂ => f z / z) (comap (fun z : ℂ => ‖z‖) atTop) (𝓝 (0 : ℂ))) :
  ∃ c : ℂ, ∀ z : ℂ, f z = c
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_28.
3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.