:: Schur's Theorem on the Stability of Networks
:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller
::
:: Copyright (c) 2006-2021 Association of Mizar Users

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

proof end;

theorem Th1: :: HURWITZ:1
for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for x being Element of L st x <> 0. L holds
- (x ") = (- x) "
proof end;

theorem Th2: :: HURWITZ:2
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for k being Element of NAT holds () . ((- (1_ L)),k) <> 0. L
proof end;

theorem Th3: :: HURWITZ:3
for L being non empty well-unital associative multLoopStr
for x being Element of L
for k1, k2 being Element of NAT holds (() . (x,k1)) * (() . (x,k2)) = () . (x,(k1 + k2))
proof end;

Lm2: ( Im () = 0 & Im (- ()) = 0 & Im () = 0 )
proof end;

theorem Th4: :: HURWITZ:4
for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for k being Element of NAT holds
( () . ((- (1_ L)),(2 * k)) = 1_ L & () . ((- (1_ L)),((2 * k) + 1)) = - (1_ L) )
proof end;

theorem Th5: :: HURWITZ:5
for z being Element of F_Complex
for k being Element of NAT holds ( . (z,k)) *' = . ((z *'),k)
proof end;

theorem Th6: :: HURWITZ:6
for F, G being FinSequence of F_Complex st len G = len F & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) holds
Sum G = (Sum F) *'
proof end;

theorem Th7: :: HURWITZ:7
for F1, F2 being FinSequence of L st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 /. i = - (F2 /. i) ) holds
Sum F1 = - (Sum F2)
proof end;

theorem Th8: :: HURWITZ:8
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for x being Element of L
for F being FinSequence of L holds x * (Sum F) = Sum (x * F)
proof end;

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

proof end;

theorem Th9: :: HURWITZ:9
for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0_. L) = 0_. L
proof end;

Lm4: for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for f being Element of () st f = p holds
- f = - p

proof end;

theorem :: HURWITZ:10
for p being Polynomial of L holds - (- p) = p by Lm3;

theorem Th11: :: HURWITZ:11
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L holds - (p1 + p2) = (- p1) + (- p2)
proof end;

theorem Th12: :: HURWITZ:12
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L holds
( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) )
proof end;

definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let F be FinSequence of ();
let i be Element of NAT ;
func Coeff (F,i) -> FinSequence of L means :Def1: :: HURWITZ:def 1
( len it = len F & ( for j being Element of NAT st j in dom it holds
ex p being Polynomial of L st
( p = F . j & it . j = p . i ) ) );
existence
ex b1 being FinSequence of L st
( len b1 = len F & ( for j being Element of NAT st j in dom b1 holds
ex p being Polynomial of L st
( p = F . j & b1 . j = p . i ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of L st len b1 = len F & ( for j being Element of NAT st j in dom b1 holds
ex p being Polynomial of L st
( p = F . j & b1 . j = p . i ) ) & len b2 = len F & ( for j being Element of NAT st j in dom b2 holds
ex p being Polynomial of L st
( p = F . j & b2 . j = p . i ) ) holds
b1 = b2
proof end;
end;

:: 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 ()
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: :: HURWITZ:13
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for F being FinSequence of () st p = Sum F holds
for i being Element of NAT holds p . i = Sum (Coeff (F,i))
proof end;

Lm5: 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 () st p29 = p2 holds
for F being FinSequence of () st p1 = Sum F holds
p2 *' p1 = Sum (p29 * F)

proof end;

theorem Th14: :: HURWITZ:14
for L being non empty associative doubleLoopStr
for p being Polynomial of L
for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p
proof end;

theorem Th15: :: HURWITZ:15
for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for x being Element of L holds - (x * p) = (- x) * p
proof end;

theorem Th16: :: HURWITZ:16
for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for x being Element of L holds - (x * p) = x * (- p)
proof end;

theorem Th17: :: HURWITZ:17
for L being non empty left-distributive doubleLoopStr
for p being Polynomial of L
for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p)
proof end;

theorem Th18: :: HURWITZ:18
for L being non empty right-distributive doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2)
proof end;

theorem Th19: :: HURWITZ:19
for L being non empty right_complementable distributive add-associative right_zeroed associative commutative doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)
proof end;

definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
func degree p -> Integer equals :: HURWITZ:def 2
(len p) - 1;
coherence
(len p) - 1 is Integer
;
end;

:: deftheorem defines degree HURWITZ:def 2 :
for L being non empty ZeroStr
for p being Polynomial of L holds degree p = (len p) - 1;

notation
let L be non empty ZeroStr ;
let p be Polynomial of L;
synonym deg p for degree p;
end;

Lm6: for L being non empty ZeroStr
for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L

proof end;

theorem Th20: :: HURWITZ:20
for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p = - 1 iff p = 0_. L )
proof end;

Lm7: for L being non empty ZeroStr
for p being Polynomial of L st deg p <> - 1 holds
p . (deg p) <> 0. L

proof end;

Lm8: for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )

proof end;

theorem :: HURWITZ:21
for p1, p2 being Polynomial of L st deg p1 <> deg p2 holds
deg (p1 + p2) = max ((deg p1),(deg p2))
proof end;

Lm9: for L being non empty ZeroStr
for p being Polynomial of L holds deg p >= - 1

proof end;

theorem Th22: :: HURWITZ:22
for p1, p2 being Polynomial of L holds deg (p1 + p2) <= max ((deg p1),(deg p2))
proof end;

theorem Th23: :: HURWITZ:23
for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative domRing-like doubleLoopStr
for p1, p2 being Polynomial of L st p1 <> 0_. L & p2 <> 0_. L holds
deg (p1 *' p2) = (deg p1) + (deg p2)
proof end;

theorem Th24: :: HURWITZ:24
for L being non empty right_complementable add-associative right_zeroed unital doubleLoopStr
for p being Polynomial of L st deg p = 0 holds
not p is with_roots
proof end;

Lm10: 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) --> ((- (() . (z,k))),(1_ L)))) . 0 = - (() . (z,k)) & ((0_. L) +* ((0,k) --> ((- (() . (z,k))),(1_ L)))) . k = 1_ L )

proof end;

Lm11: 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) --> ((- (() . (z,k))),(1_ L)))) . i = 0. L

proof end;

:: the polynomials x^k - z^k
definition
let L be non empty unital doubleLoopStr ;
let z be Element of L;
let k be Element of NAT ;
func rpoly (k,z) -> Polynomial of L equals :: HURWITZ:def 3
(0_. L) +* ((0,k) --> ((- (() . (z,k))),(1_ L)));
coherence
(0_. L) +* ((0,k) --> ((- (() . (z,k))),(1_ L))) is Polynomial of L
proof end;
end;

:: 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) --> ((- (() . (z,k))),(1_ L)));

theorem :: HURWITZ:25
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k <> 0 holds
( (rpoly (k,z)) . 0 = - (() . (z,k)) & (rpoly (k,z)) . k = 1_ L ) by Lm10;

theorem :: HURWITZ:26
for L being non empty unital doubleLoopStr
for z being Element of L
for i, k being Element of NAT st i <> 0 & i <> k holds
(rpoly (k,z)) . i = 0. L by Lm11;

theorem Th27: :: HURWITZ:27
for L being non empty non degenerated well-unital doubleLoopStr
for z being Element of L
for k being Element of NAT holds deg (rpoly (k,z)) = k
proof end;

theorem Th28: :: HURWITZ:28
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of L holds
( deg p = 1 iff ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly (1,z)) ) )
proof end;

theorem Th29: :: HURWITZ:29
for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr
for x, z being Element of L holds eval ((rpoly (1,z)),x) = x - z
proof end;

theorem Th30: :: HURWITZ:30
for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr
for z being Element of L holds z is_a_root_of rpoly (1,z)
proof end;

