-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathcylinder.v
2513 lines (2444 loc) · 113 KB
/
cylinder.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
From mathcomp Require Import freeg ssreflect ssrfun ssrbool eqtype choice seq.
From mathcomp Require Import ssrnat prime binomial bigop tuple order fintype.
From mathcomp Require Import finfun path ssralg ssrnum ssrint poly matrix.
From mathcomp Require Import finmap mpoly complex interval.
From mathcomp Require Import polydiv polyrcf polyorder qe_rcf qe_rcf_th.
(* TODO: the following imports should not be needed after cleanup. *)
From mathcomp Require Import generic_quotient classical_sets topology normedtype.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.POrderTheory Order.TotalTheory.
Import GRing.Theory Num.Theory Num.Def.
Import GRing.
Import numFieldTopology.Exports.
Require Import auxresults formula subresultant semialgebraic topology.
Require Import continuity_roots.
Local Open Scope type_scope.
Local Open Scope classical_set_scope.
Local Open Scope fset_scope.
Local Open Scope fmap_scope.
Local Open Scope ring_scope.
Local Open Scope sa_scope.
Section CylindricalDecomposition.
Variables (R : rcfType).
(* How do I assert that the restriction of a function is continuous, and not
that the function is continuous at every point in the set? *)
Fixpoint isCylindricalDecomposition n (S : {fset {SAset R^n}}) :=
SAset_partition S
/\ match n with | 0 => Logic.True | n.+1 =>
let S' := [fset SAset_cast n s | s in S] in
isCylindricalDecomposition S'
/\ forall (s' : S'),
exists m, exists xi : m.-tuple {SAfun R^n -> R^1},
(forall i, {within [set` val s'], continuous (tnth xi i)})
/\ sorted (@SAfun_lt _ _) xi
/\ [fset s in S | SAset_cast n s == val s']
= [fset SAset_cast _ x | x in partition_of_graphs_above (val s') xi]
end.
Local Notation isCD := isCylindricalDecomposition.
Lemma isCylindricalDecomposition_restrict n m S (mn : (m <= n)%N) :
@isCD n S -> isCD [fset SAset_cast m s | s in S].
Proof.
move: (n - m)%N mn (subnKC mn) S => + _ <-; elim=> [|d IHd].
rewrite addn0 => S.
congr isCD; apply/fsetP => s; apply/idP/imfsetP => [sS|[x]/= xS ->].
by exists s => //; rewrite SAset_cast_id.
by rewrite SAset_cast_id.
rewrite addnS => S /= [_] [/IHd] + _; congr isCD.
have md: (m <= m + d)%N by rewrite -{1}[m]addn0 leq_add2l.
apply/fsetP => s; rewrite -imfset_comp.
by apply/imfsetP/imfsetP => -[x]/= xS ->;
exists x => //; rewrite SAset_cast_trans// geq_min md orbT.
Qed.
Definition poly_invariant n (p : {mpoly R[n]}) (s : {SAset R^n}) :=
{in s &,
forall x y,
(sgz (meval (tnth (ngraph x)) p) = sgz (meval (tnth (ngraph y)) p))%R}.
Definition poly_adapted n p (S : {fset {SAset R^n}}) :=
forall s : S, poly_invariant p (val s).
Definition evalpmp {n} (x : 'rV[R]_n) (P : {poly {mpoly R[n]}}) :=
map_poly (meval (tnth (ngraph x))) P.
Definition truncate (T : ringType) (p : {poly T}) (d : nat) :=
(\poly_(i < minn d (size p)) p`_i)%R.
Definition truncations n
(p : {poly {mpoly R[n]}}) : {fset {poly {mpoly R[n]}}} :=
(fix F p n :=
match n with
| 0 => [fset p]
| n.+1 => if (0 < mdeg (mlead (lead_coef p)))%N then
p |` F (truncate p (size p).-1) n
else [fset p]
end) p (size p).
Lemma coef_truncate (T : ringType) (p : {poly T}) d n :
(truncate p d)`_n = p`_n *+ (n < d).
Proof.
rewrite -{2}[p]coefK !coef_poly ltn_min.
by case: (n < d)%N; rewrite ?mulr0n// mulr1n.
Qed.
Lemma truncate_trans (T : ringType) (p : {poly T}) (d e : nat) :
truncate (truncate p d) e = truncate p (minn d e).
Proof. by apply/polyP => i; rewrite !coef_truncate ltn_min -mulnb mulrnA. Qed.
Lemma truncate_size (T : ringType) (p : {poly T}) :
truncate p (size p) = p.
Proof. by rewrite /truncate minnn coefK. Qed.
Lemma truncate_ge_sizeP (T : ringType) (p : {poly T}) (d : nat) :
(truncate p d == p) = (size p <= d)%N.
Proof.
apply/eqP/idP => [<-|/minn_idPl pd].
exact/(leq_trans (size_poly _ _) (geq_minl _ _)).
by rewrite -[p]truncate_size truncate_trans pd.
Qed.
Lemma truncationsE n (p : {poly {mpoly R[n]}}) :
truncations p =
[fset truncate p d |
d in [seq d <- iota 0 (size p).+1 |
all (fun i => msize p`_i != 1) (iota d ((size p).+1 - d))]].
Proof.
have t00 k: truncate 0 k = 0 :> {poly {mpoly R[n]}}.
by apply/eqP; rewrite truncate_ge_sizeP size_poly0.
rewrite /truncations.
move dE: (size p) => d.
have {dE}: (size p <= d)%N by rewrite dE leqnn.
elim: d p => [|d IHd] p.
move=> /= /size_poly_leq0P ->.
apply/fsetP => x; rewrite coef0 msize0/= inE.
apply/eqP/imfsetP => [->|[y]]; first by exists 0.
by rewrite inE t00.
move=> sp; rewrite {}IHd; last first.
apply/(leq_trans (size_poly _ _))/(leq_trans (geq_minl _ _)).
by rewrite [d]pred_Sn -!subn1 leq_sub2r.
rewrite !iotanS.
have [->|p0] := eqVneq p 0.
rewrite lead_coef0 mlead0 mdeg0/=; apply/fsetP => x.
rewrite in_fset1; apply/eqP/imfsetP => /= [->|[k] _]; last by rewrite t00.
exists 0; last by rewrite t00.
rewrite mem_filter -iotanS in_cons eqxx andbT.
by apply/allP => i _; rewrite coef0 msize0.
case: (ltnP 0 _); last first.
rewrite leqn0 -eqSS mlead_deg ?lead_coef_eq0// lead_coefE => pn.
apply/fsetP => x; rewrite in_fset1.
apply/eqP/imfsetP => [->|[k]] /=.
exists d.+1; last by apply/esym/eqP; rewrite truncate_ge_sizeP.
rewrite mem_filter mem_rcons add0n in_cons eqxx andbT /= subSnn/= andbT.
move/leq_sizeP: sp => /(_ d.+1 (leqnn _)) ->.
by rewrite msize0.
rewrite mem_filter => /andP[] /allP sk _ ->.
apply/eqP; rewrite truncate_ge_sizeP leqNgt; apply/negP => kp.
move/(_ (size p).-1): sk.
rewrite pn mem_iota -ltnS (ltn_predK kp) kp/= subnKC.
by rewrite (leq_trans sp)// => /(_ isT).
by rewrite -ltnS; apply/(leq_trans kp)/(leq_trans sp)/(leq_trans (leqnSn _)).
rewrite -ltnS mlead_deg ?lead_coef_eq0// => pn.
apply/fsetP => x; rewrite in_fset1U.
apply/orP/imfsetP => /= [[/eqP ->|/imfsetP]|].
- exists d.+1; last by apply/esym/eqP; rewrite truncate_ge_sizeP.
rewrite mem_filter subSnn/= mem_rcons add0n mem_head.
move/leq_sizeP: sp => /(_ d.+1 (leqnn _)) ->.
by rewrite msize0.
- move=> /= [k].
rewrite mem_filter truncate_trans -iotanS mem_iota iotanS/= add0n.
move=> /andP[] /allP ks kd ->.
exists (minn (size p).-1 k) => //.
rewrite mem_filter -!iotanS mem_iota/= add0n ltnS geq_min (ltnW kd) orbT.
rewrite andbT.
apply/allP => i; rewrite mem_iota subnKC geq_min; last first.
by rewrite (leq_trans (ltnW kd))// orbT.
case: (ltnP i (size p).-1) => /= [ip /andP[] ki id|+ _]; last first.
rewrite leq_eqVlt => /orP[/eqP <-|].
by rewrite -lead_coefE eq_sym (ltn_eqF pn).
rewrite prednK; last by rewrite ltnNge leqn0 size_poly_eq0.
move=> /leq_sizeP => /(_ i (leqnn _)) ->.
by rewrite msize0.
move/(_ i): ks; rewrite mem_iota ki/= subnKC ?(ltnW kd)//.
move: id; rewrite leq_eqVlt ltnS eqSS => /orP [/eqP -> _|/[swap]/[apply]].
by move/leq_sizeP: sp => /(_ _ (leqnn _)) ->; rewrite msize0.
by rewrite coef_truncate ip mulr1n.
move=> [k]; rewrite mem_filter -!iotanS mem_iota iotanS/= add0n ltnS.
move=> /andP[] /allP sk kd ->.
case: (ltnP k (size p)) => [kp|pk]; last by left; rewrite truncate_ge_sizeP.
right; apply/imfsetP; exists k => /=; last first.
rewrite truncate_trans; congr truncate.
by apply/esym/minn_idPr; rewrite -ltnS (leq_trans kp)// leqSpred.
rewrite mem_filter -iotanS mem_iota/= add0n (leq_trans kp sp) andbT.
apply/allP => i; rewrite mem_iota subnKC// => /andP[] ki id.
rewrite coef_truncate; case: (i < _)%N; last by rewrite mulr0n msize0.
rewrite mulr1n; apply/sk; rewrite mem_iota ki/= subnKC.
exact/(leq_trans id).
exact/(leq_trans kd).
Qed.
Lemma truncations_witness n d (p : {poly {mpoly R[n]}}) (x : 'rV[R]_n) :
(size (evalpmp x p) <= d)%N -> truncate p d \in truncations p.
Proof.
rewrite truncationsE => sd; apply/imfsetP; exists (minn d (size p)); last first.
case: (ltnP d (size p)) => //; rewrite -truncate_ge_sizeP => /eqP ->.
by rewrite truncate_size.
rewrite mem_filter mem_iota/= add0n ltnS geq_minr andbT.
apply/allP => i; rewrite mem_iota geq_min.
case: (ltnP i (size p)) => [ip|+ _]; last first.
by move=> /leq_sizeP -> //; rewrite msize0.
rewrite orbF => /andP[] di _.
move/leq_sizeP: sd => /(_ _ di); rewrite coefE ip => pi0.
apply/negP => /msize_poly1P [c] /eqP c0 pE.
by rewrite pE mevalC in pi0.
Qed.
Ltac mp :=
match goal with
| |- (?x -> _) -> _ => have /[swap]/[apply]: x
end.
Import ordered_qelim.ord.
Theorem roots2_on n (P : {poly {mpoly R[n]}}) (d : nat) (s : {SAset R^n}) :
{in s, forall x, size (rootsR (evalpmp x P)) = d} ->
{xi : d.-tuple {SAfun R^n -> R^1} |
sorted (@SAfun_lt R n) xi
/\ {in s, forall x,
[seq (xi : {SAfun R^n -> R^1}) x ord0 ord0 | xi <- xi]
= (rootsR (evalpmp x P))}}.
Proof.
case: (set0Vmem s) => [-> {s}|[x xs] dE].
exists (mktuple (fun i => SAfun_const n (\row__ i%:R))).
split=> [|x]; last by rewrite inSAset0.
apply/(sortedP (SAfun_const n 0)); rewrite size_tuple => i id.
rewrite -[i.+1]/(Ordinal id : nat) nth_mktuple.
rewrite -/(Ordinal (ltnW id) : nat) nth_mktuple/=.
by apply/SAfun_ltP => x; rewrite !SAfun_constE !mxE ltr_nat.
move: dE; have [->|+ dE] := eqVneq d 0.
move=> dE; exists (mktuple (fun i => SAfun_const n 0)).
split=> [|y ys]; first by rewrite /= enum_ord0.
move/eqP: (dE _ ys); rewrite size_eq0 => /eqP -> /=.
by rewrite enum_ord0.
move: (dE _ xs); have [-> <-|] := eqVneq (evalpmp x P) 0.
by rewrite /rootsR roots0.
have [->|P0 Px0 _ d0] := eqVneq P 0.
by rewrite /evalpmp rmorph0 eqxx.
(* TODO: should this be extracted? *)
have ltn_addL (k m : nat) : (k + m < k)%N = false.
by rewrite -{2}[k]addn0 ltn_add2l.
pose G_graph (i : 'I_d) : {SAset R^(n+1)} := [set |
(Not s /\ 'X_n == NatConst _ i)
\/ (s /\
nquantify n.+1 d Exists (
(\big[And/True]_(j < d.-1) ('X_(n.+1+j) <% 'X_(n.+1+j.+1)))
/\ \big[And/True]_(j < d)
(term_mpoly (mmulti P)
(fun k => if (k : nat) == n then 'X_(n.+1+j) else 'X_k) == 0)
/\ ('forall 'X_(n.+1+d),
(term_mpoly (mmulti P)
(fun k => if (k : nat) == n then 'X_(n.+1+d) else 'X_k) == 0)
==> \big[Or/False]_(j < d) ('X_(n.+1+d) == 'X_(n.+1+j)))
/\ 'X_n == 'X_(n.+1+i)))].
have GP i (x0 : 'rV[R]_n) (y : 'rV[R]_1) :
row_mx x0 y \in G_graph i
= if x0 \in s
then y ord0 ord0 == (rootsR (evalpmp x0 P))`_i
else y == \row__ i%:R.
rewrite pi_form /cut rcf_sat_subst.
rewrite -[X in subst_env _ X]cats0 subst_env_iota_catl ?size_ngraph//.
rewrite !simp_rcf_sat -rcf_sat_take ngraph_cat take_size_cat ?size_ngraph//.
move/(_ x0) : dE; rewrite inE.
case/boolP: (rcf_sat (ngraph x0) s) => /= x0s dE; last first.
rewrite nth_cat size_map size_enum_ord ltnn subnn enum_ordSl/= orbF.
apply/eqP/eqP => [y0|/rowP ->]; last by rewrite !mxE.
apply/rowP; case; case=> [|//] j0.
by rewrite !mxE -[RHS]y0; congr (y _ _); apply/val_inj.
move: dE => /(_ isT) /eqP dE.
rewrite -ngraph_cat -[X in nquantify X]addn1.
rewrite -[X in nquantify X](size_ngraph (row_mx x0 y)).
apply/rcf_satP/eqP => [|yE].
move=> /nexistsP [z]/= []/holdsAnd zlt []/holdsAnd z0 []z0P.
rewrite nth_cat size_map size_enum_ord {1}addn1 leqnn enum_ordD map_cat.
rewrite nth_cat 2!size_map size_enum_ord ltnn subnn enum_ordSl/=.
rewrite enum_ord0/= nth_cat size_cat 2!size_map size_enum_ord/=.
rewrite [X in (_ < X)%N]addn1 -addnS -[X in (_ <= X)%N]addn0 leq_add2l/=.
rewrite mxE (unsplitK (inr ord0)) => ->.
rewrite addn1 subDnCA// subnn addn0 (rootsRPE (p:=evalpmp x0 P))//.
- move=> j; move/(_ j (mem_index_enum _) isT) : z0 => /= Pz.
apply/rootP; rewrite -[RHS]Pz.
rewrite -(mevalC (tnth (ngraph x0)) (tnth z j)) horner_map/=.
rewrite eval_term_mpoly meval_mmulti eqxx/= nth_cat size_map.
rewrite size_enum_ord [X in (_ < X)%N]addn1 ltn_addL.
rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0 -tnth_nth/=.
apply/meval_eq => k.
rewrite (ltn_eqF (ltn_ord k))/= nth_cat size_map size_enum_ord.
rewrite -[nat_of_ord k]/(nat_of_ord (@unsplit n 1 (inl k))).
rewrite ltn_ord (nth_map (unsplit (inl k))) ?size_enum_ord//.
by rewrite nth_ord_enum mxE unsplitK tnth_mktuple.
- move=> u /rootP; rewrite -(mevalC (tnth (ngraph x0)) u) horner_map/=.
move/(_ u): z0P => + Pu.
rewrite eval_term_mpoly meval_mmulti eqxx/= nth_set_nth/= eqxx; mp.
rewrite -[RHS]Pu; apply/meval_eq => j.
rewrite (ltn_eqF (ltn_ord j))/= nth_set_nth/=.
have /ltn_eqF ->: (j < n.+1 + d)%N.
apply/(leq_trans (ltn_ord j)).
by rewrite addSn -addnS -{1}[n]addn0 leq_add2l.
rewrite nth_cat size_map size_enum_ord.
rewrite -[nat_of_ord j]/(nat_of_ord (@unsplit n 1 (inl j))) ltn_ord.
rewrite (nth_map (unsplit (inl j))) ?size_enum_ord//.
by rewrite nth_ord_enum mxE unsplitK tnth_mktuple.
move=> /holdsOr -[] /= j [_] [_].
rewrite !nth_set_nth/= eqxx eqn_add2l (ltn_eqF (ltn_ord j)).
rewrite nth_cat size_map size_enum_ord {1}addn1 ltn_addL addn1.
by rewrite subDnCA// subnn addn0 mevalC => ->; apply/memt_nth.
- apply/(sortedP 0) => j; rewrite size_tuple -ltn_predRL => jd.
move/(_ (Ordinal jd) (mem_index_enum _) isT): zlt => /=.
rewrite !nth_cat size_map size_enum_ord -[n.+1]addn1.
by rewrite !ltn_addL !addn1 !subDnCA// subnn !addn0.
apply/nexistsP; exists (Tuple dE) => /=; split.
apply/holdsAnd; case=> j + _ _ /=; rewrite ltn_predRL => jd.
rewrite !nth_cat size_map size_enum_ord -[n.+1]addn1 !ltn_addL !addn1.
rewrite !subDnCA// subnn !addn0.
move/(sortedP 0): (let c := cauchy_bound (evalpmp x0 P) in
sorted_roots (- c) c (evalpmp x0 P)) => /(_ j).
by rewrite (eqP dE) => /(_ jd).
split.
apply/holdsAnd => j _ _ /=.
rewrite eval_term_mpoly meval_mmulti eqxx/= nth_cat size_map.
rewrite size_enum_ord [X in (_ < X)%N]addn1 ltn_addL.
rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0.
have: (rootsR (evalpmp x0 P))`_j \in rootsR (evalpmp x0 P).
by apply/mem_nth; rewrite (eqP dE).
move=> /root_roots/rootP.
rewrite -(mevalC (tnth (ngraph x0)) ((rootsR (evalpmp x0 P))`_j)).
rewrite horner_map/= => Pj.
rewrite -[RHS]Pj/= mevalC; apply/meval_eq => k.
rewrite (ltn_eqF (ltn_ord k))/= nth_cat size_map size_enum_ord.
rewrite -[nat_of_ord k]/(nat_of_ord (@unsplit n 1 (inl k))) ltn_ord.
rewrite (nth_map (unsplit (inl k))) ?size_enum_ord// nth_ord_enum.
by rewrite mxE unsplitK tnth_mktuple.
split=> [u|].
move: dE; have [->|{}Px0 dE] := eqVneq (evalpmp x0 P) 0.
by rewrite /rootsR roots0 => /eqP dx; rewrite -dx eqxx in d0.
rewrite eval_term_mpoly meval_mmulti eqxx/= nth_set_nth/= eqxx => Pu.
have: (u \in rootsR (evalpmp x0 P)).
rewrite in_rootsR Px0; apply/rootP.
rewrite -(mevalC (tnth (ngraph x0)) u) horner_map/=.
move: Pu; congr (_ = _); apply/meval_eq => j.
rewrite (ltn_eqF (ltn_ord j))/= nth_set_nth/=.
have /ltn_eqF ->: (j < n.+1 + d)%N.
apply/(leq_trans (ltn_ord j)).
by rewrite addSn -addnS -{1}[n]addn0 leq_add2l.
rewrite nth_cat size_map size_enum_ord.
rewrite -[nat_of_ord j]/(nat_of_ord (@unsplit n 1 (inl j))) ltn_ord.
rewrite (nth_map (unsplit (inl j))) ?size_enum_ord//.
by rewrite nth_ord_enum mxE unsplitK tnth_mktuple.
rewrite -index_mem (eqP dE) => u0.
apply/holdsOr; exists (Ordinal u0).
split; first exact/mem_index_enum.
split=> //=.
rewrite !nth_set_nth/= eqxx eqn_add2l (ltn_eqF u0).
rewrite nth_cat size_map size_enum_ord {1}addn1 ltn_addL addn1.
rewrite subDnCA// subnn addn0; apply/esym/nth_index.
by rewrite -index_mem (eqP dE).
rewrite !nth_cat size_map size_enum_ord -[n.+1]addn1 leqnn ltn_addL.
rewrite -[X in _`_X]addn0 -[X in _`_X]/(nat_of_ord (@unsplit n 1 (inr ord0))).
rewrite (nth_map (unsplit (inr ord0))) ?size_enum_ord// nth_enum_ord.
by rewrite mxE unsplitK subDnCA// subnn addn0.
have SAfun_G (i : 'I_d) :
(G_graph i \in @SAfunc _ n 1) && (G_graph i \in @SAtot _ n 1).
apply/andP; split.
apply/inSAfunc => x0 y1 y2; rewrite !GP.
case: (x0 \in s); last by move=> /eqP -> /eqP.
move=> /eqP <- /eqP/esym y12; apply/rowP; case; case=> // lt01.
by move: y12; congr (y1 _ _ = y2 _ _); apply/val_inj.
apply/inSAtot => x0; case/boolP: (x0 \in s) => [|/negPf] x0s.
by exists (\row__ (rootsR (evalpmp x0 P))`_i); rewrite GP x0s !mxE.
by exists (\row__ i%:R); rewrite GP x0s.
pose G i := MkSAfun (SAfun_G i).
have GE (i : 'I_d) (x0 : 'rV_n) :
G i x0 = \row__ (if x0 \in s then (rootsR (evalpmp x0 P))`_i else i%:R).
by apply/eqP; rewrite inSAfun GP; case: (x0 \in s) => //; rewrite mxE.
exists (mktuple G).
split.
apply/(sortedP (@SAfun_const R n 1 0)) => i; rewrite size_tuple => id.
apply/SAfun_ltP => y; rewrite (nth_mktuple _ _ (Ordinal id)).
rewrite (nth_mktuple _ _ (Ordinal (ltnW id))) !GE !mxE.
case/boolP: (y \in s) => /= ys; last by rewrite ltr_nat.
move/(sortedP 0): (let c := cauchy_bound (evalpmp y P) in
sorted_roots (- c) c (evalpmp y P)) => /(_ i).
by rewrite dE// => /(_ id).
move=> y ys; apply/(eq_from_nth (x0:=0)); first by rewrite size_tuple dE.
rewrite size_tuple => i id.
rewrite (nth_map (@SAfun_const R n 1 0)) ?size_tuple//.
by rewrite -[ i ]/(nat_of_ord (Ordinal id)) nth_mktuple GE mxE ys.
Qed.
Lemma rootsR_continuous n (p : {poly {mpoly R[n]}}) (s : {SAset R^n})
(x : 'rV[R]_n) i :
x \in s ->
{in s, forall y, size (evalpmp y p) = size (evalpmp x p)} ->
{in s, forall y,
size (gcdp (evalpmp y p) (evalpmp y p)^`())
= size (gcdp (evalpmp x p) (evalpmp x p)^`())} ->
{in s, forall y,
size (rootsR (evalpmp y p)) = size (rootsR (evalpmp x p))} ->
{within [set` s], continuous (fun y => (rootsR (evalpmp y p))`_i)}.
Proof.
case: (ltnP i (size (rootsR (evalpmp x p)))) => ir; last first.
move=> _ _ _ r_const.
apply(@subspace_eq_continuous _ _ R (fun=> 0)); last exact/cst_continuous.
move=> /= u; rewrite mem_setE => us.
by apply/esym/nth_default; rewrite (r_const u us).
case: n p s x ir => [|n] p s x ir xs s_const s'_const r_const/=;
apply/continuousP => /= A;
rewrite openE/= => /subsetP Aopen;
apply/open_subspace_ballP => /= y;
rewrite in_setI mem_setE => /andP[] {}/Aopen;
rewrite /interior inE => /nbhs_ballP[] e/= e0 yeA ys.
exists 1; split=> // z _; apply/yeA.
suff ->: z = y by apply/ballxx.
by apply/rowP => -[].
have [p0|px0] := eqVneq (size (evalpmp x p)) 0.
exists 1; split=> // z [_] zs /=; apply/yeA.
have {}p0 u : u \in s -> evalpmp u p = 0.
by move=> us; apply/eqP; rewrite -size_poly_eq0 s_const// p0.
by rewrite p0// p0//; apply/ballxx.
pose q z := map_poly (real_complex R) (evalpmp z p).
have q0 z : z \in s -> q z != 0.
by move=> zs; rewrite map_poly_eq0 -size_poly_eq0 s_const.
set e' := \big[Order.min/e]_(u <- dec_roots (q y))
\big[Order.min/e]_(v <- dec_roots (q y) | u != v) (complex.Re `|u - v| / 2).
have e'0: 0 < e'%:C%C.
rewrite ltcR lt_bigmin e0/=; apply/allP => u _.
rewrite lt_bigmin e0/=; apply/allP => v _.
apply/implyP => uv; apply/divr_gt0; last exact/ltr0Sn.
by rewrite -ltcR (normr_gt0 (u - v)) subr_eq0.
have: exists d : R, 0 < d /\
forall z, z \in s -> `|z - y| < d -> alignp e'%:C%C (q y) (q z).
case: (aligned_deformed (q y) e'0) => /= [[]] a aI [].
rewrite ltcE/= => /andP[/eqP ->] a0; rewrite complexr0 => ad.
have /fin_all_exists /= : forall (i : 'I_(size (val p)).+1),
exists delta, 0 < delta /\
forall (z : 'rV[R]_n.+1), y \in s -> `|y - z| < delta ->
`|(q y)`_i - (q z)`_i| < a%:C%C.
move=> j.
move: (@meval_continuous _ _ (val p)`_j y).
rewrite /= /continuous_at.
move=> /(@cvgr_dist_lt _ R^o).
move=> /(_ _ a0) /nbhs_ballP[] d'/= d'0 /subsetP xd'.
exists d'; split=> // z zs yz.
move: xd' => /(_ z); mp; first by rewrite -ball_normE inE/=.
rewrite inE/= !coef_map/= -rmorphB/= normc_def/= expr0n/= addr0 sqrtr_sqr.
rewrite ltcR.
by congr (normr (_ - _) < a); apply/meval_eq => k; rewrite tnth_mktuple.
move=> [d'] d'P; exists (\big[minr/1]_i d' i).
split; first by rewrite lt_bigmin ltr01; apply/allP => j _ /=; case: (d'P j).
move=> z zs; rewrite lt_bigmin => /andP[_] /allP xz; apply/ad.
split=> [|j]; first by rewrite !size_map_poly s_const// (s_const _ ys).
move: (ltn_ord j); rewrite [X in (j < X)%N]size_map_poly => jlt.
have {}jlt := leq_trans (leq_trans jlt (size_poly _ _)) (leqnSn _).
case: (d'P (Ordinal jlt)) => _ /=; apply=> //.
by rewrite -opprB normrN; apply/xz/mem_index_enum.
move=> [] d [] d0 dP.
exists d; split=> // z/=.
rewrite -ball_normE/= -opprB normrN => -[] yz zs; apply/yeA.
move: dP => /(_ z zs yz) yze.
rewrite -(@ball_normE R R^o)/=.
have: exists (fyz : [fset x in dec_roots (q y)] -> [fset x in dec_roots (q z)]),
forall u, `|val u - val (fyz u)| < e'%:C%C.
apply/(fin_all_exists (P:=fun u v => `|val u - val v| < e'%:C%C)).
case=> /= u; rewrite mem_imfset//= mem_dec_roots => /andP[_] pu.
move: yze => /(_ u pu).
rewrite -big_filter; case rsy: (seq.filter _ _) => [|v l].
by rewrite big_nil leqn0 mu_eq0 ?pu// map_poly_eq0 -size_poly_eq0 s_const.
move: (mem_head v l).
rewrite -rsy mem_filter -normrN opprB => /andP[] uv pv _.
suff vP: v \in [fset x in dec_roots (q z)].
by exists [` vP].
by rewrite mem_imfset.
move=> [/=] fyz fyze.
have eP (u v : [fset x | x in dec_roots (q y)]) :
`|val u - val v| < 2 * e'%:C%C -> u = v.
move=> uve; apply/eqP/negP => /negP uv; move: uve.
rewrite -(RRe_real (normr_real _)) mulrC mulr_natr -rmorphMn/= ltcR.
rewrite -mulr_natr.
rewrite -ltr_pdivrMr; last exact/ltr0Sn.
rewrite lt_bigmin => /andP[_] /allP-/(_ (val u))/=.
move: (fsvalP u); rewrite (mem_imfset _ _ (@inj_id _))/= => /[swap]/[apply].
rewrite lt_bigmin => /andP[_] /allP-/(_ (val v))/=.
move: (fsvalP v); rewrite (mem_imfset _ _ (@inj_id _))/= => /[swap]/[apply].
by rewrite (inj_eq val_inj) ltxx => /implyP-/(_ uv).
have R0: [char R[i]] =i pred0 by exact/char_num.
have fyzb: bijective fyz.
apply/inj_card_bij.
move=> u v fuv; apply/eP.
rewrite -(subrBB (val (fyz u))); apply/(le_lt_trans (ler_normB _ _)).
rewrite mulr2n mulrDl mul1r; apply/ltrD; first exact/fyze.
by rewrite fuv; apply/fyze.
rewrite -2!cardfE card_imfset//= card_imfset//=.
do 2 rewrite undup_id ?uniq_dec_roots//.
rewrite (size_dec_roots (q z) R0) (size_dec_roots (q y) R0).
rewrite size_divp; last by rewrite gcdp_eq0 negb_and q0.
rewrite size_divp; last by rewrite gcdp_eq0 negb_and q0.
rewrite ![(q _)^`()]deriv_map -!gcdp_map !size_map_poly -!/(evalpmp _ _).
by rewrite s_const// s_const// s'_const// s'_const.
have pyrP j: (j < size (rootsR (evalpmp y p)))%N ->
((rootsR (evalpmp y p))`_j)%:C%C \in [fset x | x in dec_roots (q y)].
rewrite (mem_imfset _ _ (@inj_id _))/= mem_dec_roots q0//=.
move=> /(mem_nth 0); rewrite in_rootsR => /andP[_] jr.
exact/rmorph_root.
rewrite -ltcR.
apply/(le_lt_trans (normc_ge_Re (_%:C%C))) => /=.
rewrite rmorphB/=.
rewrite -(r_const y ys) in ir.
suff ->: ((rootsR (evalpmp z p))`_i)%:C%C = val (fyz [` pyrP i ir]).
move: (fyze [` pyrP i ir]) => /= pye.
apply/(lt_le_trans pye).
by rewrite lecR; apply/bigmin_le_id.
have perm_eqC a: perm_eq
[seq u <- dec_roots (q a) | u \is Num.real]
[seq x%:C%C | x <- rootsR (evalpmp a p)].
apply/uniq_perm.
- exact/filter_uniq/uniq_dec_roots.
- by rewrite map_inj_uniq ?uniq_roots//; apply/complexI.
move=> u; rewrite mem_filter mem_dec_roots map_poly_eq0 .
apply/andP/mapP => [[] uR /andP[] pa0 qu|[] v + ->].
exists (complex.Re u); last by rewrite (RRe_real uR).
rewrite in_rootsR pa0.
by rewrite -(RRe_real uR) fmorph_root in qu.
rewrite in_rootsR => /andP[] pa0 pv; split.
by apply/complex_realP; exists v.
by rewrite pa0/=; apply/rmorph_root.
have ne20: 2 != 0 :> R[i] by rewrite pnatr_eq0.
have fyzr (u : [fset x | x in dec_roots (q y)]) :
((val (fyz u)) \is Num.real) -> (val u) \is Num.real.
move=> fur.
suff ->: \val u = 'Re (\val u) by apply/Creal_Re.
apply/(mulfI ne20).
rewrite -complexRe -addcJ mulr2n mulrDl mul1r; congr (_ + _)%R.
have uP: ((\val u)^* )%C \in [fset x | x in dec_roots (q y)].
rewrite (mem_imfset _ _ (@inj_id _))/= mem_dec_roots q0//=.
rewrite -complex_root_conj/= map_poly_id => [|a].
move: (fsvalP u); rewrite (mem_imfset _ _ (@inj_id _))/=.
by rewrite mem_dec_roots => /andP[_].
move=> /[dup] /(nth_index 0)/=.
rewrite -index_mem size_map_poly => + alt.
by rewrite coef_poly alt => <-; rewrite conjc_real.
rewrite -[((val u)^* )%C]/(val [` uP]).
rewrite [in LHS](eP u [` uP])//.
rewrite -(subrBB (val (fyz u))).
apply/(le_lt_trans (ler_normB _ _)).
rewrite mulr2n mulrDl mul1r; apply/ltrD; first exact/fyze.
rewrite /= -(RRe_real fur) -conjc_real -rmorphB/= norm_conjC (RRe_real fur).
exact/fyze.
have {}fyzr (u : [fset x | x in dec_roots (q y)]) :
(val u) \is Num.real = ((val (fyz u)) \is Num.real).
apply/idP/idP; last exact/fyzr.
move=> ur; apply/negP => /negP fur.
pose sr y := [fset x : [fset x in dec_roots (q y)] | val x \is Num.real].
have srE a:
[fset val x | x in sr a]
= [fset x | x in dec_roots (q a) & x \is Num.real].
apply/eqP; rewrite eqEfsubset; apply/andP; split; apply/fsubsetP => b;
rewrite (mem_imfset _ _ (@inj_id _))/=.
move=> /imfsetP[/=] c /imfsetP[/=] c' cr -> ->.
apply/andP; split=> //=.
by move: (fsvalP c'); rewrite (mem_imfset _ _ (@inj_id _))/=.
move=> /andP[] qb br; apply/imfsetP => /=.
have bP: b \in [fset x0 | x0 in dec_roots (q a)].
by rewrite mem_imfset.
exists [` bP] => //.
by rewrite (mem_imfset _ _ (@inj_id _))/=.
suff: (#|` [fset x | x in dec_roots (q z) & x \is Num.real]|
< #|` [fset x | x in dec_roots (q y) & x \is Num.real]|)%N.
rewrite [X in (X < _)%N]card_imfset//= [X in (_ < X)%N]card_imfset//=.
do 2 rewrite undup_id ?uniq_dec_roots//.
rewrite (@perm_size _ _ [seq x%:C%C | x <- rootsR (evalpmp z p)]);
last exact/perm_eqC.
rewrite [X in (_ < X)%N](@perm_size _ _
[seq x%:C%C | x <- rootsR (evalpmp y p)]); last exact/perm_eqC.
by rewrite !size_map r_const// r_const// ltnn.
rewrite -2!srE [X in (X < _)%N](card_imfset _ _ val_inj)/=.
rewrite [X in (_ < X)%N](card_imfset _ _ val_inj)/=.
suff /fsubset_leq_card zy: sr z `<=` [fset fyz x | x in (sr y `\ u)].
apply/(leq_ltn_trans zy).
rewrite [X in (X < _)%N]card_imfset/=; last exact/bij_inj.
rewrite -add1n.
have/(congr1 nat_of_bool) /= <-: u \in sr y by rewrite mem_imfset.
by rewrite -cardfsD1 leqnn.
apply/fsubsetP => /= a.
rewrite [X in _ X -> _](mem_imfset _ _ (@inj_id _))/= => ar.
case: (fyzb) => fzy fyzK fzyK.
apply/imfsetP; exists (fzy a) => /=; last by rewrite [RHS]fzyK.
rewrite in_fsetD1 -(bij_eq fyzb) fzyK; apply/andP; split.
apply/eqP; move: ar => /[swap] ->.
by move/negP: fur.
rewrite (mem_imfset _ _ (@inj_id _))/=.
by apply/fyzr; rewrite fzyK.
have fir: val (fyz.[pyrP i ir])%fmap \is Num.real.
by rewrite -fyzr/=; apply/complex_realP; exists (rootsR (evalpmp y p))`_i.
have fiR: complex.Re (val (fyz [` pyrP i ir])) \in rootsR (evalpmp z p).
rewrite in_rootsR.
move: (q0 z zs); rewrite map_poly_eq0 => -> /=.
move: (fsvalP (fyz [` pyrP i ir])).
rewrite (mem_imfset _ _ (@inj_id _))/= mem_dec_roots => /andP[_].
by rewrite -{1}[val _]RRe_real// fmorph_root.
rewrite -(RRe_real fir); congr (_%:C%C).
rewrite -(nth_index 0 fiR); congr (_`__).
rewrite -[LHS](count_lt_nth 0 (sorted_roots _ _ _) ir).
move: (fiR); rewrite -index_mem => fiRs.
rewrite -[RHS](count_lt_nth 0 (sorted_roots _ _ _) fiRs) -!/(rootsR _).
rewrite (nth_index 0 fiR).
pose sr y z := [fset x : [fset x in dec_roots (q y)] | val x < z].
have srE a b:
[fset val x | x in sr a b]
= [fset x | x in dec_roots (q a) & x < b].
apply/eqP; rewrite eqEfsubset; apply/andP; split; apply/fsubsetP => b';
rewrite (mem_imfset _ _ (@inj_id _))/=.
move=> /imfsetP[/=] c /imfsetP[/=] c' cr -> ->.
apply/andP; split=> //=.
by move: (fsvalP c'); rewrite (mem_imfset _ _ (@inj_id _))/=.
move=> /andP[] qb br; apply/imfsetP => /=.
have bP: b' \in [fset x0 | x0 in dec_roots (q a)].
by rewrite mem_imfset.
exists [` bP] => //.
by rewrite (mem_imfset _ _ (@inj_id _))/=.
have {}perm_eqC a b: perm_eq
[seq x0 <- dec_roots (q a) | (x0 < b%:C%C)%R]
[seq x%:C%C | x <- [seq x <- rootsR (evalpmp a p) | (x < b)%R]].
apply/uniq_perm.
- exact/filter_uniq/uniq_dec_roots.
- rewrite map_inj_uniq; last exact/complexI.
exact/filter_uniq/uniq_roots.
move=> u; rewrite mem_filter mem_dec_roots map_poly_eq0.
apply/andP/mapP => [[] ub /andP[] pa0|[] v + ->].
move: ub; rewrite ltcE/= => /andP[] /eqP u0 ub.
rewrite (complexE u) -u0 mulr0 addr0 fmorph_root => pu.
exists (complex.Re u) => //.
by rewrite mem_filter ub/= in_rootsR pa0.
rewrite mem_filter in_rootsR => /andP[] vb /andP[] pa0 pv; split.
by rewrite ltcR.
by rewrite pa0/=; apply/rmorph_root.
suff: (#|` [fset x | x in dec_roots (q y)
& (x < ((rootsR (evalpmp y p))`_i)%:C%C)%R]|
= #|` [fset x | x in dec_roots (q z)
& (x < val (fyz [` pyrP i ir]))%R]|)%N.
rewrite [LHS]card_imfset//= [RHS]card_imfset//=.
do 2 rewrite undup_id ?uniq_dec_roots//.
rewrite (@perm_size _ _ [seq x%:C%C | x <-
[seq x <- rootsR (evalpmp y p) | (x < (rootsR (evalpmp y p))`_i)%R]]);
last exact/perm_eqC.
rewrite -{1}(RRe_real fir).
rewrite [RHS](@perm_size _ _ [seq x%:C%C | x <-
[seq x <- rootsR (evalpmp z p) |
(x < complex.Re (val (fyz [` pyrP i ir])))%R]]); last exact/perm_eqC.
by rewrite !size_map !size_filter.
rewrite -2!srE [LHS](card_imfset _ _ val_inj)/=.
rewrite [RHS](card_imfset _ _ val_inj)/=.
suff ->: sr z (val (fyz [` pyrP i ir]))
= [fset fyz x | x in sr y (((rootsR (evalpmp y p))`_i)%:C)%C].
by rewrite [RHS](card_imfset _ _ (bij_inj fyzb)).
apply/eqP; rewrite eqEfsubset; apply/andP; split; apply/fsubsetP => /= u.
rewrite [X in _ X -> _](mem_imfset _ _ (@inj_id _))/= => ui.
case: (fyzb) => fzy fyzK fzyK.
apply/imfsetP; exists (fzy u) => /=; last by rewrite fzyK.
rewrite (mem_imfset _ _ (@inj_id _))/=.
have {}ui: val u < val (fyz [` pyrP i ir]) by [].
have ur: val u \is Num.real by apply/negP => /negP/(Nreal_ltF fir)/negP.
have fur: val (fzy u) \is Num.real by rewrite fyzr fzyK.
suff: val (fzy u) < ((rootsR (evalpmp y p))`_i)%:C%C by [].
rewrite -(RRe_real fur) ltcR ltNge; apply/negP => iu.
suff: [` pyrP i ir] = fzy u by move=> iuE; move: ui; rewrite iuE fzyK ltxx.
apply/eP.
rewrite /= -(RRe_real fur) -rmorphB/= normcR mulrC mulr_natr -rmorphMn/= ltcR.
apply/ltr_normlP; split; last first.
rewrite -subr_le0 in iu; apply/(le_lt_trans iu).
by rewrite pmulrn_lgt0// -ltcR.
rewrite opprB -(subrBB (complex.Re (val u))) opprB mulr2n; apply/ltrD.
apply/ltr_normlW.
rewrite -ltcR -normcR rmorphB/= (RRe_real fur) (RRe_real ur).
by rewrite -{2}(fzyK u); apply/fyze.
rewrite -(subrBB (complex.Re (val (fyz [` pyrP i ir])))) opprB -(add0r e').
apply/ltrD; first by rewrite subr_lt0; move: ui; rewrite ltcE => /andP[_].
apply/ltr_normlW; rewrite -ltcR -normcR rmorphB/= [X in X - _]RRe_real.
by rewrite -normrN opprB; apply/(fyze [` pyrP i ir]).
by rewrite -fyzr/=; apply/complex_realP; exists (rootsR (evalpmp y p))`_i.
move=> /imfsetP[/=] v + ->.
rewrite (mem_imfset _ _ (@inj_id _))/= => vi.
have {}vi: val v < ((rootsR (evalpmp y p))`_i)%:C%C by [].
have vr: val v \is Num.real.
apply/negP => /negP vr; move: vi; rewrite Nreal_ltF//.
by apply/complex_realP; exists (rootsR (evalpmp y p))`_i.
rewrite (mem_imfset _ _ (@inj_id _))/=.
suff: val (fyz v) < val (fyz [` pyrP i ir]) by [].
have fvr: val (fyz v) \is Num.real by rewrite -fyzr.
rewrite -(RRe_real fvr) -(RRe_real fir) ltcR ltNge; apply/negP => iv.
suff vE: v = [` pyrP i ir] by rewrite vE/= ltxx in vi.
apply/eP.
rewrite /= -(RRe_real vr) -rmorphB/= normcR mulrC mulr_natr -rmorphMn/= ltcR.
apply/ltr_normlP; split; last first.
rewrite -(RRe_real vr) ltcR -subr_lt0 in vi; apply/(lt_trans vi).
by rewrite pmulrn_lgt0// -ltcR.
rewrite opprB -(subrBB (complex.Re (val (fyz [`pyrP i ir])))) opprB mulr2n.
apply/ltrD.
apply/ltr_normlW; rewrite -ltcR -normcR rmorphB/= (RRe_real fir).
exact/(fyze [` pyrP i ir]).
rewrite -(subrBB (complex.Re (val (fyz v)))) opprB -(add0r e').
apply/ler_ltD; first by rewrite subr_le0.
apply/ltr_normlW; rewrite -ltcR -normcR rmorphB/= (RRe_real fvr) (RRe_real vr).
rewrite -normrN opprB; apply/fyze.
Qed.
Definition SAevalpmp_graph n
(p : {poly {mpoly R[n]}}) : {SAset R^(n + (size p))} :=
[set| \big[And/True]_(i < size p)
subst_formula (rcons (iota 0 n) (n + i)%N) (SAmpoly p`_i)].
Lemma SAevalpmp_graphP n (p : {poly {mpoly R[n]}}) (u : 'rV[R]_n)
(v : 'rV[R]_(size p)) :
(row_mx u v \in SAevalpmp_graph p) = (v == \row_i (evalpmp u p)`_i).
Proof.
apply/SAin_setP/eqP => [/holdsAnd /= vE|->].
apply/rowP => i; rewrite mxE coef_map/=.
move: vE => /(_ i (mem_index_enum _) isT) /holds_subst.
rewrite enum_ordD map_cat -2!map_comp -cats1 subst_env_cat.
rewrite subst_env_iota_catl/=; last by rewrite size_map size_enum_ord.
rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=.
rewrite subDnCA// subnn addn0 nth_map_ord mxE (unsplitK (inr _)) => vE.
suff: SAmpoly p`_i u = \row__ v ord0 i.
rewrite SAmpolyE => /eqP; rewrite rowPE forall_ord1 !mxE => /eqP /esym ->.
by apply/meval_eq => j; rewrite tnth_mktuple.
apply/eqP; rewrite inSAfun; apply/rcf_satP; move: vE; congr holds.
rewrite ngraph_cat/= enum_ordSl enum_ord0/= mxE; congr cat.
by apply/eq_map => j /=; rewrite mxE (unsplitK (inl _)).
apply/holdsAnd => /= i _ _; apply/holds_subst.
rewrite enum_ordD map_cat -2!map_comp -cats1 subst_env_cat.
rewrite subst_env_iota_catl/=; last by rewrite size_map size_enum_ord.
rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=.
rewrite subDnCA// subnn addn0 nth_map_ord mxE (unsplitK (inr _)) mxE coef_map/=.
move: (SAmpolyE p`_i u) => /eqP; rewrite inSAfun => /rcf_satP; congr holds.
rewrite ngraph_cat/= enum_ordSl enum_ord0/= mxE; congr (_ ++ [:: _]).
by apply/eq_map => j /=; rewrite mxE (unsplitK (inl _)).
by apply/meval_eq => j; rewrite tnth_mktuple.
Qed.
Fact SAfun_SAevalpmp n (p : {poly {mpoly R[n]}}) :
(SAevalpmp_graph p \in @SAfunc _ n (size p))
&& (SAevalpmp_graph p \in @SAtot _ n (size p)).
Proof.
apply/andP; split.
by apply/inSAfunc => u y1 y2; rewrite !SAevalpmp_graphP => /eqP -> /eqP.
apply/inSAtot => u; exists (\row_i (evalpmp u p)`_i)%R.
by rewrite SAevalpmp_graphP eqxx.
Qed.
Definition SAevalpmp n (p : {poly {mpoly R[n]}}) := MkSAfun (SAfun_SAevalpmp p).
Lemma SAevalpmpE n (p : {poly {mpoly R[n]}}) (u : 'rV[R]_n) :
SAevalpmp p u = (\row_i (evalpmp u p)`_i)%R.
Proof. by apply/eqP; rewrite inSAfun SAevalpmp_graphP. Qed.
Lemma evalpmpM n (p q : {poly {mpoly R[n]}}) (x : 'rV_n) :
(evalpmp x (p * q) = (evalpmp x p) * (evalpmp x q))%R.
Proof.
apply/polyP => i.
rewrite !coef_map/= !coefM meval_sum.
apply/eq_bigr => /= j _.
by rewrite mevalM !coef_map.
Qed.
(* TODO: subsumed by `rmorph_prod` (with occurence) *)
Lemma evalpmp_prod [I : Type] n (x : 'rV_n) (r : seq I)
(F : I -> {poly {mpoly R[n]}}) (P : pred I) :
evalpmp x (\prod_(i <- r | P i) F i) = \prod_(i <- r | P i) evalpmp x (F i).
Proof.
elim: r => [|i r IHr].
by apply/polyP => i; rewrite !big_nil/= coef_map/= !coef1 mevalMn meval1.
rewrite !big_cons; case: (P i) => [|//].
by rewrite evalpmpM IHr.
Qed.
Lemma evalpmp_prod_const n (P : {fset {poly {mpoly R[n]}}}) (s : {SAset R^n}) :
SAconnected s ->
{in P, forall p,
{in s &, forall x y, size (evalpmp x p) = size (evalpmp y p)}} ->
{in P, forall p, {in s &, forall x y,
size (gcdp (evalpmp x p) (evalpmp x p)^`())
= size (gcdp (evalpmp y p) (evalpmp y p)^`())}} ->
{in P &, forall p q, {in s &, forall x y,
size (gcdp (evalpmp x p) (evalpmp x q))
= size (gcdp (evalpmp y p) (evalpmp y q))}} ->
{in s &, forall x y,
size (gcdp (evalpmp x (\prod_(p : P) (val p)))
(evalpmp x (\prod_(p : P) (val p)))^`())
= size (gcdp (evalpmp y (\prod_(p : P) (val p)))
(evalpmp y (\prod_(p : P) (val p)))^`())} /\
{in s &, forall x y,
size (rootsR (evalpmp x (\prod_(p : P) (val p))))
= size (rootsR (evalpmp y (\prod_(p : P) (val p))))}.
Proof.
move=> Scon psize proots pqsize.
apply/all_and2 => x; apply/all_and2 => y; apply/all_and2 => xs; apply/all_and2.
case: n P s Scon psize proots pqsize x y xs
=> [|n] P s Scon psize proots pqsize x y xS yS.
by have ->: x = y by apply/rowP => -[].
case: (eqVneq (evalpmp x (\prod_(p : P) val p)) 0) => px0.
rewrite px0.
move: px0; rewrite !evalpmp_prod => /eqP/prodf_eq0/= [p] _.
rewrite -size_poly_eq0 (psize (val p) (fsvalP p) x y xS yS) size_poly_eq0.
move=> py0.
suff ->: \prod_(p : P) evalpmp y (val p) = 0 by [].
by apply/eqP/prodf_eq0; exists p.
have p0: {in P, forall p, {in s, forall x, size (evalpmp x p) != 0}}.
move=> p pP z zS; rewrite (psize _ pP z x zS xS) size_poly_eq0.
by move: px0; rewrite evalpmp_prod => /prodf_neq0/(_ [` pP] isT).
have R0: [char R[i]] =i pred0 by apply/char_num.
have pmsize: {in s &, forall x y,
size (evalpmp x (\prod_(p : P) \val p))
= size (evalpmp y (\prod_(p : P) \val p))}.
move=> {px0} {}x {}y {}xS {}yS.
rewrite !evalpmp_prod size_prod; last first.
by move=> /= p _; rewrite -size_poly_eq0 (p0 _ (fsvalP p) x xS).
rewrite size_prod; last first.
by move=> /= p _; rewrite -size_poly_eq0 (p0 _ (fsvalP p) y yS).
under eq_bigr => /= p _.
rewrite (psize _ (fsvalP p) x y xS yS).
over.
by [].
have rE (u : 'rV[R]_n.+1) :
(size (rootsR (evalpmp u (\prod_(p : P) \val p))))%:R
= SAcomp (SAnbroots _ _) (SAevalpmp (\prod_(p : P) \val p)) u ord0 ord0.
rewrite SAcompE/= SAevalpmpE SAnbrootsE mxE.
congr (size (rootsR _))%:R.
apply/polyP => i; rewrite coef_poly.
case: ltnP => ilt; last first.
exact/nth_default/(leq_trans (size_poly _ _) ilt).
by rewrite -/(nat_of_ord (Ordinal ilt)) nth_map_ord mxE.
have cE (u : 'rV[R]_n.+1) :
(size (dec_roots
(map_poly (real_complex R) (evalpmp u (\prod_(p : P) \val p)))))%:R
= SAcomp (SAnbrootsC _ _) (SAevalpmp (\prod_(p : P) \val p)) u ord0 ord0.
rewrite SAcompE/= SAevalpmpE SAnbrootsCE mxE.
congr (size (dec_roots _))%:R.
apply/polyP => i; rewrite !coef_poly.
case: ltnP => ilt; last first.
case: ltnP => [|//] ilt'.
by rewrite (nth_mktuple _ _ (Ordinal ilt')) mxE nth_default.
case: ltnP => [|//] ilt'.
by rewrite (nth_mktuple _ _ (Ordinal ilt')) mxE coef_map/=.
suff: locally_constant (SAcomp (SAnbroots _ _)
(SAevalpmp (\prod_(p : P) \val p))) [set` s]
/\ locally_constant (SAcomp (SAnbrootsC _ _)
(SAevalpmp (\prod_(p : P) \val p))) [set` s].
move=> [] rc cc; split; last first.
apply/(mulrIn (@oner_neq0 R)).
rewrite !rE; congr (_ _ ord0 ord0).
by move: {px0} x y xS yS; apply/SAconnected_locally_constant_constant.
move: cc => /(SAconnected_locally_constant_constant Scon)-/(_ x y xS yS).
move=> /(congr1 (fun x : 'rV_1 => x ord0 ord0)).
rewrite -!cE => /(mulrIn (@oner_neq0 R)).
rewrite size_dec_roots// [in RHS]size_dec_roots//.
rewrite size_divp; last by rewrite gcdp_eq0 map_poly_eq0 negb_and px0.
rewrite size_divp; last first.
rewrite gcdp_eq0 map_poly_eq0 -size_poly_eq0 (pmsize y x yS xS) negb_and.
by rewrite size_poly_eq0 px0.
rewrite !deriv_map/= -!gcdp_map !size_map_poly.
rewrite subn_pred ?leq_gcdpl//; last first.
by rewrite lt0n size_poly_eq0 gcdp_eq0 negb_and px0.
rewrite subn_pred ?leq_gcdpl//; last first.
- by rewrite -size_poly_eq0 (pmsize y x yS xS) size_poly_eq0 px0.
- rewrite lt0n size_poly_eq0 gcdp_eq0 negb_and.
by rewrite -size_poly_eq0 (pmsize y x yS xS) size_poly_eq0 px0.
rewrite !succnK (pmsize x y xS yS) => /eqP.
rewrite eqn_sub2lE; first by move=> /eqP.
by rewrite (pmsize y x yS xS) leq_gcdpl.
by rewrite leq_gcdpl// -size_poly_eq0 (pmsize y x yS xS) size_poly_eq0 px0.
move=> {x y xS yS px0}.
apply/all_and2 => x; apply/all_and2; rewrite inE/= => xs.
have ex_and: forall T (P Q : T -> Prop),
(exists x, P x /\ Q x) -> (exists x, P x) /\ (exists x, Q x).
move=> T P0 Q [] a [] Pa Qa.
by split; exists a.
apply/ex_and.
pose pc := fun (p : P) (x : 'rV[R]_n.+1) =>
map_poly (real_complex R) (evalpmp x (\val p)).
pose rx := dec_roots (\prod_(p : P) pc p x).
pose d := (\big[Order.min/1]_(x <- rx) \big[Order.min/1]_(y <- rx | y != x)
(complex.Re `|x - y| / 2))%:C%C.
have d0 : 0 < d.
rewrite ltcE/= eqxx/= lt_bigmin ltr01/=; apply/allP => u _.
rewrite -big_filter lt_bigmin ltr01/=; apply/allP => v.
rewrite mem_filter => /andP[] vu _.
apply/divr_gt0; last exact/ltr0Sn.
by rewrite -ltcR (normr_gt0 (u - v)) subr_eq0 eq_sym.
have /= dP: {in rx &, forall u v, (`|u - v| < 2*d)%R -> u = v}.
move=> u v ux vx uvd; apply/eqP; rewrite -[_ == _]negbK; apply/negP => uv.
move: uvd.
rewrite mulrC mulr_natr -rmorphMn/= -(RRe_real (normr_real _)) ltcR.
rewrite -mulr_natr.
rewrite -ltr_pdivrMr ?ltr0Sn// lt_bigmin => /andP[_] /allP-/(_ u ux) /=.
rewrite lt_bigmin => /andP[_] /allP-/(_ v vx) /implyP.
by rewrite eq_sym ltxx => /(_ uv).
have /fin_all_exists /=:
forall p : P, exists delta, 0 < delta
/\ forall (y : 'rV[R]_n.+1), y \in s -> `|x - y| < delta ->
alignp d (pc p x) (pc p y).
move=> p.
case: (aligned_deformed (pc p x) d0) => /= [[]] e eI [].
rewrite ltcE/= => /andP[/eqP ->] e0; rewrite complexr0 => ed.
have /fin_all_exists /=:
forall i : 'I_(size (val p)).+1, exists delta, 0 < delta
/\ forall (y : 'rV[R]_n.+1), y \in s -> `|x - y| < delta ->
`|(pc p x)`_i - (pc p y)`_i| < e%:C%C.
move=> i.
move: (@meval_continuous _ _ (val p)`_i x).
rewrite /= /continuous_at.
move=> /(@cvgr_dist_lt _ R^o).
move=> /(_ _ e0) /nbhs_ballP[] d'/= d'0 /subsetP xd'.
exists d'; split=> // y ys xy.
move: xd' => /(_ y); mp; first by rewrite -ball_normE inE/=.
rewrite inE/= !coef_map/= -rmorphB/= normc_def/= expr0n/= addr0 sqrtr_sqr.
rewrite ltcR.
by congr (normr (_ - _) < e); apply/meval_eq => j; rewrite tnth_mktuple.
move=> [d'] d'P; exists (\big[minr/1]_i d' i).
split; first by rewrite lt_bigmin ltr01; apply/allP => i _ /=; case: (d'P i).
move=> y ys; rewrite lt_bigmin => /andP[_] /allP xy; apply/ed.
split=> [|i].
suff ->: size (pc p y) = size (pc p x) by [].
by rewrite !size_map_poly; apply/psize => //; apply/fsvalP.
move: (ltn_ord i); rewrite [X in (i < X)%N]size_map_poly => ilt.
have {}ilt := leq_trans (leq_trans ilt (size_poly _ _)) (leqnSn _).
case: (d'P (Ordinal ilt)) => _ /=; apply=> //.
exact/xy/mem_index_enum.
move=> [d'] xd'.
have d'0: 0 < \big[minr/1]_(p : P) d' p.
rewrite lt_bigmin ltr01; apply/allP => p _ /=.
by case: (xd' p).
exists (ball x (\big[Order.min/1]_(p : P) d' p)).
have andxx (a b c : Prop) : a /\ b /\ c -> (a /\ b) /\ (a /\ c).
by move=> [] ? [] ? ?.
apply/andxx; split; first exact/open_subspaceW/ball_open.
apply/andxx; split; first by rewrite inE; apply ballxx.
apply/all_and2 => y; rewrite in_setI.
apply/all_and2 => /andP[]; rewrite inE/= => ys.
rewrite -ball_normE inE/= lt_bigmin => /andP[_] /allP/= xy.
pose rs := fun x => [fset x in (rootsR (evalpmp x (\prod_(p : P) \val p)))].
have card_rs z :
#|` rs z | = size (rootsR (evalpmp z (\prod_(p : P) \val p))).
by rewrite /rs card_imfset//= undup_id// uniq_roots.
have pc0 p z: z \in s -> pc p z != 0.
by rewrite map_poly_eq0 -size_poly_eq0; apply/p0 => //; apply/fsvalP.
have pcM0 z: z \in s -> \prod_(p : P) pc p z != 0.
by move=> zs; apply/prodf_neq0 => /= p _; apply/pc0.
have: exists (fxy : forall p,
[fset x in dec_roots (pc p x)] -> [fset x in dec_roots (pc p y)]),
forall p u, `|val u - val (fxy p u)| < d.
apply/(fin_all_exists (P:=fun p f => forall u, `|val u - val (f u)| < d)).
move=> /= p; apply/(fin_all_exists (P:=fun u v => `|val u - val v| < d)).
case=> /= u; rewrite mem_imfset//= mem_dec_roots => /andP[_] pu.
move: xy => /(_ p (mem_index_enum _)).
move: xd' => /(_ p)[_] /(_ y ys) /[apply] /(_ u pu).
rewrite -big_filter; case rsy: (seq.filter _ _) => [|v l].
by rewrite big_nil leqn0 mu_eq0 ?pu// pc0.
move: (mem_head v l).
rewrite -rsy mem_filter -normrN opprB => /andP[] uv pv _.
suff vP: v \in [fset x in dec_roots (pc p y)].
by exists [` vP].
by rewrite mem_imfset//= mem_dec_roots pc0.
move=> [/=] fxy fxyd.
have fxy_bij: forall p, bijective (fxy p).
move=> p; apply/inj_card_bij; last first.
rewrite -2!cardfE card_imfset//= card_imfset//=.
do 2 rewrite undup_id ?uniq_dec_roots//.
rewrite (size_dec_roots (pc p x) R0) (size_dec_roots (pc p y) R0).
rewrite size_divp; last by rewrite gcdp_eq0 negb_and pc0.
rewrite size_divp; last by rewrite gcdp_eq0 negb_and pc0.
rewrite ![(pc _ _)^`()]deriv_map -!gcdp_map !size_map_poly -!/(evalpmp _ _).
rewrite (psize (val p) (fsvalP p) x y xs ys).
by rewrite (proots (val p) (fsvalP p) x y xs ys).
move=> /= u v => uv; apply/val_inj/dP.
- move: (fsvalP u); rewrite (mem_imfset _ _ (@inj_id _))/=.
rewrite mem_dec_roots => /andP[_] pu.
rewrite /rx mem_dec_roots pcM0//= root_bigmul/=.
by apply/hasP; exists p => //; apply/mem_index_enum.
- move: (fsvalP v); rewrite (mem_imfset _ _ (@inj_id _))/=.
rewrite mem_dec_roots => /andP[_] pv.
rewrite /rx mem_dec_roots pcM0//= root_bigmul/=.
by apply/hasP; exists p => //; apply/mem_index_enum.
- rewrite -(subrBB (val (fxy p u))) {2}uv.
apply/(le_lt_trans (ler_normB _ _)).
by rewrite mulr2n mulrDl mul1r; apply/ltrD; apply/fxyd.
have: exists (fyx : forall p,
[fset x in dec_roots (pc p y)] -> [fset x in dec_roots (pc p x)]),
forall p, cancel (fxy p) (fyx p) /\ cancel (fyx p) (fxy p).
apply/(fin_all_exists (P:=fun p f => cancel (fxy p) f /\ cancel f (fxy p))).
move=> /= p.
by case: (fxy_bij p) => g; exists g.
move=> [] fyx fK.
have fxyK p : cancel (fxy p) (fyx p) by case: (fK p).
have {fK} fyxK p : cancel (fyx p) (fxy p) by case: (fK p).
have fyxd p (u : [fset x in dec_roots (pc p y)]) :
`|val u - val (fyx p u)| < d.
move: (fyxK p u) => /(congr1 val)/= uE.
by rewrite -{1}uE -normrN opprB; apply/fxyd.
have lift p z (u : [fset x in dec_roots (pc p z)]) :
z \in s ->
val u \in [fset x in dec_roots (\prod_(p : P) pc p z)].
case: u => /= u; rewrite mem_imfset//= mem_dec_roots => /andP[_] pu zs.