proposition: Lemma CauchyBound x: (\poly_(i < n.+1) E i).[x] = 0 -> `| x | <= `|E n|^-1 * \sum_(i < n.+1) `|E i|.
proof: Proof. move=> px0; case: (lerP `|x| 1)=> cx1. set C := _ * _; suff leC1 : 1 <= C by apply: le_trans leC1. have h1 : `|E n| > 0 by rewrite normr_gt0. rewrite -(ler_pmul2l h1) /= mulr1 /C mulrA mulfV ?normr_eq0 // mul1r. by rewrite big_ord_recr /= -{1}(add0r `|E n|) ler_add2r sumr_ge0. case e: n=> [| m]. move: pnz; rewrite -px0 e horner_poly big_ord_recl big_ord0 /=. by rewrite addr0 expr0 mulr1 /= eqxx. have h1 : E m.+1 * x^+m.+1 = - \sum_(i < m.+1) E i * x^+ i. apply/eqP; rewrite -subr_eq0 opprK -{2}px0 horner_poly (big_ord_recr n). by rewrite e //= addrC. case x0 : (x == 0). by rewrite (eqP x0) normr0 mulr_ge0 ?sumr_ge0// invr_gte0. have {h1} h2 : E m.+1 * x = - \sum_(i < m.+1) E i * x^-(m - i). have xmn0 : ~~ (x^+m == 0) by rewrite expf_eq0 x0 andbF. apply: (mulIf xmn0); rewrite mulNr big_distrl /= -mulrA -exprS h1. congr (- _); apply: congr_big; [by [] | by [] |] => [[i hi]] _ /=. have mi : m = (m - i + i)%N by rewrite subnK. rewrite {2}mi exprD -!mulrA; congr (_ * _); rewrite mulrA mulVf ?mul1r //. by rewrite expf_eq0 x0 andbF. have h3 : `|\sum_(i < m.+1) E i / x ^+ (m - i) | <= \sum_(i < m.+2) `|E i|. apply: le_trans (normr_sum m.+1 (fun i => E i / x ^+ (m - i))) _. apply: (@le_trans _ _ (\sum_(i < m.+1) `|E i|)); last first. by rewrite (big_ord_recr m.+1) /= ler_addl /= normr_ge0. suff h: forall i, (i < m.+1)%N -> `|E i/x^+(m-i)| <= `|E i|. by apply: ler_sum => //= i _; exact: h. move=> i lti; rewrite normrM -{2}(mulr1 (`|E i|)) ler_wpmul2l ?normr_ge0 //. rewrite normfV normrX invf_le1; first by rewrite exprn_cp1 // ltW. by rewrite exprn_gt0 // (lt_trans ltr01). rewrite lter_pdivl_mull; last by rewrite normr_gt0 -e. by apply: le_trans h3=> /=; rewrite -normrM h2 normrN lexx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc