fact: Definition g_lap_of_ns α {R : ring α} {K : field R} {acf : algeb_closed_field K} f L := let c₁ := ac_root (Φq f L) in let pl := [ini_pt L … oth_pts L ++ [fin_pt L]] in let tl := List.map (term_of_point f) pl in let l₁ := List.map (λ t, power t) tl in let l₂ := list_seq_except 0 (length (al f)) l₁ in ([ps_monom 1%K (- β L)] * (ps_lap_summ ps_field l₁ (λ h, let āh := ps_poly_nth h f in let ah := ps_monom (coeff_of_term R h tl) 0 in let αh := ord_of_pt h pl in [((āh - ah * ps_monom 1%K αh) * ps_monom 1%K (Qnat h * γ L))%ps] * [ps_monom c₁ 0; 1%ps … []] ^ h) + ps_lap_summ ps_field l₂ (λ l, let āl := ps_poly_nth l f in [(āl * ps_monom 1%K (Qnat l * γ L))%ps] * [ps_monom c₁ 0; 1%ps … []] ^ l)))%pslap.
imports: Utf8 QArith NPeano Sorted Misc NbarM QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHull ConvexHullMisc PolyConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq