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

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

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 (power L) . ((- (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 ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2))

proof end;

Lm2: ( Im (1_ F_Complex) = 0 & Im (- (1_ F_Complex)) = 0 & Im (0. F_Complex) = 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
( (power L) . ((- (1_ L)),(2 * k)) = 1_ L & (power 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 ((power F_Complex) . (z,k)) *' = (power F_Complex) . ((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 L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
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;

Lm3: for L being non empty right_complementable add-associative right_zeroed addLoopStr
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 (Polynom-Ring L) st f = p holds
- f = - p

proof end;

theorem :: HURWITZ:10

for L being non empty right_complementable add-associative right_zeroed addLoopStr
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 (Polynom-Ring L);
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 b₁ being FinSequence of L st
( len b₁ = len F & ( for j being Element of NAT st j in dom b₁ holds
ex p being Polynomial of L st
( p = F . j & b₁ . j = p . i ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of L st len b₁ = len F & ( for j being Element of NAT st j in dom b₁ holds
ex p being Polynomial of L st
( p = F . j & b₁ . j = p . i ) ) & len b₂ = len F & ( for j being Element of NAT st j in dom b₂ holds
ex p being Polynomial of L st
( p = F . j & b₂ . j = p . i ) ) holds
b₁ = b₂

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 (Polynom-Ring L)
for i being Element of NAT
for b₄ being FinSequence of L holds
( b₄ = Coeff (F,i) iff ( len b₄ = len F & ( for j being Element of NAT st j in dom b₄ holds
ex p being Polynomial of L st
( p = F . j & b₄ . 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 (Polynom-Ring L) 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 (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)

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 L being non empty right_complementable add-associative right_zeroed addLoopStr
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 L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
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) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = - ((power L) . (z,k)) & ((0_. L) +* ((0,k) --> ((- ((power L) . (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) --> ((- ((power L) . (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) --> ((- ((power L) . (z,k))),(1_ L)));

coherence
(0_. L) +* ((0,k) --> ((- ((power L) . (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) --> ((- ((power L) . (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 = - ((power L) . (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 = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
it . i = 0. L ) );

existence
ex b₁ being Polynomial of L st
( ( for i being Nat st i < k holds
b₁ . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b₁ . i = 0. L ) )

proof end;

uniqueness
for b₁, b₂ being Polynomial of L st ( for i being Nat st i < k holds
b₁ . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b₁ . i = 0. L ) & ( for i being Nat st i < k holds
b₂ . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b₂ . i = 0. L ) holds
b₁ = b₂

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 b₄ being Polynomial of L holds
( b₄ = qpoly (k,z) iff ( ( for i being Nat st i < k holds
b₄ . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
b₄ . 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 b₁, t being Polynomial of L st
( p = (b₁ *' s) + t & deg t < deg s )

proof end;

uniqueness
for b₁, b₂ being Polynomial of L st ex t being Polynomial of L st
( p = (b₁ *' s) + t & deg t < deg s ) & ex t being Polynomial of L st
( p = (b₂ *' s) + t & deg t < deg s ) holds
b₁ = b₂

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 b₄ being Polynomial of L holds
( b₄ = p div s iff ex t being Polynomial of L st
( p = (b₄ *' 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 * (1_. F_Complex) 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 = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *');

existence
ex b₁ being Polynomial of F_Complex st
for i being Element of NAT holds b₁ . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *')

proof end;

uniqueness
for b₁, b₂ being Polynomial of F_Complex st ( for i being Element of NAT holds b₁ . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) & ( for i being Element of NAT holds b₂ . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Polynomial of F_Complex st ( for i being Element of NAT holds b₁ . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((b₂ . i) *') ) holds
for i being Element of NAT holds b₂ . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((b₁ . i) *')

proof end;

end;

:: deftheorem Def9 defines *' HURWITZ:def 9 :
for f, b₂ being Polynomial of F_Complex holds
( b₂ = f *' iff for i being Element of NAT holds b₂ . i = ((power F_Complex) . ((- (1_ F_Complex)),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;