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