:: A Test for the Stability of Networks
:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller
::
:: Received January 17, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

theorem Th1: :: HURWITZ2:1

for x, y being Complex st Im x = 0 & Re y = 0 holds
Re (x / y) = 0

proof end;

theorem :: HURWITZ2:2

for a being Complex holds a * (a *') = |.a.| ^2

proof end;

registration

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₁ being Polynomial of F_Complex st b₁ is Hurwitz

proof end;

end;

Lm1: (2 * 0) + 1 = 1
;

registration

cluster 0 -> even ;

coherence
0 is even ;

end;

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)

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

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

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

proof end;

definition

let L be non empty ZeroStr ;
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
ex b₁ being sequence of L st
for i being even Nat holds
( b₁ . i = p . i & ( for i being odd Nat holds b₁ . i = 0. L ) )

proof end;

uniqueness
for b₁, b₂ being sequence of L st ( for i being even Nat holds
( b₁ . i = p . i & ( for i being odd Nat holds b₁ . i = 0. L ) ) ) & ( for i being even Nat holds
( b₂ . i = p . i & ( for i being odd Nat holds b₂ . i = 0. L ) ) ) holds
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
ex b₁ being sequence of L st
for i being even Nat holds
( b₁ . i = 0. L & ( for i being odd Nat holds b₁ . i = p . i ) )

proof end;

uniqueness
for b₁, b₂ being sequence of L st ( for i being even Nat holds
( b₁ . i = 0. L & ( for i being odd Nat holds b₁ . i = p . i ) ) ) & ( for i being even Nat holds
( b₂ . i = 0. L & ( for i being odd Nat holds b₂ . i = p . i ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines even_part HURWITZ2:def 1 :
for L being non empty ZeroStr
for p, b₃ being sequence of L holds
( b₃ = even_part p iff for i being even Nat holds
( b₃ . i = p . i & ( for i being odd Nat holds b₃ . i = 0. L ) ) );

:: deftheorem Def2 defines odd_part HURWITZ2:def 2 :
for L being non empty ZeroStr
for p, b₃ being sequence of L holds
( b₃ = odd_part p iff for i being even Nat holds
( b₃ . i = 0. L & ( for i being odd Nat holds b₃ . i = p . i ) ) );

registration

let L be non empty ZeroStr ;
let p be Polynomial of L;

cluster even_part p -> finite-Support ;

coherence
even_part p is finite-Support

proof end;

cluster odd_part p -> finite-Support ;

coherence
odd_part p is finite-Support

proof end;

end;

theorem Th7: :: HURWITZ2:7

for L being non empty ZeroStr holds
( even_part (0_. L) = 0_. L & odd_part (0_. L) = 0_. L )

proof end;

theorem :: HURWITZ2:8

for L being non empty multLoopStr_0 holds
( even_part (1_. L) = 1_. L & odd_part (1_. L) = 0_. L )

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

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

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

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

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)

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)

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)

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)

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

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

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

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

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)

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 )

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

proof end;

definition

let L be non empty addLoopStr ;
let f be Function of L,L;

attr f is even means :Def3: :: HURWITZ2:def 3
for x being Element of L holds f . (- x) = f . x;

attr f is odd means :Def4: :: HURWITZ2:def 4
for x being Element of L holds f . (- x) = - (f . x);

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 );

:: 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) );

definition

let L be non empty well-unital doubleLoopStr ;
let p be Polynomial of L;

attr p is even means :Def5: :: HURWITZ2:def 5
Polynomial-Function (L,p) is even ;

attr p is odd means :Def6: :: HURWITZ2:def 6
Polynomial-Function (L,p) is odd ;

end;

:: 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 );

:: 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 );

definition

let L be non trivial well-unital doubleLoopStr ;
let Z be rational_function of L;

attr Z is odd means :: HURWITZ2:def 7
( ( Z `1 is even & Z `2 is odd ) or ( Z `1 is odd & Z `2 is even ) );

end;

:: 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 ) ) );

notation

let L be non trivial well-unital doubleLoopStr ;
let Z be rational_function of L;
antonym even Z for odd ;

end;

registration

