Polynomials in the complex plane

Analytic behaviour of complex polynomials: location of zeros (Eneström–Kakeya, Sendov's problem, Jentzsch), flat and Littlewood polynomials, complementary polynomials and sup norms on the unit circle. Algebraic properties of polynomials go to Algebra; Mahler measure goes to NumberTheory.

TheoremComplementary polynomial on the unit circle#●ready to prove

Let \(P\) be a complex polynomial with \(|P(z)| \le 1\) for every complex number \(z\) with \(|z| = 1\). Then there is a complex polynomial \(Q\) with \(\deg Q \le \deg P\) such that \(|P(z)|^2 + |Q(z)|^2 = 1\) for every \(z\) with \(|z| = 1\). Here the degree of the zero polynomial is taken to be \(0\).

public theorem_wanted exists_complementary_polynomial_on_unit_circle
    (P : ℂ[X])
    (hP : ∀ z : Circle, ‖P.eval (z : ℂ)‖ ≤ 1) :
    ∃ Q : ℂ[X],
      Q.natDegree ≤ P.natDegree ∧
        ∀ z : Circle, ‖P.eval (z : ℂ)‖ ^ 2 + ‖Q.eval (z : ℂ)‖ ^ 2 = 1
Sources
  • https://link.springer.com/article/10.1007/s00220-025-05302-9. Problem exists_complementary_polynomial_on_unit_circle of the lean-eval benchmark.

TheoremEneström–Kakeya theorem#✓fully proved

Let \(n \ge 1\) and let \(a_0, a_1, \dots, a_n\) be positive real numbers. Then every complex zero \(z\) of the polynomial \(f(z) = a_0 + a_1 z + \dots + a_n z^n\) satisfies \(\rho_1 \le |z| \le \rho_2\), where \(\rho_1\) and \(\rho_2\) are the minimum and the maximum of the ratios \(a_k / a_{k+1}\) for \(0 \le k \le n - 1\).

theorem enestrom_kakeya_zero_localization
    {n : ℕ} (hn : 1 ≤ n) (a : Fin (n + 1) → ℝ) (hpos : ∀ k, 0 < a k) :
    ∀ z : ℂ,
      (∑ k : Fin (n + 1),
        Polynomial.C ((a k : ℝ) : ℂ) * Polynomial.X ^ (k : ℕ)).IsRoot z →
        (Finset.image (fun k : Fin n => a k.castSucc / a k.succ) Finset.univ).min'
          ⟨_, Finset.mem_image_of_mem _ (Finset.mem_univ ⟨0, by omega⟩)⟩ ≤ ‖z‖ ∧
        ‖z‖ ≤ (Finset.image (fun k : Fin n => a k.castSucc / a k.succ)
          Finset.univ).max'
          ⟨_, Finset.mem_image_of_mem _ (Finset.mem_univ ⟨0, by omega⟩)⟩
Sources

TheoremJentzsch's theorem#✓fully proved

Let \((a_k)_{k \ge 0}\) be complex numbers such that the power series \(\sum_{k \ge 0} a_k z^k\) has radius of convergence \(1\), and for \(n \ge 0\) let \(s_n(z) = \sum_{k=0}^{n} a_k z^k\) be its \(n\)-th partial sum. Then for every complex \(z\) with \(|z| = 1\), every real \(\varepsilon > 0\) and every natural number \(N\), there are \(n \ge N\) and a root \(w\) of the polynomial \(s_n\) with \(|w - z| < \varepsilon\).

Source: Dilcher and Ericksen, "Polynomials Whose Coefficients Are Stern Numbers", Theorem 4.3 (Jentzsch), https://cs.uwaterloo.ca/journals/JIS/VOL24/Dilcher/dilcher51.tex, lines 381-388.

theorem jentzsch_zeros_of_power_series_sections (a : Nat -> Complex)
    (hradius : (FormalMultilinearSeries.ofScalars Complex a).radius = 1) :
    ∀ (z : Complex), ‖z‖ = 1 → ∀ (epsilon : Real), 0 < epsilon → ∀ (N : Nat),
      ∃ (n : Nat), N ≤ n ∧ ∃ (w : Complex),
        (PowerSeries.trunc (n + 1) (PowerSeries.mk a)).IsRoot w ∧ dist w z < epsilon
Uses 3
Proof usesLocally uniformly bounded sequence of functions · A uniformly bounded sequence on an open set is locally uniformly bounded · Montel's theorem
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.