:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller

::

:: Received January 17, 2013

:: Copyright (c) 2013-2016 Association of Mizar Users

registration

ex b_{1} being Polynomial of F_Complex st b_{1} is Hurwitz
end;

cluster Relation-like NAT -defined the carrier of F_Complex -valued Function-like V11() V14( NAT ) V18( NAT , the carrier of F_Complex) complex-valued finite-Support Hurwitz for Element of K19(K20(NAT, the carrier of F_Complex));

existence ex b

proof end;

Lm1: (2 * 0) + 1 = 1

;

theorem Th3: :: HURWITZ2:3

for L being non empty right_complementable add-associative right_zeroed distributive associative doubleLoopStr

for k being even Element of NAT

for x being Element of L holds (power L) . ((- x),k) = (power L) . (x,k)

for k being even Element of NAT

for x being Element of L holds (power L) . ((- x),k) = (power L) . (x,k)

proof end;

theorem Th4: :: HURWITZ2:4

for L being non empty right_complementable add-associative right_zeroed distributive associative doubleLoopStr

for k being odd Element of NAT

for x being Element of L holds (power L) . ((- x),k) = - ((power L) . (x,k))

for k being odd Element of NAT

for x being Element of L holds (power L) . ((- x),k) = - ((power L) . (x,k))

proof end;

theorem Th5: :: HURWITZ2:5

for k being even Element of NAT

for x being Element of F_Complex st Re x = 0 holds

Im ((power F_Complex) . (x,k)) = 0

for x being Element of F_Complex st Re x = 0 holds

Im ((power F_Complex) . (x,k)) = 0

proof end;

theorem Th6: :: HURWITZ2:6

for k being odd Element of NAT

for x being Element of F_Complex st Re x = 0 holds

Re ((power F_Complex) . (x,k)) = 0

for x being Element of F_Complex st Re x = 0 holds

Re ((power F_Complex) . (x,k)) = 0

proof end;

definition

let L be non empty ZeroStr ;

let p be sequence of L;

ex b_{1} being sequence of L st

for i being even Nat holds

( b_{1} . i = p . i & ( for i being odd Nat holds b_{1} . i = 0. L ) )

for b_{1}, b_{2} being sequence of L st ( for i being even Nat holds

( b_{1} . i = p . i & ( for i being odd Nat holds b_{1} . i = 0. L ) ) ) & ( for i being even Nat holds

( b_{2} . i = p . i & ( for i being odd Nat holds b_{2} . i = 0. L ) ) ) holds

b_{1} = b_{2}

ex b_{1} being sequence of L st

for i being even Nat holds

( b_{1} . i = 0. L & ( for i being odd Nat holds b_{1} . i = p . i ) )

for b_{1}, b_{2} being sequence of L st ( for i being even Nat holds

( b_{1} . i = 0. L & ( for i being odd Nat holds b_{1} . i = p . i ) ) ) & ( for i being even Nat holds

( b_{2} . i = 0. L & ( for i being odd Nat holds b_{2} . i = p . i ) ) ) holds

b_{1} = b_{2}

end;
let p be sequence of L;

func even_part p -> sequence of L means :Def1: :: HURWITZ2:def 1

for i being even Nat holds

( it . i = p . i & ( for i being odd Nat holds it . i = 0. L ) );

existence for i being even Nat holds

( it . i = p . i & ( for i being odd Nat holds it . i = 0. L ) );

ex b

for i being even Nat holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

func odd_part p -> sequence of L means :Def2: :: HURWITZ2:def 2

for i being even Nat holds

( it . i = 0. L & ( for i being odd Nat holds it . i = p . i ) );

existence for i being even Nat holds

( it . i = 0. L & ( for i being odd Nat holds it . i = p . i ) );

ex b

for i being even Nat holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def1 defines even_part HURWITZ2:def 1 :

for L being non empty ZeroStr

for p, b_{3} being sequence of L holds

( b_{3} = even_part p iff for i being even Nat holds

( b_{3} . i = p . i & ( for i being odd Nat holds b_{3} . i = 0. L ) ) );

for L being non empty ZeroStr

for p, b

