Degrees of Polynomials
Degrees of polynomials over a ring
Let R be a ring and write R[x] for the ring of polynomials over R.
The length of a polynomial is the number of its coefficients. This is
a syntactical property, as the highest coefficient may be 0. Note that
the `zero' polynomial cpoly_zero has length 0,
a constant polynomial has length 1 and so forth. So the length
is always 1 higher than the `degree' (assuming that the highest
coefficient is [#]0)!
Fixpoint lth_of_poly (p : R[x]) : N :=
match p with
| cpoly_zero => 0
| cpoly_linear d q => S (lth_of_poly q)
end.
When dealing with constructive polynomials, notably over the reals or
complex numbers, the degree may be unknown, as we can not decide
whether the highest coefficient is [#]0. Hence,
degree is a relation between polynomials and natural numbers; if the
degree is unknown for polynomial p, degree(n,p) doesn't hold for
any n. If we don't know the degree of p, we may still
know it to be below or above a certain number. E.g. for the polynomial
p0 +p1 X + ... + p(n-1)
X^(n-1), if pi apart from 0, we can say that the
`degree is at least i' and if p(j+1)
= ... =pn =0 (with n the length of the polynomial), we can say
that the `degree is at most j'.
Definition degree_le n (p : R[x]) : Prop := forall m, n < m -> nth_coeff m p [=] 0.
Definition degree n (p : R[x]) : CProp := nth_coeff n p [#] 0 and degree_le n p.
Definition monic n (p : R[x]) : Prop := nth_coeff n p [=] 1 /\ degree_le n p.
Definition odd_cpoly (p : R[x]) : CProp := {n : N | Codd n | degree n p}.
Definition even_cpoly (p : R[x]) : CProp := {n : N | Ceven n | degree n p}.
Definition regular (p : R[x]) : CProp := {n : N | degree n p}.
End Degree_def.
Section Degree_props.
Variable R : CRing.
Lemma degree_le_wd : forall (p p' : R[x]) n,
p [=] p' -> degree_le n p -> degree_le n p'.
Lemma degree_wd : forall (p p' : R[x]) n, p [=] p' -> degree n p -> degree n p'.
Lemma monic_wd : forall (p p' : R[x]) n, p [=] p' -> monic n p -> monic n p'.
Lemma degree_imp_degree_le : forall (p : R[x]) n, degree n p -> degree_le n p.
Lemma degree_le_c_ : forall c : R, degree_le 0 (_C_ c).
Lemma degree_c_ : forall c : R, c [#] 0 -> degree 0 (_C_ c).
Lemma monic_c_one : monic 0 (_C_ (1:R)).
Lemma degree_le_x_ : degree_le 1 (_X_:RX).
Lemma degree_x_ : degree 1 (_X_:RX).
Lemma monic_x_ : monic 1 (_X_:RX).
Lemma degree_le_mon : forall (p : R[x]) m n,
m <= n -> degree_le m p -> degree_le n p.
Lemma degree_le_inv : forall (p : R[x]) n, degree_le n p -> degree_le n [--]p.
Lemma degree_le_plus : forall (p q : R[x]) n,
degree_le n p -> degree_le n q -> degree_le n (p[+]q).
Lemma degree_le_minus : forall (p q : R[x]) n,
degree_le n p -> degree_le n q -> degree_le n (p[-]q).
Lemma Sum_degree_le : forall (f : N -> R[x]) (n k l : N), k <= S l ->
(forall i, k <= i -> i <= l -> degree_le n (f i)) -> degree_le n (∑ k l f).
Lemma degree_inv : forall (p : R[x]) (n : N), degree n p -> degree n [--]p.
Lemma degree_plus_rht : forall (p q : R[x]) m n,
degree_le m p -> degree n q -> m < n -> degree n (p[+]q).
Lemma degree_minus_lft : forall (p q : R[x]) m n,
degree_le m p -> degree n q -> m < n -> degree n (q[-]p).
Lemma monic_plus : forall (p q : R[x]) m n,
degree_le m p -> monic n q -> m < n -> monic n (p[+]q).
Lemma monic_minus : forall (p q : R[x]) m n,
degree_le m p -> monic n q -> m < n -> monic n (q[-]p).
Lemma degree_le_mult : forall (p q : R[x]) m n,
degree_le m p -> degree_le n q -> degree_le (m + n) (p[*]q).
Lemma degree_mult_aux : forall (p q : R[x]) m n, degree_le m p -> degree_le n q ->
nth_coeff (m + n) (p[*]q) [=] nth_coeff m p[*]nth_coeff n q.
Lemma monic_mult : forall (p q : R[x]) m n,
monic m p -> monic n q -> monic (m + n) (p[*]q).
Lemma degree_le_nexp : forall (p : R[x]) m n,
degree_le m p -> degree_le (m * n) (p[^]n).
Lemma monic_nexp : forall (p : R[x]) m n, monic m p -> monic (m * n) (p[^]n).
Lemma lt_i_lth_of_poly : forall i (p : R[x]),
nth_coeff i p [#] 0 -> i < lth_of_poly p.
Lemma poly_degree_lth : forall p : R[x], degree_le (lth_of_poly p) p.
Lemma Cpoly_ex_degree : forall p : R[x], {n : N | degree_le n p}.
Lemma poly_as_sum'' : forall (p : R[x]) n,
degree_le n p -> p [=] ∑ 0 n (fun i => _C_ (nth_coeff i p) [*]_X_[^]i).
Lemma poly_as_sum' : forall p : R[x],
p [=] ∑ 0 (lth_of_poly p) (fun i => _C_ (nth_coeff i p) [*]_X_[^]i).
Lemma poly_as_sum : forall (p : R[x]) n, degree_le n p ->
forall x, p ! x [=] ∑ 0 n (fun i => nth_coeff i p[*]x[^]i).
Lemma degree_le_zero : forall p : R[x], degree_le 0 p -> {a : R | p [=] _C_ a}.
Lemma degree_le_1_imp : forall p : R[x],
degree_le 1 p -> {a : R | {b : R | p [=] _C_ a[*]_X_[+]_C_ b}}.
Lemma degree_le_cpoly_linear : forall (p : cpoly R) c n,
degree_le (S n) (c[+X*]p) -> degree_le n p.
Lemma monic_cpoly_linear : forall (p : cpoly R) c n, monic (S n) (c[+X*]p) -> monic n p.
Lemma monic_one : forall (p : cpoly R) c, monic 1 (c[+X*]p) -> forall x, p ! x [=] 1.
Lemma monic_apzero : forall (p : R[x]) n, monic n p -> p [#] 0.
End Degree_props.
Section degree_props_Field.
Degrees of polynomials over a field
Let F be a field and write F[x] for the ring of polynomials over F.Variable F : CField.
Lemma degree_mult : forall (p q : F[x]) m n,
degree m p -> degree n q -> degree (m + n) (p[*]q).
Lemma degree_nexp : forall (p : F[x]) m n, degree m p -> degree (m * n) (p[^]n).
Lemma degree_le_mult_imp : forall (p q : F[x]) m n,
degree m p -> degree_le (m + n) (p[*]q) -> degree_le n q.
Lemma degree_mult_imp : forall (p q : F[x]) m n,
degree m p -> degree (m + n) (p[*]q) -> degree n q.
End degree_props_Field.