Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.

Spectral estimates from power sums

Bounds spectral roots through Newton identities and Cauchy’s root bound, following Harcos (2015), §3 and equations (2)–(3).

theorem KloostermanWeil.Stepanov.aeval_psum_complex {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (k : ℕ) : (MvPolynomial.aeval z) (MvPolynomial.psum ι ℂ k) = ∑ i : ι, z i ^ k

theorem KloostermanWeil.Stepanov.evaluated_newton_identity {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (k : ℕ) : ↑k * (Multiset.map z Finset.univ.val).esymm k = (-1) ^ (k + 1) * ∑ a ∈ Finset.antidiagonal k with a.1 < k, (-1) ^ a.1 * (Multiset.map z Finset.univ.val).esymm a.1 * ∑ i : ι, z i ^ a.2

theorem KloostermanWeil.Stepanov.card_newton_antidiagonal (k : ℕ) : {a ∈ Finset.antidiagonal k | a.1 < k}.card = k

theorem KloostermanWeil.Stepanov.norm_esymm_power_le {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (C : ℝ) (hC : 1 ≤ C) (hpower : ∀ (n : ℕ), 0 < n → ‖∑ i : ι, z i ^ n‖ ≤ C) (N k : ℕ) (hN : 0 < N) : ‖(Multiset.map (fun (i : ι) => z i ^ N) Finset.univ.val).esymm k‖ ≤ C ^ k

Newton's identities bound every elementary symmetric function of the powered family uniformly in the outer power.

theorem KloostermanWeil.Stepanov.norm_le_one_of_power_sums_bounded {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (C : ℝ) (hC : 1 ≤ C) (hpower : ∀ (n : ℕ), 0 < n → ‖∑ i : ι, z i ^ n‖ ≤ C) (i : ι) : ‖z i‖ ≤ 1

A finite complex family with uniformly bounded positive power sums lies in the closed unit disk.

theorem KloostermanWeil.Stepanov.norm_le_one_of_power_sums_eventually {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (C : ℝ) (hC : 1 ≤ C) (n₀ : ℕ) (hpower : ∀ (n : ℕ), n₀ ≤ n → ‖∑ i : ι, z i ^ n‖ ≤ C) (i : ι) : ‖z i‖ ≤ 1

It is enough that the power-sum bound hold from one exponent onward.

theorem KloostermanWeil.Stepanov.norm_le_radius_of_power_sums_eventually {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (r C : ℝ) (hr : 0 < r) (hC : 1 ≤ C) (n₀ : ℕ) (hpower : ∀ (n : ℕ), n₀ ≤ n → ‖∑ i : ι, z i ^ n‖ ≤ C * r ^ n) (i : ι) : ‖z i‖ ≤ r

Radius-scaled version of the eventual finite power-sum criterion.