:: 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 :: (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, COMPLFLD; 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 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;