diff --git a/cylinder.v b/cylinder.v index 90dafed..862d7d9 100644 --- a/cylinder.v +++ b/cylinder.v @@ -2005,18 +2005,21 @@ have mevalE q x : q.@[tnth (ngraph x)] = (evalpmp (\row_i (x ord0 (widen_ord (leqnSn n) i))) (muni q)).[x ord0 ord_max]. rewrite horner_evalpmp -{1}(muniK q) meval_mmulti (tnth_nth 0) nth_ngraph. by apply/meval_eq => i; rewrite !tnth_mktuple mxE. +have ts x: x \in SAset_cast n.+1 t -> + \row_i x ord0 (widen_ord (leqnSn n) i) \in \val s. + move=> xt /=. + rewrite -(SAset_cast_partition_of_graphs_above rsort tpart). + apply/inSAset_castDn; exists (castmx (erefl, esym (@addn1 n)) x); split. + by rewrite -inSAset_cast. + by apply/rowP => i; rewrite !mxE castmxE; congr (x _ _); apply/val_inj. have [p0|p0] := eqVneq (evalpmp (\val (pick s)) (muni (\val p))) 0. move=> x y xt yt. suff pz0 z : z \in SAset_cast n.+1 t -> (val p).@[tnth (ngraph z)] = 0. by rewrite !pz0. move=> zt; rewrite mevalE. set q := (evalpmp _ _); suff ->: q = 0 by apply/horner0. - apply/eqP; rewrite -size_poly_eq0 /q (S'size s). - by apply/eqP; rewrite p0 size_poly0. - rewrite /= -(SAset_cast_partition_of_graphs_above rsort tpart). - apply/inSAset_castDn; exists (castmx (erefl, esym (@addn1 n)) z); split. - by rewrite -inSAset_cast. - by apply/rowP => i; rewrite !mxE castmxE; congr (z _ _); apply/val_inj. + apply/eqP; rewrite -size_poly_eq0 /q (S'size s); last exact/ts. + by apply/eqP; rewrite p0 size_poly0. case: (set0Vmem (SAimset (SAmpoly (val p)) (SAset_cast n.+1 t) :&: SAset_seq [:: 0])). move=> t0. have {}p0 x : x \in SAset_cast n.+1 t -> (val p).@[tnth (ngraph x)] != 0. @@ -2046,68 +2049,264 @@ case: (set0Vmem (SAimset (SAmpoly (val p)) (SAset_cast n.+1 t) :&: SAset_seq [:: apply/(@eq_continuous (subspace [set` SAset_cast n.+1 t]) _ (fun x : 'rV[R]_n.+1 => (val p).@[x ord0])). by move=> z; rewrite mxE. exact/continuous_subspaceT/meval_continuous. -move=> /(_ (SAset_itv `]-oo, 0[%R) (SAset_itv `]0, +oo[)). - + move=> /(_ (SAset_itv `]-oo, 0[%R) (SAset_itv `]0, +oo[)); mp. + (* N.B. This takes forever. *) + apply/open_subspace_ballP => /= z. + rewrite in_setI mem_setE inSAset_itv in_itv/= => /andP[z0] zs. + exists (- z ord0 ord0); split; first by rewrite oppr_gt0. + apply/subsetP => a; rewrite in_setI => /andP[+] _. + rewrite -ball_normE inE/= [normr _]mx_normrE => /bigmax_ltP[_]. + move=> /(_ (ord0, ord0) isT)/=; rewrite !mxE -opprB normrN => /ltr_normlW. + by rewrite -subr_lt0 -addrA subrr addr0 mem_setE inSAset_itv in_itv/=. + mp. + apply/open_subspace_ballP => /= z. + rewrite in_setI mem_setE inSAset_itv in_itv/= andbT => /andP[z0] zs. + exists (z ord0 ord0); split; first by []. + apply/subsetP => a; rewrite in_setI => /andP[+] _. + rewrite -ball_normE inE/= [normr _]mx_normrE => /bigmax_ltP[_]. + move=> /(_ (ord0, ord0) isT)/=; rewrite !mxE => /ltr_normlW. + rewrite -subr_gt0 opprB addrCA subrr addr0 mem_setE inSAset_itv in_itv/=. + by move=> ->. + mp. + apply/eqP => s0; suff: \row__ (fsval p).@[tnth (ngraph x)] \in SAset0 R 1. + by rewrite inSAset0. + rewrite -s0 inSAsetI; apply/andP; split; last first. + by rewrite inSAset_itv in_itv/= mxE. + apply/SAimsetP; exists x => //. + apply/eqP; rewrite SAmpolyE rowPE forall_ord1 !mxE; apply/eqP/meval_eq. + by move=> i; rewrite (tnth_nth 0) nth_map_ord. + mp. + apply/eqP => s0; suff: \row__ (fsval p).@[tnth (ngraph y)] \in SAset0 R 1. + by rewrite inSAset0. + rewrite -s0 inSAsetI; apply/andP; split; last first. + by rewrite inSAset_itv in_itv/= mxE y0. + apply/SAimsetP; exists y => //. + apply/eqP; rewrite SAmpolyE rowPE forall_ord1 !mxE; apply/eqP/meval_eq. + by move=> i; rewrite (tnth_nth 0) nth_map_ord. + mp. + apply/SAset_subP => _ /SAimsetP[] z /p0 z0 ->. + rewrite inSAsetU !inSAset_itv !in_itv/= andbT; apply/lt_total. + rewrite SAmpolyE mxE; move: z0; congr (_ != 0); apply/meval_eq. + by move=> i; rewrite (tnth_nth 0) nth_map_ord. + move=> /negP; apply; rewrite -subset0; apply/SAset_subP => z. + rewrite 2!inSAsetI !inSAset_itv/= !in_itv/= andbT => /andP[]/andP[_] z0. + by move=> /(lt_trans z0); rewrite ltxx. +move=> [px]; rewrite inSAsetI inSAset_seq mem_seq1 => /andP[] /SAimsetP[x] xt -> {px}. +rewrite SAmpolyE rowPE forall_ord1 !mxE => /eqP px0. +case: (roots2_on (S'constR s p)) => rp [] rpsort rproot. +have f1_inj : injective (fun x : 'rV[R]_1 => x ord0 ord0). + by move=> a b ab; apply/eqP; rewrite rowPE forall_ord1; apply/eqP. +have runiq: forall (r : seq (SAfunltType R n)), + sorted (SAfun_lt (n:=n)) r -> + {in \val s, forall x0 : 'rV_n, uniq [seq (f : {SAfun R^n -> R^1}) x0 | f <- r]}. + move=> r' r'sort y ys; rewrite -(map_inj_uniq f1_inj). + apply/lt_sorted_uniq/(sortedP 0) => i. + rewrite !size_map => ilt. + move: r'sort => /(sortedP 0)/(_ i ilt)/SAfun_ltP/(_ y) rpi. + rewrite -map_comp (nth_map 0) ?(nth_map 0)//. + by apply/(ltn_trans _ ilt). +move: (@subseq_sorted_continuous_SAfun _ _ rp r (val s)). +mp; first exact/runiq. +mp; first exact/runiq. +mp. + move=> i. + apply/(@subspace_eq_continuous _ _ _ (fun x : 'rV[R]_n => \row_(_ < 1) (rootsR (evalpmp x (muni (\val p))))`_i)). + move=> y; rewrite mem_setE => ys. + apply/eqP; rewrite rowPE forall_ord1 mxE. + by rewrite -rproot// (nth_map 0). + apply/mx_continuous => j k. + apply/(@eq_continuous (subspace [set` val s]) _ (fun x => (rootsR (evalpmp x (muni (\val p))))`_i)). + by move=> y; rewrite mxE. + apply/(rootsR_continuous (valP (pick s))). + - by move=> y ys; apply/S'size. + - move=> y ys; apply/(size_gcd_const s) => //; last exact/valP. + by apply/imfsetP; exists p. + by move=> y ys; apply/S'constR. +mp. + move=> i. + apply/(@subspace_eq_continuous _ _ _ (fun x : 'rV[R]_n => \row_(_ < 1) (rootsR (evalpmp x (\prod_(p : P' s) fsval p)))`_i)). + move=> y; rewrite mem_setE => ys. + apply/eqP; rewrite rowPE forall_ord1 mxE. + move: (rroot y ys) => /(congr1 (fun x => x`_i)). + by rewrite (nth_map 0)// => ->; apply/eqP. + apply/mx_continuous => j k. + apply/(@eq_continuous (subspace [set` val s]) _ (fun x => (rootsR (evalpmp x (\prod_(p : P' s) fsval p)))`_i)). + by move=> y; rewrite mxE. + apply/(rootsR_continuous (valP (pick s))). + - move=> y ys. + rewrite !evalpmp_prod size_prod; last first. + move=> /=; case=> /= _ /imfsetP[/=] q q0 -> _. + by rewrite -size_poly_eq0 (S'size s q y ys) size_poly_eq0. + rewrite size_prod; last first. + by move=> /=; case=> /= _ /imfsetP[/=] q q0 -> _. + congr (_.+1 - _)%N; apply/eq_bigr => /=. + case=> /= _ /imfsetP[/=] q q0 -> _. + by apply/S'size. + - by move=> y ys; apply/(size_gcdpm_const s). + by move=> y ys; apply/S'const. +mp; first exact/SAconnected_CD_cell. +mp. + move=> y ys; apply/subseq_uniqP; first exact/runiq. + apply/(inj_map f1_inj)/lt_sorted_eq. + - apply/(sortedP 0) => i; rewrite 2!size_map => ilt. + rewrite -map_comp (nth_map 0); last by apply/(ltn_trans _ ilt). + rewrite (nth_map 0)//=. + by move: rpsort => /(sortedP 0)/(_ i ilt)/SAfun_ltP/(_ y). + - + apply/(@subseq_lt_sorted _ _ _ [seq (x0 : 'rV_1) ord0 ord0 | x0 <- [seq (f : {SAfun R^n -> R^1}) y | f <- r]]). + exact/map_subseq/filter_subseq. + apply/(sortedP 0) => i; rewrite 2!size_map => ilt. + rewrite -map_comp (nth_map 0); last by apply/(ltn_trans _ ilt). + rewrite (nth_map 0)//=. + by move: rsort => /(sortedP 0)/(_ i ilt)/SAfun_ltP/(_ y). + move=> z; rewrite -map_comp; apply/mapP/mapP => -[/=]; last first. + move=> a; rewrite mem_filter => /andP[] /mapP[]/= f frp -> _ ->. + by exists f. + move=> _ /(nthP 0)[] i irp <- ->. + exists (rp`_i y) => //; rewrite mem_filter; apply/andP; split. + by apply/mapP; exists (rp`_i) => //; apply/mem_nth. + rewrite -(mem_map f1_inj) -map_comp/= rroot// in_rootsR evalpmp_prod; apply/andP; split. + apply/prodf_neq0; case=> /= _ /imfsetP[/=] q q0 -> _. + by rewrite -size_poly_eq0 (S'size s)// size_poly_eq0. + have: rp`_i y ord0 ord0 \in [seq (xi : {SAfun R^n -> R^1}) y ord0 ord0 | xi <- rp]. + by apply/mapP; exists (rp`_i) => //; apply/mem_nth. + rewrite rproot// in_rootsR => /andP[_] i0. + rewrite root_bigmul; apply/hasP. + have pP: muni (val p) \in P' s by apply/imfsetP; exists p. + exists [` pP]; first exact/mem_index_enum. + exact: i0. +move=> [rpr] [/mem_subseq rprr] rpE. +have: \row__ x ord0 ord_max \in [seq (f : {SAfun R^n -> R^1}) (\row_i (x ord0 (widen_ord (leqnSn n) i))) | f <- rp]. + rewrite -(mem_map f1_inj) -map_comp/= rproot; last exact/ts. + rewrite mxE in_rootsR; apply/andP; split. + by rewrite -size_poly_eq0 (S'size s) ?size_poly_eq0//; apply/ts. + rewrite /root -mevalE; apply/eqP; move: px0; congr (_ = 0). + by apply/meval_eq => i; rewrite (tnth_nth 0) nth_map_ord. +move=> /(nthP 0)[] i; rewrite size_map => ilt. +have ir: ((rpr`_i)%R < size r)%N. + suff: rpr`_i \in iota 0 (size r) by rewrite mem_iota. + apply/rprr/mem_nth. + by move: (rpE _ (ts _ xt)) => /(congr1 size); rewrite !size_map => <-. +move: (rpE _ (ts _ xt)) => /(congr1 (fun s => s`_i)). +rewrite [RHS](nth_map 0)//; last first. + by move: (rpE _ (ts _ xt)) => /(congr1 size); rewrite !size_map => <-. +move=> -> /esym/eqP; rewrite rowPE forall_ord1 !mxE => /eqP xE. +move: tpart => /imfsetP[/=] u /(nthP (SAset0 _ _))[j]. +rewrite size_map size_iota => jlt <-. +rewrite (nth_map 0) ?size_iota// nth_iota//. +have [_ tE|j0] := eqVneq j 0. + move: xt; rewrite tE (inSAset_cast _ _ (esym (addn1 n))) inSAsetI. + rewrite inSAset_bigcap => /andP[] /allP-/(_ (r`_(nth 0 rpr i)))/=. + mp; first exact/mem_nth. + rewrite inSAhypograph !mxE castmxE => xlt. + suff: x ord0 ord_max < x ord0 ord_max by rewrite ltxx. + move: xlt; congr (x _ _ < _). + - exact/val_inj. + - exact/val_inj/addn0. + rewrite xE; congr (r`_(rpr`_i)%R _ _ _). + by apply/rowP => k; rewrite !mxE castmxE; congr (x _ _); apply/val_inj. +have [_ tE|jr] := eqVneq j (size r).*2. + move: xt; rewrite tE (inSAset_cast _ _ (esym (addn1 n))) inSAsetI. + rewrite inSAset_bigcap => /andP[] /allP-/(_ (r`_(nth 0 rpr i)))/=. + mp; first exact/mem_nth. + rewrite inSAepigraph !mxE castmxE => xlt. + suff: x ord0 ord_max < x ord0 ord_max by rewrite ltxx. + move: xlt; congr (_ < x _ _); first last. + - exact/val_inj/addn0. + - exact/val_inj. + rewrite xE; congr (r`_(rpr`_i)%R _ _ _). + by apply/rowP => k; rewrite !mxE castmxE; congr (x _ _); apply/val_inj. +have xlE a: lsubmx (castmx (erefl 1%N, esym (addn1 n)) a) = \row_i a ord0 (widen_ord (leqnSn n) i). + by apply/rowP => k; rewrite !mxE castmxE; congr (a _ _); apply/val_inj. +have xrE (a : 'rV[R]_n.+1): a (cast_ord (esym ((erefl 1%N, esym (addn1 n)).1)%PAIR) ord0) + (cast_ord (esym ((erefl 1%N, esym (addn1 n)).2)%PAIR) (rshift n ord0)) + = a ord0 ord_max. + by congr (a _ _); apply/val_inj => //; apply/addn0. +move: jlt; rewrite ltnS leq_eqVlt (negPf jr)/= => jlt. +case: ifP => jodd tE; last first. + move: xt; rewrite tE (inSAset_cast _ _ (esym (addn1 n))) !inSAsetI. + rewrite inSAepigraph inSAhypograph !mxE castmxE xlE xrE. + rewrite xE => /andP[]/andP[] rji rij _. + have {}rsort: {in gtn (size r) &, {homo nth 0 r : i j / (i <= j)%N >-> SAfun_le i j}}. + move=> b c br cr bc. + have: sorted (SAfun_le (n:=n)) r. + move: rsort; apply/sub_sorted => f g /SAfun_ltP fg. + by apply/SAfun_leP => y; apply/ltW/fg. + rewrite sorted_pairwise; last exact/SAfun_le_trans. + move=> -/(pairwiseP 0)/(_ b c br cr). + move: bc; rewrite leq_eqVlt => /orP[/eqP -> _|/[swap]/[apply] //]. + exact/SAfun_le_refl. + case: (ltnP (rpr`_i)%R j./2) => [/leq_predn|ji]. + rewrite succnK => ij. + move: (rsort (rpr`_i)%R j./2.-1); rewrite !inE prednK; last first. + by case: j j0 jodd {jlt jr tE rji rij ij} => [//|]; case. + rewrite leq_half_double => /(_ ir (ltnW (leq_trans jlt (leqnSn _))) ij) /SAfun_leP. + move=> /(_ (\row_i x ord0 (widen_ord (leqnSn n) i)))/(lt_le_trans rji). + by rewrite ltxx. + move: (rsort j./2 (rpr`_i)%R); rewrite !inE ltn_half_double. + move=> /(_ jlt ir ji) /SAfun_leP/(_ (\row_i x ord0 (widen_ord (leqnSn n) i)))/(lt_le_trans rij). + by rewrite ltxx. +move: rsort; rewrite sorted_pairwise; last exact/SAfun_lt_trans. +move=> /(pairwiseP 0) rsort. +case: (ltnP j./2 (rpr`_i)%R) => [ji|]. + move: (rsort j./2 (rpr`_i)%R); rewrite !inE ltn_half_double. + move=> /(_ jlt ir ji) /SAfun_ltP/(_ (\row_i x ord0 (widen_ord (leqnSn n) i))). + move: xt; rewrite tE (inSAset_cast _ _ (esym (addn1 n))) inSAsetI. + move=> /andP[+] _; rewrite -[castmx _ _]hsubmxK xlE -inSAfun => /eqP ->. + by rewrite mxE castmxE xrE -xE ltxx. +rewrite leq_eqVlt => /orP[/eqP jE|ij]; last first. + move: (rsort (rpr`_i)%R j./2); rewrite !inE ltn_half_double. + move=> /(_ ir jlt ij) /SAfun_ltP/(_ (\row_i x ord0 (widen_ord (leqnSn n) i))). + move: xt; rewrite tE (inSAset_cast _ _ (esym (addn1 n))) inSAsetI. + move=> /andP[+] _; rewrite -[castmx _ _]hsubmxK xlE -inSAfun => /eqP ->. + by rewrite mxE castmxE xrE -xE ltxx. +move: tE; rewrite -jE => {j j0 jr jlt jodd rsort jE} ->. +move=> y z yr zr. +suff r0 a: a \in SAset_cast n.+1 (r`_(rpr`_i)%R :&: fsval s :*: SAsetT R 1) -> + (fsval p).@[tnth (ngraph a)] = 0. + by rewrite !r0//. +move=> {y z yr zr}; rewrite (inSAset_cast _ _ (esym (addn1 n))) inSAsetI. +rewrite -[castmx _ _]hsubmxK -inSAfun mevalE xlE inSAsetX row_mxKl. +move=> /andP[] /eqP aE /andP[] las _. +have: rsubmx (castmx (erefl 1%N, esym (addn1 n)) a) \in [seq r`_i (\row_i a ord0 (widen_ord (leqnSn n) i)) | i <- rpr]. + rewrite -aE; apply/map_f/mem_nth. + by move: (rpE _ (ts _ xt)) => /(congr1 size); rewrite !size_map => <-. +rewrite -rpE// => /(nthP 0)[] j; rewrite size_map => jlt. +rewrite (nth_map 0)// => /(congr1 (fun x : 'rV_1 => x ord0 ord0)). +rewrite !mxE castmxE xrE => {}aE. +have: a ord0 ord_max \in rootsR (evalpmp (\row_i0 a ord0 (widen_ord (leqnSn n) i0)) (muni (fsval p))). + by rewrite -rproot// -aE; apply/map_f/mem_nth. +by rewrite in_rootsR => /andP[_] /eqP. +Qed. - Search meval continuous_at. + + + - - Search sgz 1. -move=> [] y; rewrite inSAsetI inSAset_seq mem_seq1 => /andP[] /SAimsetP[]. -move=> x xt -> {y}; rewrite SAmpolyE rowPE forall_ord1 !mxE => /eqP px0. + Search mem SAset_cast. +Search size partition_of_graphs. +tE. +/(nthP (SAset0 _ _))[] j. +Check partition_of_graphs_above. +Search #|` _| size. + Search mem map injective. + Search root bigop. - Search meval mmulti. -have t0 u : u \in (SAset_cast n.+1 t) -> (val p).@[tnth (ngraph u)] = 0 -> - forall v, v \in (SAset_cast n.+1 t) -> (val p).@[tnth (ngraph v)] = 0. - move=> ut pu v. - have: (\row_i u ord0 (lift ord_max i) \in rootsR (evalpmp (\row_i u ord0 (lift ord_max i)) (\prod_(p : P' s) val p))). - Search tuple_of _.-1. -pose proots : {SAset R^n.+1} := [set| nquantify n.+1 - subst_formula - - + Search bigop (_ == 0). - rewrite - [/imfsetP|]. xS] /=. - move=> [] y; rewrite inE => /andP[] yS ys ->. - apply/imfsetP. + + Search subseq mem. - apply/andP; split; apply/allP - app - Search zip cat. - Search all2. -simple refine (exist _ _ _). - simple refine (\big[fsetU/fset0]_(s' : S') _)%fset. - have /= {S'p} s'p (q : elimp) : poly_invariant (val q) (val s') by apply/S'p. - have [x' xs'] := (pick s'). - have /roots2_on: {in val s', forall x, size (rootsR (evalpmp x p)) = size (rootsR (evalpmp x' p))}. - Search cindexR subresultant. - Search cauchy_index. - - simple refine ( - [fset @SAset_cast R (n + 1) n.+1 s | s in _])%fset. + Search sorted uniq. +rewr - Check partition_of_graphs. - - Search SAset_partition. - case=> i /=; rewrite ltnS leq_eqVlt. - case /boolP: (i == n.+1) => [/eqP -> _|_ /= ilt]; last exact: (S0 (Ordinal ilt)). - - - - Search (_ <= _.+1). - case/boolP: (val i == n.+1); last first. -case: (split (cast_ord (esym (addn1 n.+1)) i)). - exact S0. - - Admitted.