(Joint Center)Library polyorder

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import ssralg poly ssrnum zmodp polydiv interval.

Import GRing.Theory.
Import Num.Theory.

Import Pdiv.Idomain.

Set Implicit Arguments.

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)) }.

Lemma mu0 x : \mu_x 0 = 0%N.

Lemma root_mu p x : ('X - x%:P) ^+ (\mu_x p) %| p.

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.

Lemma root_le_mu p x n : p != 0 → ('X - x%:P)^+n %| p = (n \mu_x p)%N.

Lemma muP p x n : p != 0 →
  (('X - x%:P)^+n %| p) && ~~(('X - x%:P)^+n.+1 %| p) = (n == \mu_x p).

Lemma mu_gt0 p x : p != 0 → (0 < \mu_x p)%N = root p x.

Lemma muNroot p x : ~~ root p x\mu_x p = 0%N.

Lemma mu_polyC c x : \mu_x (c%:P) = 0%N.

Lemma cofactor_XsubC_mu x p n :
  ~~ root p x\mu_x (p × ('X - x%:P) ^+ n) = n.

Lemma mu_mul p q x : p × q != 0 →
  \mu_x (p × q) = (\mu_x p + \mu_x q)%N.

Lemma mu_XsubC x : \mu_x ('X - x%:P) = 1%N.

Lemma mu_mulC c p x : c != 0 → \mu_x (c *: p) = \mu_x p.

Lemma mu_opp p x : \mu_x (-p) = \mu_x p.

Lemma mu_exp p x n : \mu_x (p ^+ n) = (\mu_x p × n)%N.

Lemma mu_addr p q x : p != 0 → (\mu_x p < \mu_x q)%N
  \mu_x (p + q) = \mu_x p.

Lemma mu_addl p q x : q != 0 → (\mu_x p > \mu_x q)%N
  \mu_x (p + q) = \mu_x q.

Lemma mu_div p x n : (n \mu_x p)%N
  \mu_x (p %/ ('X - x%:P) ^+ n) = (\mu_x p - n)%N.

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.

Lemma derivn_poly0 : (p : {poly R}) n, (size p n)%N = (p^`(n) == 0).

Lemma mu_deriv : x (p : {poly R}), root p x
  \mu_x (p^`) = (\mu_x p - 1)%N.

Lemma mu_deriv_root : x (p : {poly R}), p != 0 → root p x
  \mu_x p = (\mu_x (p^`) + 1)%N.

End PolyrealIdomain.