Skip to content

Commit

Permalink
proved cylindrical_decomposition
Browse files Browse the repository at this point in the history
  • Loading branch information
@Tragicus
Tragicus committed Jul 24, 2024
1 parent 0153eac commit c9eca71
Showing 1 changed file with 254 additions and 55 deletions.
309 changes: 254 additions & 55 deletions cylinder.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.


Expand Down

0 comments on commit c9eca71

Please sign in to comment.