:: the polynomials x^(k-1) + x^(k-2)*z + x^(k-3)*z^2 + ... + x*z^(k-2) + z^(k-1)
definition
let L be non empty well-unital doubleLoopStr ;
let z be Element of L;
let k be Nat;
func qpoly (k,z) -> Polynomial of L means :Def4: :: HURWITZ:def 4
( ( for i being Nat st i < k holds
it . i = () . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
it . i = 0. L ) );
existence
ex b1 being Polynomial of L st
( ( for i being Nat st i < k holds
b1 . i = () . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b1 . i = 0. L ) )
proof end;
uniqueness
for b1, b2 being Polynomial of L st ( for i being Nat st i < k holds
b1 . i = () . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b1 . i = 0. L ) & ( for i being Nat st i < k holds
b2 . i = () . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b2 . i = 0. L ) holds
b1 = b2
proof end;
end;

:: 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 = () . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b4 . i = 0. L ) ) );

theorem :: HURWITZ:31
for L being non empty non degenerated well-unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k >= 1 holds
deg (qpoly (k,z)) = k - 1
proof end;

theorem Th32: :: HURWITZ:32
for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed commutative doubleLoopStr
for z being Element of L
for k being Element of NAT st k > 1 holds
(rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z)
proof end;

theorem Th33: :: HURWITZ:33
for L being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of L
for z being Element of L st z is_a_root_of p holds
ex s being Polynomial of L st p = (rpoly (1,z)) *' s
proof end;

