A root bound in monic coefficient coordinates #
A root of TauCeti.Polynomial.monicOfCoeff c has norm strictly less than
‖c‖ + 1. Thus locally bounded coefficient tuples give locally bounded roots,
without choosing or continuously labelling them. This is the bound used to remove
singularities of analytic root branches.
The estimate specializes Mathlib's Polynomial.IsRoot.norm_lt_cauchyBound
(Daniel Weber's formalization of Cauchy's root bound) to the finite coefficient tuple.
theorem
TauCeti.Polynomial.norm_lt_of_isRoot_monicOfCoeff
{K : Type u_1}
[NormedField K]
{d : ℕ}
(c : Fin d → K)
{z : K}
(hz : (monicOfCoeff c).IsRoot z)
:
Every root of the monic polynomial with lower coefficients c has norm
strictly less than ‖c‖ + 1.
theorem
TauCeti.Polynomial.continuousOn_eval_monicOfCoeff
{R : Type u_1}
{B : Type u_2}
[CommSemiring R]
[TopologicalSpace R]
[IsTopologicalSemiring R]
[TopologicalSpace B]
{d : ℕ}
(c : B → Fin d → R)
{r : B → R}
{t : Set B}
(hc : ContinuousOn c t)
(hr : ContinuousOn r t)
:
ContinuousOn (fun (x : B) => Polynomial.eval (r x) (monicOfCoeff (c x))) t
Evaluating a monic coefficient family at a continuous function is continuous.