:: 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 b1 being Polynomial of F_Complex st b1 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 b1 being sequence of L st
for i being even Nat holds
( b1 . i = p . i & ( for i being odd Nat holds b1 . i = 0. L ) )
proof end;
uniqueness
for b1, b2 being sequence of L st ( for i being even Nat holds
( b1 . i = p . i & ( for i being odd Nat holds b1 . i = 0. L ) ) ) & ( for i being even Nat holds
( b2 . i = p . i & ( for i being odd Nat holds b2 . i = 0. L ) ) ) holds
b1 = b2
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 b1 being sequence of L st
for i being even Nat holds
( b1 . i = 0. L & ( for i being odd Nat holds b1 . i = p . i ) )
proof end;
uniqueness
for b1, b2 being sequence of L st ( for i being even Nat holds
( b1 . i = 0. L & ( for i being odd Nat holds b1 . i = p . i ) ) ) & ( for i being even Nat holds
( b2 . i = 0. L & ( for i being odd Nat holds b2 . i = p . i ) ) ) holds
b1 = b2
proof end;
end;

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

:: deftheorem Def2 defines odd_part HURWITZ2:def 2 :
for L being non empty ZeroStr
for p, b3 being sequence of L holds
( b3 = odd_part p iff for i being even Nat holds
( b3 . i = 0. L & ( for i being odd Nat holds b3 . 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 b1 being Polynomial of L st b1 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 b1 being Polynomial of L st b1 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 b1 being Polynomial of L st
( not b1 is zero & b1 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 b1 being Polynomial of L st
( not b1 is zero & b1 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 b1 being Polynomial of F_Complex st
( not b1 is zero & b1 is real & b1 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 b1 being Polynomial of F_Complex st b1 is real holds
b1 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 b1 being real Polynomial of F_Complex st b1 is with_positive_coefficients holds
b1 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 b1 being real Polynomial of F_Complex st b1 is with_negative_coefficients holds
b1 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 b1 being real Polynomial of F_Complex st
( not b1 is constant & b1 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 b1 being rational_function of F_Complex st
( not b1 is zero & b1 is odd & b1 is real & b1 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 b1 being rational_function of F_Complex st b1 = [p1,p2] holds
b1 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;