:: A Test for the Stability of Networks
:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller
::
:: Received January 17, 2013
:: Copyright (c) 2013 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 ARYTM_3, POLYNOM2, COMPLFLD, POLYNOM1, ARYTM_1, FUNCT_1,
COMPLEX1, POLYNOM3, RELAT_1, RLVECT_1, FINSEQ_1, ZFMISC_1, INT_1,
VECTSP_1, ALGSEQ_1, GROUP_1, ALGSTR_1, POLYNOM5, SGRAPH1, ALGSTR_0,
FUNCT_4, RATFUNC1, MCART_1, HURWITZ, HURWITZ2, XBOOLE_0, POLYNOM4,
BINOP_1, PARTFUN1, LATTICES, XREAL_0, ABIAN, XCMPLX_0, SQUARE_1,
STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, NUMBERS, CARD_1, ORDINAL1, MESFUNC1,
XXREAL_0, VALUED_0, YELLOW_8;
notations TARSKI, SUBSET_1, VALUED_0, NUMBERS, ORDINAL1, XCMPLX_0, COMPLEX1,
COMPLFLD, XREAL_0, SQUARE_1, RELAT_1, ALGSTR_0, FUNCT_7, VECTSP_1,
ARYTM_3, FUNCT_1, FUNCT_2, NAT_1, NAT_D, INT_1, GROUP_1, ABIAN, BINOP_1,
XXREAL_0, STRUCT_0, ALGSTR_1, RLVECT_1, VFUNCT_1, NORMSP_1, ALGSEQ_1,
POLYNOM3, POLYNOM4, POLYNOM5, RATFUNC1, HURWITZ;
constructors BINOP_1, REAL_1, BINARITH, ALGSTR_1, POLYNOM5, BHSP_1, RELSET_1,
FUNCT_4, ARYTM_3, ABIAN, NAT_D, SQUARE_1, POLYNOM4, VFUNCT_1, RATFUNC1,
HURWITZ, ALGSEQ_1, BINOP_2, XXREAL_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, INT_1, NAT_1,
MEMBERED, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1, POLYNOM4, POLYNOM5,
XREAL_0, VALUED_0, ABIAN, FUNCT_2, RATFUNC1, POLYNOM3, VFUNCT_1,
XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FINSEQ_1, POLYNOM3, STRUCT_0, ALGSTR_0, VECTSP_1, SQUARE_1,
ARYTM_3, XREAL_0, XXREAL_0, XCMPLX_0, ALGSTR_1, COMPLFLD, ALGSEQ_1,
HURWITZ, BHSP_1, VFUNCT_1, RATFUNC1;
equalities FINSEQ_1, POLYNOM3, STRUCT_0, ALGSTR_0, VECTSP_1, SQUARE_1,
ARYTM_3, XREAL_0, XXREAL_0, XCMPLX_0, ALGSTR_1, COMPLFLD, ALGSEQ_1,
HURWITZ, BHSP_1, VFUNCT_1, RATFUNC1;
expansions FINSEQ_1, POLYNOM3, STRUCT_0, ALGSTR_0, VECTSP_1, SQUARE_1,
ARYTM_3, XREAL_0, XXREAL_0, XCMPLX_0, ALGSTR_1, COMPLFLD, ALGSEQ_1,
HURWITZ, BHSP_1, VFUNCT_1, RATFUNC1;
theorems VECTSP_1, ALGSEQ_1, FUNCT_1, FUNCT_2, POLYNOM3, FUNCOP_1, RLVECT_1,
POLYNOM4, GROUP_1, TARSKI, RATFUNC1, HURWITZ, INT_1, COMPLFLD, POLYNOM5,
ALGSTR_1, COMPLEX1, FUNCT_7, NAT_1, BHSP_1, NORMSP_1, ORDINAL1, XREAL_0,
VALUED_0, XREAL_1, XXREAL_0, ABIAN, XCMPLX_1, SQUARE_1;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
theorem reim:
for x,y being complex number st Im(x) = 0 & Re(y) = 0
holds Re(x/y) = 0
proof
let x,y be complex number;
reconsider R2 = (Re y)^2, I2 = (Im y)^2 as real number;
assume AS1: Im(x) = 0 & Re(y) = 0;
then Re(x/y)
= (Re x * 0 + Im x * Im y) / (R2 + I2) by COMPLEX1:24
.= 0 / (R2 + I2) by AS1;
hence Re(x/y) = 0;
end;
theorem
for a being complex number holds a * a*' = |.a.|^2
proof
let a be complex number;
set ac = a;
reconsider b = a*' as Complex;
reconsider Ra = Re ac, Ia = Im ac as real number;
reconsider Ra2 = Ra^2, Ia2 = Ia^2 as real number;
A: |.a.| = sqrt(Ra2 + Ia2) by COMPLEX1:def 12;
reconsider xx = Ra2 + Ia2 as real number;
Ra2 >= 0 & 0 <= Ia2 by XREAL_1:63;
then |.a.|^2 = Re ac * Re ac - Im ac * (- Im ac) +
(Re ac * (- Im ac) + Re ac * Im ac) * * by A,SQUARE_1:def 2
.= Re ac * Re ac - Im ac * (- Im ac) +
(Re ac * Im b + Re ac * Im ac) * ** by COMPLEX1:27
.= Re ac * Re ac - Im ac * Im b +
(Re ac * Im b + Re ac * Im ac) * ** by COMPLEX1:27
.= Re ac * Re ac - Im ac * Im b +
(Re ac * Im b + Re b * Im ac) * ** by COMPLEX1:27
.= Re ac * Re b - Im ac * Im b +
(Re ac * Im b + Re b * Im ac) * ** by COMPLEX1:27
.= ac * b by COMPLEX1:82;
hence thesis;
end;
registration
cluster Hurwitz for Polynomial of F_Complex;
existence
proof
take (1.F_Complex) * 1_.(F_Complex);
thus thesis by HURWITZ:38;
end;
end;
oo: 2 * 0 + 1 = 1;
registration
cluster 0 -> even;
coherence;
end;
theorem pow1:
for L being add-associative right_zeroed right_complementable
associative distributive non empty doubleLoopStr
for k being even Element of NAT
for x being Element of L
holds (power L).(-x,k) = (power L).(x,k)
proof
let L be add-associative right_zeroed right_complementable
associative distributive non empty doubleLoopStr;
let k be even Element of NAT;
let x be Element of L;
defpred P[Nat] means
$1 is even implies (power L).(-x,$1) = (power L).(x,$1);
A: now let k be Nat;
assume IV: for n being Nat st n < k holds P[n];
now assume B: k is even;
now per cases by NAT_1:23;
case C: k = 0;
hence (power L).(-x,k) = 1_ L by GROUP_1:def 7
.= (power L).(x,k) by C,GROUP_1:def 7;
end;
case k = 1;
hence (power L).(-x,k) = (power L).(x,k) by oo,B;
end;
case G: k >= 2;
then reconsider k2 = k - 2 as Element of NAT by NAT_1:21;
k - 1 >= 2 - 1 by G,XREAL_1:9;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
F: k1 + 1 = k;
D: k - 2 < k - 0 by XREAL_1:10;
consider l being Element of NAT such that H: k = 2*l by B,ABIAN:def 2;
E1: 2 * (l - 1) = k - 2 by H;
reconsider a = (power L).(-x,k1) as Element of L;
reconsider b = (power L).(x,k1) as Element of L;
reconsider y = (power L).(-x,k2) as Element of L;
reconsider z = (power L).(x,k2) as Element of L;
Z1: (power L).(-x,k2+1) = y * (-x) by GROUP_1:def 7;
Z2: (power L).(x,k2+1) = z * (x) by GROUP_1:def 7;
thus (power L).(-x,k) = (y * (-x)) * (-x) by Z1,F,GROUP_1:def 7
.= (z * (-x)) * (-x) by D,IV,E1
.= z * ((-x) * (-x)) by GROUP_1:def 3
.= z * (x * x) by VECTSP_1:10
.= b * x by Z2,GROUP_1:def 3
.= (power L).(x,k) by F,GROUP_1:def 7;
end;
end;
hence (power L).(-x,k) = (power L).(x,k);
end;
hence P[k];
end;
for k being Nat holds P[k] from NAT_1:sch 4(A);
hence thesis;
end;
theorem pow2:
for L being add-associative right_zeroed right_complementable
associative distributive non empty doubleLoopStr
for k being odd Element of NAT
for x being Element of L
holds (power L).(-x,k) = - ((power L).(x,k))
proof
let L be add-associative right_zeroed right_complementable
associative distributive non empty doubleLoopStr;
let k be odd Element of NAT;
let x be Element of L;
per cases by NAT_1:14;
suppose k = 0;
hence (power L).(-x,k) = - (power L).(x,k);
end;
suppose k >= 1;
then reconsider k1 = k - 1 as Element of NAT by INT_1:5;
F: k1 + 1 = k;
reconsider a = (power L).(-x,k1) as Element of L;
reconsider b = (power L).(x,k1) as Element of L;
(power L).(-x,k1) = (power L).(x,k1) by pow1;
hence (power L).(-x,k) = b * (-x) by F,GROUP_1:def 7
.= - (b * x) by VECTSP_1:8
.= - (power L).(x,k) by F,GROUP_1:def 7;
end;
end;
theorem pow3:
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
let k be even Element of NAT;
let x be Element of F_Complex;
assume AS2: Re(x) = 0;
defpred P[Nat] means
for k1 being Element of NAT st k1 = $1 & k1 is even
for x being Element of F_Complex st Re(x) = 0
holds Im((power F_Complex).(x,k1)) = 0;
A: now let k be Nat;
assume AS: for n being Nat st n < k holds P[n];
now per cases by NAT_1:23;
case B: k = 0;
now let k1 be Element of NAT;
assume C: k1 = k & k1 is even;
let x be Element of F_Complex;
assume Re(x) = 0;
(power F_Complex).(x,0) = 1_(F_Complex) by GROUP_1:def 7
.= 1r by COMPLFLD:def 1;
hence Im((power F_Complex).(x,k1)) = 0 by B,C,COMPLEX1:6;
end;
hence P[k];
end;
case k = 1;
hence P[k] by oo;
end;
case k >= 2;
then reconsider n = k-2 as Element of NAT by INT_1:5;
reconsider n1 = n+1 as Element of NAT by ORDINAL1:def 12;
B1: n1 + 1 = k & n + 1 = n1;
now let k1 be Element of NAT;
assume C: k1 = k & k1 is even;
let x be Element of F_Complex;
assume D: Re(x) = 0;
B2: n is even
proof
consider t being Element of NAT such that
H: k = 2 * t by C,ABIAN:def 2;
n = 2 * (t - 1) by H;
hence thesis;
end;
E: now assume n >= k;
then (k - 2) - k >= k - k by XREAL_1:11;
hence contradiction;
end;
F: (power F_Complex).(x,k1)
= (power F_Complex).(x,n1) * x by C,B1,GROUP_1:def 7
.= ((power F_Complex).(x,n) * x) * x by GROUP_1:def 7
.= (power F_Complex).(x,n) * (x * x);
set z1 = (power F_Complex).(x,n), z2 = x * x;
G: Im z2 = Re x * Im x + Re x * Im x by COMPLEX1:9
.= 0 by D;
Z: Im z1 = 0 by B2,E,AS,D;
thus Im((power F_Complex).(x,k1))
= Re z1 * Im z2 + Re z2 * Im z1 by F,COMPLEX1:9
.= 0 by G,Z;
end;
hence P[k];
end;
end;
hence P[k];
end;
for k being Nat holds P[k] from NAT_1:sch 4(A);
hence thesis by AS2;
end;
theorem pow4:
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
let k be odd Element of NAT;
let x be Element of F_Complex;
assume AS2: Re(x) = 0;
defpred P[Nat] means
for k1 being Element of NAT st k1 = $1 & k1 is odd
for x being Element of F_Complex st Re(x) = 0
holds Re((power F_Complex).(x,k1)) = 0;
A: now let k be Nat;
assume AS: for n being Nat st n < k holds P[n];
now per cases by NAT_1:23;
case B: k = 1;
now let k1 be Element of NAT;
assume C: k1 = k & k1 is odd;
let x be Element of F_Complex;
assume D: Re(x) = 0;
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
1 = 0 + 1; then
(power F_Complex).(x,1)
= (power F_Complex).(x,z) * x by GROUP_1:def 7
.= 1_(F_Complex) * x by GROUP_1:def 7
.= x by VECTSP_1:def 8;
hence Re((power F_Complex).(x,k1)) = 0 by D,C,B;
end;
hence P[k];
end;
case k = 0;
hence P[k];
end;
case k >= 2;
then reconsider n = k-2 as Element of NAT by INT_1:5;
reconsider n1 = n+1 as Element of NAT by ORDINAL1:def 12;
B1: n1 + 1 = k & n + 1 = n1;
now let k1 be Element of NAT;
assume C: k1 = k & k1 is odd;
let x be Element of F_Complex;
assume D: Re(x) = 0;
B2: n is odd
proof
consider t being Integer such that
H: k = 2 * t + 1 by C,ABIAN:1;
n = 2 * (t - 1) + 1 by H;
hence thesis;
end;
E: now assume n >= k;
then (k - 2) - k >= k - k by XREAL_1:11;
hence contradiction;
end;
F: (power F_Complex).(x,k1)
= (power F_Complex).(x,n1) * x by C,B1,GROUP_1:def 7
.= ((power F_Complex).(x,n) * x) * x by GROUP_1:def 7
.= (power F_Complex).(x,n) * (x * x);
set z1 = (power F_Complex).(x,n), z2 = x * x;
G: Im z2 = Re x * Im x + Re x * Im x by COMPLEX1:9
.= 0 by D;
Z: Re z1 = 0 by B2,E,AS,D;
thus Re((power F_Complex).(x,k1))
= Re z1 * Re z2 - Im z1 * Im z2 by F,COMPLEX1:9
.= 0 by G,Z;
end;
hence P[k];
end;
end;
hence P[k];
end;
for k being Nat holds P[k] from NAT_1:sch 4(A);
hence thesis by AS2;
end;
begin :: Even and Odd Part of Polynomials
definition
let L be non empty ZeroStr;
let p be sequence of L;
func even_part p -> sequence of L means :defeven:
for i being even Nat holds it.i = p.i &
for i being odd Nat holds it.i = 0.L;
existence
proof
defpred P[element,element] means
for i being natural number st i = $1 holds
(i is even implies $2 = p.($1)) &
(i is odd implies $2 = 0.L);
A: now let x be element;
assume AS: x in NAT;
thus ex y being element st y in the carrier of L & P[x,y]
proof
reconsider m = x as natural number by AS;
per cases;
suppose B: m is even;
take p.m;
thus thesis by B;
end;
suppose B: m is odd;
take 0.L;
thus thesis by B;
end;
end;
end;
consider f being Function of NAT,the carrier of L such that
B: for x being element st x in NAT holds P[x,f.x]
from FUNCT_2:sch 1(A);
take f;
C: now let i be even natural number;
i is Element of NAT by ORDINAL1:def 12;
hence f.i = p.i by B;
end;
now let i be odd natural number;
i is Element of NAT by ORDINAL1:def 12;
hence f.i = 0.L by B;
end;
hence thesis by C;
end;
uniqueness
proof
let z1,z2 be sequence of L;
assume A10: for i being even Nat holds z1.i = p.i &
for i being odd Nat holds z1.i = 0.L;
assume A11: for i being even Nat holds z2.i = p.i &
for i being odd Nat holds z2.i = 0.L;
A12: dom z1 = NAT by FUNCT_2:def 1 .= dom z2 by FUNCT_2:def 1;
now let x be element;
assume x in dom z1;
then reconsider m = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case A: m is even;
hence z1.m = p.m by A10 .= z2.m by A,A11;
end;
case B: m is odd;
hence z1.m = 0.L by A10 .= z2.m by B,A11;
end;
end;
hence z1.x = z2.x;
end;
hence z1 = z2 by A12,FUNCT_1:2;
end;
func odd_part p -> sequence of L means :defodd:
for i being even Nat holds it.i = 0.L &
for i being odd Nat holds it.i = p.i;
existence
proof
defpred P[element, element] means
for i being natural number st i = $1 holds
(i is even implies $2 = 0.L) &
(i is odd implies $2 = p.($1));
A: now let x be element;
assume AS: x in NAT;
thus ex y being element st y in the carrier of L & P[x,y]
proof
reconsider m = x as natural number by AS;
per cases;
suppose B: m is even;
take 0.L;
thus thesis by B;
end;
suppose B: m is odd;
take p.m;
thus thesis by B;
end;
end;
end;
consider f being Function of NAT,the carrier of L such that
B: for x being element st x in NAT holds P[x,f.x]
from FUNCT_2:sch 1(A);
take f;
C: now let i be even natural number;
i is Element of NAT by ORDINAL1:def 12;
hence f.i = 0.L by B;
end;
now let i be odd natural number;
i is Element of NAT by ORDINAL1:def 12;
hence f.i = p.i by B;
end;
hence thesis by C;
end;
uniqueness
proof
let z1,z2 be sequence of L;
assume A10: for i being even Nat holds z1.i = 0.L &
for i being odd Nat holds z1.i = p.i;
assume A11: for i being even Nat holds z2.i = 0.L &
for i being odd Nat holds z2.i = p.i;
A12: dom z1 = NAT by FUNCT_2:def 1 .= dom z2 by FUNCT_2:def 1;
now let x be element;
assume x in dom z1;
then reconsider m = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case A: m is even;
hence z1.m = 0.L by A10 .= z2.m by A,A11;
end;
case B: m is odd;
hence z1.m = p.m by A10 .= z2.m by B,A11;
end;
end;hence z1.x = z2.x;
end;
hence z1 = z2 by A12,FUNCT_1:2;
end;
end;
registration
let L be non empty ZeroStr;
let p be Polynomial of L;
cluster even_part p -> finite-Support;
coherence
proof
set e = even_part p;
ex n being Nat st for i being Nat st i >= n holds e.i = 0.L
proof
set l = len p;
take l;
now let x be Nat;
reconsider i = x as Element of NAT by ORDINAL1:def 12;
assume AS: x >= l;
now per cases;
case i is even;
hence e.i = p.i by defeven .= 0.L by AS,ALGSEQ_1:8;
end;
case i is odd;
hence e.i = 0.L by defeven;
end;
end;
hence e.x = 0.L;
end;
hence thesis;
end;
hence thesis;
end;
cluster odd_part p -> finite-Support;
coherence
proof
set o = odd_part p;
ex n being Nat st for i being Nat st i >= n holds o.i = 0.L
proof
set l = len p;
take l;
now let x be Nat;
reconsider i = x as Element of NAT by ORDINAL1:def 12;
assume AS: x >= l;
now per cases;
case i is odd;
hence o.i = p.i by defodd .= 0.L by AS,ALGSEQ_1:8;
end;
case i is even;
hence o.i = 0.L by defodd;
end;
end;
hence o.x = 0.L;
end;
hence thesis;
end;
hence thesis;
end;
end;
theorem evod0:
for L being non empty ZeroStr
holds even_part 0_.(L) = 0_.(L) & odd_part 0_.(L) = 0_.(L)
proof
let L be non empty ZeroStr;
set e = even_part(0_.(L)), p = 0_.(L);
A: dom p = NAT by FUNCT_2:def 1 .= dom e by FUNCT_2:def 1;
now let x be element;
assume x in dom p;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case i is even;
hence e.i = p.i by defeven;
end;
case i is odd;
hence e.i = 0.L by defeven .= p.i by FUNCOP_1:7;
end;
end;
hence p.x = e.x;
end;
hence even_part 0_.(L) = 0_.(L) by A,FUNCT_1:2;
set o = odd_part(0_.(L));
A: dom p = NAT by FUNCT_2:def 1 .= dom o by FUNCT_2:def 1;
now let x be element;
assume x in dom p;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case i is odd;
hence o.i = p.i by defodd;
end;
case i is even;
hence o.i = 0.L by defodd .= p.i by FUNCOP_1:7;
end;
end;
hence p.x = o.x;
end;
hence odd_part 0_.(L) = 0_.(L) by A,FUNCT_1:2;
end;
theorem
for L being non empty multLoopStr_0
holds even_part 1_.(L) = 1_.(L) & odd_part 1_.(L) = 0_.(L)
proof
let L be non empty multLoopStr_0;
set e = even_part(1_.(L)), p = 1_.(L);
A: dom p = NAT by FUNCT_2:def 1 .= dom e by FUNCT_2:def 1;
now let x be element;
assume x in dom p;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case i is even;
hence e.i = p.i by defeven;
end;
case B: i is odd;
hence e.i = 0.L by defeven .= p.i by B,POLYNOM3:30;
end;
end;
hence p.x = e.x;
end;
hence even_part 1_.(L) = 1_.(L) by A,FUNCT_1:2;
set o = odd_part(1_.(L)), p = 0_.(L);
A: dom p = NAT by FUNCT_2:def 1 .= dom o by FUNCT_2:def 1;
now let x be element;
assume x in dom p;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case B: i is odd;
hence o.i = (1_.(L)).i by defodd
.= 0.L by B,POLYNOM3:30 .= p.i by FUNCOP_1:7;
end;
case i is even;
hence o.i = 0.L by defodd .= p.i by FUNCOP_1:7;
end;
end;
hence p.x = o.x;
end;
hence odd_part 1_.(L) = 0_.(L) by A,FUNCT_1:2;
end;
theorem evod2:
for L being left_zeroed right_zeroed non empty addLoopStr,
p being Polynomial of L
holds even_part p + odd_part p = p
proof
let L be left_zeroed right_zeroed non empty addLoopStr,
p be Polynomial of L;
set e = even_part p, o = odd_part p;
A: dom p = NAT by FUNCT_2:def 1 .= dom(e+o) by FUNCT_2:def 1;
now let x be element;
assume x in dom p;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case B: i is even;
hence e.i + o.i = e.i + 0.L by defodd
.= e.i by RLVECT_1:def 4 .= p.i by defeven,B;
end;
case B: i is odd;
hence e.i + o.i = 0.L + o.i by defeven
.= o.i by ALGSTR_1:def 2 .= p.i by defodd,B;
end;
end;
hence p.x = (e+o).x by NORMSP_1:def 2;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem evod3:
for L being left_zeroed right_zeroed non empty addLoopStr,
p being Polynomial of L
holds odd_part p + even_part p = p
proof
let L be left_zeroed right_zeroed non empty addLoopStr,
p be Polynomial of L;
set e = even_part p, o = odd_part p;
A: dom p = NAT by FUNCT_2:def 1 .= dom(o+e) by FUNCT_2:def 1;
now let x be element;
assume x in dom p;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case B: i is even;
hence o/.i + e/.i = 0.L + e.i by defodd
.= e.i by ALGSTR_1:def 2 .= p/.i by defeven,B;
end;
case B: i is odd;
hence o/.i + e/.i = o.i + 0.L by defeven
.= o.i by RLVECT_1:def 4 .= p/.i by defodd,B;
end;
end;
hence p.x = (o+e).x by NORMSP_1:def 2;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being Polynomial of L
holds p - odd_part p = even_part p
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr,
p be Polynomial of L;
set e = even_part p, o = odd_part p;
A: dom(p-o) = NAT by FUNCT_2:def 1 .= dom e by FUNCT_2:def 1;
now let x be element;
assume x in dom e;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
p = e + o by evod2;
then p.i = e.i + o.i by NORMSP_1:def 2;
then p.i - o.i = e.i + (o.i + - o.i) by RLVECT_1:def 3
.= e.i + 0.L by RLVECT_1:5
.= e.i by RLVECT_1:def 4;
hence (p-o).x = e.x by POLYNOM3:27;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being Polynomial of L
holds p - even_part p = odd_part p
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr,
p be Polynomial of L;
set e = even_part p, o = odd_part p;
A: dom(p-e) = NAT by FUNCT_2:def 1 .= dom o by FUNCT_2:def 1;
now let x be element;
assume x in dom o;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
p = o + e by evod3;
then p.i = o.i + e.i by NORMSP_1:def 2;
then p.i - e.i = o.i + (e.i + - e.i) by RLVECT_1:def 3
.= o.i + 0.L by RLVECT_1:5
.= o.i by RLVECT_1:def 4;
hence (p-e).x = o.x by POLYNOM3:27;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p being Polynomial of L
holds even_part p - p = - odd_part p
proof
let L be add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p be Polynomial of L;
set e = even_part p, o = odd_part p;
A: dom(e-p) = NAT by FUNCT_2:def 1 .= dom(-o) by FUNCT_2:def 1;
now let x be element;
assume x in dom(-o);
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
p = e + o by evod2;
then p.i = e.i + o.i by NORMSP_1:def 2;
then e.i - p.i = e.i + (-o.i + - e.i) by RLVECT_1:31
.= (e.i + -e.i) + - o.i by RLVECT_1:def 3
.= - o.i + 0.L by RLVECT_1:5
.= - o.i by RLVECT_1:def 4
.= (-o).i by BHSP_1:44;
hence (e-p).x = (-o).x by POLYNOM3:27;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p being Polynomial of L
holds odd_part p - p = - even_part p
proof
let L be add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p be Polynomial of L;
set e = even_part p, o = odd_part p;
A: dom(o-p) = NAT by FUNCT_2:def 1 .= dom(-e) by FUNCT_2:def 1;
now let x be element;
assume x in dom(-e);
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
p = o + e by evod2;
then p.i = o.i + e.i by NORMSP_1:def 2;
then o.i - p.i = o.i + (-e.i + - o.i) by RLVECT_1:31
.= (o.i + -o.i) + - e.i by RLVECT_1:def 3
.= 0.L + - e.i by RLVECT_1:5
.= - e.i by RLVECT_1:def 4
.= (-e).i by BHSP_1:44;
hence (o-p).x = (-e).x by POLYNOM3:27;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem evod8:
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p,q being Polynomial of L
holds even_part(p+q) = even_part(p) + even_part(q)
proof
let L be add-associative right_zeroed right_complementable
Abelian non empty addLoopStr;
let p,q be Polynomial of L;
set epq = even_part(p+q),
ep = even_part(p),
eq = even_part(q);
A: dom epq = NAT by FUNCT_2:def 1 .= dom(ep + eq) by FUNCT_2:def 1;
now let x be element;
assume x in dom(epq);
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case B: i is even;
thus(ep + eq).i = ep.i + eq.i by NORMSP_1:def 2
.= p.i + eq.i by B,defeven
.= p.i + q.i by B,defeven
.= (p+q).i by NORMSP_1:def 2
.= (epq).i by B,defeven;
end;
case B: i is odd;
thus (ep + eq).i = ep.i + eq.i by NORMSP_1:def 2
.= 0.L + eq.i by B,defeven
.= 0.L + 0.L by B,defeven
.= 0.L by RLVECT_1:def 4
.= (epq).i by B,defeven;
end;
end;
hence (ep + eq).x = (epq).x;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem evod9:
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p,q being Polynomial of L
holds odd_part(p+q) = odd_part(p) + odd_part(q)
proof
let L be add-associative right_zeroed right_complementable
Abelian non empty addLoopStr;
let p,q be Polynomial of L;
set opq = odd_part(p+q),
op = odd_part(p),
oq = odd_part(q);
A: dom opq = NAT by FUNCT_2:def 1 .= dom(op + oq) by FUNCT_2:def 1;
now let x be element;
assume x in dom(opq);
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case B: i is odd;
thus(op + oq).i = op.i + oq.i by NORMSP_1:def 2
.= p.i + oq.i by B,defodd
.= p.i + q.i by B,defodd
.= (p+q).i by NORMSP_1:def 2
.= (opq).i by B,defodd;
end;
case B: i is even;
thus (op + oq).i = op.i + oq.i by NORMSP_1:def 2
.= 0.L + oq.i by B,defodd
.= 0.L + 0.L by B,defodd
.= 0.L by RLVECT_1:def 4
.= (opq).i by B,defodd;
end;
end;
hence (op + oq).x = (opq).x;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem evenLMp1:
for L being well-unital non empty doubleLoopStr
for p being Polynomial of L st deg p is even
holds even_part Leading-Monomial(p) = Leading-Monomial(p)
proof
let L be well-unital non empty doubleLoopStr;
let p be Polynomial of L;
assume AS: deg p is even;
set LMp = Leading-Monomial(p);
set e = even_part LMp;
A: dom e = NAT by FUNCT_2:def 1 .= dom LMp by FUNCT_2:def 1;
now let x be element;
assume x in dom e;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case len p = 0;
then p = 0_.(L) by POLYNOM4:5;
then LMp = 0_.(L) by POLYNOM4:13;
hence e.x = LMp.x by evod0;
end;
case len p <> 0;
then len p + 1 > 0 + 1 by XREAL_1:8;
then len p >= 1 by NAT_1:13;
then B: len p -' 1 = deg p by XREAL_1:233;
now per cases;
case i is even;
hence e.i = LMp.i by defeven;
end;
case C: i is odd;
hence LMp.i = 0.L by B,AS,POLYNOM4:def 1
.= e.i by C,defeven;
end;
end;
hence e.x = LMp.x;
end;
end;
hence e.x = LMp.x;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem evenLMp2:
for L being well-unital non empty doubleLoopStr
for p being Polynomial of L st deg p is odd
holds even_part Leading-Monomial(p) = 0_.(L)
proof
let L be well-unital non empty doubleLoopStr;
let p be Polynomial of L;
assume AS: deg p is odd;
set LMp = Leading-Monomial(p);
set e = even_part LMp;
A: dom 0_.(L) = NAT by FUNCT_2:def 1 .= dom e by FUNCT_2:def 1;
now let x be element;
assume x in dom 0_.(L);
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case len p = 0;
then p = 0_.(L) by POLYNOM4:5;
then LMp = 0_.(L) by POLYNOM4:13;
hence e.x = (0_.(L)).x by evod0;
end;
case len p <> 0;
then len p + 1 > 0 + 1 by XREAL_1:8;
then len p >= 1 by NAT_1:13;
then B: len p -' 1 = deg p by XREAL_1:233;
now per cases;
case C: i is even;
hence e.i = LMp.i by defeven
.= 0.L by C,B,AS,POLYNOM4:def 1
.= (0_.(L)).i by FUNCOP_1:7;
end;
case i is odd;
hence e.i = 0.L by defeven
.= (0_.(L)).i by FUNCOP_1:7;
end;
end;
hence e.x = (0_.(L)).x;
end;
end;
hence e.x = (0_.(L)).x;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem oddLMp1:
for L being well-unital non empty doubleLoopStr
for p being Polynomial of L st deg p is even
holds odd_part Leading-Monomial(p) = 0_.(L)
proof
let L be well-unital non empty doubleLoopStr;
let p be Polynomial of L;
assume AS: deg p is even;
set LMp = Leading-Monomial(p);
set o = odd_part LMp;
A: dom 0_.(L) = NAT by FUNCT_2:def 1 .= dom o by FUNCT_2:def 1;
now let x be element;
assume x in dom 0_.(L);
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case len p = 0;
then p = 0_.(L) by POLYNOM4:5;
then LMp = 0_.(L) by POLYNOM4:13;
hence o.x = (0_.(L)).x by evod0;
end;
case len p <> 0;
then len p + 1 > 0 + 1 by XREAL_1:8;
then len p >= 1 by NAT_1:13;
then B: len p -' 1 = deg p by XREAL_1:233;
now per cases;
case C: i is odd;
hence o.i = LMp.i by defodd
.= 0.L by C,B,AS,POLYNOM4:def 1
.= (0_.(L)).i by FUNCOP_1:7;
end;
case i is even;
hence o.i = 0.L by defodd
.= (0_.(L)).i by FUNCOP_1:7;
end;
end;
hence o.x = (0_.(L)).x;
end;
end;
hence o.x = (0_.(L)).x;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem oddLMp2:
for L being well-unital non empty doubleLoopStr
for p being Polynomial of L st deg p is odd
holds odd_part Leading-Monomial(p) = Leading-Monomial(p)
proof
let L be well-unital non empty doubleLoopStr;
let p be Polynomial of L;
assume AS: deg p is odd;
set LMp = Leading-Monomial(p);
set o = odd_part LMp;
A: dom o = NAT by FUNCT_2:def 1 .= dom LMp by FUNCT_2:def 1;
now let x be element;
assume x in dom o;
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now per cases;
case len p = 0;
then p = 0_.(L) by POLYNOM4:5;
then LMp = 0_.(L) by POLYNOM4:13;
hence o.x = LMp.x by evod0;
end;
case len p <> 0;
then len p + 1 > 0 + 1 by XREAL_1:8;
then len p >= 1 by NAT_1:13;
then B: len p -' 1 = deg p by XREAL_1:233;
now per cases;
case i is odd;
hence o.i = LMp.i by defodd;
end;
case C: i is even;
hence LMp.i = 0.L by B,AS,POLYNOM4:def 1
.= o.i by C,defodd;
end;
end;
hence o.x = LMp.x;
end;
end;
hence o.x = LMp.x;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem deg0:
for L being well-unital add-associative right_zeroed right_complementable
Abelian associative distributive non degenerated doubleLoopStr
for p being non zero Polynomial of L
holds deg even_part(p) <> deg odd_part(p)
proof
let L be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non degenerated doubleLoopStr;
let p be non zero Polynomial of L;
set e = even_part(p), o = odd_part(p);
per cases;
suppose A: o = 0_.(L) or e = 0_.(L);
then C: deg o = - 1 or deg e = - 1 by HURWITZ:20;
D: 0_.(L) + 0_.(L) = 0_.(L) by POLYNOM3:28;
now per cases by A;
case o = 0_.(L);
then e <> 0_.(L) by D,evod2;
hence thesis by C,HURWITZ:20;
end;
case e = 0_.(L);
then o <> 0_.(L) by D,evod2;
hence thesis by C,HURWITZ:20;
end;
end;
hence thesis;
end;
suppose o <> 0_.(L) & e <> 0_.(L);
then reconsider e,o as non zero Polynomial of L by RATFUNC1:def 1;
reconsider de = degree e as Element of NAT by ORDINAL1:def 12;
reconsider deo = degree o as Element of NAT by ORDINAL1:def 12;
now assume AS: deg e = deg o;
degree e + 1 = len e;
then F: e.de <> 0.L by ALGSEQ_1:10;
degree o + 1 = len o;
then G: o.deo <> 0.L by ALGSEQ_1:10;
now per cases;
case degree e is even;
hence contradiction by G,AS,defodd;
end;
case degree e is odd;
hence contradiction by F,defeven;
end;
end;
hence contradiction;
end;
hence thesis;
end;
end;
theorem
for L being well-unital add-associative right_zeroed right_complementable
associative Abelian distributive non degenerated doubleLoopStr
for p being Polynomial of L
holds deg even_part(p) <= deg p & deg odd_part(p) <= deg p
proof
let L be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non degenerated doubleLoopStr;
let p be Polynomial of L;
set e = even_part(p), o = odd_part(p);
per cases;
suppose p = 0_.(L);
hence thesis by evod0;
end;
suppose p <> 0_.(L);
then reconsider pp = p as non zero Polynomial of L by RATFUNC1:def 1;
p = e + o by evod2;
then A: deg pp = max(deg(e),deg(o)) by deg0,HURWITZ:21;
hence deg even_part(p) <= deg p by XXREAL_0:25;
thus deg odd_part(p) <= deg p by A,XXREAL_0:25;
end;
end;
theorem evoddeg:
for L being well-unital add-associative right_zeroed right_complementable
associative Abelian distributive non degenerated doubleLoopStr
for p being Polynomial of L
holds deg p = max( deg even_part(p), deg odd_part(p))
proof
let L be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non degenerated doubleLoopStr;
let p be Polynomial of L;
set e = even_part(p), o = odd_part(p);
per cases;
suppose A: p = 0_.(L);
then e = 0_.(L) & o = 0_.(L) by evod0;
hence thesis by A;
end;
suppose p <> 0_.(L);
then reconsider pp = p as non zero Polynomial of L by RATFUNC1:def 1;
p = e + o by evod2;
then deg pp = max(deg(e),deg(o)) by deg0,HURWITZ:21;
hence thesis;
end;
end;
begin :: Even and Odd Polynomials and Rational Functions
definition
let L be non empty addLoopStr;
let f be Function of L,L;
attr f is even means :deffuncteven:
for x being Element of L holds f.(-x) = f.x;
attr f is odd means :deffunctodd:
for x being Element of L holds f.(-x) = - f.x;
end;
definition
let L be well-unital non empty doubleLoopStr;
let p be Polynomial of L;
attr p is even means :defpoleven:
Polynomial-Function(L,p) is even;
attr p is odd means :defpolodd:
Polynomial-Function(L,p) is odd;
end;
definition
let L be well-unital non trivial doubleLoopStr;
let Z be rational_function of L;
attr Z is odd means
(Z`1 is even & Z`2 is odd) or (Z`1 is odd & Z`2 is even);
end;
notation
let L be well-unital non trivial doubleLoopStr;
let Z be rational_function of L;
antonym Z is even for Z is odd;
end;
registration
let L be well-unital non empty doubleLoopStr;
cluster even for Polynomial of L;
existence
proof
set p = 0_.(L);
take p;
set f = Polynomial-Function(L,p);
A: now let x be Element of L;
thus f.x = eval(p,x) by POLYNOM5:def 12
.= 0.L by POLYNOM4:17;
end;
now let x be Element of L;
thus f.(-x) = 0.L by A .= f.x by A;
end;
hence thesis by deffuncteven;
end;
end;
registration
let L be add-associative right_zeroed right_complementable
well-unital non empty doubleLoopStr;
cluster odd for Polynomial of L;
existence
proof
set p = 0_.(L);
take p;
set f = Polynomial-Function(L,p);
A: now let x be Element of L;
thus f.x = eval(p,x) by POLYNOM5:def 12
.= 0.L by POLYNOM4:17;
end;
now let x be Element of L;
thus f.(-x) = 0.L by A .= -0.L by RLVECT_1:12 .= - f.x by A;
end;
hence thesis by deffunctodd;
end;
end;
registration
let L be well-unital add-associative right_zeroed right_complementable
associative non degenerated doubleLoopStr;
cluster non zero even for Polynomial of L;
existence
proof
set p = 1_.(L);
take p;
set f = Polynomial-Function(L,p);
A: now let x be Element of L;
thus f.x = eval(p,x) by POLYNOM5:def 12
.= 1.L by POLYNOM4:18;
end;
now let x be Element of L;
thus f.(-x) = 1.L by A .= f.x by A;
end;
hence thesis by deffuncteven;
end;
end;
registration
let L be add-associative right_zeroed right_complementable
Abelian well-unital non degenerated doubleLoopStr;
cluster non zero odd for Polynomial of L;
existence
proof
set p = rpoly(1,0.L);
take p;
set f = Polynomial-Function(L,p);
now let x be Element of L;
thus f.(-x) = eval(p,-x) by POLYNOM5:def 12
.= (-x) - 0.L by HURWITZ:29
.= - x by RLVECT_1:13
.= - (x - 0.L) by RLVECT_1:13
.= - eval(p,x) by HURWITZ:29
.= - f.x by POLYNOM5:def 12;
end;
then f is odd;
hence thesis;
end;
end;
theorem eveneval:
for L being well-unital non empty doubleLoopStr
for p being even Polynomial of L
for x being Element of L
holds eval(p,-x) = eval(p,x)
proof
let L be well-unital non empty doubleLoopStr;
let p be even Polynomial of L;
let x be Element of L;
thus eval(p,-x) = Polynomial-Function(L,p).(-x) by POLYNOM5:def 12
.= Polynomial-Function(L,p).x by deffuncteven,defpoleven
.= eval(p,x) by POLYNOM5:def 12;
end;
theorem oddeval:
for L being add-associative right_zeroed right_complementable Abelian
well-unital non degenerated doubleLoopStr
for p being odd Polynomial of L
for x being Element of L
holds eval(p,-x) = - eval(p,x)
proof
let L be add-associative right_zeroed right_complementable Abelian
well-unital non degenerated doubleLoopStr;
let p be odd Polynomial of L;
let x be Element of L;
A: Polynomial-Function(L,p) is odd by defpolodd;
thus eval(p,-x) = Polynomial-Function(L,p).(-x) by POLYNOM5:def 12
.= - Polynomial-Function(L,p).x by A
.= - eval(p,x) by POLYNOM5:def 12;
end;
registration
let L be well-unital non empty doubleLoopStr;
cluster 0_.(L) -> even;
coherence
proof
set f = Polynomial-Function(L,0_.(L));
now let x be Element of L;
thus f.(-x) = eval(0_.(L),-x) by POLYNOM5:def 12
.= 0.L by POLYNOM4:17
.= eval(0_.(L),x) by POLYNOM4:17
.= f.x by POLYNOM5:def 12;
end;
then f is even;
hence thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable
well-unital non empty doubleLoopStr;
cluster 0_.(L) -> odd;
coherence
proof
set f = Polynomial-Function(L,0_.(L));
now let x be Element of L;
thus f.(-x) = eval(0_.(L),-x) by POLYNOM5:def 12
.= 0.L by POLYNOM4:17
.= - 0.L by RLVECT_1:12
.= - eval(0_.(L),x) by POLYNOM4:17
.= - f.x by POLYNOM5:def 12;
end;
hence thesis by deffunctodd;
end;
end;
registration
let L be well-unital add-associative right_zeroed right_complementable
associative non degenerated doubleLoopStr;
cluster 1_.(L) -> even;
coherence
proof
set f = Polynomial-Function(L,1_.(L));
now let x be Element of L;
thus f.(-x) = eval(1_.(L),-x) by POLYNOM5:def 12
.= 1.L by POLYNOM4:18
.= eval(1_.(L),x) by POLYNOM4:18
.= f.x by POLYNOM5:def 12;
end;
then f is even;
hence 1_.(L) is even;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital left-distributive non empty doubleLoopStr;
let p,q be even Polynomial of L;
cluster p + q -> even;
coherence
proof
set g = Polynomial-Function(L,p+q);
now let x be Element of L;
thus g.(-x) = eval(p+q,-x) by POLYNOM5:def 12
.= eval(p,-x) + eval(q,-x) by POLYNOM4:19
.= eval(p,x) + eval(q,-x) by eveneval
.= eval(p,x) + eval(q,x) by eveneval
.= eval(p+q,x) by POLYNOM4:19
.= g.x by POLYNOM5:def 12;
end;
hence thesis by deffuncteven;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital left-distributive non degenerated doubleLoopStr;
let p,q be odd Polynomial of L;
cluster p + q -> odd;
coherence
proof
set g = Polynomial-Function(L,p+q);
now let x be Element of L;
thus g.(-x) = eval(p+q,-x) by POLYNOM5:def 12
.= eval(p,-x) + eval(q,-x) by POLYNOM4:19
.= (- eval(p,x)) + eval(q,-x) by oddeval
.= (- eval(p,x)) + (- eval(q,x)) by oddeval
.= - (eval(p,x) + eval(q,x)) by RLVECT_1:31
.= - eval(p+q,x) by POLYNOM4:19
.= - g.x by POLYNOM5:def 12;
end;
then g is odd;
hence thesis;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
associative well-unital distributive non degenerated doubleLoopStr;
let p be Polynomial of L;
cluster even_part(p) -> even;
coherence
proof
defpred P[Nat] means
for p being Polynomial of L st len p = $1
holds even_part(p) is even;
A: now let k be Nat;
assume AS1: for n being Nat st n < k holds P[n];
now let p be Polynomial of L;
assume AS2: len p = k;
now per cases;
case k = 0;
then p = 0_.(L) by AS2,POLYNOM4:5;
hence even_part(p) is even by evod0;
end;
case X: k <> 0;
set LMp = Leading-Monomial(p);
set g = Polynomial-Function(L,LMp);
LMp + (p-LMp) = (LMp + - LMp) + p by POLYNOM3:26
.= (LMp - LMp) + p
.= 0_.(L) + p by POLYNOM3:29
.= p by POLYNOM3:28;
then B: even_part(p) = even_part(LMp) + even_part(p-LMp) by evod8;
consider t being Polynomial of L such that
C: len t < len p & p = t + Leading-Monomial(p) &
for n being Element of NAT st n < len p-1 holds t.n = p.n
by X,AS2,POLYNOM4:16;
p - LMp = t + (LMp - LMp) by C,POLYNOM3:26
.= t + 0_.(L) by POLYNOM3:29
.= t by POLYNOM3:28;
then IV: even_part(p-LMp) is even by C,AS1,AS2;
now per cases;
case Z: deg p is even;
now let x be Element of L;
len p + 1 > 0 + 1 by AS2,X,XREAL_1:8;
then len p >= 1 by NAT_1:13;
then E: len p -' 1 = deg p by XREAL_1:233;
thus g.x = eval(LMp,x) by POLYNOM5:def 12
.= p.(len p-'1) * (power L).(x,len p-'1) by POLYNOM4:22
.= p.(len p-'1) * (power L).(-x,len p-'1) by E,Z,pow1
.= eval(LMp,-x) by POLYNOM4:22
.= g.(-x) by POLYNOM5:def 12;
end;
then g is even;
hence even_part(LMp) is even by Z,evenLMp1;
end;
case deg p is odd;
then even_part(LMp) = 0_.(L) by evenLMp2;
hence even_part(LMp) is even;
end;
end;
hence even_part(p) is even by IV,B;
end;
end;
hence even_part(p) is even;
end;
hence P[k];
end;
I: for k being Nat holds P[k] from NAT_1:sch 4(A);
consider k being Nat such that H: len p = k;
thus thesis by H,I;
end;
cluster odd_part(p) -> odd;
coherence
proof
defpred P[Nat] means
for p being Polynomial of L st len p = $1
holds odd_part(p) is odd;
A: now let k be Nat;
assume AS1: for n being Nat st n < k holds P[n];
now let p be Polynomial of L;
assume AS2: len p = k;
now per cases;
case k = 0;
then p = 0_.(L) by AS2,POLYNOM4:5;
hence odd_part(p) is odd by evod0;
end;
case X: k <> 0;
set LMp = Leading-Monomial(p);
set g = Polynomial-Function(L,LMp);
LMp + (p-LMp) = (LMp + - LMp) + p by POLYNOM3:26
.= (LMp - LMp) + p
.= 0_.(L) + p by POLYNOM3:29
.= p by POLYNOM3:28;
then B: odd_part(p) = odd_part(LMp) + odd_part(p-LMp) by evod9;
consider t being Polynomial of L such that
C: len t < len p & p = t + Leading-Monomial(p) &
for n being Element of NAT st n < len p-1 holds t.n = p.n
by X,AS2,POLYNOM4:16;
p - LMp = t + (LMp - LMp) by C,POLYNOM3:26
.= t + 0_.(L) by POLYNOM3:29
.= t by POLYNOM3:28;
then IV: odd_part(p-LMp) is odd by C,AS1,AS2;
now per cases;
case Z: deg p is odd;
then D: odd_part(LMp) = LMp by oddLMp2;
now let x be Element of L;
len p + 1 > 0 + 1 by AS2,X,XREAL_1:8;
then len p >= 1 by NAT_1:13;
then E: len p -' 1 = deg p by XREAL_1:233;
thus - g.x = - eval(LMp,x) by POLYNOM5:def 12
.= - (p.(len p-'1) * (power L).(x,len p-'1)) by POLYNOM4:22
.= p.(len p-'1) * (-(power L).(x,len p-'1)) by VECTSP_1:8
.= p.(len p-'1) * (power L).(-x,len p-'1) by E,Z,pow2
.= eval(LMp,-x) by POLYNOM4:22
.= g.(-x) by POLYNOM5:def 12;
end;
hence odd_part(LMp) is odd by D,deffunctodd;
end;
case deg p is even;
then odd_part(LMp) = 0_.(L) by oddLMp1;
hence odd_part(LMp) is odd;
end;
end;
hence odd_part(p) is odd by IV,B;
end;
end;
hence odd_part(p) is odd;
end;
hence P[k];
end;
I: for k being Nat holds P[k] from NAT_1:sch 4(A);
consider k being Nat such that H: len p = k;
thus thesis by H,I;
end;
end;
theorem evodroot:
for L being Abelian add-associative right_zeroed right_complementable
well-unital distributive non degenerated 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
let L be Abelian add-associative right_zeroed right_complementable
well-unital distributive non degenerated doubleLoopStr;
let p be even Polynomial of L;
let q be odd Polynomial of L;
let x be Element of L;
assume H: x is_a_common_root_of p,q;
then H1: eval(p,x) = 0.L by POLYNOM5:def 6;
eval(p+q,-x) = eval(p,-x) + eval(q,-x) by POLYNOM4:19
.= eval(p,x) + eval(q,-x) by eveneval
.= eval(p,x) + - eval(q,x) by oddeval
.= 0.L + - 0.L by H1,H,POLYNOM5:def 6
.= 0.L by RLVECT_1:5;
hence -x is_a_root_of p+q by POLYNOM5:def 6;
end;
theorem
for p being Hurwitz Polynomial of F_Complex
holds even_part(p), odd_part(p) have_no_common_roots
proof
let p be Hurwitz Polynomial of F_Complex;
set e = even_part(p), o = odd_part(p);
let x be Element of F_Complex;
assume AS: x is_a_common_root_of e,o;
A2: x is_a_root_of e+o by AS,RATFUNC1:16;
e + o = p by evod2;
then L: Re(x) < 0 & Re(-x) < 0 by AS,evodroot,A2,HURWITZ:def 8;
reconsider s = x as complex number;
Re(-s) = - Re(s) by COMPLEX1:17;
hence contradiction by L,COMPLFLD:2;
end;
begin :: Real Positive Polynomials and Rational Functions
definition
let p be Polynomial of F_Complex;
attr p is real means :defrealpo:
for i being Nat holds p.i is real number;
attr p is positive means
for x being Element of F_Complex holds Re(x) > 0 implies Re(eval(p,x)) > 0;
end;
registration
cluster 0_.(F_Complex) -> real non positive;
coherence
proof
set p = 0_.(F_Complex);
now let i be Nat;
p.i = 0.F_Complex by FUNCOP_1:7,ORDINAL1:def 12
.= 0 by COMPLFLD:def 1;
hence p.i is real number;
end;
hence p is real;
A: Re(1.F_Complex) > 0 by COMPLEX1:6,COMPLFLD:def 1;
eval(p,1.F_Complex) = 0.F_Complex by POLYNOM4:17 .= 0 by COMPLFLD:def 1;
hence p is non positive by A,COMPLEX1:4;
end;
cluster 1_.(F_Complex) -> real positive;
coherence
proof
set p = 1_.(F_Complex);
now let i be Nat;
now per cases;
case i = 0;
then p.i = 1.F_Complex by POLYNOM3:30
.= 1 by COMPLEX1:def 4,COMPLFLD:def 1;
hence p.i is real number;
end;
case i <> 0;
then p.i = 0.F_Complex by POLYNOM3:30
.= 0 by COMPLFLD:def 1;
hence p.i is real number;
end;
end;
hence p.i is real number;
end;
hence p is real;
thus p is positive by POLYNOM4:18,COMPLFLD:8,COMPLEX1:6;
end;
end;
registration
cluster non zero real positive for Polynomial of F_Complex;
existence
proof
set p = 1_.(F_Complex);
take p;
thus p is non zero;
thus p is real;
thus p is positive;
end;
end;
registration
cluster real -> real-valued for Polynomial of F_Complex;
coherence
proof
let p be Polynomial of F_Complex;
assume AS: p is real;
now let y be element;
assume y in rng p;
then consider x being element such that
H: x in dom p & p.x = y by FUNCT_1:def 3;
reconsider x as Element of NAT by H,FUNCT_2:def 1;
p.x is real number by AS;
hence y in REAL by H,XREAL_0:def 1;
end;
hence thesis by VALUED_0:def 3,TARSKI:def 3;
end;
end;
registration
let p be real Polynomial of F_Complex;
cluster even_part(p) -> real;
coherence
proof
set e = even_part p;
now let i be Nat;
now per cases;
case i is odd;
then e.i = 0.F_Complex by defeven .= 0 by COMPLFLD:def 1;
hence e.i is real number;
end;
case i is even;
then e.i = p.i by defeven;
hence e.i is real number;
end;
end;
hence e.i is real number;
end;
hence thesis;
end;
cluster odd_part(p) -> real;
coherence
proof
set o = odd_part p;
now let i be Nat;
now per cases;
case i is even;
then o.i = 0.F_Complex by defodd .= 0 by COMPLFLD:def 1;
hence o.i is real number;
end;
case i is odd;
then o.i = p.i by defodd;
hence o.i is real number;
end;
end;
hence o.i is real number;
end;
hence thesis;
end;
end;
definition
let L be non empty addLoopStr;
let p be Polynomial of L;
attr p is with_all_coefficients means :wacoeff:
for i being Nat st i <= deg p holds p.i <> 0;
end;
definition
let p be real Polynomial of F_Complex;
attr p is with_positive_coefficients means
for i being Nat st i <= deg p holds p.i > 0;
attr p is with_negative_coefficients means
for i being Nat st i <= deg p holds p.i < 0;
end;
registration
cluster with_positive_coefficients -> with_all_coefficients
for real Polynomial of F_Complex;
coherence
proof
let p be real Polynomial of F_Complex;
assume p is with_positive_coefficients;
hence p is with_all_coefficients;
end;
cluster with_negative_coefficients -> with_all_coefficients
for real Polynomial of F_Complex;
coherence
proof
let p be real Polynomial of F_Complex;
assume p is with_negative_coefficients;
hence p is with_all_coefficients;
end;
end;
registration
cluster non constant with_positive_coefficients
for real Polynomial of F_Complex;
existence
proof
set L = F_Complex;
set x = 1.F_Complex;
set p = (0_.(L)+*(0,x))+*(1,x);
F1: dom(0_.(L)) = NAT by FUNCOP_1:13;
then F2: dom(0_.(L)+*(0,x)) = NAT by FUNCT_7:30;
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
Z0: p.0 = (0_.(L)+*(z,x)).z by FUNCT_7:32
.= x by F1,FUNCT_7:31
.= 1 by COMPLFLD:def 1,COMPLEX1:def 4;
Z1: p.1 = x by F2,FUNCT_7:31
.= 1 by COMPLFLD:def 1,COMPLEX1:def 4;
Z2: now let i be Nat;
now per cases by NAT_1:23;
case i = 0;
hence p.i is real number by Z0;
end;
case i = 1;
hence p.i is real number by Z1;
end;
case AS: i >= 2;
then i <> 1;
then p.i = (0_.(L)+*(0,x)).i by FUNCT_7:32
.= (0_.(L)).i by AS,FUNCT_7:32
.= 0.L by FUNCOP_1:7,ORDINAL1:def 12
.= 0 by COMPLFLD:def 1;
hence p.i is real number;
end;
end;
hence p.i is real number;
end;
ex n being Nat st for i being Nat st i >= n holds p.i = 0.L
proof
take 2;
now let i be Nat;
assume AS: i >= 2;
then 1 <> i;
hence p.i = (0_.(L)+*(0,x)).i by FUNCT_7:32
.= (0_.(L)).i by AS,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
hence thesis;
end;
then reconsider p as Polynomial of L by ALGSEQ_1:def 1;
now let i be Nat;
assume AS: i >= 2;
then 1 <> i;
hence p.i = (0_.(L)+*(0,x)).i by FUNCT_7:32
.= (0_.(L)).i by AS,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
then D1: 2 is_at_least_length_of p;
now let m be Nat;
assume AS: m is_at_least_length_of p;
now assume m < 2;
then m < 1 + 1;
then p.1 = 0.L by AS,INT_1:7;
hence contradiction by F2,FUNCT_7:31;
end;
hence 2 <= m;
end;
then E: len p = 2 by D1,ALGSEQ_1:def 3;
reconsider p as real Polynomial of F_Complex by Z2,defrealpo;
take p;
thus p is non constant by E;
now let i be Nat;
assume i <= deg p;
then E2: i < 1 + 1 by E,NAT_1:13;
now per cases by E2,NAT_1:23;
case i = 0;
hence p.i > 0 by Z0;
end;
case i = 1;
hence p.i > 0 by Z1;
end;
end;
hence p.i > 0;
end;
hence p is with_positive_coefficients;
end;
end;
registration
let p be non zero with_all_coefficients real Polynomial of F_Complex;
cluster even_part p -> non zero;
coherence
proof
set e = even_part p;
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
0 <= degree p;
then B: p.z <> z by wacoeff;
e.z = p.z by defeven;
then e.z <> 0.F_Complex by B,COMPLFLD:def 1;
hence thesis by FUNCOP_1:7;
end;
end;
registration
let p be non constant with_all_coefficients real Polynomial of F_Complex;
cluster odd_part p -> non zero;
coherence
proof
set o = odd_part p;
0 + 1 <= degree p by INT_1:7,RATFUNC1:def 2;
then B: p.1 <> 0 by wacoeff;
o.1 = p.1 by defodd,oo;
then o.1 <> 0.F_Complex by B,COMPLFLD:def 1;
hence thesis by FUNCOP_1:7;
end;
end;
definition
let Z be rational_function of F_Complex;
attr Z is real means :defreal:
for i being Nat holds (Z`1).i is real number & (Z`2).i is real number;
attr Z is positive means
for x being Element of F_Complex
st Re(x) > 0 & eval(Z`2,x) <> 0 holds Re(eval(Z,x)) > 0;
end;
registration
cluster non zero odd real positive for rational_function of F_Complex;
existence
proof
set f = rpoly(1,0.F_Complex);
set p = [ f, 1_.(F_Complex) ];
Y: now let x be Element of F_Complex;
thus eval(f,x) = x - 0.F_Complex by HURWITZ:29
.= x by RLVECT_1:13;
end;
take p;
thus p is non zero;
set fp = Polynomial-Function(F_Complex,f);
now let x be Element of F_Complex;
thus fp.(-x) = eval(f,-x) by POLYNOM5:def 12
.= (-x) - 0.F_Complex by HURWITZ:29
.= - x by RLVECT_1:13
.= - (x - 0.F_Complex) by RLVECT_1:13
.= - eval(f,x) by HURWITZ:29
.= - fp.x by POLYNOM5:def 12;
end;
then fp is odd;
then f is odd;
hence p is odd;
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
now let i be Nat;
AA: i in NAT by ORDINAL1:def 12;
now per cases;
case B: i = 0;
C: 0 + 1 = 1;
f.i = -power(F_Complex).(0.F_Complex,1) by B,HURWITZ:25
.= -power(F_Complex).(0.F_Complex,z) * 0.F_Complex by C,GROUP_1:def 7
.= 0.F_Complex by RLVECT_1:12;
hence f.i is real number by COMPLFLD:def 1;
end;
case i = 1;
then f.i = 1.F_Complex by HURWITZ:25
.= 1r by COMPLFLD:def 1;
hence f.i is real number by COMPLEX1:def 4;
end;
case i <> 1 & i <> 0;
then f.i = 0.F_Complex by HURWITZ:26,AA
.= 0 by COMPLFLD:def 1;
hence f.i is real number;
end;
end;
hence (p`1).i is real number;
thus (p`2).i is real number;
end;
hence p is real;
now let x be Element of F_Complex;
assume G: Re(x) > 0 & eval(p`2,x) <> 0;
D: eval(1_.(F_Complex),x) = 1_ (F_Complex) by POLYNOM4:18;
1.(F_Complex) <> 0.(F_Complex);
then F: (1.(F_Complex))" * 1.(F_Complex) = 1.(F_Complex)
by VECTSP_1:def 10;
eval(p,x) = x * (1.(F_Complex))" by Y,D
.= x * 1.(F_Complex) by F,VECTSP_1:def 4
.= x by VECTSP_1:def 4;
hence Re(eval(p,x)) > 0 by G;
end;
hence p is positive;
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
proof
set p = [p1,p2];
for i being Nat holds
(p`1).i is real number & (p`2).i is real number;
hence thesis by defreal;
end;
end;
begin :: The Theorem
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 evim:
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
let p be real Polynomial of F_Complex;
let x be Element of F_Complex;
defpred P[Nat] means
for p being Polynomial of F_Complex st p is real & len p = $1 holds
(for x being Element of F_Complex st Re(x) = 0
holds Im(eval(even_part(p),x)) = 0);
B: now let k be Nat;
assume AS1: for n being Nat st n < k holds P[n];
now let p be Polynomial of F_Complex;
assume AS2: p is real & len p = k;
now per cases by NAT_1:14;
case k = 0;
then p = 0_.(F_Complex) by AS2,POLYNOM4:5;
then A: even_part(p) = 0_.(F_Complex) by evod0;
thus for x being Element of F_Complex st Re(x) = 0
holds Im(eval(even_part(p),x)) = 0
proof
let x be Element of F_Complex;
assume Re(x) = 0;
eval(even_part(p),x) = 0.F_Complex by A,POLYNOM4:17
.= 0 by COMPLFLD:def 1;
hence thesis by COMPLEX1:4;
end;
end;
case X: k >= 1;
set LMp = Leading-Monomial(p);
LMp + (p-LMp) = (LMp + - LMp) + p by POLYNOM3:26
.= (LMp - LMp) + p
.= 0_.(F_Complex) + p by POLYNOM3:29
.= p by POLYNOM3:28;
then B: even_part(p) = even_part(LMp) + even_part(p-LMp) by evod8;
thus for x being Element of F_Complex st Re(x) = 0
holds Im(eval(even_part(p),x)) = 0
proof
let x be Element of F_Complex;
assume AS3: Re(x) = 0;
consider t being Polynomial of F_Complex such that
C: len t < len p & p = t + Leading-Monomial(p) &
for n being Element of NAT st n < len p-1 holds t.n = p.n
by X,AS2,POLYNOM4:16;
D1: p - LMp = t + (LMp - LMp) by C,POLYNOM3:26
.= t + 0_.(F_Complex) by POLYNOM3:29
.= t by POLYNOM3:28;
now let n be Nat;
A: n in NAT by ORDINAL1:def 12;
now per cases;
case n < len p-1;
then t.n = p.n by C,A;
hence t.n is real number by AS2;
end;
case D: n >= len p-1;
reconsider lp = len p-1 as Element of NAT by X,AS2,INT_1:5;
len t < lp + 1 by C;
then lp >= len t by NAT_1:13;
then t.n = 0.F_Complex by ALGSEQ_1:8,D,XXREAL_0:2;
hence t.n is real number by COMPLFLD:def 1;
end;
end;
hence t.n is real number;
end;
then D: t is real;
F: Im(eval(even_part(LMp),x)) = 0
proof
now per cases;
case deg p is odd;
then even_part(LMp) = 0_.(F_Complex) by evenLMp2;
then eval(even_part(LMp),x) = 0.F_Complex by POLYNOM4:17
.= 0 by COMPLFLD:def 1;
hence thesis by COMPLEX1:4;
end;
case G: deg p is even;
then H: eval(even_part(LMp),x)
= eval(LMp,x) by evenLMp1
.= p.(len p-'1) * (power F_Complex).(x,len p-'1)
by POLYNOM4:22;
set z1 = p.(len p-'1), z2 = (power F_Complex).(x,len p-'1);
len p -' 1 = deg p by AS2,X,XREAL_1:233;
then I: Im z2 = 0 by AS3,G,pow3;
z1 in REAL by AS2,XREAL_0:def 1;
then J: Im z1 = 0 by COMPLEX1:def 2;
thus Im(eval(even_part(LMp),x))
= Re z1 * Im z2 + Re z2 * Im z1 by H,COMPLEX1:9
.= 0 by I,J;
end;
end;
hence thesis;
end;
thus Im(eval(even_part(p),x))
= Im(eval(even_part(LMp),x) + eval(even_part(p-LMp),x))
by B,POLYNOM4:19
.= 0 + Im(eval(even_part(p-LMp),x)) by F,COMPLEX1:8
.= 0 by D,C,D1,AS3,AS2,AS1;
end;
end;
end;
hence for x being Element of F_Complex st Re(x) = 0
holds Im(eval(even_part(p),x)) = 0;
end;
hence P[k];
end;
I: for k being Nat holds P[k] from NAT_1:sch 4(B);
consider n being Nat such that H: len p = n;
thus thesis by I,H;
end;
theorem odim:
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
let p be real Polynomial of F_Complex;
let x be Element of F_Complex;
defpred P[Nat] means
for p being Polynomial of F_Complex st p is real & len p = $1 holds
(for x being Element of F_Complex st Re(x) = 0
holds Re(eval(odd_part(p),x)) = 0);
B: now let k be Nat;
assume AS1: for n being Nat st n < k holds P[n];
now let p be Polynomial of F_Complex;
assume AS2: p is real & len p = k;
now per cases by NAT_1:14;
case k = 0;
then p = 0_.(F_Complex) by AS2,POLYNOM4:5;
then A: odd_part(p) = 0_.(F_Complex) by evod0;
thus for x being Element of F_Complex st Re(x) = 0
holds Re(eval(odd_part(p),x)) = 0
proof
let x be Element of F_Complex;
assume Re(x) = 0;
eval(odd_part(p),x) = 0.F_Complex by A,POLYNOM4:17
.= 0 by COMPLFLD:def 1;
hence thesis by COMPLEX1:4;
end;
end;
case X: k >= 1;
set LMp = Leading-Monomial(p);
LMp + (p-LMp) = (LMp + - LMp) + p by POLYNOM3:26
.= (LMp - LMp) + p
.= 0_.(F_Complex) + p by POLYNOM3:29
.= p by POLYNOM3:28;
then B: odd_part(p) = odd_part(LMp) + odd_part(p-LMp) by evod9;
thus for x being Element of F_Complex st Re(x) = 0
holds Re(eval(odd_part(p),x)) = 0
proof
let x be Element of F_Complex;
assume AS3: Re(x) = 0;
consider t being Polynomial of F_Complex such that
C: len t < len p & p = t + Leading-Monomial(p) &
for n being Element of NAT st n < len p-1 holds t.n = p.n
by X,AS2,POLYNOM4:16;
D1: p - LMp = t + (LMp - LMp) by C,POLYNOM3:26
.= t + 0_.(F_Complex) by POLYNOM3:29
.= t by POLYNOM3:28;
now let n be Nat;
A: n in NAT by ORDINAL1:def 12;
now per cases;
case n < len p-1;
then t.n = p.n by C,A;
hence t.n is real number by AS2;
end;
case D: n >= len p-1;
reconsider lp = len p - 1 as Element of NAT by X,AS2,INT_1:5;
len t < lp + 1 by C;
then lp >= len t by NAT_1:13;
then t.n = 0.F_Complex by D,XXREAL_0:2,ALGSEQ_1:8;
hence t.n is real number by COMPLFLD:def 1;
end;
end;
hence t.n is real number;
end;
then D2: t is real;
F: Re(eval(odd_part(LMp),x)) = 0
proof
now per cases;
case deg p is even;
then odd_part(LMp) = 0_.(F_Complex) by oddLMp1;
then eval(odd_part(LMp),x) = 0.F_Complex by POLYNOM4:17
.= 0 by COMPLFLD:def 1;
hence thesis by COMPLEX1:4;
end;
case G: deg p is odd;
then H: eval(odd_part(LMp),x)
= eval(LMp,x) by oddLMp2
.= p.(len p-'1) * (power F_Complex).(x,len p-'1)
by POLYNOM4:22;
set z1 = p.(len p-'1), z2 = (power F_Complex).(x,len p-'1);
len p -' 1 = deg p by AS2,X,XREAL_1:233;
then I: Re z2 = 0 by AS3,G,pow4;
z1 in REAL by AS2,XREAL_0:def 1;
then J: Im z1 = 0 by COMPLEX1:def 2;
thus Re(eval(odd_part(LMp),x))
= Re z1 * Re z2 - Im z1 * Im z2 by H,COMPLEX1:9
.= 0 by J,I;
end;
end;
hence thesis;
end;
thus Re(eval(odd_part(p),x))
= Re(eval(odd_part(LMp),x) + eval(odd_part(p-LMp),x))
by B,POLYNOM4:19
.= 0 + Re(eval(odd_part(p-LMp),x)) by F,COMPLEX1:8
.= 0 by D2,C,D1,AS3,AS2,AS1;
end;
end;
end;
hence for x being Element of F_Complex st Re(x) = 0
holds Re(eval(odd_part(p),x)) = 0;
end;
hence P[k];
end;
I: for k being Nat holds P[k] from NAT_1:sch 4(B);
consider n being Nat such that H: len p = n;
thus thesis by I,H;
end;
theorem main1:
for p be non constant with_positive_coefficients real 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
let p be non constant
with_positive_coefficients real Polynomial of F_Complex;
assume AS: [even_part(p),odd_part(p)] is positive &
even_part(p),odd_part(p) have_no_common_roots;
set p1 = even_part(p), p2 = odd_part(p);
set z = [p1,p2];
per cases;
suppose p1 - p2 = 0_.(F_Complex);
then p1 + (p2 + -p2) = 0_.(F_Complex) + p2 by POLYNOM3:26;
then p1 + (p2 - p2) = 0_.(F_Complex) + p2;
then p1 + 0_.(F_Complex) = 0_.(F_Complex) + p2 by POLYNOM3:29;
then H1: p1 = 0_.(F_Complex) + p2 by POLYNOM3:28;
H: for x being Element of F_Complex holds eval(p2,x) <> 0.F_Complex
proof
let x be Element of F_Complex;
assume eval(p2,x) = 0.F_Complex;
then x is_a_root_of p2 by POLYNOM5:def 6;
then x is_a_common_root_of p1,p2 by H1,POLYNOM3:28;
hence thesis by AS;
end;
A: for x being Element of F_Complex holds eval(z,x) = 1.F_Complex
proof
let x be Element of F_Complex;
C: eval(p2,x) <> 0.F_Complex by H;
thus eval(z,x) = eval(p2,x) * eval(p2,x)" by H1,POLYNOM3:28
.= 1.F_Complex by C,VECTSP_1:def 10;
end;
D: Re(1.F_Complex) = 1 by COMPLFLD:def 1,COMPLEX1:6;
now let x be Element of F_Complex;
assume x is_a_root_of p1 + p2;
then 0.F_Complex = eval(p1 + p2,x) by POLYNOM5:def 6
.= eval(p1,x) + eval(p2,x) by POLYNOM4:19
.= eval(p2,x) + eval(p2,x) by H1,POLYNOM3:28;
then 2 * eval(p2,x) = 0 by COMPLFLD:def 1;
then 0.F_Complex = eval(p2,x) by COMPLFLD:def 1;
hence Re(x) < 0 by H;
end;
hence ((for x being Element of F_Complex st Re(x) = 0 & eval(p2,x) <> 0
holds Re(eval(z,x)) >= 0) &
p1 + p2 is Hurwitz) by A,D;
end;
suppose p1 - p2 <> 0_.(F_Complex); then reconsider
pp = p1 - p2 as non zero Polynomial of F_Complex by RATFUNC1:def 1;
set w = [ p1 + p2, pp];
Z1: now let x be Element of F_Complex;
assume U0: eval(z`2,x) = 0.F_Complex;
U1: eval(pp,x) = eval(p1,x) - eval(p2,x) by POLYNOM4:21
.= eval(p1,x) by RLVECT_1:13,U0;
U2: eval(p1+p2,x) = eval(p1,x) + eval(p2,x) by POLYNOM4:19
.= eval(p1,x) by RLVECT_1:def 4,U0;
now assume eval(p1,x) = 0.F_Complex;
then x is_a_common_root_of p1,p2 by U0,POLYNOM5:def 6;
hence contradiction by AS;
end;
hence eval(w,x) = 1.F_Complex by VECTSP_1:def 10,U2,U1;
end;
Z2: now let x be Element of F_Complex;
assume F: eval(w,x) = 1.F_Complex &
eval(p2,x) <> 0.F_Complex & eval(p2,x) <> eval(p1,x);
S: now assume eval(pp,x) = 0.F_Complex;
then eval(p1,x) - eval(p2,x) = 0.F_Complex by POLYNOM4:21;
then eval(p2,x) = (eval(p1,x) - eval(p2,x)) + eval(p2,x)
by RLVECT_1:def 4
.= eval(p1,x) + (-eval(p2,x) + eval(p2,x))
.= eval(p1,x) + 0.F_Complex by RLVECT_1:5
.= eval(p1,x) by RLVECT_1:def 4;
hence contradiction by F;
end;
reconsider a = eval(p2,x) as complex number;
1.F_Complex * eval(pp,x)
= eval(p1+p2,x) * ((eval(pp,x))" * eval(pp,x)) by F
.= eval(p1+p2,x) * 1.F_Complex by S,VECTSP_1:def 10
.= eval(p1+p2,x) by VECTSP_1:def 4;
then eval(p1+p2,x) = eval(pp,x) by VECTSP_1:def 8
.= eval(p1,x) - eval(p2,x) by POLYNOM4:21;
then eval(p1,x) + eval(p2,x) = eval(p1,x) - eval(p2,x) by POLYNOM4:19;
then a = -a by COMPLFLD:2;
hence eval(z`2,x) = 0.F_Complex by COMPLFLD:def 1;
end;
Z: now let x be Element of F_Complex;
assume F: eval(p2,x) <> 0.F_Complex & eval(p2,x) <> eval(p1,x);
eval(w,x) - 1.F_Complex <> 1.F_Complex - 1.F_Complex by F,Z2;
then V1: eval(w,x) - 1.F_Complex <> 0.F_Complex by RLVECT_1:15;
ZYY: 1 = 1.F_Complex by COMPLFLD:def 1,COMPLEX1:def 4;
then ZY: eval(w,x) - 1 = eval(w,x) - 1.F_Complex by COMPLFLD:3;
ZA: eval(p1-p2,x) = eval(p1,x) - eval(p2,x) by POLYNOM4:21;
ZU: now assume eval(p1-p2,x) = 0.F_Complex;
then eval(p1,x) - eval(p2,x) = 0.F_Complex by POLYNOM4:21;
hence contradiction by F,RLVECT_1:21;
end;
ZV: eval(p1-p2,x) + eval(p1+p2,x)
= (eval(p1,x) - eval(p2,x)) + (eval(p1,x) + eval(p2,x))
by ZA,POLYNOM4:19
.= (eval(p2,x) - eval(p2,x)) + (eval(p1,x) + eval(p1,x))
.= 0.F_Complex + (eval(p1,x) + eval(p1,x)) by RLVECT_1:def 10
.= eval(p1,x) + eval(p1,x) by RLVECT_1:def 4;
ZB: eval(p1+p2,x) * (eval(p1-p2,x))" - eval(p1-p2,x) * (eval(p1-p2,x))"
= eval(p1+p2,x) * (eval(p1-p2,x))" + (-eval(p1-p2,x))*(eval(p1-p2,x))"
by VECTSP_1:8
.= (eval(p1+p2,x) + -eval(p1-p2,x)) * (eval(p1-p2,x))"
.= (eval(p1,x) + eval(p2,x) - eval(p1-p2,x)) * (eval(p1-p2,x))"
by POLYNOM4:19
.= (eval(p1,x) + eval(p2,x) - (eval(p1,x) - eval(p2,x))) *
(eval(p1-p2,x))" by POLYNOM4:21
.= (eval(p1,x) + eval(p2,x) + (eval(p2,x) + (-eval(p1,x)))) *
(eval(p1-p2,x))" by RLVECT_1:33
.= ((eval(p1,x) + (-eval(p1,x))) + eval(p2,x) + eval(p2,x)) *
(eval(p1-p2,x))"
.= (0.F_Complex + eval(p2,x) + eval(p2,x)) *
(eval(p1-p2,x))" by RLVECT_1:def 10
.= (eval(p2,x) + eval(p2,x)) * (eval(p1-p2,x))" by ALGSTR_1:def 2
.= (eval(p2+p2,x)) * (eval(p1-p2,x))" by POLYNOM4:19;
YY: eval(z,x) * (eval(w,x) - 1)
= (eval(p1,x) * (eval(p2,x))") * (eval(w,x) - 1.F_Complex)
by COMPLEX1:def 4,COMPLFLD:8,COMPLFLD:3
.= (eval(p1,x) * (eval(p2,x))") *
(eval(w,x) - eval(p1-p2,x) * (eval(p1-p2,x))")
by ZU,VECTSP_1:def 10
.= (eval(p1,x) * (eval(p2,x))") *
((eval(p2,x) + eval(p2,x)) * (eval(p1-p2,x))")
by ZB,POLYNOM4:19
.= eval(p1,x) * 2 *((eval(p2,x))" * eval(p2,x)) * (eval(p1-p2,x))"
.= eval(p1,x) * 2 * 1.F_Complex * (eval(p1-p2,x))"
by F,VECTSP_1:def 10
.= (2 * eval(p1,x)) * (eval(p1-p2,x))" by ZYY;
1 + eval(w,x)
= eval(p1-p2,x) * (eval(p1-p2,x))" +
eval(p1+p2,x) * (eval(p1-p2,x))" by ZYY,ZU,VECTSP_1:def 10
.= (eval(p1,x) + eval(p1,x)) * (eval(p1-p2,x))" by ZV;
then (1 + eval(w,x)) * (eval(w,x) - 1)"
= (eval(z,x) * (eval(w,x) - 1)) * (eval(w,x) - 1)" by YY
.= eval(z,x) * ((eval(w,x) - 1) * (eval(w,x) - 1)")
.= eval(z,x) *
((eval(w,x) - 1.F_Complex) * (eval(w,x) - 1.F_Complex)")
by ZY,V1,COMPLFLD:5
.= eval(z,x) * 1.F_Complex by V1,VECTSP_1:def 10
.= eval(z,x) by VECTSP_1:def 4;
hence (1 + eval(w,x)) / (eval(w,x) - 1) = eval(z,x);
end;
FF: now let x be real number;
assume 0 <= x & x * x = 1;
then 0 < x & x = x" by XCMPLX_1:210;
hence x = 1 by XCMPLX_1:223;
end;
Y: for x be Element of F_Complex,
E2, E1 being real number st
E2 = |.eval(w,x).|^2 & E1 = |.eval(w,x) - 1 .|^2 &
eval(p2,x) <> 0.F_Complex & eval(p2,x) <> eval(p1,x) holds
Re(eval(z,x)) = (E2 - 1) / E1
proof let x be Element of F_Complex,
E2, E1 be real number;
assume Y0: E2 = |.eval(w,x).|^2 & E1 = |.eval(w,x) - 1 .|^2;
assume Y1: eval(p2,x) <> 0.F_Complex & eval(p2,x) <> eval(p1,x);
set z1 = 1 + eval(w,x), z2 = eval(w,x) - 1;
E1: Re(z1) = Re(eval(w,x)) + 1 by COMPLEX1:8,COMPLEX1:6,COMPLEX1:def 4;
E2: Re(z2) = Re(eval(w,x)) - 1 by COMPLEX1:def 4,COMPLEX1:6,COMPLEX1:19;
E3: Im(z1) = 0 + Im(eval(w,x)) by COMPLEX1:8,COMPLEX1:6,COMPLEX1:def 4;
E4: Im(z2) = Im(eval(w,x)) - Im(1r) by COMPLEX1:19,COMPLEX1:def 4
.= Im(eval(w,x)) + 0 by COMPLEX1:6;
reconsider R2 = (Re z2)^2, I2 = (Im z2)^2 as real number;
reconsider RR = (Re(eval(w,x)))^2,
II = (Im(eval(w,x)))^2 as real number;
Re((1 + eval(w,x)) / (eval(w,x) - 1))
= (Re z1 * Re z2 + Im z1 * Im z2) / (R2 + I2) by COMPLEX1:24
.= ((RR + II) - 1) / (R2 + I2) by E1,E2,E3,E4
.= (|.eval(w,x)*eval(w,x).| - 1) / (R2 + I2) by COMPLEX1:68
.= (|.eval(w,x).|*|.eval(w,x).| - 1) / (R2 + I2) by COMPLEX1:65
.= (E2 - 1) / (|.z2*z2.|) by COMPLEX1:68,Y0
.= (E2 - 1) / E1 by COMPLEX1:65,Y0;
hence Re(eval(z,x)) = (E2 - 1) / E1 by Y1,Z;
end;
X: for x being Element of F_Complex
holds (eval(p2,x) <> eval(p1,x) & Re(eval(z,x)) >= 0)
implies |.eval(w,x).| >= 1
proof
let x be Element of F_Complex;
reconsider E2 = |.eval(w,x) - 1 .|^2 as real number;
reconsider E1 = |.eval(w,x).|^2 as real number;
assume AS: eval(p2,x) <> eval(p1,x) & Re(eval(z,x)) >= 0;
X3: E2 >= 0 by XREAL_1:63;
now per cases by AS;
case eval(p2,x) = 0.F_Complex;
then eval(w,x) = 1.F_Complex by Z1
.= 1 by COMPLFLD:def 1,COMPLEX1:def 4;
hence |.eval(w,x).| >= 1 by COMPLEX1:48;
end;
case Re(eval(z,x)) > 0 & eval(p2,x) <> 0.F_Complex;
then R3: (E1 - 1) / E2 > 0 by AS,Y;
then E1 - 1 > 0 by X3;
then R3a: (E1 - 1) + 1 > 0 + 1 by XREAL_1:8;
now per cases;
case eval(w,x) = 0;
hence |.eval(w,x).| >= 1 by X3,R3,COMPLEX1:44;
end;
case eval(w,x) <> 0;
then R1: |.eval(w,x).| > 0 by COMPLEX1:47;
now assume R2: |.eval(w,x).| < 1;
then E1 <= |.eval(w,x).| by R1,SQUARE_1:42;
hence contradiction by R3a,R2,XXREAL_0:2;
end;
hence |.eval(w,x).| >= 1;
end;
end;
hence |.eval(w,x).| >= 1;
end;
case Re(eval(z,x)) = 0 & eval(p2,x) <> 0.F_Complex;
then X2: (E1 - 1) / E2 = 0 by AS,Y;
now per cases;
case |.(eval(w,x) - 1).|^2 = 0;
then |.(eval(w,x) - 1).| = 0;
then eval(w,x) - 1 = 0 by COMPLEX1:45;
hence |.eval(w,x).| = 1 by COMPLEX1:48;
end;
case |.(eval(w,x) - 1).|^2 <> 0;
then E1 - 1 = 0 by X2;
hence |.eval(w,x).| = 1 by FF,COMPLEX1:46;
end;
end;
hence |.eval(w,x).| >= 1;
end;
end;
hence |.eval(w,x).| >= 1;
end;
thus for x being Element of F_Complex st Re(x) = 0 & eval(p2,x) <> 0
holds Re(eval(z,x)) >= 0
proof
let x be Element of F_Complex;
assume T: Re(x) = 0 & eval(p2,x) <> 0;
then T1: Im(eval(p1,x)) = 0 by evim;
T2: Re(eval(p2,x)) = 0 by T,odim;
T4: eval(p2,x) <> 0.F_Complex by T,COMPLFLD:def 1;
reconsider y1 = eval(p1,x) as complex number;
reconsider y2 = eval(p2,x) as complex number;
Re(eval(p1,x)/eval(p2,x)) = Re(y1/y2) by T4,COMPLFLD:6
.= 0 by T1,T2,reim;
hence thesis;
end;
now let x be Element of F_Complex;
assume HU2: Re(x) >= 0;
reconsider RW = |.eval(w,x).|^2 as real number;
now per cases;
case F: eval(p2,x) = eval(p1,x);
F3: now assume eval(p1,x) = 0.F_Complex; then
x is_a_common_root_of p1,p2 by F,POLYNOM5:def 6;
hence contradiction by AS;
end;
now assume eval(p1+p2,x) = 0.F_Complex;
then F4: eval(p1,x) + eval(p1,x) = 0.F_Complex by F,POLYNOM4:19
.= 0 by COMPLFLD:def 1;
reconsider a = eval(p1,x) as complex number;
thus contradiction by F4,F3,COMPLFLD:def 1;
end;
hence not(x is_a_root_of p1 + p2) by POLYNOM5:def 6;
end;
case F: eval(p2,x) <> eval(p1,x);
now per cases by HU2;
case T: Re(x) = 0;
then T1: Im(eval(p1,x)) = 0 by evim;
T2: Re(eval(p2,x)) = 0 by T,odim;
now per cases;
case U0: eval(p2,x) = 0;
then U0a: eval(p2,x) = 0.F_Complex by COMPLFLD:def 1;
U1: eval(pp,x) = eval(p1,x) - eval(p2,x) by POLYNOM4:21
.= eval(p1,x) - 0.F_Complex by U0,COMPLFLD:def 1
.= eval(p1,x) by RLVECT_1:13;
U2: eval(p1+p2,x) = eval(p1,x) + eval(p2,x) by POLYNOM4:19
.= eval(p1,x) by U0;
now assume eval(p1,x) = 0.F_Complex;
then x is_a_common_root_of p1,p2 by U0a,POLYNOM5:def 6;
hence contradiction by AS;
end; then
eval(w,x) = 1.F_Complex by VECTSP_1:def 10,U1,U2
.= 1r by COMPLFLD:def 1;
hence |.eval(w,x).| = 1 by COMPLEX1:48;
end;
case Ta: eval(p2,x) <> 0;
then T4: eval(p2,x) <> 0.F_Complex by COMPLFLD:def 1;
T5: eval(p2,x) <> 0.F_Complex by Ta,COMPLFLD:def 1;
reconsider y1 = eval(p1,x) as complex number;
reconsider y2 = eval(p2,x) as complex number;
reconsider E1 = |.eval(w,x) - 1 .|^2 as real number;
Re(eval(p1,x)/eval(p2,x)) = Re(y1/y2) by T4,COMPLFLD:6
.= 0 by T1,T2,reim;
then Re(eval(z,x)) = 0;
then X2: (RW - 1) / E1 = 0 by F,T5,Y;
now per cases;
case |.(eval(w,x) - 1).|^2 = 0;
then |.(eval(w,x) - 1).| = 0;
then eval(w,x) - 1 = 0 by COMPLEX1:45;
hence |.eval(w,x).| = 1 by COMPLEX1:48;
end;
case |.(eval(w,x) - 1).|^2 <> 0;
then RW - 1 = 0 by X2;
hence |.eval(w,x).| = 1 by FF,COMPLEX1:46;
end;
end;
hence |.eval(w,x).| = 1;
end;
end;
then eval(w`1,x) <> 0 by COMPLEX1:47;
then eval(p1+p2,x) <> 0.F_Complex by COMPLFLD:def 1;
hence not(x is_a_root_of p1 + p2) by POLYNOM5:def 6;
end;
case Re(x) > 0 & eval(z`2,x) <> 0;
then Re(eval(z,x)) > 0 by AS;
then |.eval(w,x).| >= 1 by X,F;
then eval(w`1,x) <> 0 by COMPLEX1:47;
then eval(p1+p2,x) <> 0.F_Complex by COMPLFLD:def 1;
hence not(x is_a_root_of p1 + p2) by POLYNOM5:def 6;
end;
case Re(x) > 0 & eval(z`2,x) = 0;
then U0: eval(p2,x) = 0.F_Complex by COMPLFLD:def 1;
U1: eval(pp,x) = eval(p1,x) - eval(p2,x) by POLYNOM4:21
.= eval(p1,x) by U0,RLVECT_1:13;
U2: eval(p1+p2,x) = eval(p1,x) + eval(p2,x) by POLYNOM4:19
.= eval(p1,x) by U0,RLVECT_1:def 4;
now assume eval(p1,x) = 0.F_Complex;
then x is_a_common_root_of p1,p2 by U0,POLYNOM5:def 6;
hence contradiction by AS;
end; then
eval(w,x) = 1.F_Complex by VECTSP_1:def 10,U1,U2
.= 1r by COMPLFLD:def 1;
then eval(w`1,x) <> 0 by COMPLEX1:47,COMPLEX1:48;
then eval(p1+p2,x) <> 0.F_Complex by COMPLFLD:def 1;
hence not(x is_a_root_of p1 + p2) by POLYNOM5:def 6;
end;
end;
hence not(x is_a_root_of p1 + p2);
end;
end;
hence not(x is_a_root_of p1 + p2);
end;
hence p1 + p2 is Hurwitz;
end;
end;
theorem
for p be non constant with_positive_coefficients real 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
let p be non constant with_positive_coefficients
real Polynomial of F_Complex;
set e = even_part p, o = odd_part p;
set f = [e,o];
assume AS: [e,o] is one_port_function & degree([e,o]) = degree p;
H0: f is non zero;
degree f = max ( degree f`1, degree f`2 ) by AS,evoddeg;
then f is irreducible by H0,RATFUNC1:30;
then e + o is Hurwitz by AS,main1;
hence p is Hurwitz by evod2;
end;
*