proposition: Lemma ch1_correct l d a b (q : {poly R}): (size l <= d.+1)%N -> a < b -> q = \sum_(i < d.+1) l`_i *: bernp a b d i -> changes (seqn0 l) = 1%N -> unique_root_for (horner q) a b.
proof: Proof. wlog : l q / (0 <= (seqn0 l)`_0). move=> main s ab qq c1. case sg : (0 <= (seqn0 l)`_0). apply: (main l q sg) => //. have ur : unique_root_for (horner (-q)) a b. apply: (main (map (fun x => -x) l) (-q)) => //. rewrite seqn0_oppr (nth_map 0). by rewrite ler_oppr oppr0 ltW // ltNge sg. rewrite lt0n; apply/negP; move/eqP=>abs; move: sg. by rewrite nth_default ?abs ?lexx. by rewrite size_map. rewrite -(mul1r q) -mulNr qq big_distrr; apply/eq_bigr. move=> i _ /=; case ci : (i < size l)%N. by rewrite (nth_map 0) // mulNr mul1r scaleNr. move/negbT: ci; rewrite -leqNgt => ci. rewrite !nth_default //; last by rewrite size_map. by rewrite !scale0r mulr0. by rewrite seqn0_oppr changes_oppr. case: ur => [x [inx xr xu]]. exists x; split; first by []. by apply/eqP; rewrite -oppr_eq0 -hornerN; apply/eqP. by move=> u inu /eqP; rewrite -oppr_eq0 -hornerN => /eqP; apply:xu. move=> sg s ab qq c1. suff : one_root1 q a b by apply: one_root1_unique. apply: (@Bernstein_isolate _ d) => //. rewrite lt0n size_poly_eq0; apply/negP => /eqP => abs. move/eqP: qq; rewrite abs eq_sym=> /eqP. move: (ab); rewrite lt_def eq_sym; case/andP => ab' _ sb. have := bernp_free ab' sb => bf {ab' sb abs sg}. have abs : (seqn0 l) = [::]. move: l s bf {a b q ab c1}. elim: d => [ | d IH]. move=> [ | a l]; first by []. case: l => /=; last by []. by move=> _ l0; have := (l0 ord0) => /= => ->; rewrite eqxx /=. move=> [ | a l] /=; first by []. rewrite ltnS=> s l0; have := (l0 ord0) => /= => ->; rewrite eqxx /=. apply: IH => //; move=> [i] /=; rewrite -ltnS => ci. by have := (l0 (Ordinal ci)). by move: c1; rewrite abs. rewrite qq; apply: size_weighted_sum_leq. move=> [i ci]; rewrite size_bernp ?leqnn //. by move: ab; rewrite lt_def eq_sym; case/andP. have anb : a != b. by move: ab; rewrite lt_def eq_sym; case/andP. rewrite qq Mobius_weighted_sum //; last by move=> [i ci]; rewrite size_bernp. have t : forall i : 'I_d.+1, true -> l`_i *: Mobius d a b (bernp a b d i) = (l`_i * ('C(d, i))%:R) *: 'X ^+ (d - i). by move=> [i ci]; rewrite Mobius_bernp //= scalerA. rewrite (eq_bigr _ t) {t}. have binp : forall i, (i < d.+1)%N -> (0:R) < ('C(d, i))%:R. by move => i ci; rewrite ltr0n bin_gt0 -ltnS. apply: (changes1_alternate s binp) => //. 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