proposition: Lemma bound_poly_boundP (z : creal) i (q : {poly {poly F}}) (a r : F) j : poly_bound q.[(z i)%:P]^`N(j.+1) a r <= bound_poly_bound z q a r j.
proof: Proof. rewrite /poly_bound. pose f (q : {poly F}) (k : nat) := `|q^`N(j.+1)`_k| * (`|a| + `|r|) ^+ k. rewrite ler_add //=. rewrite (big_ord_widen (sizeY q) (f q.[(z i)%:P])); last first. rewrite size_nderivn leq_subLR (leq_trans (max_size_evalC _ _)) //. by rewrite leq_addl. rewrite big_mkcond /= ler_sum // /f => k _. case: ifP=> _; last by rewrite mulr_ge0 ?exprn_ge0 ?addr_ge0 ?normr_ge0. rewrite ler_wpmul2r ?exprn_ge0 ?addr_ge0 ?normr_ge0 //. rewrite !horner_coef. rewrite !(@big_morph _ _ (fun p => p^`N(j.+1)) 0 +%R); do ?[by rewrite raddf0|by move=> x y /=; rewrite raddfD]. rewrite !coef_sum. rewrite (le_trans (ler_norm_sum _ _ _)) //. rewrite ger0_norm; last first. rewrite sumr_ge0=> //= l _. rewrite coef_nderivn mulrn_wge0 ?natr_ge0 //. rewrite -polyC_exp coefMC coef_norm_poly2 mulr_ge0 ?normr_ge0 //. by rewrite exprn_ge0 ?ltW ?ubound_gt0. rewrite size_norm_poly2 ler_sum //= => l _. rewrite !{1}coef_nderivn normrMn ler_pmuln2r ?bin_gt0 ?leq_addr //. rewrite -!polyC_exp !coefMC coef_norm_poly2 normrM ler_wpmul2l ?normr_ge0 //. rewrite normrX; case: (val l)=> // {}l. by rewrite ler_pexpn2r -?topredE //= ?uboundP ?ltW ?ubound_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)