A normalized finite-sum root estimate

Abstract

Nonnegative finite inverse-power sums control the norm of a complex root by its argument.

Theorem 1.1 (The argument-dependent estimate).

$$\forall (J:\mathrm{Type})[Fintype\left(J\right)],\forall a\in J\to \mathrm{Real},\forall k\in J\to \mathrm{Nat},\forall a0\in \mathrm{Real},\forall z\in \mathrm{Complex},\left(\forall i\in J,0\le a\left(i\right)\right)\Rightarrow \left(0<a0\Rightarrow \left(1<\Vert z\Vert \Rightarrow \left((a0:\mathrm{Complex})+\sum _{(i:J)}(a\left(i\right):\mathrm{Complex})\cdot (z^{-1}{)}^{k\left(i\right)}=0\Rightarrow \Vert z\Vert \le (\frac{{\sum }_{(i:J)}a\left(i\right)}{a0}{)}^{\frac{|\mathrm{Complex}.\arg \left(z\right)|}{\mathrm{Real}.\mathrm{pi}}}\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/DegreeRoots/EscapeWitness.normalized_escape_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a be nonnegative real weights on a finite type, k natural exponents, and a0 a positive real constant. If a0 plus the weighted inverse powers of z vanishes and the norm of z exceeds one, then its norm is at most the ratio of total weight to a0, raised to |Complex.arg z|/Real.pi. For positive argument, put lam=Real.log ‖z‖/Complex.arg z and take the real part after multiplication by 1+lam·Complex.I. The estimate Real.exp(−lam·t)(Real.cos t+lam·Real.sin t)≥−Real.exp(−lam·Real.pi) for lam>0 and t≥0 bounds each summand. Complex conjugation handles negative argument; a positive constant and nonnegative weights exclude argument zero.

References

• Truth anchor: D5/S3/Zeros/DegreeRoots/EscapeWitness.normalized_escape_bound