:: Exponential Function on Complex {B}anach Algebra
:: by Noboru Endou
::
:: Received April 6, 2004
:: Copyright (c) 2004-2026 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, CLOPBAN2, SUBSET_1, NAT_1, SEQ_1, RELAT_1, COMSEQ_3,
ARYTM_3, CARD_1, PREPOWER, FUNCT_1, MESFUNC1, LOPBAN_4, SEQ_2, ORDINAL2,
ARYTM_1, SUPINF_2, REAL_1, XXREAL_0, NORMSP_1, PRE_TOPC, XXREAL_2,
SERIES_1, COMPLEX1, SIN_COS, XBOOLE_0, STRUCT_0, NEWTON, REALSET1,
VALUED_1, XCMPLX_0, LOPBAN_3, CARD_3, VALUED_0, RSSPACE3, ALGSTR_0;
notations RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, PRE_TOPC, XCMPLX_0, XXREAL_0,
XREAL_0, ORDINAL1, NUMBERS, CLOPBAN3, COMPLEX1, REAL_1, NAT_1, STRUCT_0,
ALGSTR_0, NEWTON, RLVECT_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, LOPBAN_4,
NAT_D, SIN_COS, BHSP_4, NORMSP_0, CLVECT_1, CSSPACE3, CLOPBAN2, LOPBAN_3,
NORMSP_1;
constructors REAL_1, SQUARE_1, SEQ_2, COMSEQ_3, NAT_D, SIN_COS, BHSP_4,
LOPBAN_4, CSSPACE3, CLOPBAN3, RELSET_1, COMSEQ_2, NUMBERS, LOPBAN_3;
registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, CLOPBAN2, CLOPBAN3, VALUED_0, SEQ_2, NEWTON, NAT_1,
FUNCT_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions CLVECT_1;
expansions CLVECT_1;
theorems ABSVALUE, RLVECT_1, XCMPLX_0, XCMPLX_1, XREAL_0, SEQ_2, SEQM_3,
COMSEQ_3, SIN_COS, SERIES_1, NAT_1, INT_1, NEWTON, FUNCT_2, SEQ_4,
LOPBAN_3, CLOPBAN3, CLVECT_1, COMPLEX1, CSSPACE3, XREAL_1, XXREAL_0,
LOPBAN_4, BHSP_4, NORMSP_1, VALUED_0, ORDINAL1, NORMSP_0, GROUP_1,
VECTSP_1;
schemes SEQ_1, NAT_1, FUNCT_2, CLASSES1;
begin :: Basic Properties of Exponential Function on Complex Banach Algebra
reserve X for Complex_Banach_Algebra,
w,z,z1,z2 for Element of X,
k,l,m,n,n1, n2 for Nat,
seq,seq1,seq2,s,s9 for sequence of X,
rseq for Real_Sequence;
Lm1: z* (z #N n) =z #N (n+1) & (z #N n) *z= z #N (n+1) & z* (z #N n) =(z #N n)
*z
proof
defpred P[Nat] means z* (z #N $1)=z #N ($1 +1);
A1: z #N (0+1) =z GeoSeq.(0+1) by CLOPBAN3:def 8
.=z GeoSeq.0 * z by CLOPBAN3:def 7
.=1.X * z by CLOPBAN3:def 7
.=z by VECTSP_1:def 8;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
thus z* (z #N (k+1)) =z * (z GeoSeq.(k+1)) by CLOPBAN3:def 8
.= z* (z GeoSeq.(k)*z) by CLOPBAN3:def 7
.=z* (z #N k *z ) by CLOPBAN3:def 8
.=(z * z #N k) *z by GROUP_1:def 3
.=z GeoSeq.(k+1) * z by A3,CLOPBAN3:def 8
.=z GeoSeq.((k+1)+1) by CLOPBAN3:def 7
.=z #N ((k+1)+1) by CLOPBAN3:def 8;
end;
z*(z #N0 ) =z * (z GeoSeq.0) by CLOPBAN3:def 8
.=z * 1.X by CLOPBAN3:def 7
.=z by VECTSP_1:def 4;
then
A4: P[0] by A1;
A5: for n be Nat holds P[n] from NAT_1:sch 2(A4,A2);
now
let n;
thus z * z #N n =z #N (n+1) by A5;
thus (z #N n) *z =z GeoSeq.n * z by CLOPBAN3:def 8
.=z GeoSeq.(n+1) by CLOPBAN3:def 7
.=z #N (n+1) by CLOPBAN3:def 8;
hence z * (z #Nn) =(z #N n) * z by A5;
end;
hence thesis;
end;
Lm2: for z,w st z,w are_commutative holds w* (z #N n) = (z #N n)*w & z* (w #N
n) = (w #N n)*z
proof
let z,w such that
A1: z,w are_commutative;
defpred P[Nat] means
w* (z #N $1) =(z #N $1)*w & z* (w #N $1) = (
w #N $1)*z;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
A4: z*(w #N (k+1) )=z*( (w #N k) *w) by Lm1
.=(z*(w #N k)) *w by GROUP_1:def 3
.=(w #N k)*(z *w) by A3,GROUP_1:def 3
.=(w #N k)*(w *z) by A1,LOPBAN_4:def 1
.=(w #N k)*w *z by GROUP_1:def 3
.=(w #N (k+1) ) *z by Lm1;
w*(z #N (k+1) )=w*( (z #N k) *z) by Lm1
.=(w*(z #N k)) *z by GROUP_1:def 3
.=(z #N k)*(w *z) by A3,GROUP_1:def 3
.=(z #N k)*(z *w) by A1,LOPBAN_4:def 1
.=((z #N k))*z *w by GROUP_1:def 3
.=(z #N (k+1) ) *w by Lm1;
hence thesis by A4;
end;
A5: (w #N0 ) = (w GeoSeq.0) by CLOPBAN3:def 8
.= 1.X by CLOPBAN3:def 7;
then
A6: z*(w #N0 )=z by VECTSP_1:def 4
.=(w #N0 ) *z by A5,VECTSP_1:def 8;
A7: (z #N0 ) = (z GeoSeq.0) by CLOPBAN3:def 8
.= 1.X by CLOPBAN3:def 7;
then w*(z #N0 )=w by VECTSP_1:def 4
.=(z #N0 ) *w by A7,VECTSP_1:def 8;
then
A8: P[0] by A6;
for n be Nat holds P[n] from NAT_1:sch 2(A8,A2);
hence thesis;
end;
theorem Th1:
seq1 is convergent & seq2 is convergent & lim(seq1-seq2)=0.X
implies lim seq1 = lim seq2
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent and
A3: lim(seq1-seq2)=0.X;
lim(seq1)-lim(seq2) =0.X by A1,A2,A3,CLVECT_1:120;
then lim(seq1)-lim(seq2) + lim(seq2) = lim(seq2) by RLVECT_1:def 4;
then lim(seq1)-(lim(seq2) - lim(seq2)) = lim(seq2) by CLOPBAN3:38;
then lim(seq1)-0.X = lim(seq2) by RLVECT_1:15;
hence thesis by RLVECT_1:13;
end;
theorem Th2:
for z st for n being Nat holds s.n = z holds lim s = z
proof
let z;
assume
A1: for n being Nat holds s.n = z;
A2: now
let p be Real such that
A3: 0<p;
reconsider k = 0 as Nat;
take k;
let n such that
k<=n;
s.n = z by A1;
hence ||.s.n - z.|| < p by A3,CLVECT_1:107;
end;
then s is convergent;
hence thesis by A2,CLVECT_1:def 16;
end;
theorem Th3:
s is convergent & s9 is convergent implies s * s9 is convergent
proof
assume that
A1: s is convergent and
A2: s9 is convergent;
consider g1 be Point of X such that
A3: for p being Real st 0<p ex n st for m st n<=m holds ||.s.m-g1.||<p
by A1;
||.s.|| is bounded by A1,CLVECT_1:117,SEQ_2:13;
then consider R be Real such that
A4: for n holds ||.s.||.n < R by SEQ_2:def 3;
A5: now
let n;
||.s.n.||= ||.s.||.n by NORMSP_0:def 4;
hence ||.s.n.|| < R by A4;
end;
||. s.1 .|| = ||. s .||.1 by NORMSP_0:def 4;
then 0<= ||.s.||.1 by CLVECT_1:105;
then
A6: 0 < R by A4;
consider g2 be Point of X such that
A7: for p being Real st 0<p ex n st for m st n<=m holds ||.s9.m-g2.||<p
by A2;
take g=g1*g2;
let p be Real;
reconsider R as Real;
A8: 0+0<||.g2.||+R by A6,CLVECT_1:105,XREAL_1:8;
assume
A9: 0<p;
then consider n1 such that
A10: for m st n1<=m holds ||.s.m-g1.||<p/(||.g2.||+R) by A3,A8;
consider n2 such that
A11: for m st n2<=m holds ||.s9.m-g2.||<p/(||.g2.||+R) by A7,A8,A9;
take n=n1+n2;
let m such that
A12: n<=m;
n2<=n by NAT_1:12;
then n2<=m by A12,XXREAL_0:2;
then
A13: ||.s9.m-g2.||<p/(||.g2.||+R) by A11;
A14: 0<=||.s.m.|| by CLVECT_1:105;
A15: ||.s.m*(s9.m-g2).|| <= ||.s.m.||*||.s9.m-g2.|| by CLOPBAN3:38;
A16: 0<=||.s9.m-g2.|| by CLVECT_1:105;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A12,XXREAL_0:2;
then
A17: ||.s.m-g1.||<=p/(||.g2.||+R) by A10;
||.((s*s9).m)-g.|| =||.s.m*s9.m-g1*g2.|| by LOPBAN_3:def 7
.=||.(s.m*s9.m-s.m*g2)+(s.m*g2-g1*g2).|| by CLOPBAN3:38
.=||.s.m*(s9.m-g2)+(s.m*g2-g1*g2).|| by CLOPBAN3:38
.=||.s.m*(s9.m-g2)+(s.m-g1)*g2.|| by CLOPBAN3:38;
then
A18: ||.((s*s9).m)-g.||<= ||.s.m*(s9.m-g2).||+||.(s.m-g1)*g2.|| by
CLVECT_1:def 13;
||.s.m.||<R by A5;
then ||.s.m.||*||.s9.m-g2.||<R*(p/(||.g2.||+R)) by A14,A16,A13,XREAL_1:96;
then
A19: ||.s.m*(s9.m-g2).||<R*(p/(||.g2.||+R)) by A15,XXREAL_0:2;
A20: ||.(s.m-g1)*g2.||<=||.g2.||*||.s.m-g1.|| by CLOPBAN3:38;
0<=||.g2.|| by CLVECT_1:105;
then ||.g2.||*||.s.m-g1.|| <=||.g2.||*(p/(||.g2.||+R)) by A17,XREAL_1:64;
then
A21: ||.(s.m-g1)*g2.||<=||.g2.||*(p/(||.g2.||+R)) by A20,XXREAL_0:2;
R*(p/(||.g2.||+R))+||.g2.||*(p/(||.g2.||+R)) =(p/(||.g2.||+R))*(||.g2 .||+R)
.=p by A8,XCMPLX_1:87;
then ||.s.m*(s9.m-g2).||+||.(s.m-g1)*g2.||<p by A19,A21,XREAL_1:8;
hence thesis by A18,XXREAL_0:2;
end;
theorem Th4:
s is convergent implies z * s is convergent
proof
A1: 0<=||.z.|| by CLVECT_1:105;
assume s is convergent;
then consider g1 be Point of X such that
A2: for p being Real st 0<p ex n st for m st n<=m holds ||.s.m-g1.||<p;
take g=z*g1;
let p be Real;
assume
A3: 0<p;
A4: 0+0< ||.z.||+1 by CLVECT_1:105,XREAL_1:8;
then consider n such that
A5: for m st n<=m holds ||.s.m-g1.||<p/(||.z.||+1) by A2,A3;
take n;
let m;
assume n<=m;
then
A6: ||.s.m-g1.||< p/(||.z.||+1) by A5;
A7: ||.z*(s.m-g1).|| <= ||.z.||*||.s.m-g1.|| by CLOPBAN3:38;
0<=||.s.m-g1.|| by CLVECT_1:105;
then ||.z.||*||.s.m-g1.||<= ||.z.||*(p/(||.z.||+1)) by A1,A6,XREAL_1:66;
then
A8: ||.z*(s.m-g1).||<=||.z.||*(p/(||.z.||+1)) by A7,XXREAL_0:2;
A9: ||.((z*s).m)-g.|| =||.z*s.m-z*g1.|| by LOPBAN_3:def 5
.=||.z*(s.m-g1).|| by CLOPBAN3:38;
0+ ||.z.|| < ||.z.||+1 by XREAL_1:8;
then
A10: ||.z.||*(p/(||.z.||+1)) < ( ||.z.||+1) *(p/(||.z.||+1)) by A1,A3,
XREAL_1:97;
( ||.z.||+1) *(p/(||.z.||+1)) =p by A4,XCMPLX_1:87;
hence thesis by A9,A8,A10,XXREAL_0:2;
end;
theorem Th5:
s is convergent implies s*z is convergent
proof
A1: 0<=||.z.|| by CLVECT_1:105;
assume s is convergent;
then consider g1 be Point of X such that
A2: for p being Real st 0<p ex n st for m st n<=m holds ||.s.m-g1.||<p;
take g=g1*z;
let p be Real;
assume
A3: 0<p;
A4: 0+0< ||.z.||+1 by CLVECT_1:105,XREAL_1:8;
then consider n such that
A5: for m st n<=m holds ||.s.m-g1.||<p/(||.z.||+1) by A2,A3;
take n;
let m;
assume n<=m;
then
A6: ||.s.m-g1.||< p/(||.z.||+1) by A5;
A7: ||.(s.m-g1)*z.|| <=||.s.m-g1.||* ||.z.|| by CLOPBAN3:38;
0<=||.s.m-g1.|| by CLVECT_1:105;
then ||.s.m-g1.||* ||.z.||<=(p/(||.z.||+1))* ||.z.|| by A1,A6,XREAL_1:66;
then
A8: ||.(s.m-g1)*z.||<=(p/(||.z.||+1))*||.z.|| by A7,XXREAL_0:2;
A9: ||.((s*z).m)-g.|| =||.s.m*z-g1*z.|| by LOPBAN_3:def 6
.=||.(s.m-g1)*z.|| by CLOPBAN3:38;
0+ ||.z.|| < ||.z.||+1 by XREAL_1:8;
then
A10: (p/(||.z.||+1))*||.z.||< (p/(||.z.||+1)) * ( ||.z.||+1) by A1,A3,
XREAL_1:97;
(p/(||.z.||+1))* ( ||.z.||+1) = p by A4,XCMPLX_1:87;
hence thesis by A9,A8,A10,XXREAL_0:2;
end;
theorem Th6:
s is convergent implies lim (z * s) =z* lim(s)
proof
assume
A1: s is convergent;
set g1=lim(s);
set g=z*g1;
A2: 0+0< ||.z.||+1 by CLVECT_1:105,XREAL_1:8;
A3: 0<=||.z.|| by CLVECT_1:105;
A4: now
let p be Real;
assume
A5: 0<p;
then consider n such that
A6: for m st n<=m holds ||.s.m-g1.||<p/(||.z.||+1) by A1,A2,CLVECT_1:def 16;
take n;
let m;
assume n<=m;
then
A7: ||.s.m-g1.||< p/(||.z.||+1) by A6;
0<=||.s.m-g1.|| by CLVECT_1:105;
then
A8: ||.z.||*||.s.m-g1.||<= ||.z.||*(p/(||.z.||+1)) by A3,A7,XREAL_1:66;
||.z*(s.m-g1).|| <= ||.z.||*||.s.m-g1.|| by CLOPBAN3:38;
then
A9: ||.z*(s.m-g1).||<=||.z.||*(p/(||.z.||+1)) by A8,XXREAL_0:2;
A10: ||.((z*s).m)-g.|| =||.z*s.m-z*g1.|| by LOPBAN_3:def 5
.=||.z*(s.m-g1).|| by CLOPBAN3:38;
0+ ||.z.|| < ||.z.||+1 by XREAL_1:8;
then
A11: ||.z.||*(p/(||.z.||+1)) < ( ||.z.||+1) *(p/(||.z.||+1)) by A3,A5,
XREAL_1:97;
( ||.z.||+1) *(p/(||.z.||+1)) = p by A2,XCMPLX_1:87;
hence ||.((z*s).m)-g.|| < p by A10,A9,A11,XXREAL_0:2;
end;
z*s is convergent by A1,Th4;
hence thesis by A4,CLVECT_1:def 16;
end;
theorem Th7:
s is convergent implies lim (s*z) = lim(s)*z
proof
assume
A1: s is convergent;
set g1=lim(s);
set g=g1*z;
A2: 0+0< ||.z.||+1 by CLVECT_1:105,XREAL_1:8;
A3: 0<=||.z.|| by CLVECT_1:105;
A4: now
let p be Real;
assume
A5: 0<p;
then consider n such that
A6: for m st n<=m holds ||.s.m-g1.||<p/(||.z.||+1) by A1,A2,CLVECT_1:def 16;
take n;
let m;
assume n<=m;
then
A7: ||.s.m-g1.||< p/(||.z.||+1) by A6;
0<=||.s.m-g1.|| by CLVECT_1:105;
then
A8: ||.s.m-g1.||* ||.z.||<=(p/(||.z.||+1))* ||.z.|| by A3,A7,XREAL_1:66;
||.(s.m-g1)*z.|| <=||.s.m-g1.||* ||.z.|| by CLOPBAN3:38;
then
A9: ||.(s.m-g1)*z.||<=(p/(||.z.||+1))*||.z.|| by A8,XXREAL_0:2;
A10: ||.((s*z).m)-g.|| =||.s.m*z-g1*z.|| by LOPBAN_3:def 6
.=||.(s.m-g1)*z.|| by CLOPBAN3:38;
0+ ||.z.|| < ||.z.||+1 by XREAL_1:8;
then
A11: (p/(||.z.||+1))*||.z.||< (p/(||.z.||+1)) * ( ||.z.||+1) by A3,A5,
XREAL_1:97;
(p/(||.z.||+1))* ( ||.z.||+1) =p by A2,XCMPLX_1:87;
hence ||.((s*z).m)-g.|| < p by A10,A9,A11,XXREAL_0:2;
end;
s*z is convergent by A1,Th5;
hence thesis by A4,CLVECT_1:def 16;
end;
theorem Th8:
s is convergent & s9 is convergent implies lim(s*s9)=(lim s)*(lim s9)
proof
assume that
A1: s is convergent and
A2: s9 is convergent;
||.s.|| is bounded by A1,CLVECT_1:117,SEQ_2:13;
then consider R be Real such that
A3: for n holds ||.s.||.n < R by SEQ_2:def 3;
set g2=lim s9;
set g1=lim s;
set g=g1*g2;
A4: now
let n;
||.s.n.||= ||.s.||.n by NORMSP_0:def 4;
hence ||.s.n.|| < R by A3;
end;
||. s.1 .|| = ||. s .||.1 by NORMSP_0:def 4;
then 0<= ||.s.||.1 by CLVECT_1:105;
then
A5: 0 < R by A3;
reconsider R as Real;
A6: 0+0<||.g2.||+R by A5,CLVECT_1:105,XREAL_1:8;
A7: 0<=||.g2.|| by CLVECT_1:105;
A8: now
let p be Real;
assume
A9: 0<p;
then consider n1 such that
A10: for m st n1<=m holds ||.s.m-g1.||<p/(||.g2.||+R) by A1,A6,CLVECT_1:def 16;
consider n2 such that
A11: for m st n2<=m holds ||.s9.m-g2.||<p/(||.g2.||+R) by A2,A6,A9,
CLVECT_1:def 16;
take n=n1+n2;
let m such that
A12: n<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A12,XXREAL_0:2;
then ||.s.m-g1.||<=p/(||.g2.||+R) by A10;
then
A13: ||.g2.||*||.s.m-g1.|| <=||.g2.||*(p/(||.g2.||+R)) by A7,XREAL_1:64;
||.(s.m-g1)*g2.||<=||.g2.||*||.s.m-g1.|| by CLOPBAN3:38;
then
A14: ||.(s.m-g1)*g2.||<=||.g2.||*(p/(||.g2.||+R)) by A13,XXREAL_0:2;
A15: 0<=||.s.m.|| by CLVECT_1:105;
||.((s*s9).m)-g.|| =||.s.m*s9.m-g1*g2.|| by LOPBAN_3:def 7
.=||.(s.m*s9.m-s.m*g2)+(s.m*g2-g1*g2).|| by CLOPBAN3:38
.=||.s.m*(s9.m-g2)+(s.m*g2-g1*g2).|| by CLOPBAN3:38
.=||.s.m*(s9.m-g2)+(s.m-g1)*g2.|| by CLOPBAN3:38;
then
A16: ||.((s*s9).m)-g.||<= ||.s.m*(s9.m-g2).||+||.(s.m-g1)*g2.|| by
CLVECT_1:def 13;
A17: ||.s.m*(s9.m-g2).|| <= ||.s.m.||*||.s9.m-g2.|| by CLOPBAN3:38;
n2<=n by NAT_1:12;
then n2<=m by A12,XXREAL_0:2;
then
A18: ||.s9.m-g2.||<p/(||.g2.||+R) by A11;
A19: 0<=||.s9.m-g2.|| by CLVECT_1:105;
||.s.m.||<R by A4;
then ||.s.m.||*||.s9.m-g2.||<R*(p/(||.g2.||+R)) by A15,A19,A18,XREAL_1:96;
then
A20: ||.s.m*(s9.m-g2).||<R*(p/(||.g2.||+R)) by A17,XXREAL_0:2;
R*(p/(||.g2.||+R))+||.g2.||*(p/(||.g2.||+R)) =(p/(||.g2.||+R))*(||.g2
.||+R)
.=p by A6,XCMPLX_1:87;
then ||.s.m*(s9.m-g2).||+||.(s.m-g1)*g2.||<p by A20,A14,XREAL_1:8;
hence ||.((s*s9).m)-g.||<p by A16,XXREAL_0:2;
end;
s*s9 is convergent by A1,A2,Th3;
hence thesis by A8,CLVECT_1:def 16;
end;
theorem Th9:
Partial_Sums(z * seq) = z * Partial_Sums(seq) & Partial_Sums(seq
*z ) = Partial_Sums(seq) *z
proof
A1: Partial_Sums(seq *z ) = Partial_Sums(seq) *z
proof
defpred P[Nat] means
Partial_Sums(seq*z).$1= (Partial_Sums(seq)
*z).$1;
A2: now
let n;
assume
A3: P[n];
Partial_Sums( seq*z).(n+1) =Partial_Sums( seq*z).n + (seq*z).(n+1)
by BHSP_4:def 1
.=(Partial_Sums(seq).n *z )+ (seq*z).(n+1) by A3,LOPBAN_3:def 6
.=(Partial_Sums(seq).n*z)+ (seq.(n+1)*z) by LOPBAN_3:def 6
.= ( Partial_Sums(seq).n + seq.(n+1))*z
by VECTSP_1:def 3
.= ( Partial_Sums(seq).(n+1))*z by BHSP_4:def 1
.= (Partial_Sums(seq)*z ).(n+1) by LOPBAN_3:def 6;
hence P[n+1];
end;
Partial_Sums(seq*z).0 = (seq*z).0 by BHSP_4:def 1
.= seq.0*z by LOPBAN_3:def 6
.=Partial_Sums(seq).0 *z by BHSP_4:def 1
.=(Partial_Sums(seq)*z).0 by LOPBAN_3:def 6;
then
A4: P[0];
for n holds P[n] from NAT_1:sch 2(A4,A2);
then for n being Element of NAT holds P[n];
hence thesis by FUNCT_2:63;
end;
Partial_Sums(z * seq) = z * Partial_Sums(seq)
proof
defpred P[Nat] means
Partial_Sums(z *seq).$1= (z * Partial_Sums
(seq)).$1;
A5: now
let n;
assume
A6: P[n];
Partial_Sums(z * seq).(n+1) =Partial_Sums(z * seq).n + (z * seq).(n+
1) by BHSP_4:def 1
.=(z * Partial_Sums(seq).n )+ (z * seq).(n+1) by A6,LOPBAN_3:def 5
.=(z * Partial_Sums(seq).n )+ (z * seq.(n+1)) by LOPBAN_3:def 5
.= z * ( Partial_Sums(seq).n + seq.(n+1))
by VECTSP_1:def 2
.= z * ( Partial_Sums(seq).(n+1)) by BHSP_4:def 1
.= (z * Partial_Sums(seq)).(n+1) by LOPBAN_3:def 5;
hence P[n+1];
end;
Partial_Sums(z*seq).0 =(z * seq).0 by BHSP_4:def 1
.=z * seq.0 by LOPBAN_3:def 5
.=z * Partial_Sums(seq).0 by BHSP_4:def 1
.=(z * Partial_Sums(seq)).0 by LOPBAN_3:def 5;
then
A7: P[0];
for n holds P[n] from NAT_1:sch 2(A7,A5);
then for n being Element of NAT holds P[n];
hence thesis by FUNCT_2:63;
end;
hence thesis by A1;
end;
theorem Th10:
||.Partial_Sums(seq).k.|| <= Partial_Sums(||.seq.||).k
proof
defpred P[Nat] means
||. Partial_Sums(seq).$1 .|| <= Partial_Sums
(||.seq.||).$1;
A1: now
let k;
assume P[k];
then
A2: ||. Partial_Sums(seq).k.|| + ||.(seq).(k+1).|| <= Partial_Sums(||.seq
.|| ).k + ||.(seq).(k+1).|| by XREAL_1:6;
A3: ||. Partial_Sums(seq).k + (seq).(k+1) .|| <= ||. Partial_Sums(seq).k
.|| + ||. (seq).(k+1) .|| by CLVECT_1:def 13;
||. Partial_Sums(seq).(k+1) .|| =||. Partial_Sums(seq).k + (seq).(k+1)
.|| by BHSP_4:def 1;
then
||. Partial_Sums(seq).(k+1) .|| <= Partial_Sums(||.seq.||).k + ||.seq.
(k+1).|| by A3,A2,XXREAL_0:2;
then
||. Partial_Sums(seq).(k+1) .|| <= Partial_Sums(||.seq.||).k+||.seq.||
.(k+1) by NORMSP_0:def 4;
hence P[k+1] by SERIES_1:def 1;
end;
Partial_Sums(||.seq.||).0 = (||.seq.||).0 by SERIES_1:def 1
.= ||. seq.0 .|| by NORMSP_0:def 4;
then
A4: P[0] by BHSP_4:def 1;
for k holds P[k] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th11:
(for n st n <= m holds seq1.n = seq2.n) implies Partial_Sums(
seq1).m =Partial_Sums(seq2).m
proof
defpred P[Nat] means
$1 <= m implies Partial_Sums(seq1).$1=
Partial_Sums(seq2).$1;
assume
A1: for n st n <= m holds seq1.n = seq2.n;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
assume
A4: k+1 <= m;
k < k+1 by XREAL_1:29;
hence Partial_Sums(seq1).(k+1) =Partial_Sums(seq2).k+seq1.(k+1) by A3,A4,
BHSP_4:def 1,XXREAL_0:2
.=Partial_Sums(seq2).k+seq2.(k+1) by A1,A4
.=Partial_Sums(seq2).(k+1) by BHSP_4:def 1;
end;
A5: P[0]
proof
assume
0 <= m;
thus Partial_Sums(seq1).0=seq1.0 by BHSP_4:def 1
.=seq2.0 by A1
.=Partial_Sums(seq2).0 by BHSP_4:def 1;
end;
for k holds P[k] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th12:
(for n holds ||. seq.n .|| <= rseq.n) & rseq is convergent & lim
(rseq)=0 implies seq is convergent & lim(seq)=0.X
proof
assume that
A1: for n holds ||. seq.n .|| <= rseq.n and
A2: rseq is convergent and
A3: lim(rseq)=0;
now
let p be Real;
assume 0<p;
then consider n such that
A4: for m st n<=m holds |.rseq.m-0 .|<p by A2,A3,SEQ_2:def 7;
now
let m;
assume n<=m;
then
A5: |.rseq.m-0 .|<p by A4;
A6: ||. seq.m-0.X .|| = ||. seq.m .|| by RLVECT_1:13;
A7: rseq.m <= |.rseq.m.| by ABSVALUE:4;
||. seq.m .|| <= rseq.m by A1;
then ||. seq.m - 0.X .|| <= |.rseq.m.| by A6,A7,XXREAL_0:2;
hence ||. seq.m - 0.X .|| < p by A5,XXREAL_0:2;
end;
hence ex n st for m st n<=m holds ||. seq.m - (0.X) .|| < p;
end;
then
A8: for p be Real st 0<p
ex n st for m st n<=m holds ||. seq.m - 0.X .|| < p;
hence seq is convergent;
hence thesis by A8,CLVECT_1:def 16;
end;
definition
let X,z;
func z ExpSeq -> sequence of X means
:Def1:
for n holds it.n = 1r/(n!) * (z #N n);
existence
proof
deffunc U(Nat) = 1r/(($1)!) *(z #N $1);
consider s being sequence of X such that
A1: for n being Element of NAT holds s.n = U(n) from FUNCT_2:sch 4;
take s;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1,S2 be sequence of X;
assume that
A2: for n be Nat holds S1.n = 1r/(n!) *(z #N n) and
A3: for n be Nat holds S2.n = 1r/(n!) *(z #N n);
for n be Element of NAT holds S1.n = S2.n
proof
let n be Element of NAT;
S1.n = 1r/(n!) *(z #N n) by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
scheme
ExNormSpaceCASE {CNS()->non empty Complex_Banach_Algebra, F(Nat,
Nat)-> Point of CNS() }: for k holds ex seq be sequence of CNS() st
for n holds (n <= k implies seq.n=F(k,n)) & (n > k implies seq.n=0.CNS()) proof
let k;
defpred P[object,object] means
ex n st (n=$1 & (n <= k implies $2=F(k,n )) & (n >
k implies $2=0.CNS()));
A1: now
let x be object;
assume x in NAT;
then consider n such that
A2: n=x;
reconsider y=CHK(n,k) * F (k,n) as object;
A3: n > k implies CHK(n,k) * F (k,n) =0.CNS() by CLVECT_1:1,SIN_COS:def 1;
take y;
now
assume n <= k;
hence CHK(n,k ) * F (k,n) =1r * F(k,n) by COMPLEX1:def 4,SIN_COS:def 1
.=F(k,n) by CLVECT_1:def 5;
end;
hence P[x,y] by A2,A3;
end;
consider f be Function such that
A4: dom f =NAT and
A5: for x be object st x in NAT holds P[x,f.x] from CLASSES1:sch 1(A1);
now
let x be object;
assume x in NAT;
then
ex n st n=x & (n <= k implies f.x=F(k,n)) & (n > k implies f.x=0.CNS(
)) by A5;
hence f.x in the carrier of CNS();
end;
then reconsider f as sequence of CNS() by A4,FUNCT_2:3;
take seq=f;
let n;
n in NAT by ORDINAL1:def 12;
then
ex l be Nat st l=n & (l <= k implies seq.n=F(k,l)) & (l > k
implies seq.n=0.CNS()) by A5;
hence thesis;
end;
definition
let n,X,z,w;
func Expan(n,z,w) -> sequence of X means
:Def2:
for k be Nat
holds ( k <= n implies it.k=((Coef(n)).k) * (z #N k) * (w #N (n-' k)) ) & (n <
k implies it.k=0.X);
existence
proof
deffunc U(Nat,Nat) = ((Coef($1)).$2) * (z #N $2) * (
w #N ($1 -' $2));
for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) & (k
> n implies seq.k=0.X) from ExNormSpaceCASE;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds (k <= n implies seq1.k =((Coef(n)).k) * (z #N k) * (w
#N (n-' k)))& (k > n implies seq1.k=0.X) and
A2: for k holds (k <= n implies seq2.k = ((Coef(n)).k) * (z #N k) * (w
#N (n-' k)) )& (k > n implies seq2.k=0.X);
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence seq1.k =((Coef(n)).k) * (z #N k) * (w #N (n-' k)) by A1
.= seq2.k by A2,A3;
end;
suppose
A4: k > n;
hence seq1.k = 0.X by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2 by FUNCT_2:63;
end;
end;
definition
let n,X,z,w;
func Expan_e(n,z,w) -> sequence of X means
:Def3:
for k be Nat
holds ( k <= n implies it.k=((Coef_e(n)).k) * (z #N k) * (w #N (n-' k)) ) & ( n
< k implies it.k=0.X );
existence
proof
deffunc U(Nat,Nat) = ((Coef_e($1)).$2) * (z #N $2) *
(w #N ($1-'$2));
for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) & (k
> n implies seq.k=0.X ) from ExNormSpaceCASE;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds (k <= n implies seq1.k =((Coef_e(n)).k) * (z #N k) * (
w #N (n-' k)) ) & (k > n implies seq1.k=0.X ) and
A2: for k holds (k <= n implies seq2.k = ((Coef_e(n)).k) * (z #N k) *
(w #N (n-' k)) ) & (k > n implies seq2.k=0.X );
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence seq1.k =((Coef_e(n)).k) * (z #N k) * (w #N (n-' k)) by A1
.= seq2.k by A2,A3;
end;
suppose
A4: k > n;
hence seq1.k = 0.X by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2 by FUNCT_2:63;
end;
end;
definition
let n,X,z,w;
func Alfa(n,z,w) -> sequence of X means
:Def4:
for k be Nat holds
( k <= n implies it.k= (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) ) & ( n < k
implies it.k=0.X);
existence
proof
deffunc U(Nat,Nat) = (z ExpSeq).$2 * Partial_Sums(w
ExpSeq).($1 -' $2);
for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) & (k
> n implies seq.k=0.X ) from ExNormSpaceCASE;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds (k <= n implies seq1.k = (z ExpSeq).k * Partial_Sums(w
ExpSeq).(n-'k) ) & (k > n implies seq1.k=0.X ) and
A2: for k holds (k <= n implies seq2.k = (z ExpSeq).k * Partial_Sums(w
ExpSeq).(n-'k) ) & (k > n implies seq2.k=0.X );
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence seq1.k = (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) by A1
.= seq2.k by A2,A3;
end;
suppose
A4: k > n;
hence seq1.k = 0.X by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2 by FUNCT_2:63;
end;
end;
definition
let X,z,w,n;
func Conj(n,z,w) -> sequence of X means
:Def5:
for k be Nat holds
( k <= n implies it.k= (z ExpSeq).k * (Partial_Sums(w ExpSeq).n -Partial_Sums(w
ExpSeq).(n-'k))) & ( n < k implies it.k=0.X );
existence
proof
deffunc U(Nat,Nat) = (z ExpSeq).$2 * (Partial_Sums(w
ExpSeq).$1 -Partial_Sums(w ExpSeq).($1-'$2));
for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k) ) & (
k > n implies seq.k=0.X) from ExNormSpaceCASE;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds (k <= n implies seq1.k =(z ExpSeq).k * (Partial_Sums(w
ExpSeq).n -Partial_Sums(w ExpSeq).(n-'k)) ) & (k > n implies seq1.k=0.X)
and
A2: for k holds (k <= n implies seq2.k = (z ExpSeq).k * (Partial_Sums(
w ExpSeq).n -Partial_Sums(w ExpSeq).(n-'k)) )& (k > n implies seq2.k=0.X);
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence seq1.k =(z ExpSeq).k * (Partial_Sums(w ExpSeq).n -Partial_Sums(w
ExpSeq).(n-'k)) by A1
.= seq2.k by A2,A3;
end;
suppose
A4: k > n;
hence seq1.k = 0.X by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2 by FUNCT_2:63;
end;
end;
theorem Th13:
z ExpSeq.(n+1) = (1r/(n+1) * z) * (z ExpSeq.n) & z ExpSeq.0=1.X
& ||.(z ExpSeq).n.|| <= (||.z.|| rExpSeq ).n
proof
defpred X[Nat] means ||. ((z ExpSeq)).$1 .|| <=( ||.z.|| rExpSeq ).$1;
A1: (z ExpSeq).0=1r/(0!) * z #N 0 by Def1
.=1r/(0!)*(z GeoSeq).0 by CLOPBAN3:def 8
.=1r * 1.X by CLOPBAN3:def 7,SIN_COS:1
.=1.X by CLVECT_1:def 5;
A2: now
let n be Nat;
thus (z ExpSeq).(n+1)=1r/((n+1)!) * z #N (n+1) by Def1
.=1r/((n+1)!) * (z GeoSeq).(n+1) by CLOPBAN3:def 8
.=1r/((n+1)!) * ((z GeoSeq).n * z) by CLOPBAN3:def 7
.=1r/((n+1)!) * (z #N n * z) by CLOPBAN3:def 8
.=1r/(n! * (n+1))*(z #N n * z) by SIN_COS:1
.=((1r*1r)/(n! * (n+1)))*(z* z #N n ) by Lm1,COMPLEX1:def 4
.=((1r/(n!)) * (1r/(n+1)) )*(z* z #N n ) by XCMPLX_1:76
.=((1r/(n+1))*z)*((1r/(n!)) * z #N n ) by CLOPBAN3:38
.=((1r/(n+1))*z)*(z ExpSeq.n) by Def1;
end;
A3: for n be Nat st X[n] holds X[n+1]
proof
let n such that
A4: X[n];
0<= ||. (1r/(n+1) *z) .|| by CLVECT_1:105;
then
A5: ||.(1r/(n+1) *z).|| * ||.(z ExpSeq.n).|| <= ||.(1r/(n+1) *z).|| * (
||.z.|| rExpSeq).n by A4,XREAL_1:64;
A6: ||. (1r/(n+1) *z)*(z ExpSeq.n ) .|| <= ||. (1r/(n+1) *z) .|| * ||. (z
ExpSeq.n ) .|| by CLOPBAN3:38;
|.(n+1).| = n+1 by ABSVALUE:def 1;
then |. 1r/(n+1) .| = 1/(n+1) by COMPLEX1:48,67;
then
A7: ||. (1r/(n+1) *z) .|| = 1/(n+1) * ||.z.|| by CLVECT_1:def 13;
A8: 1/(n+1) * ||.z.|| * (||.z.|| rExpSeq).n = 1/(n+1) * ( (||.z.||
rExpSeq).n * ||.z.|| )
.= 1/(n+1) * ( ((||.z.||)|^n)/(n!)*||.z.|| ) by SIN_COS:def 5
.= 1/(n+1) * ( ((||.z.||)|^n)*||.z.||/(n!) ) by XCMPLX_1:74
.= 1/(n+1) * ( (||.z.||)|^(n+1)/(n!) ) by NEWTON:6
.= ((||.z.||)|^ (n+1)) /((n)!*(n+1)) by XCMPLX_1:103
.= ((||.z.||)|^ (n+1)) /((n+1)!) by NEWTON:15
.= ( ||.z.|| rExpSeq ).(n+1) by SIN_COS:def 5;
||. ((z ExpSeq)).(n+1) .|| = ||. (1r/(n+1) *z )*(z ExpSeq.n) .|| by A2;
hence thesis by A6,A7,A5,A8,XXREAL_0:2;
end;
( ||.z.|| rExpSeq ).0 = ((||.z.||) |^ 0) / (0!) by SIN_COS:def 5
.= 1/(0!) by NEWTON:4
.= 1/((Prod_real_n).0) by SIN_COS:def 3
.= 1/1 by SIN_COS:def 2
.= 1;
then
A9: X[0] by A1,CLOPBAN3:38;
for n holds X[n] from NAT_1:sch 2(A9,A3);
hence thesis by A2,A1;
end;
theorem
0 < k implies (Shift seq).k=seq.(k -' 1) by LOPBAN_4:15;
theorem Th15:
Partial_Sums(seq).k=Partial_Sums(Shift seq).k+seq.k
proof
defpred X[Nat] means
Partial_Sums(seq).$1=Partial_Sums(Shift seq)
.$1+seq.$1;
A1: for k st X[k] holds X[k+1]
proof
let k;
assume Partial_Sums(seq).k=Partial_Sums(Shift(seq)).k+seq.k;
hence
Partial_Sums(seq).(k+1) = (Partial_Sums(Shift(seq)).k+seq.k) + seq.(k
+1) by BHSP_4:def 1
.=(Partial_Sums(Shift(seq)).k+(Shift(seq)).(k+1)) + seq.(k+1) by
LOPBAN_4:def 5
.=Partial_Sums(Shift(seq)).(k+1)+seq.(k+1) by BHSP_4:def 1;
end;
Partial_Sums(seq).0 = seq.0 by BHSP_4:def 1
.= 0.X + seq.0 by RLVECT_1:4
.= (Shift(seq)).0 + seq.0 by LOPBAN_4:def 5
.= Partial_Sums(Shift(seq)).0+seq.0 by BHSP_4:def 1;
then
A2: X[0];
for k holds X[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th16:
for z,w st z,w are_commutative holds (z+w) #N n = Partial_Sums(
Expan(n,z,w)).n
proof
let z,w such that
A1: z,w are_commutative;
defpred X[Nat] means
(z+w) #N $1 = Partial_Sums(Expan($1,z,w)).$1;
A2: for n st X[n] holds X[n+1]
proof
let n such that
A3: (z+w) #N n = Partial_Sums(Expan(n,z,w)).n;
A4: n < n+1 by XREAL_1:29;
now
let k be Element of NAT;
A5: n in NAT by ORDINAL1:def 12;
A6: now
A7: now
assume
A8: k < n+1;
A9: now
A10: k+1-1 <= n+1-1 by A8,A5,INT_1:7;
then
A11: (n-'k)+1=n-k+1 by XREAL_1:233
.=n+1-k
.=(n+1-'k) by A8,XREAL_1:233;
(n+1-k) <> 0 by A8;
then
A12: n! /( (k!) * ((n-'k)!) ) =(n! * (n+1-k))/(((k!) * ((n-'k
)!)) * (n+1-k+0*<i>)) by XCMPLX_1:91
.=(n! * (n+1-k))/((k!) * (((n-'k)!) * (n+1-k+0*<i>)))
.=(n! * (n+1-k))/((k!) * ((n+1-'k)!)) by A10,SIN_COS:2;
assume
A13: k<>0;
then
A14: 0<k;
then
A15: 0+1 <= k by INT_1:7;
then
A16: (k-'1)+1 =k-1+1 by XREAL_1:233
.=k;
k < k+1 by XREAL_1:29;
then k-1 <= k+1-1 by XREAL_1:9;
then k-1 <= n by A10,XXREAL_0:2;
then
A17: k-'1 <= n by A15,XREAL_1:233;
then
A18: (n-'(k-'1)) =n-(k-'1) by XREAL_1:233
.=n-(k-1) by A15,XREAL_1:233
.=n+1-k
.=n+1-'k by A8,XREAL_1:233;
(((k-'1)!) * (((n-'(k-'1)))!)) * k = k * ((k-'1)!) * (((n
-'(k-'1)))!)
.=(k+0*<i>) * ((k-'1)!) * (((n-'(k-'1)))!)
.=(k! ) * ((n+1-'k)! ) by A14,A18,SIN_COS:2;
then
A19: n! / (((k-'1)!) * (((n-'(k-'1)))!)) =(n! * k)/((k! ) * (
(n+1-'k)! )) by A13,XCMPLX_1:91;
(Coef(n)).k +(Coef(n)).(k -' 1) =n! /( (k!) * ((n-'k)!) )
+(Coef(n)).(k-'1) by A10,SIN_COS:def 6
.=n! /( (k!) * ((n-'k)!) ) +n! /(((k-'1)!)*(((n-'(k-'1)))
!)) by A17,SIN_COS:def 6;
then
A20: (Coef(n)).k +(Coef(n)).(k-'1) =((n! * (n+1-k))+(n! * k)) /
((k!) * ((n+1-'k)!)) by A12,A19,XCMPLX_1:62
.= ( n! * (n+1-k+k) ) / ((k!) * ((n+1-'k)!))
.= ( n! * (n+1-k+k+(0+0)*<i>) ) / ((k!) * ((n+1-'k)!))
.=((n+1)! ) / ((k! ) * ((n+1-'k)! )) by SIN_COS:1
.=(Coef(n+1)).k by A8,SIN_COS:def 6;
A21: (n-'(k-'1))=n-(k-'1) by A17,XREAL_1:233
.=n-(k-1) by A15,XREAL_1:233
.=n+1-k
.=(n+1-'k) by A8,XREAL_1:233;
(( Expan(n,z,w)*w )+Shift(( Expan(n,z,w)*z))).k =( Expan(n,z,
w)*w).k+(Shift((Expan(n,z,w)*z))).k by NORMSP_1:def 2
.=(Expan(n,z,w).k)*w + (Shift(( Expan(n,z,w)*z))).k by
LOPBAN_3:def 6
.=(Expan(n,z,w).k)*w + (Expan(n,z,w)*z).( k-'1) by A13,
LOPBAN_4:15
.=(Expan(n,z,w).k)*w + ( Expan(n,z,w).(k-'1))*z by LOPBAN_3:def 6
.=( (Coef(n)).k * (z #N k) * (w #N (n-' k)) ) *w + ( Expan(n,z
,w).(k-'1))*z by A10,Def2
.=(((Coef(n)).k * (z #N k) * (w #N (n-' k)))) *w + ( ((Coef(n)
).(k -' 1) * (z #N (k-'1)) * (w #N (n-' (k -' 1)))))*z by A17,Def2
.=((Coef(n)).k * ((z #N k)) * ((w #N (n-' k))*w)) + ( ((Coef(n
)).(k -' 1)) * (z #N (k -' 1)) * (w #N (n-' (k-'1)))) *z by GROUP_1:def 3
.=((Coef(n)).k * ((z #N k)) * ((w #N ((n-' k)+1)))) + ( ((Coef
(n)).(k -' 1)) * (z #N (k -' 1)) * (w #N (n-' (k-'1)))) *z by Lm1
.=((Coef(n)).k * ((z #N k)) * ((w #N ((n-' k)+1)))) + ((Coef(n
)).(k -' 1)) * (z #N (k -' 1)) *((w #N (n-' (k-'1))) *z) by GROUP_1:def 3
.=((Coef(n)).k * ((z #N k)) * ((w #N ((n-' k)+1)))) + ((Coef(n
)).(k -' 1)) * (z #N (k -' 1)) *(z*(w #N (n-' (k-'1)))) by A1,Lm2
.=((Coef(n)).k * ((z #N k)) * ((w #N ((n-' k)+1)))) + ((Coef(n
)).(k -' 1)) * (z #N (k -' 1)) *z*(w #N (n-' (k-'1))) by GROUP_1:def 3
.=((Coef(n)).k * ((z #N k)) * ((w #N ((n-' k)+1)))) + ((Coef(n
)).(k -'1))*((z #N (k -'1))*z)*(w #N (n-'(k-'1))) by CLOPBAN3:38
.=((Coef(n)).k * ((z #N k)) * ((w #N ((n-' k)+1)))) + ((Coef(n
)).(k -'1))*(z #N ((k -'1)+1))*(w #N (n-'(k-'1))) by Lm1;
then ((Expan(n,z,w)*w)+Shift((Expan(n,z,w)*z))) .k =(Coef(n)).k *
((z #N k) * (w #N (n+1-'k))) + (Coef(n)).((k -' 1)) *(z #N k) *(w #N (n+1-'k))
by A11,A21,A16,CLOPBAN3:38
.=(Coef(n)).k * ((z #N k) * (w #N (n+1-'k))) + (Coef(n)).((k
-' 1)) *((z #N k) *(w #N (n+1-'k))) by CLOPBAN3:38
.= ((Coef(n)).k +(Coef(n)).(k -' 1) ) * ((z #N k) * (w #N ((n+
1) -' k) )) by CLOPBAN3:38;
then
((Expan(n,z,w)*w)+Shift((Expan(n,z,w)*z))).k =(Coef(n+1)).k *
(z #N k) * (w #N (n+1-'k) ) by A20,CLOPBAN3:38
.=Expan(n+1,z,w).k by A8,Def2;
hence
(( Expan(n,z,w)*w)+Shift((Expan(n,z,w)*z))).k = Expan(n+1,z,w
) . k;
end;
now
A22: n+1-'0 =n+1-0 by XREAL_1:233;
then
A23: (Coef(n+1)).0 = (n+1)! /(1 * ((n+1)!)) by SIN_COS:1,def 6
.= 1 by XCMPLX_1:60;
A24: n-'0 =n-0 by XREAL_1:233;
then
A25: (Coef(n)).0 = n! /(1 * (n!)) by SIN_COS:1,def 6
.= 1 by XCMPLX_1:60;
assume
A26: k=0;
then
(( Expan(n,z,w)*w)+Shift(( Expan(n,z,w)*z))).k = ( Expan(n,z,
w)*w).0+(Shift((Expan(n,z,w)*z))).0 by NORMSP_1:def 2
.=(Expan(n,z,w).0 *w) + (Shift(( Expan(n,z,w)*z))).0 by
LOPBAN_3:def 6
.=( Expan(n,z,w).0 *w ) + 0.X by LOPBAN_4:def 5
.=( Expan(n,z,w).0 *w) by RLVECT_1:def 4
.= ((Coef(n)).0 * (z #N 0) * (w #N (n-'0)))*w by Def2
.= (Coef(n)).0 *(z #N 0) *((w #N (n-' 0))*w) by GROUP_1:def 3
.= (Coef(n+1)).0 *(z #N 0)* (w #N ((n+1)-'0)) by A24,A22,A25,A23
,Lm1
.= Expan(n+1,z,w).k by A26,Def2;
hence
((Expan(n,z,w)*w)+Shift(( Expan(n,z,w)*z))).k = Expan(n+1,z,w
) . k;
end;
hence ((Expan(n,z,w)*w)+Shift((Expan(n,z,w)*z))).k =Expan(n+1,z,w).k
by A9;
end;
A27: now
A28: n+1-'(n+1)= n+1-(n+1) by XREAL_1:233
.= 0;
then
A29: (Coef(n+1)).(n+1) = (n+1)! /(((n+1)!) * 1) by SIN_COS:1,def 6
.= 1 by XCMPLX_1:60;
A30: n < n+1 by XREAL_1:29;
A31: n-'n= n-n by XREAL_1:233
.= 0;
then
A32: (Coef(n)).n = n! /((n!) * 1) by SIN_COS:1,def 6
.= 1 by XCMPLX_1:60;
assume
A33: k=n+1;
then
(( Expan(n,z,w)*w)+Shift((Expan(n,z,w)*z))).k = (Expan(n,z,w)*w
).(n+1)+(Shift((Expan(n,z,w)*z ))).(n+1) by NORMSP_1:def 2
.= (Expan(n,z,w).(n+1) *w) + (Shift((Expan(n,z,w)*z))).(n+1) by
LOPBAN_3:def 6
.= (0.X*w) + (Shift(( Expan(n,z,w)*z))).(n+1) by A30,Def2
.= (0.X) + (Shift(( Expan(n,z,w)*z))).(n+1) by CLOPBAN3:38
.= (Shift((Expan(n,z,w)*z ))).(n+1) by RLVECT_1:def 4
.= (( Expan(n,z,w)*z)).(n) by LOPBAN_4:def 5
.= (Expan(n,z,w)).n *z by LOPBAN_3:def 6
.=((Coef(n)).n * (z #N n) * (w #N (n-' n))) *z by Def2
.=(Coef(n)).n * (z #N n) * ((w #N (n-' n)) *z) by GROUP_1:def 3
.=(Coef(n)).n * (z #N n) * ( z*(w #N (n-' n))) by A1,Lm2
.=(Coef(n)).n * (z #N n) * z*(w #N (n-' n)) by GROUP_1:def 3
.=(Coef(n)).n *( (z #N n) * z)*(w #N (n-' n)) by CLOPBAN3:38
.= ((Coef(n+1)).(n+1) * (z #N (n+1)) * (w #N (n-' n))) by A32,A29
,Lm1
.= Expan(n+1,z,w).k by A33,A31,A28,Def2;
hence
((Expan(n,z,w)*w) +Shift((Expan(n,z,w)*z))).k= Expan(n+1,z,w).k;
end;
assume k <= (n+1);
hence
((Expan(n,z,w)*w)+Shift((Expan(n,z,w)*z))).k =Expan(n+1,z,w).k by A27
,A7,XXREAL_0:1;
end;
now
assume
A34: n+1 < k;
then
A35: n+1-1 < k -1 by XREAL_1:9;
then
A36: n+0 < k-1+1 by XREAL_1:8;
0+1 <= n+1 by XREAL_1:6;
then
A37: k-1 =k-'1 by A34,XREAL_1:233,XXREAL_0:2;
(( Expan(n,z,w)*w)+Shift(( Expan(n,z,w)*z))).k =(Expan(n,z,w)*w).
k + (Shift((Expan(n,z,w)*z))).k by NORMSP_1:def 2
.=(Expan(n,z,w).k*w) + (Shift(( Expan(n,z,w)*z))).k by LOPBAN_3:def 6
.=(Expan(n,z,w).k*w) + ((Expan(n,z,w)*z)).(k -' 1) by A34,LOPBAN_4:15
.=(Expan(n,z,w).k*w) + ((Expan(n,z,w).(k -' 1)*z)) by LOPBAN_3:def 6
.=( 0.X*w )+ ((Expan(n,z,w).(k -' 1))*z) by A36,Def2
.= 0.X+ ((Expan(n,z,w).(k -' 1))*z) by CLOPBAN3:38
.=0.X + ( 0.X*z) by A35,A37,Def2
.=0.X + 0.X by CLOPBAN3:38
.=0.X by RLVECT_1:def 4;
hence (( Expan(n,z,w)*w)+Shift((Expan(n,z,w)*z))).k =Expan(n+1,z,w).k
by A34,Def2;
end;
hence ((Expan(n,z,w)*w)+Shift((Expan(n,z,w)*z))).k =Expan(n+1,z,w).k by
A6;
end;
then
A38: ( Expan(n,z,w)*w)+Shift(( Expan(n,z,w)*z)) =Expan(n+1,z,w) by FUNCT_2:63;
A39: n < n+1 by XREAL_1:29;
Partial_Sums((Expan(n,z,w)*w)).(n+1) =Partial_Sums((Expan(n,z,w)*w)).
n+(Expan(n,z,w)*w).(n+1) by BHSP_4:def 1
.=Partial_Sums((Expan(n,z,w)*w)).n + Expan(n,z,w).(n+1) *w by
LOPBAN_3:def 6;
then
A40: Partial_Sums(( Expan(n,z,w)*w)).(n+1) =Partial_Sums((Expan(n,z,w)*w))
.n +0.X *w by A39,Def2
.=Partial_Sums((Expan(n,z,w)*w)).n +0.X by CLOPBAN3:38
.=Partial_Sums((Expan(n,z,w)*w)).n by RLVECT_1:def 4;
Partial_Sums((Expan(n,z,w)*z)).(n+1) = Partial_Sums((Expan(n,z,w)*z))
.n+(Expan(n,z,w)*z).(n+1) by BHSP_4:def 1
.= Partial_Sums((Expan(n,z,w)*z)).n + Expan(n,z,w).(n+1) *z by
LOPBAN_3:def 6;
then
A41: Partial_Sums(( Expan(n,z,w)*z)).(n+1) =Partial_Sums((Expan(n,z,w)*z))
.n +0.X *z by A4,Def2
.=Partial_Sums((Expan(n,z,w)*z)).n +0.X by CLOPBAN3:38
.=Partial_Sums((Expan(n,z,w)*z)).n by RLVECT_1:def 4;
0 +n < n+1 by XREAL_1:29;
then
A42: Expan(n,z,w).(n+1)=0.X by Def2;
Partial_Sums(( Expan(n,z,w)*z)).(n+1) =Partial_Sums(Shift(( Expan(n,z
,w)*z))).(n+1) +( Expan(n,z,w)*z).(n+1) by Th15;
then
A43: Partial_Sums(( Expan(n,z,w)*z)).(n+1) =Partial_Sums(Shift(( Expan(n,z
,w)*z))).(n+1) + Expan(n,z,w).(n+1)*z by LOPBAN_3:def 6
.=Partial_Sums(Shift(( Expan(n,z,w)*z))).(n+1) +0.X by A42,CLOPBAN3:38
.= Partial_Sums(Shift((Expan(n,z,w)*z))).(n+1) by RLVECT_1:def 4;
now
let k be Element of NAT;
thus ( Expan(n,z,w)*(z+w) ).k= Expan(n,z,w).k *(z+w) by LOPBAN_3:def 6
.= Expan(n,z,w).k * z + Expan(n,z,w).k *w
by VECTSP_1:def 2
.=( Expan(n,z,w)*z).k+ Expan(n,z,w).k *w by LOPBAN_3:def 6
.=(Expan(n,z,w)*z).k+(Expan(n,z,w)*w).k by LOPBAN_3:def 6
.=( (Expan(n,z,w)*z)+(Expan(n,z,w)*w)).k by NORMSP_1:def 2;
end;
then
A44: Expan(n,z,w)*(z+w) =( Expan(n,z,w)*z)+(Expan(n,z,w)*w) by FUNCT_2:63;
(z+w) #N (n+1) =((z+w) GeoSeq ).(n+1) by CLOPBAN3:def 8
.=((z+w) GeoSeq ).n * (z+w) by CLOPBAN3:def 7
.=(Partial_Sums(Expan(n,z,w)).n) * (z+w) by A3,CLOPBAN3:def 8
.=(Partial_Sums(Expan(n,z,w))*(z+w)) .n by LOPBAN_3:def 6
.=(Partial_Sums(Expan(n,z,w)*(z+w))).n by Th9;
then (z+w) #N (n+1) =( Partial_Sums( (Expan(n,z,w)*z)) +Partial_Sums(( (
Expan(n,z,w)*w)))).n by A44,CLOPBAN3:15
.= Partial_Sums((Expan(n,z,w)*z)).n +Partial_Sums((Expan(n,z,w)*w)).n
by NORMSP_1:def 2;
hence
(z+w) #N (n+1) =(Partial_Sums(( Expan(n,z,w)*w)) + Partial_Sums(Shift
(( Expan(n,z,w)*z)))).(n+1) by A41,A40,A43,NORMSP_1:def 2
.=Partial_Sums(Expan(n+1,z,w)).(n+1) by A38,CLOPBAN3:15;
end;
A45: (z+w) #N 0 =((z+w) GeoSeq).0 by CLOPBAN3:def 8
.=1.X by CLOPBAN3:def 7;
A46: 0-'0=0-0 by XREAL_0:def 2
.=0;
Partial_Sums(Expan(0,z,w)).0 = Expan(0,z,w).0 by BHSP_4:def 1
.= (Coef(0)).0 * (z #N 0) * (w #N 0) by A46,Def2
.= 1r/(1r * 1r) * z #N 0 * w #N 0 by A46,COMPLEX1:def 4,SIN_COS:1,def 6
.= z #N 0 * w #N 0 by CLVECT_1:def 5,COMPLEX1:def 4
.= (z GeoSeq).0 * w #N 0 by CLOPBAN3:def 8
.= (z GeoSeq).0 * (w GeoSeq).0 by CLOPBAN3:def 8
.= 1.X * (w GeoSeq).0 by CLOPBAN3:def 7
.= 1.X * 1.X by CLOPBAN3:def 7
.= 1.X by VECTSP_1:def 4;
then
A47: X[0] by A45;
for n holds X[n] from NAT_1:sch 2(A47,A2);
hence thesis;
end;
theorem Th17:
Expan_e(n,z,w) = (1r/(n!)) * Expan(n,z,w)
proof
now
let k be Element of NAT;
A1: now
reconsider s = n! as Element of COMPLEX by XCMPLX_0:def 2;
A2: 1r/((k!) * ((n-'k)!)) =(((n!) * 1r)/(n!)) /((k!) * ((n-'k)!))
by COMPLEX1:def 4,XCMPLX_1:60
.= (1r/(n!)) * (n!) /((k!) * ((n-'k)!)) by XCMPLX_1:74;
assume
A3: k <= n;
hence Expan_e(n,z,w).k = (Coef_e(n)).k * (z #N k) * (w #N (n -' k))
by Def3
.= 1r/((k!) * ((n-'k)!)) * (z #N k) * (w #N (n-'k))
by A3,SIN_COS:def 7;
hence Expan_e(n,z,w).k = (1r/(n!)) * (n!) /((k!) * ((n-'k)!)) * ((z
#N k) * (w #N (n-'k))) by A2,CLOPBAN3:38
.= (1r/(n!)) * ((n!) /((k!) * ((n-'k)!))) * ((z #N k) * (w #N (n
-'k))) by XCMPLX_1:74
.= (1r/s) * ((s /((k!) * ((n-'k)!))) * ((z #N k) * (w #N (n-'k))))
by CLOPBAN3:38
.= (1r/s) * (s /((k!) * ((n-'k)!)) * (z #N k) * (w #N (n-' k)))
by CLOPBAN3:38
.= (1r/(n!)) * ((Coef(n)).k * ((z #N k)) * (w #N (n-'k)))
by A3,SIN_COS:def 6
.= (1r/(n!)) * Expan(n,z,w).k by A3,Def2
.= ( (1r/(n!)) * Expan(n,z,w) ).k by CLVECT_1:def 14;
end;
now
assume
A4: n <k;
hence Expan_e(n,z,w).k = 0.X by Def3
.=(1r/(n!)) * 0.X by CLVECT_1:1
.=(1r/(n!)) * Expan(n,z,w).k by A4,Def2
.=((1r/(n!)) * Expan(n,z,w)).k by CLVECT_1:def 14;
end;
hence Expan_e(n,z,w).k = ( (1r/(n!)) * Expan(n,z,w) ).k by A1;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th18:
for z,w st z,w are_commutative holds 1r/(n!) *((z+w) #N n) =
Partial_Sums(Expan_e(n,z,w)).n
proof
let z,w;
assume z,w are_commutative;
hence 1r/(n!)*((z+w) #N n) = 1r/(n!)*(Partial_Sums(Expan(n,z,w)).n) by Th16
.= ((1r/(n!)) * (Partial_Sums(Expan(n,z,w)))).n by CLVECT_1:def 14
.= Partial_Sums((1r/(n!)) * Expan(n,z,w)).n by CLOPBAN3:19
.= Partial_Sums(Expan_e(n,z,w)).n by Th17;
end;
theorem Th19:
0.X ExpSeq is norm_summable & Sum(0.X ExpSeq)=1.X
proof
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
defpred X[set] means Partial_Sums( ||. 0.X ExpSeq.||).$1=jj;
A1: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat such that
A2: Partial_Sums(||.0.X ExpSeq .||).n=jj;
thus
Partial_Sums(||.0.X ExpSeq .||).(n+1) =1 + ||.0.X ExpSeq .||.(n+1) by A2,
SERIES_1:def 1
.=1 + ||.(0.X ExpSeq ).(n+1).|| by NORMSP_0:def 4
.=1 + ||.(1r/(n+1) * 0.X)*(0.X ExpSeq .n) .|| by Th13
.=1 + ||.(0.X)*(0.X ExpSeq .n) .|| by CLVECT_1:1
.=1 + ||.0.X.|| by CLOPBAN3:38
.=1 + 0 by CLOPBAN3:38
.=jj;
end;
Partial_Sums(||.(0.X ExpSeq).||).0 =||. (0.X ExpSeq) .||.0 by SERIES_1:def 1
.=||. (0.X ExpSeq).0 .|| by NORMSP_0:def 4
.=||. 1.X .|| by Th13
.=1 by CLOPBAN3:38;
then
A3: X[0];
for n being Nat holds X[n] from NAT_1:sch 2(A3,A1);
then Partial_Sums(||.0.X ExpSeq .||) is constant by VALUED_0:def 18;
then
A4: ||.0.X ExpSeq .|| is summable by SERIES_1:def 2;
defpred X[set] means Partial_Sums(0.X ExpSeq ).$1=1.X;
A5: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(0.X ExpSeq ).n=1.X;
hence Partial_Sums(0.X ExpSeq ).(n+1) =1.X + (0.X ExpSeq ).(n+1) by
BHSP_4:def 1
.=1.X + (1r/(n+1) *0.X)*(0.X ExpSeq .n) by Th13
.=1.X + (0.X)*(0.X ExpSeq .n) by CLVECT_1:1
.=1.X + 0.X by CLOPBAN3:38
.=1.X by RLVECT_1:def 4;
end;
Partial_Sums(0.X ExpSeq ).0 =(0.X ExpSeq ).0 by BHSP_4:def 1
.=1.X by Th13;
then
A6: X[0];
for n holds X[n] from NAT_1:sch 2(A6,A5);
then lim(Partial_Sums(0.X ExpSeq ))=1.X by Th2;
hence thesis by A4,CLOPBAN3:def 2,def 3;
end;
registration
let X;
let z be Element of X;
cluster z ExpSeq -> norm_summable;
coherence
proof
ex m be Nat st for n be Nat st m<=n holds ||.(z
ExpSeq).n.|| <= (||.z.|| rExpSeq ).n
proof
take 0;
thus thesis by Th13;
end;
hence thesis by CLOPBAN3:27,SIN_COS:45;
end;
end;
theorem Th20:
(z ExpSeq).0 = 1.X & Expan(0,z,w).0 = 1.X
proof
thus (z ExpSeq).0 = 1r/(0!)*(z #N 0) by Def1
.= 1r/(0!)*(z GeoSeq).0 by CLOPBAN3:def 8
.= 1r * 1.X by CLOPBAN3:def 7,SIN_COS:1
.= 1.X by CLVECT_1:def 5;
A1: 0-'0=0 by XREAL_1:232;
hence Expan(0,z,w).0 = (Coef(0)).0 * (z #N 0) * (w #N 0) by Def2
.= 1r/(1r * 1r) * z #N 0 * w #N 0 by A1,COMPLEX1:def 4,SIN_COS:1,def 6
.= z #N 0 * w #N 0 by CLVECT_1:def 5,COMPLEX1:def 4
.= (z GeoSeq).0 * w #N 0 by CLOPBAN3:def 8
.= (z GeoSeq).0 * (w GeoSeq).0 by CLOPBAN3:def 8
.= 1.X * (w GeoSeq).0 by CLOPBAN3:def 7
.= 1.X * 1.X by CLOPBAN3:def 7
.= 1.X by VECTSP_1:def 4;
end;
theorem Th21:
l <= k implies (Alfa(k+1,z,w)).l = (Alfa(k,z,w)).l + Expan_e(k+1 ,z,w).l
proof
assume
A1: l <= k;
A2: k < k+1 by XREAL_1:29;
then
A3: l <= k+1 by A1,XXREAL_0:2;
A4: (z ExpSeq).l * (w ExpSeq).(((k+1)-' l)) =1r/(l!)*(z #N l) * (w ExpSeq).
(((k+1)-' l)) by Def1
.=1r/(l!)*(z #N l) * (1r/(((k+1)-'l )!)*(w #N (((k+1)-'l)))) by Def1
.=(1r/(l!)* (1r/(((k+1)-'l)!))*((z #N l) *(w #N (((k+1)-'l))))) by
CLOPBAN3:38
.=((1r*1r)/((l!) * (((k+1)-'l)!) )*((z #N l) *(w #N (((k+1)-'l))))) by
XCMPLX_1:76
.= ((Coef_e(k+1)).l) * ((z #N l) * (w #N (((k+1)-'l)))) by A3,
COMPLEX1:def 4,SIN_COS:def 7
.= ((Coef_e(k+1)).l) * (z #N l) * (w #N (((k+1)-'l))) by CLOPBAN3:38
.=Expan_e(k+1,z,w).l by A3,Def3;
(k+1-'l)=k+1-l by A1,A2,XREAL_1:233,XXREAL_0:2;
then
A5: (k+1-'l)=k-l+1 .=(k-'l)+1 by A1,XREAL_1:233;
then
(Alfa(k+1,z,w)).l =((z ExpSeq).l )* (Partial_Sums(w ExpSeq).((k -' l)+1)
) by A3,Def4
.=(z ExpSeq).l * (Partial_Sums(w ExpSeq).((k -' l)) +(w ExpSeq).(((k+1)
-'l))) by A5,BHSP_4:def 1
.=((z ExpSeq).l * (Partial_Sums(w ExpSeq).((k -' l))) +((z ExpSeq).l * (
w ExpSeq).(( (k+1) -' l)))) by VECTSP_1:def 2
.=(Alfa(k,z,w)).l+((z ExpSeq).l * (w ExpSeq).(( (k+1) -' l))) by A1,Def4;
hence thesis by A4;
end;
theorem Th22:
Partial_Sums((Alfa(k+1,z,w))).k = (Partial_Sums( Alfa(k,z,w) )).
k + (Partial_Sums( Expan_e(k+1,z,w) )).k
proof
now
let l be Nat;
assume l <= k;
hence (Alfa(k+1,z,w)).l = (Alfa(k,z,w)).l + Expan_e(k+1,z,w).l by Th21
.= ( (Alfa(k,z,w)) + Expan_e(k+1,z,w)).l by NORMSP_1:def 2;
end;
hence
Partial_Sums((Alfa(k+1,z,w))).k =Partial_Sums(((Alfa(k,z,w)) + Expan_e(
k+1,z,w))).k by Th11
.=(Partial_Sums(( Alfa(k,z,w))) +Partial_Sums(( Expan_e(k+1,z,w )))).k
by CLOPBAN3:15
.= (Partial_Sums(( Alfa(k,z,w)))).k + (Partial_Sums(( Expan_e(k+1,z,w) )
)).k by NORMSP_1:def 2;
end;
theorem Th23:
(z ExpSeq).k=(Expan_e(k,z,w)).k
proof
0 = k -k;
then
A1: k-'k=0 by XREAL_1:233;
hence (Expan_e(k,z,w)).(k)=((Coef_e(k)).k) * (z #N k) * (w #N 0) by Def3
.=( (Coef_e(k)).k) * (z #N k) * 1.X by CLOPBAN3:39
.=( (Coef_e(k)).k) * (z #N k) by VECTSP_1:def 4
.=(1r/((k!) * 1r)) * (z #N k) by A1,COMPLEX1:def 4,SIN_COS:1,def 7
.=(z ExpSeq).k by Def1,COMPLEX1:def 4;
end;
theorem Th24:
for z,w st z,w are_commutative holds Partial_Sums((z+w) ExpSeq).
n = Partial_Sums(Alfa(n,z,w)).n
proof
let z,w such that
A1: z,w are_commutative;
defpred X[Nat] means
Partial_Sums((z+w) ExpSeq).$1=Partial_Sums(
Alfa($1,z,w)).$1;
A2: for k st X[k] holds X[k+1]
proof
let k such that
A3: Partial_Sums((z+w) ExpSeq).k=Partial_Sums(Alfa(k,z,w)).k;
k+1-'(k+1)=0 by XREAL_1:232;
then
(Alfa(k+1,z,w)).(k+1) =(z ExpSeq).(k+1) * Partial_Sums(w ExpSeq).0 by Def4
.=(z ExpSeq).(k+1) * ((w ExpSeq).0) by BHSP_4:def 1
.=(z ExpSeq).(k+1) * 1.X by Th20
.=(z ExpSeq).(k+1) by VECTSP_1:def 4
.=(Expan_e(k+1,z,w)).(k+1) by Th23;
then
A4: (Partial_Sums(( Expan_e(k+1,z,w) ))).k + (Alfa(k+1,z,w)).(k+1) =(
Partial_Sums(( Expan_e(k+1,z,w) ))).(k+1) by BHSP_4:def 1
.=1r/((k+1)!) * (z+w) #N (k+1) by A1,Th18;
Partial_Sums((Alfa(k+1,z,w))).(k+1) =Partial_Sums((Alfa(k+1,z,w))).k+(
Alfa(k+1,z,w)).(k+1) by BHSP_4:def 1
.=((Partial_Sums(Alfa(k,z,w))).k + (Partial_Sums(Expan_e(k+1,z,w))).k)
+ (Alfa(k+1,z,w)).(k+1) by Th22
.= Partial_Sums((z+w) ExpSeq).k + ((Partial_Sums(Expan_e(k+1,z,w))).k
+ (Alfa(k+1,z,w)).(k+1)) by A3,RLVECT_1:def 3;
then Partial_Sums((Alfa(k+1,z,w))).(k+1) = Partial_Sums((z+w) ExpSeq).k +
(z+w) ExpSeq.(k+1) by A4,Def1
.= Partial_Sums((z+w) ExpSeq).(k+1) by BHSP_4:def 1;
hence Partial_Sums((z+w) ExpSeq).(k+1)=Partial_Sums(Alfa(k+1,z,w)).(k+1);
end;
A5: Partial_Sums((z+w) ExpSeq).0 =((z+w) ExpSeq).0 by BHSP_4:def 1
.=1.X by Th20;
A6: 0-'0=0 by XREAL_1:232;
Partial_Sums(Alfa(0,z,w)).0 = Alfa(0,z,w).0 by BHSP_4:def 1
.= (z ExpSeq).0 * Partial_Sums(w ExpSeq).0 by A6,Def4
.= (z ExpSeq).0 * (w ExpSeq).0 by BHSP_4:def 1
.=1.X * (w ExpSeq).0 by Th20
.=1.X * 1.X by Th20
.= 1.X by VECTSP_1:def 4;
then
A7: X[0] by A5;
for n holds X[n] from NAT_1:sch 2(A7,A2);
hence thesis;
end;
theorem Th25:
for z,w st z,w are_commutative holds Partial_Sums(z ExpSeq).k *
Partial_Sums(w ExpSeq).k - Partial_Sums((z+w) ExpSeq).k = Partial_Sums(Conj(k,z
,w)).k
proof
let z,w;
assume z,w are_commutative;
then
A1: (Partial_Sums(z ExpSeq).k) * (Partial_Sums(w ExpSeq).k) -Partial_Sums((z
+w) ExpSeq).k =Partial_Sums(z ExpSeq).k * Partial_Sums(w ExpSeq).k -
Partial_Sums(Alfa(k,z,w)).k by Th24
.=( Partial_Sums(z ExpSeq)* (Partial_Sums(w ExpSeq).k) ).k -Partial_Sums
(Alfa(k,z,w)).k by LOPBAN_3:def 6
.=(Partial_Sums((z ExpSeq)*(Partial_Sums(w ExpSeq).k))) .k -Partial_Sums
(Alfa(k,z,w)).k by Th9
.=(Partial_Sums( (z ExpSeq)*(Partial_Sums(w ExpSeq).k) ) -Partial_Sums(
Alfa(k,z,w))).k by NORMSP_1:def 3
.=Partial_Sums((( (z ExpSeq)*(Partial_Sums(w ExpSeq).k))) -(Alfa(k,z,w))
).k by CLOPBAN3:16;
for l be Nat st l <= k holds ((z ExpSeq)*(Partial_Sums(w
ExpSeq).k) - (Alfa(k,z,w))).l =Conj(k,z,w).l
proof
let l be Nat such that
A2: l <= k;
thus ((z ExpSeq)*( Partial_Sums(w ExpSeq).k) - (Alfa(k,z,w))).l = ((z
ExpSeq)*(Partial_Sums(w ExpSeq).k) ).l - (Alfa(k,z,w)).l by NORMSP_1:def 3
.= ( (z ExpSeq).l )*( Partial_Sums(w ExpSeq).k) - Alfa(k,z,w).l by
LOPBAN_3:def 6
.=((z ExpSeq).l) * ( Partial_Sums(w ExpSeq).k) -((z ExpSeq).l) * (
Partial_Sums(w ExpSeq).(k-'l)) by A2,Def4
.=((z ExpSeq).l) * ( Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).
(k-'l) ) by CLOPBAN3:38
.=Conj(k,z,w).l by A2,Def5;
end;
hence thesis by A1,Th11;
end;
theorem Th26:
0 <= (||. z .|| rExpSeq).n
proof
defpred P[Nat] means 0 <= ||.z.|| |^$1;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
A3: 0 <= ||.z.|| by CLVECT_1:105;
||.z.|| |^ (k+1) = ||.z.|| |^ k * ||.z.|| by NEWTON:6;
hence thesis by A2,A3;
end;
A4: P[0] by NEWTON:4;
for k holds P[k] from NAT_1:sch 2(A4,A1);
then
A5: 0 <= ||.z.|| |^n;
A6: ||.z.|| |^n/(n!) = ||.z.|| |^n *((n!))" by XCMPLX_0:def 9;
thus thesis by A5,A6,SIN_COS:def 5;
end;
theorem Th27:
||. Partial_Sums((z ExpSeq)).k .|| <= Partial_Sums(||.z.||
rExpSeq).k & Partial_Sums((||.z.|| rExpSeq)).k <= Sum(||.z.|| rExpSeq) & ||.
Partial_Sums(( z ExpSeq)).k .|| <= Sum(||.z.|| rExpSeq)
proof
defpred X[Nat] means
||. Partial_Sums(( z ExpSeq)).$1 .|| <=
Partial_Sums((||.z.|| rExpSeq)).$1;
A1: Partial_Sums((||.z.|| rExpSeq)).0 = ((||.z.|| rExpSeq)).0 by SERIES_1:def 1
.= ((||.z.|| ) |^ 0 ) / (0!) by SIN_COS:def 5
.= 1 by NEWTON:4,12;
A2: for k st X[k] holds X[k+1]
proof
let k;
assume
||. Partial_Sums(( z ExpSeq)).k .|| <= Partial_Sums((||.z.|| rExpSeq)).k;
then
A3: ||. Partial_Sums(( z ExpSeq)).k.|| + (||.z.|| rExpSeq).(k+1) <=
Partial_Sums((||.z.|| rExpSeq)).k + (||.z.|| rExpSeq).(k+1) by XREAL_1:6;
A4: ||. Partial_Sums(( z ExpSeq)).k + ((z ExpSeq)).(k+1) .|| <= ||.
Partial_Sums(( z ExpSeq)).k.|| + ||. ((z ExpSeq)).(k+1) .|| by CLOPBAN3:38;
||. ((z ExpSeq)).(k+1) .|| <=(||.z.|| rExpSeq).(k+1) by Th13;
then
A5: ||. Partial_Sums(( z ExpSeq)).k.|| + ||. ((z ExpSeq)).(k+1) .|| <= ||.
Partial_Sums(( z ExpSeq)).k.|| + (||.z.|| rExpSeq).(k+1) by XREAL_1:7;
A6: Partial_Sums((||.z.|| rExpSeq)).k + (||.z.|| rExpSeq).(k+1) =
Partial_Sums((||.z.|| rExpSeq)).(k+1) by SERIES_1:def 1;
||. Partial_Sums(( z ExpSeq)).(k+1) .|| =||. Partial_Sums(( z ExpSeq))
.k + ((z ExpSeq)).(k+1) .|| by BHSP_4:def 1;
then ||. Partial_Sums(( z ExpSeq)).(k+1) .|| <= ||. Partial_Sums(( z
ExpSeq)).k.|| + (||.z.|| rExpSeq).(k+1) by A4,A5,XXREAL_0:2;
hence thesis by A3,A6,XXREAL_0:2;
end;
||. Partial_Sums(( z ExpSeq)).0 .|| = ||. ((z ExpSeq)).0 .|| by BHSP_4:def 1
.= ||. 1r/ (0!)*(z #N 0).|| by Def1
.= ||. 1r/(0!)*((z GeoSeq)).0 .|| by CLOPBAN3:def 8
.= ||. 1r * 1.X.|| by CLOPBAN3:def 7,SIN_COS:1
.= ||. 1.X.|| by CLVECT_1:def 5
.= 1 by CLOPBAN3:38;
then
A7: X[0] by A1;
A8: for k holds X[k] from NAT_1:sch 2(A7,A2);
hence
||. Partial_Sums(( z ExpSeq)).k .|| <= Partial_Sums((||.z.|| rExpSeq)). k;
A9: for n holds 0 <= (||.z.|| rExpSeq).n by Th26;
||.z.|| rExpSeq is summable by SIN_COS:45;
then
A10: Partial_Sums(||.z.|| rExpSeq) is bounded_above by A9,SERIES_1:17;
then Partial_Sums((||.z.|| rExpSeq)).k <= lim(Partial_Sums((||.z.|| rExpSeq
) )) by A9,SEQ_4:37,SERIES_1:16;
hence Partial_Sums((||.z.|| rExpSeq)).k <= Sum(||.z.|| rExpSeq) by
SERIES_1:def 3;
now
let k;
lim(Partial_Sums((||.z.|| rExpSeq)))=Sum(||.z.|| rExpSeq) by SERIES_1:def 3
;
hence
Partial_Sums((||.z.|| rExpSeq)).k <= Sum(||.z.|| rExpSeq) by A9,A10,
SEQ_4:37,SERIES_1:16;
end;
then
A11: Partial_Sums((||.z.|| rExpSeq)).k <= Sum(||.z.|| rExpSeq);
||. Partial_Sums(( z ExpSeq)).k .|| <= Partial_Sums((||.z.|| rExpSeq)).
k by A8;
hence thesis by A11,XXREAL_0:2;
end;
theorem Th28:
1 <= Sum(||.z.|| rExpSeq)
proof
||. Partial_Sums(z ExpSeq).0 .|| =||. (z ExpSeq).0 .|| by BHSP_4:def 1
.=||. 1.X.|| by Th13
.=1 by CLOPBAN3:38;
hence thesis by Th27;
end;
theorem Th29:
|.(Partial_Sums(||.z.|| rExpSeq)).n.| = Partial_Sums(||.z.||
rExpSeq).n & ( n <= m implies |.(Partial_Sums(||.z.|| rExpSeq).m-Partial_Sums
(||.z.|| rExpSeq).n).|
= Partial_Sums(||.z.|| rExpSeq).m-Partial_Sums(||.z.||
rExpSeq).n )
proof
for n holds 0 <= (||. z .|| rExpSeq).n by Th26;
hence thesis by COMSEQ_3:9;
end;
theorem Th30:
|.Partial_Sums(||.Conj(k,z,w).||).n.|=Partial_Sums(||.Conj(k,z, w).||).n
proof
A1: now
let n;
||.Conj(k,z,w).||.n=||.(Conj(k,z,w)).n.|| by NORMSP_0:def 4;
hence 0 <= ||.Conj(k,z,w).||.n by CLVECT_1:105;
end;
then Partial_Sums(||.Conj(k,z,w).||) is non-decreasing by SERIES_1:16;
then
A2: Partial_Sums(||.Conj(k,z,w).||).0 <= Partial_Sums(||.Conj(k,z,w).||).n
by SEQM_3:6;
A3: Partial_Sums(||.Conj(k,z,w).||).0=(||.Conj(k,z,w).||).0 by SERIES_1:def 1;
0 <= (||.Conj(k,z,w).||).0 by A1;
hence thesis by A2,A3,ABSVALUE:def 1;
end;
theorem Th31:
for p being Real st p>0 ex n st for k st n <= k holds
|.Partial_Sums(||.Conj(k,z,w).||).k.| < p
proof
let p be Real such that
A1: p>0;
reconsider pp = p as Real;
set p1=min((pp/(4 * Sum(||.z.|| rExpSeq))),(pp/(4 * Sum(||.w.|| rExpSeq))));
A2: 1 <= Sum(||.w.|| rExpSeq) by Th28;
A3: 1 <= Sum(||.z.|| rExpSeq) by Th28;
then
A4: p1 > 0 by A1,A2,XXREAL_0:15;
Partial_Sums(( w ExpSeq )) is convergent by CLOPBAN3:def 1;
then for s be Real st 0<s
ex n be Nat st for m be Nat
st n<=m holds ||.Partial_Sums(( w ExpSeq )).m -Partial_Sums(( w ExpSeq )).n.||<
s by CLOPBAN3:4;
then Partial_Sums(( w ExpSeq )) is Cauchy_sequence_by_Norm by CLOPBAN3:5;
then consider n2 such that
A5: for k,l be Nat st n2 <= k & n2 <= l holds ||.
Partial_Sums(( w ExpSeq )).k - Partial_Sums(( w ExpSeq )).l.|| < p1 by A4,
CSSPACE3:8;
( ||.z.|| rExpSeq ) is summable by SIN_COS:45;
then Partial_Sums(( ||.z.|| rExpSeq )) is convergent by SERIES_1:def 2;
then consider n1 such that
A6: for k,l be Nat st n1 <= k & n1 <= l holds |.
Partial_Sums(( ||.z.|| rExpSeq )).k - Partial_Sums(( ||.z.|| rExpSeq )).l.|
< p1
by A4,COMSEQ_3:4;
set n3=n1+n2;
take n4 = n3+n3;
A7: now
let n;
let k;
now
let l be Nat such that
A8: l <= k;
A9: ||.(z ExpSeq).l * (Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq)
.(k-'l)) .|| <=||.(z ExpSeq).l.|| * ||.(Partial_Sums(w ExpSeq).k -Partial_Sums(
w ExpSeq).(k-'l)).|| by CLOPBAN3:38;
0 <=||.(Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l)).||
by CLVECT_1:105;
then
A10: ||.(z ExpSeq).l.|| * ||.(Partial_Sums(w ExpSeq).k -Partial_Sums(w
ExpSeq).(k-'l)).|| <=(||.z.|| rExpSeq).l * ||.(Partial_Sums(w ExpSeq).k -
Partial_Sums(w ExpSeq).(k-'l)).|| by Th13,XREAL_1:64;
||.Conj(k,z,w).||.l =||.( Conj(k,z,w).l) .|| by NORMSP_0:def 4
.=||.(z ExpSeq).l * (Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq
).(k-'l)) .|| by A8,Def5;
hence ||.Conj(k,z,w).||.l <=(||.z.|| rExpSeq).l * ||.(Partial_Sums(w
ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l)).|| by A9,A10,XXREAL_0:2;
end;
hence for l be Nat st l <= k holds ||.Conj(k,z,w).||.l <=(||.z
.|| rExpSeq).l * ||.(Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l))
.||;
end;
A11: now
let k;
now
let l be Nat;
A12: ||.Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l).|| <=
||.Partial_Sums(w ExpSeq).k .|| + ||.Partial_Sums(w ExpSeq).(k-'l).|| by
CLVECT_1:104;
||.Partial_Sums(w ExpSeq).(k-'l).|| <= Sum(||.w.|| rExpSeq) by Th27;
then
A13: Sum(||.w.|| rExpSeq) + ||.Partial_Sums(w ExpSeq).(k-'l).|| <= Sum(
||.w.|| rExpSeq)+ Sum(||.w.|| rExpSeq) by XREAL_1:6;
||.Partial_Sums(w ExpSeq).k .|| <= Sum(||.w.|| rExpSeq) by Th27;
then
||.Partial_Sums(w ExpSeq).k .|| + ||.Partial_Sums(w ExpSeq).(k -'l)
.|| <= Sum(||.w.|| rExpSeq) + ||.Partial_Sums(w ExpSeq).(k-'l).|| by
XREAL_1:6;
then ||.Partial_Sums(w ExpSeq).k .|| + ||.Partial_Sums(w ExpSeq).(k-'l)
.|| <= 2 * Sum(||.w.|| rExpSeq) by A13,XXREAL_0:2;
then
A14: ||.Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l).|| <= 2
* Sum(||.w.|| rExpSeq) by A12,XXREAL_0:2;
assume l <= k;
then
A15: ||.Conj(k,z,w).||.l <= (||.z.|| rExpSeq).l * ||.Partial_Sums(w
ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l).|| by A7;
0 <= (||.z.|| rExpSeq).l by Th26;
then (||.z.|| rExpSeq).l * ||.Partial_Sums(w ExpSeq).k -Partial_Sums(w
ExpSeq).(k-'l).|| <= (||.z.|| rExpSeq).l * (2 * Sum(||.w.|| rExpSeq)) by A14,
XREAL_1:64;
hence ||.Conj(k,z,w).||.l <= (||.z.|| rExpSeq).l * (2 * Sum(||.w.||
rExpSeq)) by A15,XXREAL_0:2;
end;
hence for l be Nat st l <= k holds ||.Conj(k,z,w).||.l <= (||.z
.|| rExpSeq).l * (2 * Sum(||.w.|| rExpSeq));
end;
now
A16: 0 <> Sum(||.w.|| rExpSeq) by Th28;
A17: (2 * Sum(||.w.|| rExpSeq) ) * (p/(4 * Sum(||.w.|| rExpSeq))) =(2 *
Sum(||.w.|| rExpSeq) ) * (p * (4 * Sum (||.w.|| rExpSeq))") by XCMPLX_0:def 9
.=((2 * Sum(||.w.|| rExpSeq) ) * p ) * (4 * Sum(||.w.|| rExpSeq))"
.=((2 * p ) * Sum(||.w.|| rExpSeq) ) /(4 * Sum(||.w.|| rExpSeq)) by
XCMPLX_0:def 9
.= (2 * p )/4 by A16,XCMPLX_1:91
.= p/2;
A18: 0 <> Sum(||.z.|| rExpSeq) by Th28;
A19: Sum(||.z.|| rExpSeq) * (p/(4 * Sum(||.z.|| rExpSeq))) =Sum(||.z.||
rExpSeq) * (p*(4*Sum(||.z.|| rExpSeq))") by XCMPLX_0:def 9
.=(Sum(||.z.|| rExpSeq) * p) * (4 * Sum(||.z.|| rExpSeq))"
.=(Sum(||.z.|| rExpSeq) * p)/(4 * Sum(||.z.|| rExpSeq)) by XCMPLX_0:def 9
.=p/4 by A18,XCMPLX_1:91;
let k such that
A20: n4 <= k;
A21: 0+n3 <= n3+n3 by XREAL_1:6;
then k-'n3=k-n3 by A20,XREAL_1:233,XXREAL_0:2;
then
A22: k=(k-'n3)+n3;
A23: n3 <= k by A20,A21,XXREAL_0:2;
now
let l be Nat;
assume
A24: l <= n3;
then
A25: n3+n3-n3 <= n3+n3-l by XREAL_1:10;
n4-l <= k-l by A20,XREAL_1:9;
then
A26: n3 <= k-l by A25,XXREAL_0:2;
A27: 0+n2 <= n1+n2 by XREAL_1:6;
l <= k by A23,A24,XXREAL_0:2;
then
A28: ||.Conj(k,z,w).||.l <=(||.z.|| rExpSeq).l * ||.(Partial_Sums(w
ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l)).|| by A7;
A29: 0 <= (||.z.|| rExpSeq).l by Th26;
0+n3 <= n3+n3 by XREAL_1:6;
then n2 <= n4 by A27,XXREAL_0:2;
then
A30: n2 <= k by A20,XXREAL_0:2;
k-'l=k-l by A23,A24,XREAL_1:233,XXREAL_0:2;
then n2 <= k-'l by A27,A26,XXREAL_0:2;
then
||.Partial_Sums(( w ExpSeq )).k - Partial_Sums(( w ExpSeq )).( k-'l
) .|| < p1 by A5,A30;
then (||.z.|| rExpSeq).l * ||.Partial_Sums(( w ExpSeq )).k -
Partial_Sums(( w ExpSeq )).(k-'l).|| <= (||.z.|| rExpSeq).l * p1 by A29,
XREAL_1:64;
hence ||.Conj(k,z,w).||.l <= p1 * (||.z.|| rExpSeq).l by A28,XXREAL_0:2;
end;
then
A31: Partial_Sums(||.Conj(k,z,w).||).n3 <= Partial_Sums(||.z.|| rExpSeq).
n3 * p1 by COMSEQ_3:7;
A32: n1+0 <= n1+n2 by XREAL_1:6;
then n1 <= k by A23,XXREAL_0:2;
then
|.(Partial_Sums(||.z.|| rExpSeq).k-Partial_Sums(||.z.|| rExpSeq).n3
).| <= p1 by A6,A32;
then Partial_Sums(||.z.|| rExpSeq).k-Partial_Sums(||.z.|| rExpSeq).n3 <=
p1 by A20,A21,Th29,XXREAL_0:2;
then
A33: (Partial_Sums(||.z.|| rExpSeq).k -Partial_Sums(||.z.|| rExpSeq).n3) *
(2 * Sum(||.w.|| rExpSeq)) <= p1 * (2 * Sum(||.w.|| rExpSeq)) by A2,
XREAL_1:64;
for l be Nat st l <= k holds ||.Conj(k,z,w).||.l <= (2 *
Sum(||.w.|| rExpSeq)) * (||.z.|| rExpSeq).l by A11;
then
Partial_Sums(||.Conj(k,z,w).||).(k) -Partial_Sums(||.Conj(k,z,w) .||)
. n3 <= (Partial_Sums(||.z.|| rExpSeq).(k) -Partial_Sums(||.z.|| rExpSeq).n3) *
(2 * Sum(||.w.|| rExpSeq)) by A22,COMSEQ_3:8;
then
A34: Partial_Sums(||.Conj(k,z,w).||).k-Partial_Sums(||.Conj(k,z,w).||) .n3
<= p1 * (2 * Sum(||.w.|| rExpSeq)) by A33,XXREAL_0:2;
A35: 0+p/4 < p/4 + p/4 by A1,XREAL_1:6;
Partial_Sums(||.z.|| rExpSeq).n3 * p1 <= Sum(||.z.|| rExpSeq) * p1 by A4
,Th27,XREAL_1:64;
then
A36: Partial_Sums(||.Conj(k,z,w).||).n3 <= Sum(||.z.|| rExpSeq) * p1 by A31,
XXREAL_0:2;
Sum(||.z.|| rExpSeq) * p1 <= Sum(||.z.|| rExpSeq) * (p/(4 * Sum(||.z
.|| rExpSeq))) by A3,XREAL_1:64,XXREAL_0:17;
then Partial_Sums(||.Conj(k,z,w).||).n3 <= p/4 by A36,A19,XXREAL_0:2;
then
A37: Partial_Sums(||.Conj(k,z,w).||).n3 < p/2 by A35,XXREAL_0:2;
(2 * Sum(||.w.|| rExpSeq)) * p1 <= (2 * Sum(||.w.|| rExpSeq)) * (p/(4
* Sum(||.w.|| rExpSeq))) by A2,XREAL_1:64,XXREAL_0:17;
then Partial_Sums(||.Conj(k,z,w).||).k -Partial_Sums(||.Conj(k,z,w).||).
n3 <= p/2 by A34,A17,XXREAL_0:2;
then (Partial_Sums(||.Conj(k,z,w).||).k -Partial_Sums(||.Conj(k,z,w).||).
n3) +Partial_Sums(||.Conj(k,z,w).||).n3 < (p/2)+(p/2) by A37,XREAL_1:8;
hence |.Partial_Sums(||.Conj(k,z,w).||).k.| < p by Th30;
end;
hence thesis;
end;
theorem Th32:
for seq st for k holds seq.k=Partial_Sums((Conj(k,z,w))).k holds
seq is convergent & lim(seq)=0.X
proof
deffunc U(Nat) = Partial_Sums(||.Conj($1,z,w).||).$1;
ex rseq be Real_Sequence st for k holds rseq.k = U(k) from SEQ_1:sch 1;
then consider rseq be Real_Sequence such that
A1: for k holds rseq.k=Partial_Sums(||.Conj(k,z,w).||).k;
let seq such that
A2: for k holds seq.k=Partial_Sums((Conj(k,z,w))).k;
A3: now
let k;
||.seq.k.||=||.Partial_Sums((Conj(k,z,w))).k.|| by A2;
hence ||.seq.k.|| <= Partial_Sums(||.Conj(k,z,w).||).k by Th10;
end;
A4: now
let k;
||.seq.k.|| <= Partial_Sums(||.Conj(k,z,w).||).k by A3;
hence ||.seq.k.|| <= rseq.k by A1;
end;
A5: now
let p be Real;
assume p>0;
then consider n such that
A6: for k st n <= k holds |.Partial_Sums(||.Conj(k,z,w).||).k.| < p by Th31;
take n;
now
let k such that
A7: n <= k;
|.rseq.k-0 .|=|.Partial_Sums(||.Conj(k,z,w).||).k.| by A1;
hence |.rseq.k-0 .| < p by A6,A7;
end;
hence for k st n <= k holds |.rseq.k-0 .| < p;
end;
then
A8: rseq is convergent by SEQ_2:def 6;
then lim(rseq) =0 by A5,SEQ_2:def 7;
hence thesis by A4,A8,Th12;
end;
Lm3: for z,w st z,w are_commutative holds Sum(z ExpSeq) * Sum(w ExpSeq) = Sum(
(z+w) ExpSeq)
proof
let z,w such that
A1: z,w are_commutative;
deffunc U(Nat) = Partial_Sums(Conj($1,z,w)).$1;
ex seq st for k being Element of NAT holds seq.k= U(k) from FUNCT_2:sch 4;
then consider seq be sequence of X such that
A2: for k being Element of NAT holds seq.k=Partial_Sums(Conj(k,z,w)).k;
A3: for k being Nat holds seq.k=Partial_Sums(Conj(k,z,w)).k
proof let k be Nat;
k in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
now
let k be Element of NAT;
thus seq.k=Partial_Sums(Conj(k,z,w)).k by A2
.=Partial_Sums(z ExpSeq).k * Partial_Sums(w ExpSeq).k -Partial_Sums((z
+w) ExpSeq).k by A1,Th25
.=(Partial_Sums(z ExpSeq) * Partial_Sums(w ExpSeq)).k -Partial_Sums((z
+w) ExpSeq).k by LOPBAN_3:def 7
.=(Partial_Sums(z ExpSeq) * Partial_Sums(w ExpSeq) -Partial_Sums((z+w)
ExpSeq) ).k by NORMSP_1:def 3;
end;
then
A4: seq=Partial_Sums(z ExpSeq) * Partial_Sums(w ExpSeq) -Partial_Sums((z+w)
ExpSeq) by FUNCT_2:63;
A5: Partial_Sums(w ExpSeq) is convergent by CLOPBAN3:def 1;
A6: lim(seq)=0.X by A3,Th32;
A7: Partial_Sums((z+w) ExpSeq) is convergent by CLOPBAN3:def 1;
A8: Partial_Sums(z ExpSeq) is convergent by CLOPBAN3:def 1;
then
A9: Partial_Sums(z ExpSeq) * Partial_Sums(w ExpSeq) is convergent by A5,Th3;
A10: lim(Partial_Sums(z ExpSeq) * Partial_Sums(w ExpSeq)) =lim(Partial_Sums(
z ExpSeq)) * lim(Partial_Sums(w ExpSeq)) by A8,A5,Th8;
thus Sum((z+w) ExpSeq) =lim(Partial_Sums((z+w) ExpSeq)) by CLOPBAN3:def 2
.=lim(Partial_Sums(z ExpSeq)) * lim(Partial_Sums(w ExpSeq)) by A4,A7,A9,A10
,A6,Th1
.=Sum(z ExpSeq) * lim(Partial_Sums(w ExpSeq)) by CLOPBAN3:def 2
.=Sum(z ExpSeq) * Sum(w ExpSeq) by CLOPBAN3:def 2;
end;
definition
let X;
func exp_ X -> Function of the carrier of X, the carrier of X means
:Def6:
for z being Element of X holds it.z=Sum(z ExpSeq);
existence
proof
deffunc U(Element of X ) = Sum($1 ExpSeq);
ex f being Function of the carrier of X, the carrier of X st for z be
Element of X holds f.z = U(z) from FUNCT_2:sch 4;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of the carrier of X, the carrier of X;
assume that
A1: for z be Element of X holds f1.z=Sum(z ExpSeq) and
A2: for z be Element of X holds f2.z=Sum(z ExpSeq);
for z be Element of X holds f1.z = f2.z
proof
let z be Element of X;
thus f1.z=Sum(z ExpSeq) by A1
.=f2.z by A2;
end;
hence f1=f2 by FUNCT_2:63;
end;
end;
definition
let X,z;
func exp z -> Element of X equals
(exp_ X).z;
correctness;
end;
theorem
for z holds exp(z)=Sum(z ExpSeq) by Def6;
theorem Th34:
for z1,z2 st z1,z2 are_commutative holds exp(z1+z2)=exp(z1) *exp
(z2) & exp(z2+z1)=exp(z2) *exp(z1) & exp(z1+z2)=exp(z2+z1) & exp(z1),exp(z2)
are_commutative
proof
let z1,z2 such that
A1: z1,z2 are_commutative;
A2: exp(z2+z1)=Sum((z2+z1) ExpSeq) by Def6
.=Sum(z2 ExpSeq)*Sum(z1 ExpSeq) by A1,Lm3
.=exp(z2)*Sum(z1 ExpSeq) by Def6
.=exp(z2) *exp(z1) by Def6;
exp(z1+z2)=Sum((z1+z2) ExpSeq) by Def6
.=Sum(z1 ExpSeq)*Sum(z2 ExpSeq) by A1,Lm3
.=exp(z1)*Sum(z2 ExpSeq) by Def6
.=exp(z1) *exp(z2) by Def6;
hence thesis by A2,LOPBAN_4:def 1;
end;
theorem
for z1,z2 st z1,z2 are_commutative holds z1 * exp(z2)=exp(z2) * z1
proof
let z1,z2 such that
A1: z1,z2 are_commutative;
now
let n be Element of NAT;
thus (z1*(z2 ExpSeq)).n =z1*(z2 ExpSeq).n by LOPBAN_3:def 5
.=z1*(1r/(n!)*(z2 #N n)) by Def1
.=(1r/(n!))*(z1*(z2 #N n)) by CLOPBAN3:38
.=(1r/(n!))*((z2 #N n)*z1) by A1,Lm2
.=(1r/(n!)*(z2 #N n))*z1 by CLOPBAN3:38
.=((z2 ExpSeq).n)*z1 by Def1
.=((z2 ExpSeq)*z1).n by LOPBAN_3:def 6;
end;
then
A2: z1*(z2 ExpSeq) = (z2 ExpSeq) *z1 by FUNCT_2:63;
A3: Partial_Sums( z2 ExpSeq) is convergent by CLOPBAN3:def 1;
thus z1*exp(z2) =z1*Sum(z2 ExpSeq) by Def6
.=z1*lim (Partial_Sums(z2 ExpSeq)) by CLOPBAN3:def 2
.=lim(z1*Partial_Sums(z2 ExpSeq)) by A3,Th6
.=lim(Partial_Sums(z1*(z2 ExpSeq))) by Th9
.=lim(Partial_Sums(z2 ExpSeq)*z1) by A2,Th9
.=lim(Partial_Sums(z2 ExpSeq))*z1 by A3,Th7
.=Sum(z2 ExpSeq) *z1 by CLOPBAN3:def 2
.=exp(z2) *z1 by Def6;
end;
theorem Th36:
exp(0.X) = 1.X
proof
exp(0.X) =Sum( 0.X ExpSeq) by Def6
.=1.X by Th19;
hence thesis;
end;
theorem Th37:
exp(z)*exp(-z)= 1.X & exp(-z)*exp(z)= 1.X
proof
z *(-z) =z *((-1r)*z) by CLVECT_1:3
.=(-1r)*(z*z) by CLOPBAN3:38
.=(-1r)*z*z by CLOPBAN3:38
.=(-z)*z by CLVECT_1:3;
then
A1: z,(-z) are_commutative by LOPBAN_4:def 1;
hence exp(z)*exp(-z) =exp(z+(-z)) by Th34
.=exp(0.X) by RLVECT_1:5
.=1.X by Th36;
thus exp(-z)*exp(z) =exp((-z)+z) by A1,Th34
.=exp(0.X) by RLVECT_1:5
.=1.X by Th36;
end;
theorem
exp(z) is invertible & (exp(z))" = exp(-z) & exp(-z) is invertible & (
exp(-z))" = exp(z)
proof
A1: exp(-z)*exp(z)= 1.X by Th37;
A2: exp(z)*exp(-z)= 1.X by Th37;
hence exp(z) is invertible by A1,LOPBAN_3:def 4;
hence (exp(z))" = exp(-z) by A2,A1,LOPBAN_3:def 8;
thus exp(-z) is invertible by A2,A1,LOPBAN_3:def 4;
hence thesis by A2,A1,LOPBAN_3:def 8;
end;
theorem Th39:
for z for s,t be Complex holds s*z,t*z are_commutative
proof
let z;
let s,t be Complex;
(s*z) *(t*z) =(s*t)*(z*z) by CLOPBAN3:38
.=(t*z)*(s*z) by CLOPBAN3:38;
hence thesis by LOPBAN_4:def 1;
end;
theorem
for z for s,t be Complex holds exp(s*z)*exp(t*z) = exp((s+t)*z) & exp(
t*z)*exp(s*z) = exp((t+s)*z) & exp((s+t)*z) = exp((t+s)*z) & exp(s*z),exp(t*z)
are_commutative
proof
let z;
let s,t be Complex;
A1: s*z,t*z are_commutative by Th39;
hence
A2: exp(s*z)*exp(t*z) = exp(s*z+t*z) by Th34
.= exp((s+t)*z) by CLOPBAN3:38;
thus
A3: exp(t*z)*exp(s*z) = exp(t*z+s*z) by A1,Th34
.= exp((t+s)*z) by CLOPBAN3:38;
thus exp((s+t)*z) = exp((t+s)*z);
thus thesis by A2,A3,LOPBAN_4:def 1;
end;