let L be non empty well-unital doubleLoopStr ;

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₁ being Polynomial of L st b₁ is even

proof end;

end;

registration

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

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₁ being Polynomial of L st b₁ is odd

proof end;

end;

registration

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

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₁ being Polynomial of L st
( not b₁ is zero & b₁ is even )

proof end;

end;

registration

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

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₁ being Polynomial of L st
( not b₁ is zero & b₁ is odd )

proof end;

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)

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

proof end;

registration

let L be non empty well-unital doubleLoopStr ;

cluster 0_. L -> even ;

coherence
0_. L is even

proof end;

end;

registration

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

cluster 0_. L -> odd ;

coherence
0_. L is odd

proof end;

end;

registration

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

cluster 1_. L -> even ;

coherence
1_. L is even

proof end;

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;

cluster p + q -> even ;

coherence
p + q is even

proof end;

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;

cluster p + q -> odd ;

coherence
p + q is odd

proof end;

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;

cluster even_part p -> even ;

coherence
even_part p is even

proof end;

cluster odd_part p -> odd ;

coherence
odd_part p is odd

proof end;

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

proof end;

theorem :: HURWITZ2:27

for p being Hurwitz Polynomial of F_Complex holds even_part p, odd_part p have_no_common_roots

proof end;

definition

let p be Polynomial of F_Complex;

attr p is real means :Def8: :: HURWITZ2:def 8
for i being Nat holds p . i is Real;

attr p is positive means :: HURWITZ2:def 9
for x being Element of F_Complex st Re x > 0 holds
Re (eval (p,x)) > 0 ;

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 );

:: 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 );

registration

cluster 0_. F_Complex -> real non positive ;

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

proof end;

cluster 1_. F_Complex -> real positive ;

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

proof end;

end;

registration

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₁ being Polynomial of F_Complex st
( not b₁ is zero & b₁ is real & b₁ is positive )

proof end;

end;

registration

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₁ being Polynomial of F_Complex st b₁ is real holds
b₁ is real-valued

proof end;

end;

registration

let p be real Polynomial of F_Complex;

cluster even_part p -> real ;

coherence
even_part p is real

proof end;

cluster odd_part p -> real ;

coherence
odd_part p is real

proof end;

end;

definition

let L be non empty addLoopStr ;
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 ;

end;

:: 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 );

definition

let p be real Polynomial of F_Complex;

attr p is with_positive_coefficients means :: HURWITZ2:def 11
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 ;

end;

:: 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 );

:: 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 );

registration

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₁ being real Polynomial of F_Complex st b₁ is with_positive_coefficients holds
b₁ is with_all_coefficients ;

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₁ being real Polynomial of F_Complex st b₁ is with_negative_coefficients holds
b₁ is with_all_coefficients ;

end;

registration

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₁ being real Polynomial of F_Complex st
( not b₁ is constant & b₁ is with_positive_coefficients )

proof end;

end;

registration

let p be non zero real with_all_coefficients Polynomial of F_Complex;

cluster even_part p -> non zero ;

coherence
not even_part p is zero

proof end;

end;

registration

let p be non constant real with_all_coefficients Polynomial of F_Complex;

cluster odd_part p -> non zero ;

coherence
not odd_part p is zero

proof end;

end;

definition

let Z be rational_function of F_Complex ;

attr Z is real means :: HURWITZ2:def 13
for i being Nat holds
( (Z `1) . i is Real & (Z `2) . i is Real );

attr Z is positive means :: HURWITZ2:def 14
for x being Element of F_Complex st Re x > 0 & eval ((Z `2),x) <> 0 holds
Re (eval (Z,x)) > 0 ;

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 ) );

:: 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 );

registration

cluster non zero odd real positive for rational_function of F_Complex ;

existence
ex b₁ being rational_function of F_Complex st
( not b₁ is zero & b₁ is odd & b₁ is real & b₁ is positive )

proof end;

end;

registration

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

cluster [p1,p2] -> real for rational_function of F_Complex ;

coherence
for b₁ being rational_function of F_Complex st b₁ = [p1,p2] holds
b₁ is real ;

end;

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;

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

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

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 )

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

proof end;