definition
let L be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ;
let p, s be Polynomial of L;
assume A1: s <> 0_. L ;
func p div s -> Polynomial of L means :Def5: :: HURWITZ:def 5
ex t being Polynomial of L st
( p = (it *' s) + t & deg t < deg s );
existence
ex b1, t being Polynomial of L st
( p = (b1 *' s) + t & deg t < deg s )
proof end;
uniqueness
for b1, b2 being Polynomial of L st ex t being Polynomial of L st
( p = (b1 *' s) + t & deg t < deg s ) & ex t being Polynomial of L st
( p = (b2 *' s) + t & deg t < deg s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines div HURWITZ:def 5 :
for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 ) );

definition
let L be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ;
let p, s be Polynomial of L;
func p mod s -> Polynomial of L equals :: HURWITZ:def 6
p - ((p div s) *' s);
coherence
p - ((p div s) *' s) is Polynomial of L
;
end;

:: deftheorem defines mod HURWITZ:def 6 :
for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, s being Polynomial of L holds p mod s = p - ((p div s) *' s);

definition
let L be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ;
let p, s be Polynomial of L;
pred s divides p means :: HURWITZ:def 7
p mod s = 0_. L;
end;

:: deftheorem defines divides HURWITZ:def 7 :
for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, s being Polynomial of L holds
( s divides p iff p mod s = 0_. L );

theorem Th34: :: HURWITZ:34
for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, s being Polynomial of L st s <> 0_. L holds
( s divides p iff ex t being Polynomial of L st t *' s = p )
proof end;

theorem :: HURWITZ:35
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of L
for z being Element of L st z is_a_root_of p holds
rpoly (1,z) divides p
proof end;

theorem :: HURWITZ:36
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of L
for z being Element of L st p <> 0_. L & z is_a_root_of p holds
deg (p div (rpoly (1,z))) = (deg p) - 1
proof end;

definition
let f be Polynomial of F_Complex;
attr f is Hurwitz means :: HURWITZ:def 8
for z being Element of F_Complex st z is_a_root_of f holds
Re z < 0 ;
end;

:: deftheorem 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 :: HURWITZ:37
not 0_. F_Complex is Hurwitz
proof end;

theorem :: HURWITZ:38
for x being Element of F_Complex st x <> 0. F_Complex holds
x * () is Hurwitz
proof end;

theorem Th39: :: HURWITZ:39
for x, z being Element of F_Complex st x <> 0. F_Complex holds
( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 )
proof end;

theorem Th40: :: HURWITZ:40
for f being Polynomial of F_Complex
for z being Element of F_Complex st z <> 0. F_Complex holds
( f is Hurwitz iff z * f is Hurwitz )
proof end;

Lm12: 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

proof end;

theorem Th41: :: HURWITZ:41
for f, g being Polynomial of F_Complex holds
( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) )
proof end;

definition
let f be Polynomial of F_Complex;
func f *' -> Polynomial of F_Complex means :Def9: :: HURWITZ:def 9
for i being Element of NAT holds it . i = ( . ((- ()),i)) * ((f . i) *');
existence
ex b1 being Polynomial of F_Complex st
for i being Element of NAT holds b1 . i = ( . ((- ()),i)) * ((f . i) *')
proof end;
uniqueness
for b1, b2 being Polynomial of F_Complex st ( for i being Element of NAT holds b1 . i = ( . ((- ()),i)) * ((f . i) *') ) & ( for i being Element of NAT holds b2 . i = ( . ((- ()),i)) * ((f . i) *') ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Polynomial of F_Complex st ( for i being Element of NAT holds b1 . i = ( . ((- ()),i)) * ((b2 . i) *') ) holds
for i being Element of NAT holds b2 . i = ( . ((- ()),i)) * ((b1 . i) *')
proof end;
end;

:: 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 = ( . ((- ()),i)) * ((f . i) *') );

theorem Th42: :: HURWITZ:42
for f being Polynomial of F_Complex holds deg (f *') = deg f
proof end;

theorem :: HURWITZ:43
canceled;

::\$CT
theorem Th43: :: HURWITZ:44
for f being Polynomial of F_Complex
for z being Element of F_Complex holds (z * f) *' = (z *') * (f *')
proof end;

theorem Th44: :: HURWITZ:45
for f being Polynomial of F_Complex holds (- f) *' = - (f *')
proof end;

theorem Th45: :: HURWITZ:46
for f, g being Polynomial of F_Complex holds (f + g) *' = (f *') + (g *')
proof end;

theorem Th46: :: HURWITZ:47
for f, g being Polynomial of F_Complex holds (f *' g) *' = (f *') *' (g *')
proof end;

Lm13: 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

proof end;

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>) & uv < 0 holds
( ( u < 0 implies |.(x - xv).| < |.(x + (xv *')).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) )

proof end;

theorem Th47: :: HURWITZ:48
for x, z being Element of F_Complex holds eval (((rpoly (1,z)) *'),x) = (- x) - (z *')
proof end;

theorem Th48: :: HURWITZ:49
for f being Polynomial of F_Complex st f is Hurwitz holds
for x being Element of F_Complex st Re x >= 0 holds
0 < |.(eval (f,x)).|
proof end;

theorem Th49: :: HURWITZ:50
for f being Polynomial of F_Complex st deg f >= 1 & f is Hurwitz holds
for x being Element of F_Complex holds
( ( Re x < 0 implies |.(eval (f,x)).| < |.(eval ((f *'),x)).| ) & ( Re x > 0 implies |.(eval (f,x)).| > |.(eval ((f *'),x)).| ) & ( Re x = 0 implies |.(eval (f,x)).| = |.(eval ((f *'),x)).| ) )
proof end;

definition
let f be Polynomial of F_Complex;
let z be Element of F_Complex;
func F* (f,z) -> Polynomial of F_Complex equals :: HURWITZ:def 10
((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *'));
coherence
((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *')) is Polynomial of F_Complex
;
end;

:: 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 Th50: :: HURWITZ:51
for a, b being Element of F_Complex st |.a.| > |.b.| holds
for f being Polynomial of F_Complex st deg f >= 1 holds
( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz )
proof end;

theorem Th51: :: HURWITZ:52
for f being Polynomial of F_Complex st deg f >= 1 holds
for rho being Element of F_Complex st Re rho < 0 & f is Hurwitz holds
(F* (f,rho)) div (rpoly (1,rho)) is Hurwitz
proof end;

theorem :: HURWITZ:53
for f being Polynomial of F_Complex st deg f >= 1 & ex rho being Element of F_Complex st
( Re rho < 0 & |.(eval (f,rho)).| >= |.(eval ((f *'),rho)).| ) holds
not f is Hurwitz by Th49;

:: Schur's criterion
theorem :: HURWITZ:54
for f being Polynomial of F_Complex st deg f >= 1 holds
for rho being Element of F_Complex st Re rho < 0 & |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| holds
( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz )
proof end;