proposition: Lemma integral_horner_root w (p q : {poly K}) : p \is monic -> root p w -> {in p : seq K, integralRange RtoK} -> {in q : seq K, integralRange RtoK} -> integralOver RtoK q.[w].
proof: Proof. move=> mon_p pw0 intRp intRq. pose memR y := exists x, y = RtoK x. have memRid x: memR (RtoK x) by exists x. have memR_nat n: memR n%:R by rewrite -(rmorph_nat RtoK) /=. have [memR0 memR1]: memR 0 * memR 1 := (memR_nat 0, memR_nat 1). have memRN1: memR (- 1) by exists (- 1); rewrite rmorphN1. pose rVin (E : K -> Prop) n (a : 'rV[K]_n) := forall i, E (a 0 i). pose pXin (E : K -> Prop) (r : {poly K}) := forall i, E r`_i. pose memM E n (X : 'rV_n) y := exists a, rVin E n a /\ y = (a *m X^T) 0 0. pose finM E S := exists n, exists X, forall y, memM E n X y <-> S y. have tensorM E n1 n2 X Y: finM E (memM (memM E n2 Y) n1 X). exists (n1 * n2)%N, (mxvec (X^T *m Y)) => y. split=> [[a [Ea Dy]] | [a1 [/fin_all_exists[a /all_and2[Ea Da1]] ->]]]. exists (Y *m (vec_mx a)^T); split=> [i|]. exists (row i (vec_mx a)); split=> [j|]; first by rewrite !mxE; apply: Ea. by rewrite -row_mul -{1}[Y]trmxK -trmx_mul !mxE. by rewrite -[Y]trmxK -!trmx_mul mulmxA -mxvec_dotmul trmx_mul trmxK vec_mxK. exists (mxvec (\matrix_i a i)); split. by case/mxvec_indexP=> i j; rewrite mxvecE mxE; apply: Ea. rewrite -[mxvec _]trmxK -trmx_mul mxvec_dotmul -mulmxA trmx_mul !mxE. apply: eq_bigr => i _; rewrite Da1 !mxE; congr (_ * _). by apply: eq_bigr => j _; rewrite !mxE. suffices [m [X [[u [_ Du]] idealM]]]: exists m, exists X, let M := memM memR m X in M 1 /\ forall y, M y -> M (q.[w] * y). - do [set M := memM _ m X; move: q.[w] => z] in idealM *. have MX i: M (X 0 i). by exists (delta_mx 0 i); split=> [j|]; rewrite -?rowE !mxE. have /fin_all_exists[a /all_and2[Fa Da1]] i := idealM _ (MX i). have /fin_all_exists[r Dr] i := fin_all_exists (Fa i). pose A := \matrix_(i, j) r j i; pose B := z%:M - map_mx RtoK A. have XB0: X *m B = 0. apply/eqP; rewrite mulmxBr mul_mx_scalar subr_eq0; apply/eqP/rowP=> i. by rewrite !mxE Da1 mxE; apply: eq_bigr=> j _; rewrite !mxE mulrC Dr. exists (char_poly A); first exact: char_poly_monic. have: (\det B *: (u *m X^T)) 0 0 == 0. rewrite scalemxAr -linearZ -mul_mx_scalar -mul_mx_adj mulmxA XB0 /=. by rewrite mul0mx trmx0 mulmx0 mxE. rewrite mxE -Du mulr1 rootE -horner_evalE -!det_map_mx; congr (\det _ == 0). rewrite !raddfB /= !map_scalar_mx /= map_polyX horner_evalE hornerX. by apply/matrixP=> i j; rewrite !mxE map_polyC /horner_eval hornerC. pose gen1 x E y := exists2 r, pXin E r & y = r.[x]; pose gen := foldr gen1 memR. have gen1S (E : K -> Prop) x y: E 0 -> E y -> gen1 x E y. by exists y%:P => [i|]; rewrite ?hornerC ?coefC //; case: ifP. have genR S y: memR y -> gen S y. by elim: S => //= x S IH in y * => /IH; apply/gen1S/IH. have gen0 := genR _ 0 memR0; have gen_1 := genR _ 1 memR1. have{gen1S} genS S y: y \in S -> gen S y. elim: S => //= x S IH /predU1P[-> | /IH//]; last exact: gen1S. by exists 'X => [i|]; rewrite ?hornerX // coefX; apply: genR. pose propD (R : K -> Prop) := forall x y, R x -> R y -> R (x + y). have memRD: propD memR. by move=> _ _ [a ->] [b ->]; exists (a + b); rewrite rmorphD. have genD S: propD (gen S). elim: S => //= x S IH _ _ [r1 Sr1 ->] [r2 Sr2 ->]; rewrite -hornerD. by exists (r1 + r2) => // i; rewrite coefD; apply: IH. have gen_sum S := big_ind _ (gen0 S) (genD S). pose propM (R : K -> Prop) := forall x y, R x -> R y -> R (x * y). have memRM: propM memR. by move=> _ _ [a ->] [b ->]; exists (a * b); rewrite rmorphM. have genM S: propM (gen S). elim: S => //= x S IH _ _ [r1 Sr1 ->] [r2 Sr2 ->]; rewrite -hornerM. by exists (r1 * r2) => // i; rewrite coefM; apply: gen_sum => j _; apply: IH. have gen_horner S r y: pXin (gen S) r -> gen S y -> gen S r.[y]. move=> Sq Sy; rewrite horner_coef; apply: gen_sum => [[i _] /= _]. by elim: {2}i => [|n IHn]; rewrite ?mulr1 // exprSr mulrA; apply: genM. pose S := w :: q ++ p; suffices [m [X defX]]: finM memR (gen S). exists m, X => M; split=> [|y /defX Xy]; first exact/defX. apply/defX/genM => //; apply: gen_horner => // [i|]; last exact/genS/mem_head. rewrite -[q]coefK coef_poly; case: ifP => // lt_i_q. by apply: genS; rewrite inE mem_cat mem_nth ?orbT. pose intR R y := exists r, [/\ r \is monic, root r y & pXin R r]. pose fix genI s := if s is y :: s1 then intR (gen s1) y /\ genI s1 else True. have{mon_p pw0 intRp intRq}: genI S. split; set S1 := _ ++ _; first exists p. split=> // i; rewrite -[p]coefK coef_poly; case: ifP => // lt_i_p. by apply: genS; rewrite mem_cat orbC mem_nth. set S2 := S1; have: all [in S1] S2 by apply/allP. elim: S2 => //= y S2 IH /andP[S1y S12]; split; last exact: IH. have{q S S1 IH S1y S12 intRp intRq} [q mon_q qx0]: integralOver RtoK y. by move: S1y; rewrite mem_cat => /orP[]; [apply: intRq | apply: intRp]. exists (map_poly RtoK q); split=> // [|i]; first exact: monic_map. by rewrite coef_map /=; apply: genR. elim: {w p q}S => /= [_|x S IH [[p [mon_p px0 Sp]] /IH{IH}[m2 [X2 defS]]]]. exists 1, 1 => y; split=> [[a [Fa ->]] | Fy]. by rewrite tr_scalar_mx mulmx1; apply: Fa. by exists y%:M; split=> [i|]; rewrite 1?ord1 ?tr_scalar_mx ?mulmx1 mxE. pose m1 := (size p).-1; pose X1 := \row_(i < m1) x ^+ i. have [m [X defM]] := tensorM memR m1 m2 X1 X2; set M := memM _ _ _ in defM. exists m, X => y; rewrite -/M; split=> [/defM[a [M2a]] | [q Sq]] -> {y}. exists (rVpoly a) => [i|]. by rewrite coef_rVpoly; case/insub: i => // i; apply/defS/M2a. rewrite mxE (horner_coef_wide _ (size_poly _ _)) -/(rVpoly a). by apply: eq_bigr => i _; rewrite coef_rVpoly_ord !mxE. have M_0: M 0 by exists 0; split=> [i|]; rewrite ?mul0mx mxE. have M_D: propD M. move=> _ _ [a [Fa ->]] [b [Fb ->]]; exists (a + b). by rewrite mulmxDl !mxE; split=> // i /[1!mxE]; apply: memRD. have{M_0 M_D} Msum := big_ind _ M_0 M_D. rewrite horner_coef; apply: (Msum) => i _; case: i q`_i {Sq}(Sq i) => /=. elim: {q}(size q) => // n IHn i i_le_n y Sy. have [i_lt_m1 | m1_le_i] := ltnP i m1. apply/defM; exists (y *: delta_mx 0 (Ordinal i_lt_m1)); split=> [j|]. by apply/defS; rewrite !mxE /= mulr_natr; case: eqP. by rewrite -scalemxAl -rowE !mxE. rewrite -(subnK m1_le_i) exprD -[x ^+ m1]subr0 -(rootP px0) horner_coef. rewrite polySpred ?monic_neq0 // -/m1 big_ord_recr /= -lead_coefE. rewrite opprD addrC (monicP mon_p) mul1r subrK !mulrN -mulNr !mulr_sumr. apply: Msum => j _; rewrite mulrA mulrACA -exprD; apply: IHn. by rewrite -addnS addnC addnBA // leq_subLR leq_add. by rewrite -mulN1r; do 2!apply: (genM) => //; apply: genR. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)