proposition: Theorem summation_split_val : ∀ f L γ₁ c₁ pl tl l, newton_segments f = Some L → pl = [ini_pt L … oth_pts L ++ [fin_pt L]] → tl = List.map (term_of_point f) pl → l = List.map (λ t, power t) tl → (ps_pol_summ ps_field l (λ h, let āh := ps_poly_nth h f in POL [(āh * ps_monom 1%K (Qnat h * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h) = ps_pol_summ ps_field l (λ h, let ah := ps_monom (coeff_of_term h tl) 0 in let αh := ord_of_pt h pl in POL [(ah * ps_monom 1%K (αh + Qnat h * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h) + ps_pol_summ ps_field l (λ h, let āh := ps_poly_nth h f in let ah := ps_monom (coeff_of_term h tl) 0 in let αh := ord_of_pt h pl in POL [((āh - ah * ps_monom 1%K αh) * ps_monom 1%K (Qnat h * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h))%pspol.
proof: Proof. intros f L γ₁ c₁ pl tl l HL Hpl Htl Hl. progress unfold ps_pol_add, ps_pol_summ. rewrite poly_summation_add; simpl. apply lap_eq_list_fold_right; intros i a b Hi Heq. apply lap_add_compat; [ assumption | simpl ]. rewrite <- lap_mul_add_distr_r; simpl. apply lap_mul_compat; [ idtac | reflexivity ]. constructor; [ simpl | reflexivity ]. rewrite ps_monom_add_r. rewrite rng_mul_assoc. rewrite rng_mul_add_distr_r. simpl. rewrite rng_mul_opp_l; simpl. rewrite rng_add_assoc; simpl. rewrite rng_add_comm; simpl. rewrite rng_add_assoc; simpl. rewrite rng_add_opp_l, rng_add_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol