-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathpolyorder.v
272 lines (226 loc) · 9.53 KB
/
polyorder.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
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
From mathcomp
Require Import ssralg poly ssrnum zmodp polydiv interval.
Import GRing.Theory.
Import Num.Theory.
Import Pdiv.Idomain.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Section Multiplicity.
Variable R : idomainType.
Implicit Types x y c : R.
Implicit Types p q r d : {poly R}.
(* Definition multiplicity (x : R) (p : {poly R}) : nat := *)
(* (odflt ord0 (pick (fun i : 'I_(size p).+1 => ((('X - x%:P) ^+ i %| p)) *)
(* && (~~ (('X - x%:P) ^+ i.+1 %| p))))). *)
(* Notation "'\mu_' x" := (multiplicity x) *)
(* (at level 8, format "'\mu_' x") : ring_scope. *)
(* Lemma mu0 : forall x, \mu_x 0 = 0%N. *)
(* Proof. *)
(* by move=> x; rewrite /multiplicity; case: pickP=> //= i; rewrite !dvdp0. *)
(* Qed. *)
(* Lemma muP : forall p x, p != 0 -> *)
(* (('X - x%:P) ^+ (\mu_x p) %| p) && ~~(('X - x%:P) ^+ (\mu_x p).+1 %| p). *)
(* Proof. *)
(* move=> p x np0; rewrite /multiplicity; case: pickP=> //= hp. *)
(* have {hp} hip: forall i, i <= size p *)
(* -> (('X - x%:P) ^+ i %| p) -> (('X - x%:P) ^+ i.+1 %| p). *)
(* move=> i; rewrite -ltnS=> hi; move/negbT: (hp (Ordinal hi)). *)
(* by rewrite -negb_imply negbK=> /implyP. *)
(* suff: forall i, i <= size p -> ('X - x%:P) ^+ i %| p. *)
(* move=> /(_ _ (leqnn _)) /(size_dvdp np0). *)
(* rewrite -[size _]prednK; first by rewrite size_exp size_XsubC mul1n ltnn. *)
(* by rewrite lt0n size_poly_eq0 expf_eq0 polyXsubC_eq0 lt0n size_poly_eq0 np0. *)
(* elim=> [|i ihi /ltnW hsp]; first by rewrite expr0 dvd1p. *)
(* by rewrite hip // ihi. *)
(* Qed. *)
(* Lemma cofactor_XsubC : forall p a, p != 0 -> *)
(* exists2 q : {poly R}, (~~ root q a) & p = q * ('X - a%:P) ^+ (\mu_a p). *)
(* Proof. *)
(* move=> p a np0. *)
Definition multiplicity (x : R) (p : {poly R}) :=
if p == 0 then 0%N else sval (multiplicity_XsubC p x).
Notation "'\mu_' x" := (multiplicity x)
(at level 8, format "'\mu_' x") : ring_scope.
Lemma mu_spec p a : p != 0 ->
{ q : {poly R} & (~~ root q a)
& ( p = q * ('X - a%:P) ^+ (\mu_a p)) }.
Proof.
move=> nz_p; rewrite /multiplicity -if_neg.
by case: (_ p a) => m /=/sig2_eqW[q]; rewrite nz_p; exists q.
Qed.
Lemma mu0 x : \mu_x 0 = 0%N.
Proof. by rewrite /multiplicity {1}eqxx. Qed.
Lemma root_mu p x : ('X - x%:P) ^+ (\mu_x p) %| p.
Proof.
case p0: (p == 0); first by rewrite (eqP p0) mu0 expr0 dvd1p.
case: (@mu_spec p x); first by rewrite p0.
by move=> q qn0 hp //=; rewrite {2}hp dvdp_mulIr.
Qed.
(* Lemma size_exp_XsubC : forall x n, size (('X - x%:P) ^+ n) = n.+1. *)
(* Proof. *)
(* move=> x n; rewrite -[size _]prednK ?size_exp ?size_XsubC ?mul1n //. *)
(* by rewrite ltnNge leqn0 size_poly_eq0 expf_neq0 // polyXsubC_eq0. *)
(* Qed. *)
Lemma root_muN p x : p != 0 ->
(('X - x%:P)^+(\mu_x p).+1 %| p) = false.
Proof.
move=> pn0; case: (mu_spec x pn0)=> q qn0 hp /=.
rewrite {2}hp exprS dvdp_mul2r; last first.
by rewrite expf_neq0 // polyXsubC_eq0.
apply: negbTE; rewrite -eqp_div_XsubC; apply: contra qn0.
by move/eqP->; rewrite rootM root_XsubC eqxx orbT.
Qed.
Lemma root_le_mu p x n : p != 0 -> ('X - x%:P)^+n %| p = (n <= \mu_x p)%N.
Proof.
move=> pn0; case: leqP=> hn; last apply/negP=> hp.
apply: (@dvdp_trans _ (('X - x%:P) ^+ (\mu_x p))); last by rewrite root_mu.
by rewrite dvdp_Pexp2l // size_XsubC.
suff : ('X - x%:P) ^+ (\mu_x p).+1 %| p by rewrite root_muN.
by apply: dvdp_trans hp; rewrite dvdp_Pexp2l // size_XsubC.
Qed.
Lemma muP p x n : p != 0 ->
(('X - x%:P)^+n %| p) && ~~(('X - x%:P)^+n.+1 %| p) = (n == \mu_x p).
Proof. by move=> hp0; rewrite !root_le_mu; case: (ltngtP n (\mu_x p))=> hn. Qed.
Lemma mu_gt0 p x : p != 0 -> (0 < \mu_x p)%N = root p x.
Proof. by move=> pn0; rewrite -root_le_mu// expr1 root_factor_theorem. Qed.
Lemma muNroot p x : ~~ root p x -> \mu_x p = 0%N.
Proof.
case p0: (p == 0); first by rewrite (eqP p0) rootC eqxx.
by move=> pnx0; apply/eqP; rewrite -leqn0 leqNgt mu_gt0 ?p0.
Qed.
Lemma mu_polyC c x : \mu_x (c%:P) = 0%N.
Proof.
case c0: (c == 0); first by rewrite (eqP c0) mu0.
by apply: muNroot; rewrite rootC c0.
Qed.
Lemma cofactor_XsubC_mu x p n :
~~ root p x -> \mu_x (p * ('X - x%:P) ^+ n) = n.
Proof.
move=> p0; apply/eqP; rewrite eq_sym -muP//; last first.
apply: contra p0; rewrite mulf_eq0 expf_eq0 polyXsubC_eq0 andbF orbF.
by move/eqP->; rewrite root0.
rewrite dvdp_mulIr /= exprS dvdp_mul2r -?root_factor_theorem //.
by rewrite expf_eq0 polyXsubC_eq0 andbF //.
Qed.
Lemma mu_mul p q x : p * q != 0 ->
\mu_x (p * q) = (\mu_x p + \mu_x q)%N.
Proof.
move=>hpqn0; apply/eqP; rewrite eq_sym -muP//.
rewrite exprD dvdp_mul ?root_mu//=.
move:hpqn0; rewrite mulf_eq0 negb_or; case/andP=> hp0 hq0.
move: (mu_spec x hp0)=> [qp qp0 hp].
move: (mu_spec x hq0)=> [qq qq0 hq].
rewrite {2}hp {2}hq exprS exprD !mulrA [qp * _ * _]mulrAC.
rewrite !dvdp_mul2r ?expf_neq0 ?polyXsubC_eq0 // -eqp_div_XsubC.
move: (mulf_neq0 qp0 qq0); rewrite -hornerM; apply: contra; move/eqP->.
by rewrite hornerM hornerXsubC subrr mulr0.
Qed.
Lemma mu_XsubC x : \mu_x ('X - x%:P) = 1%N.
Proof.
apply/eqP; rewrite eq_sym -muP; last by rewrite polyXsubC_eq0.
by rewrite expr1 dvdpp/= -{2}[_ - _]expr1 dvdp_Pexp2l // size_XsubC.
Qed.
Lemma mu_mulC c p x : c != 0 -> \mu_x (c *: p) = \mu_x p.
Proof.
move=> cn0; case p0: (p == 0); first by rewrite (eqP p0) scaler0.
by rewrite -mul_polyC mu_mul ?mu_polyC// mulf_neq0 ?p0 ?polyC_eq0.
Qed.
Lemma mu_opp p x : \mu_x (-p) = \mu_x p.
Proof.
rewrite -mulN1r -polyC1 -polyC_opp mul_polyC mu_mulC //.
by rewrite -oppr0 (inj_eq (inv_inj (@opprK _))) oner_eq0.
Qed.
Lemma mu_exp p x n : \mu_x (p ^+ n) = (\mu_x p * n)%N.
Proof.
elim: n p => [|n ihn] p; first by rewrite expr0 mu_polyC muln0.
case p0: (p == 0); first by rewrite (eqP p0) exprS mul0r mu0 mul0n.
by rewrite exprS mu_mul ?ihn ?mulnS// mulf_eq0 expf_eq0 p0 andbF.
Qed.
Lemma mu_addr p q x : p != 0 -> (\mu_x p < \mu_x q)%N ->
\mu_x (p + q) = \mu_x p.
Proof.
move=> pn0 mupq.
have pqn0 : p + q != 0.
move: mupq; rewrite ltnNge; apply: contra.
by rewrite -[q]opprK subr_eq0; move/eqP->; rewrite opprK mu_opp leqnn.
have qn0: q != 0 by move: mupq; apply: contraL; move/eqP->; rewrite mu0 ltn0.
case: (mu_spec x pn0)=> [qqp qqp0] hp.
case: (mu_spec x qn0)=> [qqq qqq0] hq.
rewrite hp hq -(subnK (ltnW mupq)).
rewrite mu_mul ?mulf_eq0; last first.
rewrite expf_eq0 polyXsubC_eq0 andbF orbF.
by apply: contra qqp0; move/eqP->; rewrite root0.
rewrite mu_exp mu_XsubC mul1n [\mu_x qqp]muNroot // add0n.
rewrite exprD mulrA -mulrDl mu_mul; last first.
by rewrite mulrDl -mulrA -exprD subnK 1?ltnW // -hp -hq.
rewrite muNroot ?add0n ?mu_exp ?mu_XsubC ?mul1n //.
rewrite rootE !hornerE horner_exp hornerXsubC subrr.
by rewrite -subnSK // subnS exprS mul0r mulr0 addr0.
Qed.
Lemma mu_addl p q x : q != 0 -> (\mu_x p > \mu_x q)%N ->
\mu_x (p + q) = \mu_x q.
Proof. by move=> q0 hmu; rewrite addrC mu_addr. Qed.
Lemma mu_div p x n : (n <= \mu_x p)%N ->
\mu_x (p %/ ('X - x%:P) ^+ n) = (\mu_x p - n)%N.
Proof.
move=> hn.
case p0: (p == 0); first by rewrite (eqP p0) div0p mu0 sub0n.
case: (@mu_spec p x); rewrite ?p0 // => q hq hp.
rewrite {1}hp -{1}(subnK hn) exprD mulrA.
rewrite Pdiv.IdomainMonic.mulpK; last by apply: monic_exp; apply: monicXsubC.
rewrite mu_mul ?mulf_eq0 ?expf_eq0 ?polyXsubC_eq0 ?andbF ?orbF; last first.
by apply: contra hq; move/eqP->; rewrite root0.
by rewrite mu_exp muNroot // add0n mu_XsubC mul1n.
Qed.
End Multiplicity.
Notation "'\mu_' x" := (multiplicity x)
(at level 8, format "'\mu_' x") : ring_scope.
Section PolyrealIdomain.
(*************************************************************************)
(* This should be replaced by a 0-characteristic condition + integrality *)
(* and merged into poly and polydiv *)
(*************************************************************************)
Variable R : realDomainType.
Lemma size_deriv (p : {poly R}) : size p^`() = (size p).-1.
Proof.
have [lep1|lt1p] := leqP (size p) 1.
by rewrite {1}[p]size1_polyC // derivC size_poly0 -subn1 (eqnP lep1).
rewrite size_poly_eq // mulrn_eq0 -subn2 -subSn // subn2.
by rewrite lead_coef_eq0 -size_poly_eq0 -(subnKC lt1p).
Qed.
Lemma derivn_poly0 : forall (p : {poly R}) n, (size p <= n)%N = (p^`(n) == 0).
Proof.
move=> p n; apply/idP/idP.
move=> Hpn; apply/eqP; apply/polyP=>i; rewrite coef_derivn.
rewrite nth_default; first by rewrite mul0rn coef0.
by apply: leq_trans Hpn _; apply leq_addr.
elim: n {-2}n p (leqnn n) => [m | n ihn [| m]] p.
- by rewrite leqn0; move/eqP->; rewrite derivn0 leqn0 -size_poly_eq0.
- by move=> _; apply: ihn; rewrite leq0n.
- rewrite derivSn => hmn hder; case e: (size p) => [|sp] //.
rewrite -(prednK (ltn0Sn sp)) [(_.-1)%N]lock -e -lock -size_deriv ltnS.
exact: ihn.
Qed.
Lemma mu_deriv : forall x (p : {poly R}), root p x ->
\mu_x (p^`()) = (\mu_x p - 1)%N.
Proof.
move=> x p px0; have [-> | nz_p] := eqVneq p 0; first by rewrite derivC mu0.
have [q nz_qx Dp] := mu_spec x nz_p.
case Dm: (\mu_x p) => [|m]; first by rewrite Dp Dm mulr1 (negPf nz_qx) in px0.
rewrite subn1 Dp Dm !derivCE exprS mul1r mulrnAr -mulrnAl mulrA -mulrDl.
rewrite cofactor_XsubC_mu // rootE !(hornerE, hornerMn) subrr mulr0 add0r.
by rewrite mulrn_eq0.
Qed.
Lemma mu_deriv_root : forall x (p : {poly R}), p != 0 -> root p x ->
\mu_x p = (\mu_x (p^`()) + 1)%N.
Proof.
by move=> x p p0 rpx; rewrite mu_deriv // subn1 addn1 prednK // mu_gt0.
Qed.
End PolyrealIdomain.