proposition: Lemma bernp_free : forall (l : nat -> R), \sum_(i < deg.+1) l i *: bernp a b deg i = 0 -> forall i : 'I_deg.+1, l i = 0.
proof: Proof. have bman0 : b - a != 0 by rewrite subr_eq0 eq_sym. move/(expf_neq0 deg): (bman0) => bmadeg. move=> l; rewrite -[X in X = 0]scale1r -(mulVf bmadeg) -scalerA. rewrite -relocateK; last first. apply (leq_trans (size_sum _ _ _)); apply/bigmax_leqP. move=> i _; apply: (leq_trans (size_scale_leq _ _)). by rewrite size_bernp ?leqnn //; case : i => i /=; rewrite ltnS. move/eqP; rewrite scaler_eq0 invr_eq0 (negbTE bmadeg) orFb. have t : forall i : 'I_deg.+1, (size (bernp a b deg i) <= deg.+1)%N. by move=> [i ci] /=; rewrite size_bernp. rewrite (Mobius_weighted_sum l t) {t}. have xdi : forall i, (i < deg.+1)%N -> size (('X : {poly R}) ^+i) = i.+1. by move=> i; rewrite -['X]subr0 size_exp_XsubC. have t: forall i : nat, (i < deg.+1)%N -> Mobius deg a b (bernp a b deg i) = ('C(deg, i)%:R)%:P * 'X ^+ (deg - i). move=> i ci. rewrite (_ : bernp a b deg i = ('C(deg, i)%:R / (b - a)^+ deg)%:P * (((b - a) ^+ deg / 'C(deg, deg - i)%:R)%:P * bernp a b deg (deg - (deg - i)))); last first. rewrite mulrA -polyCM !mulrA mulfVK //. rewrite bin_sub // mulfV ?mul1r ?subKn // pnatr_eq0. by rewrite -lt0n bin_gt0. have di : (deg - i <= deg)%N by rewrite leq_subr. rewrite -bern_coeffs_mon // !mul_polyC MobiusZ; last first. rewrite /relocate /shift_poly /scaleX_poly xdi; last by rewrite ltnS. rewrite ltnNge ltnS di /=. rewrite size_comp_poly2; last by rewrite size_XaddC. rewrite size_recip // !size_comp_poly2 ?xdi ?ltnS //. by rewrite size_XaddC. by rewrite size_XmulC. by rewrite MobiusK ?xdi ?ltnS // -!mul_polyC mulrA -polyCM mulfVK. rewrite relocate0; last first. have T : forall i : 'I_deg.+1, (size (Mobius deg a b (bernp a b deg i)) <= deg.+1)%N. move=> [i ci]; rewrite t //. rewrite size_Cmul; last by rewrite pnatr_eq0 -lt0n bin_gt0. by rewrite xdi; rewrite ltnS leq_subr. apply: size_weighted_sum_leq => i _; apply: T. rewrite -(big_mkord (fun _ => true) (fun i => l i *: Mobius deg a b (bernp a b deg i))) big_nat_rev /= add0n. have t' : forall i, (0 <= i < deg.+1)%N -> l (deg.+1 - i.+1)%N *: Mobius deg a b (bernp a b deg (deg.+1 - i.+1)) = (l (deg - i)%N * ('C(deg, deg - i))%:R) *: 'X^i. move=> i;case/andP=> _ ci. rewrite subSS t; last by rewrite ltnS leq_subr. by rewrite -!mul_polyC mulrA polyCM subKn. rewrite (eq_big_nat _ _ t') big_mkord => t2. have t3 := (@monomial_free _ (fun i => l (deg - i)%N * ('C(deg, deg - i))%:R) t2). move=> [i ci] /=. have t4 : ('C(deg, i))%:R != 0 :> R. by rewrite pnatr_eq0 -lt0n bin_gt0. apply: (mulIf t4); rewrite mul0r. have t5: (i <= deg)%N by rewrite -ltnS. rewrite -(subKn t5); apply: t3. by rewrite ltnS leq_subr. 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