( b

( b

:: deftheorem Def2 defines odd_part HURWITZ2:def 2 :

for L being non empty ZeroStr

for p, b_{3} being sequence of L holds

( b_{3} = odd_part p iff for i being even Nat holds

( b_{3} . i = 0. L & ( for i being odd Nat holds b_{3} . i = p . i ) ) );

for L being non empty ZeroStr

for p, b

( b

( b

registration

let L be non empty ZeroStr ;

let p be Polynomial of L;

coherence

even_part p is finite-Support

odd_part p is finite-Support

end;
let p be Polynomial of L;

coherence

even_part p is finite-Support

proof end;

coherence odd_part p is finite-Support

proof end;

theorem Th9: :: HURWITZ2:9

for L being non empty left_zeroed right_zeroed addLoopStr

for p being Polynomial of L holds (even_part p) + (odd_part p) = p

for p being Polynomial of L holds (even_part p) + (odd_part p) = p

proof end;

theorem Th10: :: HURWITZ2:10

for L being non empty left_zeroed right_zeroed addLoopStr

for p being Polynomial of L holds (odd_part p) + (even_part p) = p

for p being Polynomial of L holds (odd_part p) + (even_part p) = p

proof end;

theorem :: HURWITZ2:11

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of L holds p - (odd_part p) = even_part p

for p being Polynomial of L holds p - (odd_part p) = even_part p

proof end;

theorem :: HURWITZ2:12

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of L holds p - (even_part p) = odd_part p

for p being Polynomial of L holds p - (even_part p) = odd_part p

proof end;

theorem :: HURWITZ2:13

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for p being Polynomial of L holds (even_part p) - p = - (odd_part p)

for p being Polynomial of L holds (even_part p) - p = - (odd_part p)

proof end;

theorem :: HURWITZ2:14

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for p being Polynomial of L holds (odd_part p) - p = - (even_part p)

for p being Polynomial of L holds (odd_part p) - p = - (even_part p)

proof end;

theorem Th15: :: HURWITZ2:15

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for p, q being Polynomial of L holds even_part (p + q) = (even_part p) + (even_part q)

for p, q being Polynomial of L holds even_part (p + q) = (even_part p) + (even_part q)

proof end;

theorem Th16: :: HURWITZ2:16

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for p, q being Polynomial of L holds odd_part (p + q) = (odd_part p) + (odd_part q)

for p, q being Polynomial of L holds odd_part (p + q) = (odd_part p) + (odd_part q)

proof end;

theorem Th17: :: HURWITZ2:17

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L st deg p is even holds

even_part (Leading-Monomial p) = Leading-Monomial p

for p being Polynomial of L st deg p is even holds

even_part (Leading-Monomial p) = Leading-Monomial p

proof end;

theorem Th18: :: HURWITZ2:18

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L st deg p is odd holds

even_part (Leading-Monomial p) = 0_. L

for p being Polynomial of L st deg p is odd holds

even_part (Leading-Monomial p) = 0_. L

proof end;

theorem Th19: :: HURWITZ2:19

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L st deg p is even holds

odd_part (Leading-Monomial p) = 0_. L

for p being Polynomial of L st deg p is even holds

odd_part (Leading-Monomial p) = 0_. L

proof end;

theorem Th20: :: HURWITZ2:20

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L st deg p is odd holds

odd_part (Leading-Monomial p) = Leading-Monomial p

for p being Polynomial of L st deg p is odd holds

odd_part (Leading-Monomial p) = Leading-Monomial p

proof end;

theorem Th21: :: HURWITZ2:21

for L being non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for p being non zero Polynomial of L holds deg (even_part p) <> deg (odd_part p)

for p being non zero Polynomial of L holds deg (even_part p) <> deg (odd_part p)

proof end;

theorem :: HURWITZ2:22

for L being non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for p being Polynomial of L holds

( deg (even_part p) <= deg p & deg (odd_part p) <= deg p )

for p being Polynomial of L holds

( deg (even_part p) <= deg p & deg (odd_part p) <= deg p )

proof end;

theorem Th23: :: HURWITZ2:23

for L being non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for p being Polynomial of L holds deg p = max ((deg (even_part p)),(deg (odd_part p)))

for p being Polynomial of L holds deg p = max ((deg (even_part p)),(deg (odd_part p)))

proof end;

:: deftheorem Def3 defines even HURWITZ2:def 3 :

for L being non empty addLoopStr

for f being Function of L,L holds

( f is even iff for x being Element of L holds f . (- x) = f . x );

for L being non empty addLoopStr

for f being Function of L,L holds

( f is even iff for x being Element of L holds f . (- x) = f . x );

:: deftheorem Def4 defines odd HURWITZ2:def 4 :

for L being non empty addLoopStr

for f being Function of L,L holds

( f is odd iff for x being Element of L holds f . (- x) = - (f . x) );

for L being non empty addLoopStr

for f being Function of L,L holds

( f is odd iff for x being Element of L holds f . (- x) = - (f . x) );

:: deftheorem Def5 defines even HURWITZ2:def 5 :

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L holds

( p is even iff Polynomial-Function (L,p) is even );

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L holds

( p is even iff Polynomial-Function (L,p) is even );

:: deftheorem Def6 defines odd HURWITZ2:def 6 :

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L holds

( p is odd iff Polynomial-Function (L,p) is odd );

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L holds

( p is odd iff Polynomial-Function (L,p) is odd );

:: deftheorem defines odd HURWITZ2:def 7 :

for L being non trivial well-unital doubleLoopStr

for Z being rational_function of L holds

( Z is odd iff ( ( Z `1 is even & Z `2 is odd ) or ( Z `1 is odd & Z `2 is even ) ) );

for L being non trivial well-unital doubleLoopStr

for Z being rational_function of L holds

( Z is odd iff ( ( Z `1 is even & Z `2 is odd ) or ( Z `1 is odd & Z `2 is even ) ) );

notation

let L be non trivial well-unital doubleLoopStr ;

let Z be rational_function of L;

antonym even Z for odd ;

end;
let Z be rational_function of L;

antonym even Z for odd ;

registration

let L be non empty well-unital doubleLoopStr ;

ex b_{1} being Polynomial of L st b_{1} is even

end;
cluster Relation-like NAT -defined the carrier of L -valued Function-like V11() V14( NAT ) V18( NAT , the carrier of L) finite-Support even for Element of K19(K20(NAT, the carrier of L));

existence ex b

proof end;

registration

let L be non empty right_complementable add-associative right_zeroed well-unital doubleLoopStr ;

ex b_{1} being Polynomial of L st b_{1} is odd

end;
cluster Relation-like NAT -defined the carrier of L -valued Function-like V11() V14( NAT ) V18( NAT , the carrier of L) finite-Support odd for Element of K19(K20(NAT, the carrier of L));

existence ex b

proof end;

registration

let L be non degenerated right_complementable add-associative right_zeroed well-unital associative doubleLoopStr ;

ex b_{1} being Polynomial of L st

( not b_{1} is zero & b_{1} is even )

end;
cluster Relation-like NAT -defined the carrier of L -valued Function-like V11() V14( NAT ) V18( NAT , the carrier of L) finite-Support non zero even for Element of K19(K20(NAT, the carrier of L));

existence ex b

( not b

proof end;

registration

let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital doubleLoopStr ;

ex b_{1} being Polynomial of L st

( not b_{1} is zero & b_{1} is odd )

end;
cluster Relation-like NAT -defined the carrier of L -valued Function-like V11() V14( NAT ) V18( NAT , the carrier of L) finite-Support non zero odd for Element of K19(K20(NAT, the carrier of L));

existence ex b

( not b

proof end;

theorem Th24: :: HURWITZ2:24

for L being non empty well-unital doubleLoopStr

for p being even Polynomial of L

for x being Element of L holds eval (p,(- x)) = eval (p,x)

for p being even Polynomial of L

for x being Element of L holds eval (p,(- x)) = eval (p,x)

proof end;

theorem Th25: :: HURWITZ2:25

for L being non degenerated right_complementable Abelian add-associative right_zeroed well-unital doubleLoopStr

for p being odd Polynomial of L

for x being Element of L holds eval (p,(- x)) = - (eval (p,x))

for p being odd Polynomial of L

for x being Element of L holds eval (p,(- x)) = - (eval (p,x))

proof end;

registration

let L be non empty right_complementable add-associative right_zeroed well-unital doubleLoopStr ;

coherence

0_. L is odd

end;
coherence

0_. L is odd

proof end;

registration

let L be non degenerated right_complementable add-associative right_zeroed well-unital associative doubleLoopStr ;

coherence

1_. L is even

end;
coherence

1_. L is even

proof end;

registration

let L be non empty right_complementable Abelian add-associative right_zeroed left-distributive well-unital doubleLoopStr ;

let p, q be even Polynomial of L;

coherence

p + q is even

end;
let p, q be even Polynomial of L;

coherence

p + q is even

proof end;

registration

let L be non degenerated right_complementable Abelian add-associative right_zeroed left-distributive well-unital doubleLoopStr ;

let p, q be odd Polynomial of L;

coherence

p + q is odd

end;
let p, q be odd Polynomial of L;

coherence

p + q is odd

proof end;

registration

let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;

let p be Polynomial of L;

coherence

even_part p is even

odd_part p is odd

end;
let p be Polynomial of L;

coherence

even_part p is even

proof end;

coherence odd_part p is odd

proof end;

theorem Th26: :: HURWITZ2:26

for L being non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being even Polynomial of L

for q being odd Polynomial of L

for x being Element of L st x is_a_common_root_of p,q holds

- x is_a_root_of p + q

for p being even Polynomial of L

for q being odd Polynomial of L

for x being Element of L st x is_a_common_root_of p,q holds

- x is_a_root_of p + q

proof end;

:: deftheorem Def8 defines real HURWITZ2:def 8 :

for p being Polynomial of F_Complex holds

( p is real iff for i being Nat holds p . i is Real );

for p being Polynomial of F_Complex holds

( p is real iff for i being Nat holds p . i is Real );

:: deftheorem defines positive HURWITZ2:def 9 :

for p being Polynomial of F_Complex holds

( p is positive iff for x being Element of F_Complex st Re x > 0 holds

Re (eval (p,x)) > 0 );

for p being Polynomial of F_Complex holds

( p is positive iff for x being Element of F_Complex st Re x > 0 holds

Re (eval (p,x)) > 0 );

registration

coherence

( 0_. F_Complex is real & not 0_. F_Complex is positive )

( 1_. F_Complex is real & 1_. F_Complex is positive )

end;
( 0_. F_Complex is real & not 0_. F_Complex is positive )

proof end;

coherence ( 1_. F_Complex is real & 1_. F_Complex is positive )

proof end;

registration

ex b_{1} being Polynomial of F_Complex st

( not b_{1} is zero & b_{1} is real & b_{1} is positive )
end;

cluster Relation-like NAT -defined the carrier of F_Complex -valued Function-like V11() V14( NAT ) V18( NAT , the carrier of F_Complex) complex-valued finite-Support non zero real positive for Element of K19(K20(NAT, the carrier of F_Complex));

existence ex b

( not b

proof end;

registration

for b_{1} being Polynomial of F_Complex st b_{1} is real holds

b_{1} is real-valued
end;

cluster Function-like V18( NAT , the carrier of F_Complex) finite-Support real -> real-valued for Element of K19(K20(NAT, the carrier of F_Complex));

coherence for b

b

proof end;

registration

let p be real Polynomial of F_Complex;

coherence

even_part p is real

odd_part p is real

end;
coherence

even_part p is real

proof end;

coherence odd_part p is real

proof end;

definition

let L be non empty addLoopStr ;

let p be Polynomial of L;

end;
let p be Polynomial of L;

attr p is with_all_coefficients means :Def10: :: HURWITZ2:def 10

for i being Nat st i <= deg p holds

p . i <> 0 ;

for i being Nat st i <= deg p holds

p . i <> 0 ;

:: deftheorem Def10 defines with_all_coefficients HURWITZ2:def 10 :

for L being non empty addLoopStr

for p being Polynomial of L holds

( p is with_all_coefficients iff for i being Nat st i <= deg p holds

p . i <> 0 );

for L being non empty addLoopStr

for p being Polynomial of L holds

( p is with_all_coefficients iff for i being Nat st i <= deg p holds

p . i <> 0 );

definition

let p be real Polynomial of F_Complex;

end;
attr p is with_positive_coefficients means :: HURWITZ2:def 11

for i being Nat st i <= deg p holds

p . i > 0 ;

for i being Nat st i <= deg p holds

p . i > 0 ;

attr p is with_negative_coefficients means :: HURWITZ2:def 12

for i being Nat st i <= deg p holds

p . i < 0 ;

for i being Nat st i <= deg p holds

p . i < 0 ;

:: deftheorem defines with_positive_coefficients HURWITZ2:def 11 :

for p being real Polynomial of F_Complex holds

( p is with_positive_coefficients iff for i being Nat st i <= deg p holds

p . i > 0 );

for p being real Polynomial of F_Complex holds

( p is with_positive_coefficients iff for i being Nat st i <= deg p holds

p . i > 0 );

:: deftheorem defines with_negative_coefficients HURWITZ2:def 12 :

for p being real Polynomial of F_Complex holds

( p is with_negative_coefficients iff for i being Nat st i <= deg p holds

p . i < 0 );

for p being real Polynomial of F_Complex holds

( p is with_negative_coefficients iff for i being Nat st i <= deg p holds

p . i < 0 );

registration

for b_{1} being real Polynomial of F_Complex st b_{1} is with_positive_coefficients holds

b_{1} is with_all_coefficients
;

for b_{1} being real Polynomial of F_Complex st b_{1} is with_negative_coefficients holds

b_{1} is with_all_coefficients
;

end;

cluster Function-like V18( NAT , the carrier of F_Complex) finite-Support real with_positive_coefficients -> real with_all_coefficients for Element of K19(K20(NAT, the carrier of F_Complex));

coherence for b

b

cluster Function-like V18( NAT , the carrier of F_Complex) finite-Support real with_negative_coefficients -> real with_all_coefficients for Element of K19(K20(NAT, the carrier of F_Complex));

coherence for b

b

registration

ex b_{1} being real Polynomial of F_Complex st

( not b_{1} is constant & b_{1} is with_positive_coefficients )
end;

cluster Relation-like NAT -defined the carrier of F_Complex -valued Function-like V11() V14( NAT ) V18( NAT , the carrier of F_Complex) complex-valued ext-real-valued real-valued finite-Support non constant real with_positive_coefficients for Element of K19(K20(NAT, the carrier of F_Complex));

existence ex b

( not b

proof end;

registration

let p be non zero real with_all_coefficients Polynomial of F_Complex;

coherence

not even_part p is zero

end;
coherence

not even_part p is zero

proof end;

registration

let p be non constant real with_all_coefficients Polynomial of F_Complex;

coherence

not odd_part p is zero

end;
coherence

not odd_part p is zero

proof end;

definition

let Z be rational_function of F_Complex ;

end;
:: deftheorem defines real HURWITZ2:def 13 :

for Z being rational_function of F_Complex holds

( Z is real iff for i being Nat holds

( (Z `1) . i is Real & (Z `2) . i is Real ) );

for Z being rational_function of F_Complex holds

( Z is real iff for i being Nat holds

( (Z `1) . i is Real & (Z `2) . i is Real ) );

:: deftheorem defines positive HURWITZ2:def 14 :

for Z being rational_function of F_Complex holds

( Z is positive iff for x being Element of F_Complex st Re x > 0 & eval ((Z `2),x) <> 0 holds

Re (eval (Z,x)) > 0 );

for Z being rational_function of F_Complex holds

( Z is positive iff for x being Element of F_Complex st Re x > 0 & eval ((Z `2),x) <> 0 holds

Re (eval (Z,x)) > 0 );

registration

existence

ex b_{1} being rational_function of F_Complex st

( not b_{1} is zero & b_{1} is odd & b_{1} is real & b_{1} is positive )

end;
ex b

( not b

proof end;

registration

let p1 be real Polynomial of F_Complex;

let p2 be non zero real Polynomial of F_Complex;

coherence

for b_{1} being rational_function of F_Complex st b_{1} = [p1,p2] holds

b_{1} is real
;

end;
let p2 be non zero real Polynomial of F_Complex;

coherence

for b

b

definition

mode one_port_function is real positive rational_function of F_Complex ;

mode reactance_one_port_function is odd real positive rational_function of F_Complex ;

end;
mode reactance_one_port_function is odd real positive rational_function of F_Complex ;

theorem Th28: :: HURWITZ2:28

for p being real Polynomial of F_Complex

for x being Element of F_Complex st Re x = 0 holds

Im (eval ((even_part p),x)) = 0

for x being Element of F_Complex st Re x = 0 holds

Im (eval ((even_part p),x)) = 0

proof end;

theorem Th29: :: HURWITZ2:29

for p being real Polynomial of F_Complex

for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0

for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0

proof end;

theorem Th30: :: HURWITZ2:30

for p being non constant real with_positive_coefficients Polynomial of F_Complex st [(even_part p),(odd_part p)] is positive & even_part p, odd_part p have_no_common_roots holds

( ( for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds

Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) & (even_part p) + (odd_part p) is Hurwitz )

( ( for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds

Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) & (even_part p) + (odd_part p) is Hurwitz )

proof end;

theorem :: HURWITZ2:31

for p being non constant real with_positive_coefficients Polynomial of F_Complex st [(even_part p),(odd_part p)] is one_port_function & degree [(even_part p),(odd_part p)] = degree p holds

p is Hurwitz

p is Hurwitz

proof end;