:: Schur's Theorem on the Stability of Networks
:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller
::
:: Received October 19, 2006
:: Copyright (c) 2006-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, NAT_1, RELAT_1,
ARYTM_3, TARSKI, ORDINAL4, PARTFUN1, XXREAL_0, FUNCT_1, SUBSET_1,
STRUCT_0, BINOP_1, VECTSP_1, LATTICES, SUPINF_2, ARYTM_1, GROUP_1,
CARD_1, MESFUNC1, COMPLFLD, COMPLEX1, CARD_3, POLYNOM1, POLYNOM3,
SGRAPH1, INT_1, ALGSEQ_1, VECTSP_2, POLYNOM5, AFINSQ_1, POLYNOM2,
FUNCT_4, FUNCOP_1, XCMPLX_0, SQUARE_1, HURWITZ;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0,
ALGSTR_0, VECTSP_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_D,
XXREAL_0, FINSEQ_1, INT_1, NAT_1, FUNCOP_1, STRUCT_0, RLVECT_1, VFUNCT_1,
GROUP_1, POLYNOM1, COMPLEX1, COMPLFLD, BINOP_1, NORMSP_1, ALGSEQ_1,
FUNCT_4, POLYNOM3, POLYNOM4, POLYNOM5, VECTSP_1, SQUARE_1;
constructors BINOP_1, REAL_1, SQUARE_1, FINSOP_1, BINARITH, VECTSP_2,
ALGSTR_1, POLYNOM4, POLYNOM5, NAT_D, RELSET_1, FVSUM_1, VFUNCT_1,
ALGSEQ_1, BINOP_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NAT_1, INT_1, FINSEQ_1, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1,
POLYNOM3, POLYNOM4, POLYNOM5, FUNCOP_1, CARD_1, VFUNCT_1, FUNCT_2,
MEMBERED;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
begin
theorem :: HURWITZ:1
for L being add-associative right_zeroed right_complementable
associative commutative well-unital distributive almost_left_invertible non
empty doubleLoopStr for x being Element of L st x <> 0.L holds -(x") = (-x)";
theorem :: HURWITZ:2
for L being add-associative right_zeroed right_complementable
associative commutative well-unital almost_left_invertible distributive non
degenerated non empty doubleLoopStr for k being Element of NAT holds power(L)
.(-1_L,k) <> 0.L;
theorem :: HURWITZ:3
for L being associative well-unital non empty 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);
theorem :: HURWITZ:4
for L being add-associative right_zeroed right_complementable
well-unital distributive non empty 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;
theorem :: 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);
theorem :: 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)
*';
theorem :: HURWITZ:7
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr, 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;
theorem :: HURWITZ:8
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for x being Element of L for F being
FinSequence of L holds x * Sum(F) = Sum(x*F);
begin
theorem :: HURWITZ:9
for L being add-associative right_zeroed right_complementable
non empty addLoopStr holds -0_.(L) = 0_.(L);
theorem :: HURWITZ:10
for L being add-associative right_zeroed right_complementable non
empty addLoopStr for p being Polynomial of L holds -(-p) = p;
theorem :: HURWITZ:11
for L being add-associative right_zeroed right_complementable
Abelian distributive non empty doubleLoopStr for p1,p2 being Polynomial of L
holds -(p1 + p2) = (-p1) + (-p2);
theorem :: HURWITZ:12
for L being add-associative right_zeroed right_complementable
distributive Abelian non empty doubleLoopStr for p1,p2 being Polynomial of L
holds -(p1 *' p2) = (-p1) *' p2 & -(p1 *' p2) = p1 *' (-p2);
definition
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
let F be FinSequence of Polynom-Ring(L);
let i be Element of NAT;
func Coeff(F,i) -> FinSequence of L means
:: HURWITZ:def 1
len it = len F & for j
being Element of NAT st j in dom it ex p being Polynomial of L st p = F.j & it.
j = p.i;
end;
theorem :: HURWITZ:13
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for p being Polynomial of L for F being
FinSequence of Polynom-Ring(L) st p = Sum F for i being Element of NAT holds p.
i = Sum Coeff(F,i);
theorem :: HURWITZ:14
for L being associative non empty doubleLoopStr for p being
Polynomial of L for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) *
p;
theorem :: HURWITZ:15
for L being add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr for p being Polynomial of L for x
being Element of L holds - (x * p) = (-x) * p;
theorem :: HURWITZ:16
for L being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for p being Polynomial of L for x
being Element of L holds - (x * p) = x * (-p);
theorem :: HURWITZ:17
for L being left-distributive non empty doubleLoopStr for p
being Polynomial of L for x1, x2 being Element of L holds (x1 + x2) * p = x1 *
p + x2 * p;
theorem :: HURWITZ:18
for L being right-distributive non empty doubleLoopStr for p1,
p2 being Polynomial of L for x being Element of L holds x * (p1 + p2) = (x * p1
) + (x * p2);
theorem :: HURWITZ:19
for L being add-associative right_zeroed right_complementable
distributive commutative associative non empty doubleLoopStr for p1,p2 being
Polynomial of L for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2);
definition
let L be non empty ZeroStr;
let p be Polynomial of L;
func degree p -> Integer equals
:: HURWITZ:def 2
len p - 1;
end;
notation
let L be non empty ZeroStr;
let p be Polynomial of L;
synonym deg p for degree p;
end;
theorem :: HURWITZ:20
for L being non empty ZeroStr for p being Polynomial of L holds
deg p = -1 iff p = 0_.(L);
theorem :: HURWITZ:21
for L being add-associative right_zeroed right_complementable non
empty addLoopStr for p1,p2 being Polynomial of L st deg p1 <> deg p2 holds deg
(p1 + p2) = max(deg(p1),deg(p2));
theorem :: HURWITZ:22
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr for p1,p2 being Polynomial of L holds deg(p1 +
p2) <= max(deg(p1),deg(p2));
theorem :: HURWITZ:23
for L being add-associative right_zeroed right_complementable
distributive commutative associative well-unital domRing-like non empty
doubleLoopStr for p1,p2 being Polynomial of L st p1 <> 0_.(L) & p2 <> 0_.(L)
holds deg(p1 *' p2) = deg(p1) + deg(p2);
theorem :: HURWITZ:24
for L being add-associative right_zeroed right_complementable
unital non empty doubleLoopStr for p being Polynomial of L st deg p = 0 holds
not(p is with_roots);
:: the polynomials x^k - z^k
definition
let L be unital non empty 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);
end;
theorem :: HURWITZ:25
for L being unital non empty 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;
theorem :: HURWITZ:26
for L being unital non empty 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;
theorem :: HURWITZ:27
for L being well-unital non degenerated non empty doubleLoopStr
for z being Element of L for k being Element of NAT holds deg rpoly(k,z) = k;
theorem :: HURWITZ:28
for L being add-associative right_zeroed right_complementable
well-unital commutative associative distributive almost_left_invertible non
degenerated non empty 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);
theorem :: HURWITZ:29
for L being add-associative right_zeroed right_complementable
Abelian well-unital non degenerated non empty doubleLoopStr for x,z being
Element of L holds eval(rpoly(1,z),x) = x - z;
theorem :: HURWITZ:30
for L being add-associative right_zeroed right_complementable
well-unital Abelian non degenerated non empty doubleLoopStr for z being
Element of L holds z is_a_root_of rpoly(1,z);
:: 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 well-unital non empty doubleLoopStr;
let z be Element of L;
let k be Nat;
func qpoly(k,z) -> Polynomial of L means
:: 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;
end;
theorem :: HURWITZ:31
for L being well-unital non degenerated non empty doubleLoopStr for
z being Element of L for k being Element of NAT st k >= 1 holds deg qpoly(k,z)
= k - 1;
theorem :: HURWITZ:32
for L being add-associative right_zeroed right_complementable
left-distributive well-unital commutative non empty 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);
theorem :: HURWITZ:33
for L being Abelian add-associative right_zeroed
right_complementable well-unital associative distributive commutative non
empty doubleLoopStr for p being Polynomial of L for z being Element of L st z
is_a_root_of p ex s being Polynomial of L st p = rpoly(1,z) *' s;
begin :: Division of Polynomials
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let p,s be Polynomial of L such that
s <> 0_.(L);
func p div s -> Polynomial of L means
:: HURWITZ:def 5
ex t being Polynomial of L st p = it *' s + t & deg t < deg s;
end;
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let p,s be Polynomial of L;
func p mod s -> Polynomial of L equals
:: HURWITZ:def 6
p - (p div s) *' s;
end;
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let p,s be Polynomial of L;
pred s divides p means
:: HURWITZ:def 7
p mod s = 0_.(L);
end;
theorem :: HURWITZ:34
for L being Abelian add-associative right_zeroed
right_complementable well-unital associative commutative distributive
almost_left_invertible non empty 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
;
theorem :: HURWITZ:35
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
degenerated non empty 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;
theorem :: HURWITZ:36
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
degenerated non empty 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;
begin :: Schur's Theorem
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;
theorem :: HURWITZ:37
0_.(F_Complex) is non Hurwitz;
theorem :: HURWITZ:38
for x being Element of F_Complex st x <> 0.F_Complex holds x * 1_.(
F_Complex) is Hurwitz;
theorem :: 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;
theorem :: 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;
theorem :: HURWITZ:41
for f,g being Polynomial of F_Complex holds f *' g is Hurwitz
iff f is Hurwitz & g is Hurwitz;
definition
let f be Polynomial of F_Complex;
func f*' -> Polynomial of F_Complex means
:: HURWITZ:def 9
for i being Element of NAT
holds it.i = power(F_Complex).(-1_F_Complex,i) * (f.i)*';
involutiveness;
end;
theorem :: HURWITZ:42
for f being Polynomial of F_Complex holds deg(f*') = deg(f);
::$CT
theorem :: HURWITZ:44
for f being Polynomial of F_Complex for z being Element of
F_Complex holds (z * f)*' = (z*') * (f*');
theorem :: HURWITZ:45
for f being Polynomial of F_Complex holds (-f)*' = -(f*');
theorem :: HURWITZ:46
for f,g being Polynomial of F_Complex holds (f + g)*' = (f*') + (g*');
theorem :: HURWITZ:47
for f,g being Polynomial of F_Complex holds (f *' g)*' = (f*') *' (g*');
theorem :: HURWITZ:48
for x,z being Element of F_Complex holds eval(rpoly(1,z)*',x) = -x - (z*');
theorem :: HURWITZ:49
for f being Polynomial of F_Complex st f is Hurwitz for x being
Element of F_Complex st Re(x) >= 0 holds 0 < |.eval(f,x).|;
theorem :: HURWITZ:50
for f being Polynomial of F_Complex st deg(f) >= 1 & f is
Hurwitz 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).|);
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*';
end;
theorem :: HURWITZ:51
for a,b being Element of F_Complex st |.a.| > |.b.| for f being
Polynomial of F_Complex st deg(f) >= 1 holds f is Hurwitz iff a * f - b * (f*')
is Hurwitz;
theorem :: HURWITZ:52
for f being Polynomial of F_Complex st deg(f) >= 1 for rho being
Element of F_Complex st Re(rho) < 0 holds f is Hurwitz implies F*(f,rho) div
rpoly(1,rho) is Hurwitz;
theorem :: HURWITZ:53
for f being Polynomial of F_Complex st deg(f) >= 1 holds (ex rho being
Element of F_Complex st Re(rho) < 0 & |.eval(f,rho).| >= |.eval(f*',rho).|)
implies f is non Hurwitz;
::$N Schur's criterion
theorem :: HURWITZ:54
for f being Polynomial of F_Complex st deg(f) >= 1 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;