:: Exponential Function on Complex {B}anach Algebra :: by Noboru Endou :: :: Received April 6, 2004 :: Copyright (c) 2004-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, 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
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*)) by XCMPLX_1:91
.=(n! * (n+1-k))/((k!) * (((n-'k)!) * (n+1-k+0*)))
.=(n! * (n+1-k))/((k!) * ((n+1-'k)!)) by A10,SIN_COS:2;
assume
A13: k<>0;
then
A14: 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;