proposition: Lemma relocate_weighted_sum n (f : nat -> R) (g : nat -> {poly R}) : (forall i : 'I_n, (size (g i) <= deg.+1)%N) -> relocate (\sum_(i < n) f i *: g i) = \sum_(i < n) f i *: relocate (g i).
proof: Proof. rewrite /relocate /shift_poly /scaleX_poly linear_sum /= => cg. have s : (size (\sum_(i < n) (f i *: g i))%R <= deg.+1)%N. apply: (leq_trans (size_sum _ _ _)). by apply/bigmax_leqP => i _; apply/(leq_trans (size_scale_leq _ _))/cg. rewrite ltnNge s linear_sum /=. have s' : forall i : 'I_n, (size (f i *: g i \Po ('X + (-1)%:P) \Po ('X * (b - a)%:P))%R <= deg.+1)%N. move=> i; rewrite !size_comp_poly2. by apply/(leq_trans (size_scale_leq _ _))/cg. by apply: size_XaddC. by apply: size_XmulC; rewrite subr_eq0 eq_sym. rewrite (@recip_sum _ (fun i => (f i *: g i \shift -1) \scale (b - a)) s'). rewrite linear_sum. apply: eq_bigr => i _ /=. rewrite ltnNge cg /=. rewrite /shift_poly /scaleX_poly !linearZ recipZ ?linearZ //=. rewrite !size_comp_poly2 //; first by apply: size_XaddC. by apply: size_XmulC; rewrite subr_eq0 eq_sym. 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