:: The Exponential Function on {B}anach Algebra :: by Yasunari Shidama :: :: Received February 13, 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, 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
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 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;