Library closed_poly
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice bigop.
Require Import ssralg poly polydiv polyorder fintype.
Require Import ssrcomplements.
Require Import ssralg poly polydiv polyorder fintype.
Require Import ssrcomplements.
This file contains facts about polynomials with coefficients in a closed
field.
In what follows, we pose
p = (X - r1)^+a1 * (X - r2)^+a2 * ... * (X - rn)^+an
root_seq p == the sequence of all roots of polynomial p.
i.e. [:: r1; r1; ...; r2; r2; ...; rn; ... rn]
or a permutation of this sequence
root_seq_uniq p == the sequence of all distinct roots of
polynomial p (i.e the sequence [:: r1; ...; rn])
root_mu_seq p == the sequence of pair off the roots and
their multiplicity in polynomial p.
(i.e the sequence [:: (r1,a1); ... ; (rn,an) ])
root_seq_poly s == the concatenation of the sequences root_mu_seq p
for all polynomials p in the sequence s.
linear_factor_seq p == the sequence of linear factors that appear in the
decomposition of polynomial p. (i.e the sequence
[:: (X - r1)^+a1; ... ; (X - rn)^+an])
Set Implicit Arguments.
Section poly_closedFieldType.
Variable F : closedFieldType.
Import GRing.Theory.
Local Open Scope ring_scope.
Definition root_seq : {poly F} -> seq F :=
let fix loop (p : {poly F}) (n : nat) :=
if n is n.+1 then
if (size p != 1%N) =P true is ReflectT p_neq0
then let x := projT1 (sigW (closed_rootP p p_neq0)) in
x :: loop (p %/ ('X - x%:P)) n
else [::]
else [::]
in fun p => loop p (size p).
Lemma root_root_seq (p : {poly F}) x : p != 0 -> x \in root_seq p = root p x.
Lemma root_seq_cons (p : {poly F}) x s : root_seq p = x :: s ->
s = root_seq (p %/ ('X - x%:P)).
Lemma root_seq_eq (p : {poly F}) :
p = lead_coef p *: \prod_(x <- root_seq p) ('X - x%:P).
Lemma root_seq0 : root_seq 0 = [::].
Lemma size_root_seq p : size (root_seq p) = (size p).-1.
Lemma root_seq_nil (p : {poly F}) : (size p <= 1) = ((root_seq p) == [::]).
Lemma sub_root_div (p q : {poly F}) (Hq : q != 0) :
p %| q -> {subset (root_seq p) <= (root_seq q)} .
Definition root_seq_uniq p := undup (root_seq p).
Lemma prod_XsubC_count (p : {poly F}):
p = (lead_coef p) *:
\prod_(x <- root_seq_uniq p) ('X - x%:P)^+ (count (pred1 x) (root_seq p)).
Lemma count_root_seq p x : count (pred1 x) (root_seq p) = \mu_x p.
Definition root_mu_seq p := [seq (x,(\mu_x p)) | x <- (root_seq_uniq p)].
Lemma root_mu_seq_pos x p : p != 0 -> x \in root_mu_seq p -> 0 < x.2.
Definition root_seq_poly (s : seq {poly F}) := flatten (map root_mu_seq s).
Lemma root_seq_poly_pos x s : (forall p , p \in s -> p !=0) ->
x \in root_seq_poly s -> 0 < x.2.
Definition linear_factor_seq p :=
[seq ('X - x.1%:P)^+x.2 | x <- (root_mu_seq p)].
Lemma monic_linear_factor_seq p : forall q, q \in linear_factor_seq p ->
q \is monic.
Lemma size_linear_factor_leq1 p : forall q, q \in linear_factor_seq p ->
1 < size q.
Lemma coprimep_linear_factor_seq p :
forall (i j : 'I_(size (linear_factor_seq p))),
i != j ->
coprimep (linear_factor_seq p)`_i (linear_factor_seq p)`_j.
Lemma prod_XsubC_mu (p : {poly F}):
p = (lead_coef p) *: \prod_(x <- root_seq_uniq p) ('X - x%:P)^+(\mu_x p).
Lemma monic_prod_XsubC p :
p \is monic -> p = \prod_(x <- root_seq_uniq p) ('X - x%:P)^+(\mu_x p).
Lemma prod_factor (p : {poly F}):
p = (lead_coef p) *: \prod_(x <- linear_factor_seq p) x.
Lemma monic_prod_factor p :
p \is monic -> p = \prod_(x <- linear_factor_seq p) x.
Lemma uniq_root_mu_seq (p : {poly F}) : uniq (root_seq p) ->
forall x, x \in root_mu_seq p -> x.2 = 1%N.
Lemma uniq_root_dvdp p q : q != 0 ->
(uniq (root_seq q)) -> p %| q -> (uniq (root_seq p)).
Lemma root_root_mu_seq p : [seq x.1 | x <- root_mu_seq p] = root_seq_uniq p.
End poly_closedFieldType.
This page has been generated by coqdoc