proposition: Lemma TM_mul_correct (x0 : R) (X0 X : I.type) (TMf TMg : rpa) f g n : contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) TMf f -> i_validTM x0 (I.convert X) TMg g -> i_validTM x0 (I.convert X) (TM_mul TMf TMg X0 X n) (fun xr => Xmul (f xr) (g xr)).
proof: Proof. move=> Hx0 [Fdef Fnai Fzero HinX Fmain] [Gdef Gnai Gzero _ Gmain]. split =>//. - move=> x Hx Dx. rewrite /= /mul_error. do 3![rewrite I.add_propagate_r //]. case Ef: (f x) => [|fx]. rewrite I.mul_propagate_l //; exact: Fdef Ef. case Eg: (g x) => [|gx //]. rewrite I.mul_propagate_r //; exact: Gdef Eg. by rewrite Ef Eg in Dx. - move=> HX; rewrite /TM_mul /= /mul_error. rewrite I.add_propagate_r // I.add_propagate_r // I.add_propagate_r //. by rewrite I.mul_propagate_l // Fnai. - have [qf Hf1 Hf2] := Fmain. have [qg Hg1 Hg2] := Gmain. step_xr (Xreal 0 + Xreal 0)%XR; last by rewrite /= Rplus_0_l. apply: J.add_correct. apply: (mul_0_contains_0_r _ (y := (Xreal (PolR.mul_tail tt n qf qg).[x0 - x0]))); last first. apply: pow_contains_0 =>//. rewrite <- (Rminus_eq_0 x0). now apply J.sub_correct. apply: Bnd.ComputeBound_correct. exact: Pol.mul_tail_correct. exact: J.sub_correct. step_xr (Xreal 0 + Xreal 0)%XR; last by rewrite /= Rplus_0_l. apply: J.add_correct. apply: (mul_0_contains_0_l _ (y := (Xreal qg.[x0 - x0]))) =>//. apply: Bnd.ComputeBound_correct=>//. exact: J.sub_correct. step_xr (Xreal 0 + Xreal 0)%XR; last by rewrite /= Rplus_0_l. apply: J.add_correct. apply: (mul_0_contains_0_l _ (y := (Xreal qf.[x0 - x0]))) =>//. apply: Bnd.ComputeBound_correct=>//. exact: J.sub_correct. exact: (mul_0_contains_0_l _ (y := Xreal 0)). have [pf Hf1 Hf2] := Fmain. have [pg Hg1 Hg2] := Gmain. exists (PolR.mul_trunc tt n pf pg); first exact: Pol.mul_trunc_correct. move=> x Hx. case Dx: (Xmul (f x) (g x)) => [|mfg]. step_xi IInan =>//; rewrite /mul_error; do 3![rewrite I.add_propagate_r //]. case Ef: (f x) Dx => [|fx]. rewrite I.mul_propagate_l //; exact: Fdef Ef. case Eg: (g x) => [|gx //]. rewrite I.mul_propagate_r //; exact: Gdef Eg. move/(_ x Hx) in Hf2; move/(_ x Hx) in Hg2. step_r ((PolR.mul_tail tt n pf pg).[x - x0] * (x - x0)^n.+1 + (((proj_val (f x) - pf.[x - x0]) * pg.[x - x0] + ((proj_val (g x) - pg.[x - x0]) * pf.[x - x0] + (proj_val (f x) - pf.[x - x0]) * (proj_val (g x) - pg.[x - x0])))))%R. apply: J.add_correct. apply: J.mul_correct. apply: Bnd.ComputeBound_correct. exact: Pol.mul_tail_correct. apply: J.sub_correct =>//; exact: HinX0. rewrite pow_powerRZ; apply: J.power_int_correct. apply: J.sub_correct=>//; exact: HinX0. apply: J.add_correct. apply: J.mul_correct =>//. apply: Bnd.ComputeBound_correct =>//. by apply: J.sub_correct =>//; exact: HinX0. apply: J.add_correct. apply: J.mul_correct =>//. apply: Bnd.ComputeBound_correct =>//. by apply: J.sub_correct =>//; exact: HinX0. exact: J.mul_correct. clear - Fdef Gdef Dx Hx. have Hdfx := Fdef x Hx. have Hdgx := Gdef x Hx. set sf := pf.[x - x0]%R. set sg := pg.[x - x0]%R. rewrite !PolR.hornerE PolR.size_mul_trunc PolR.size_mul_tail. rewrite (big_endo (fun r => r * (x-x0) ^ n.+1)%R); first last. by rewrite Rmult_0_l. by move=> a b /=; rewrite Rmult_plus_distr_r. rewrite (eq_big_nat _ _ (F2 := fun i => PolR.mul_coeff tt pf pg (i + n.+1) * (x - x0) ^ (i + n.+1))%R); last first. move=> i Hi; rewrite Rmult_assoc; congr Rmult; last by rewrite pow_add. rewrite PolR.nth_mul_tail ifF; first by rewrite addnC. by case/andP: Hi; case: leqP. rewrite -(big_addn 0 _ n.+1 predT (fun i => PolR.mul_coeff tt pf pg i * (x - x0) ^ i)%R). set e := ((proj_val _ - sf) * sg + ((_ - sg) * sf + (_ - sf) * (_ - sg)))%R. rewrite Rplus_comm. have->: e = (proj_val (f x * g x)%XR - sf * sg)%R. rewrite /e. case: (f x) Dx => [|fx] //. case: (g x) => [|gx] //. intros _. rewrite /=. ring. rewrite Rplus_assoc -Dx; congr Rplus. rewrite {}/e {}/sf {}/sg. rewrite !PolR.hornerE. apply: (Rplus_eq_reg_r (proj_val (f x * g x)%XR)). congr Rplus. rewrite -!PolR.hornerE /=. rewrite -PolR.horner_mul PolR.hornerE. set bign1 := \big[Rplus/0%R]_(0 <= i < n.+1) _. apply: (Rplus_eq_reg_r bign1); rewrite Rplus_opp_l /bign1. set big := \big[Rplus/0%R]_(0 <= i < _) _. apply: (Rplus_eq_reg_l big); rewrite -!Rplus_assoc Rplus_opp_r /big Rplus_0_l. rewrite PolR.size_mul add0n Rplus_0_r. case: (ltnP n ((PolR.size pf + PolR.size pg).-1)) => Hn. rewrite [RHS](big_cat_nat _ _ (n := n.+1)) //=. rewrite Rplus_comm; congr Rplus. rewrite !big_mkord; apply: eq_bigr. move=> [i Hi] _ /=; rewrite PolR.nth_mul_trunc ifF; last by apply: negbTE; rewrite -leqNgt. rewrite PolR.nth_mul ifF //. apply: negbTE; rewrite -ltnNge; rewrite ltnS in Hi. exact: leq_ltn_trans Hi Hn. rewrite -(add0n n.+1) !big_addn !big_mkord; apply: eq_bigr. move=> [i Hi] _ /=; rewrite PolR.nth_mul ifF //. apply: negbTE; rewrite -ltnNge. by rewrite -addSn leq_addLR. rewrite -{1}(add0n n.+1) big_addn big_mkord big1; last first. move=> [i Hi] _ /=. rewrite -subn_eq0 in Hn. by rewrite -subn_gt0 subnS (eqP Hn) in Hi. rewrite Rplus_0_l. set np := (PolR.size pf + PolR.size pg).-1. rewrite [in LHS](big_cat_nat _ _ (n := np)) //=; last exact: leqW. set big0 := \big[Rplus/0%R]_(_.-1 <= i < n.+1) _. have->: big0 = 0%R. rewrite /big0. rewrite /big0 -/np -(add0n np) big_addn big_mkord. rewrite big1 // => [[i Hi] _] /=. rewrite PolR.nth_mul_trunc ifF; last first. rewrite ltn_subRL addnC in Hi. by rewrite -ltnS ltnNge Hi. rewrite PolR.mul_coeffE PolR.mul_coeff_eq0 ?Rmult_0_l //. move=> k Hk. case: (leqP (PolR.size pf) k) => Hk0. left; rewrite PolR.nth_default //. right; rewrite PolR.nth_default //. rewrite -leq_addLR //. rewrite -(ltn_add2l (PolR.size pg)) [addn (_ pg) (_ pf)]addnC in Hk0. move/ltn_leq_pred in Hk0. apply: leq_trans Hk0 _. by rewrite leq_addl. rewrite Rplus_0_r !big_mkord; apply: eq_bigr. move=> [i Hi] _ /=. rewrite PolR.nth_mul_trunc PolR.nth_mul' ifF ?PolR.mul_coeffE //. apply: negbTE; rewrite -ltnNge ltnS. exact: leq_trans (ltnW Hi) Hn. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound