begin
Lm1:
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of L
for G being FinSequence
for k being Nat st G = F | (Seg k) & len F = k + 1 holds
( G is FinSequence of L & dom G c= dom F & len G = k & F = G ^ <*(F /. (k + 1))*> )
theorem Th1:
theorem Th2:
theorem Th3:
Lm2:
( Im (1_ F_Complex) = 0 & Im (- (1_ F_Complex)) = 0 & Im (0. F_Complex) = 0 )
Lm3:
for z being Element of F_Complex st Im z = 0 holds
z *' = z
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
begin
Lm4:
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds - (- p) = p
theorem Th9:
Lm5:
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for f being Element of (Polynom-Ring L) st f = p holds
- f = - p
theorem
theorem Th11:
theorem Th12:
:: deftheorem Def1 defines Coeff HURWITZ:def 1 :
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for F being FinSequence of (Polynom-Ring L)
for i being Element of NAT
for b4 being FinSequence of L holds
( b4 = Coeff (F,i) iff ( len b4 = len F & ( for j being Element of NAT st j in dom b4 holds
ex p being Polynomial of L st
( p = F . j & b4 . j = p . i ) ) ) );
theorem Th13:
Lm6:
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L
for p29 being Element of (Polynom-Ring L) st p29 = p2 holds
for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p29 * F)
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
:: deftheorem defines degree HURWITZ:def 2 :
for L being non empty ZeroStr
for p being Polynomial of L holds degree p = (len p) - 1;
Lm7:
for L being non empty ZeroStr
for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L
theorem Th20:
Lm8:
for L being non empty ZeroStr
for p being Polynomial of L st deg p <> - 1 holds
p . (deg p) <> 0. L
Lm9:
for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )
theorem
Lm10:
for L being non empty ZeroStr
for p being Polynomial of L holds deg p >= - 1
theorem Th22:
theorem Th23:
theorem Th24:
Lm11:
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k <> 0 holds
( ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = - ((power L) . (z,k)) & ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L )
Lm12:
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT
for i being Nat st i <> 0 & i <> k holds
((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L
:: deftheorem defines rpoly HURWITZ:def 3 :
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT holds rpoly (k,z) = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)));
theorem
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
:: deftheorem Def4 defines qpoly HURWITZ:def 4 :
for L being non empty well-unital doubleLoopStr
for z being Element of L
for k being Nat
for b4 being Polynomial of L holds
( b4 = qpoly (k,z) iff ( ( for i being Nat st i < k holds
b4 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b4 . i = 0. L ) ) );
theorem
theorem Th32:
theorem Th33:
begin
:: deftheorem Def5 defines div HURWITZ:def 5 :
for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, s being Polynomial of L st s <> 0_. L holds
for b4 being Polynomial of L holds
( b4 = p div s iff ex t being Polynomial of L st
( p = (b4 *' s) + t & deg t < deg s ) );
:: deftheorem defines mod HURWITZ:def 6 :
for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, s being Polynomial of L holds p mod s = p - ((p div s) *' s);
:: deftheorem Def7 defines divides HURWITZ:def 7 :
for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, s being Polynomial of L holds
( s divides p iff p mod s = 0_. L );
theorem Th34:
theorem
theorem
begin
:: deftheorem Def8 defines Hurwitz HURWITZ:def 8 :
for f being Polynomial of F_Complex holds
( f is Hurwitz iff for z being Element of F_Complex st z is_a_root_of f holds
Re z < 0 );
theorem
theorem
theorem Th39:
theorem Th40:
Lm13:
for f, g, h being Polynomial of F_Complex st f = g *' h holds
for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds
x is_a_root_of f
theorem Th41:
:: deftheorem Def9 defines *' HURWITZ:def 9 :
for f, b2 being Polynomial of F_Complex holds
( b2 = f *' iff for i being Element of NAT holds b2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') );
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
Lm14:
for x, xv being Element of COMPLEX
for u, v, uv, vv being Element of REAL st x = u + (v * <i>) & xv = uv + (vv * <i>) holds
(|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv
Lm15:
for x, xv being Element of COMPLEX
for u, v, uv, vv being Element of REAL st x = u + (v * <i>) & xv = uv + (vv * <i>) & uv < 0 holds
( ( u < 0 implies |.(x - xv).| < |.(x + (xv *')).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) )
theorem Th48:
theorem Th49:
theorem Th50:
:: deftheorem defines F* HURWITZ:def 10 :
for f being Polynomial of F_Complex
for z being Element of F_Complex holds F* (f,z) = ((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *'));
theorem Th51:
theorem Th52:
theorem
theorem