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