:: by Yasunari Shidama

::

:: Received February 13, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

definition

let X be non empty multMagma ;

let x, y be Element of X;

reflexivity

for x being Element of X holds x * x = x * x ;

symmetry

for x, y being Element of X st x * y = y * x holds

y * x = x * y ;

end;
let x, y be Element of X;

reflexivity

for x being Element of X holds x * x = x * x ;

symmetry

for x, y being Element of X st x * y = y * x holds

y * x = x * y ;

:: deftheorem defines are_commutative LOPBAN_4:def 1 :

for X being non empty multMagma

for x, y being Element of X holds

( x,y are_commutative iff x * y = y * x );

for X being non empty multMagma

for x, y being Element of X holds

( x,y are_commutative iff x * y = y * x );

Lm1: for X being Banach_Algebra

for z being Element of X

for n being Nat holds

( 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 end;

Lm2: for X being Banach_Algebra

for n being Nat

for z, w being Element of X st z,w are_commutative holds

( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z )

proof end;

theorem Th1: :: LOPBAN_4:1

for X being Banach_Algebra

for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X holds

lim seq1 = lim seq2

for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X holds

lim seq1 = lim seq2

proof end;

theorem Th2: :: LOPBAN_4:2

for X being Banach_Algebra

for s being sequence of X

for z being Element of X st ( for n being Nat holds s . n = z ) holds

lim s = z

for s being sequence of X

for z being Element of X st ( for n being Nat holds s . n = z ) holds

lim s = z

proof end;

theorem Th3: :: LOPBAN_4:3

for X being Banach_Algebra

for s, s9 being sequence of X st s is convergent & s9 is convergent holds

s * s9 is convergent

for s, s9 being sequence of X st s is convergent & s9 is convergent holds

s * s9 is convergent

proof end;

theorem Th4: :: LOPBAN_4:4

for X being Banach_Algebra

for z being Element of X

for s being sequence of X st s is convergent holds

z * s is convergent

for z being Element of X

for s being sequence of X st s is convergent holds

z * s is convergent

proof end;

theorem Th5: :: LOPBAN_4:5

for X being Banach_Algebra

for z being Element of X

for s being sequence of X st s is convergent holds

s * z is convergent

for z being Element of X

for s being sequence of X st s is convergent holds

s * z is convergent

proof end;

theorem Th6: :: LOPBAN_4:6

for X being Banach_Algebra

for z being Element of X

for s being sequence of X st s is convergent holds

lim (z * s) = z * (lim s)

for z being Element of X

for s being sequence of X st s is convergent holds

lim (z * s) = z * (lim s)

proof end;

theorem Th7: :: LOPBAN_4:7

for X being Banach_Algebra

for z being Element of X

for s being sequence of X st s is convergent holds

lim (s * z) = (lim s) * z

for z being Element of X

for s being sequence of X st s is convergent holds

lim (s * z) = (lim s) * z

proof end;

theorem Th8: :: LOPBAN_4:8

for X being Banach_Algebra

for s, s9 being sequence of X st s is convergent & s9 is convergent holds

lim (s * s9) = (lim s) * (lim s9)

for s, s9 being sequence of X st s is convergent & s9 is convergent holds

lim (s * s9) = (lim s) * (lim s9)

proof end;

theorem Th9: :: LOPBAN_4:9

for X being Banach_Algebra

for z being Element of X

for seq being sequence of X holds

( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z )

for z being Element of X

for seq being sequence of X holds

( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z )

proof end;

theorem Th10: :: LOPBAN_4:10

for X being Banach_Algebra

for k being Nat

for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

for k being Nat

for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

proof end;

theorem Th11: :: LOPBAN_4:11

for X being Banach_Algebra

for m being Nat

for seq1, seq2 being sequence of X st ( for n being Nat st n <= m holds

seq1 . n = seq2 . n ) holds

(Partial_Sums seq1) . m = (Partial_Sums seq2) . m

for m being Nat

for seq1, seq2 being sequence of X st ( for n being Nat st n <= m holds

seq1 . n = seq2 . n ) holds

(Partial_Sums seq1) . m = (Partial_Sums seq2) . m

proof end;

theorem Th12: :: LOPBAN_4:12

for X being Banach_Algebra

for seq being sequence of X

for rseq being Real_Sequence st ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds

( seq is convergent & lim seq = 0. X )

for seq being sequence of X

for rseq being Real_Sequence st ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds

( seq is convergent & lim seq = 0. X )

proof end;

definition

let X be Banach_Algebra;

let z be Element of X;

ex b_{1} being sequence of X st

for n being Nat holds b_{1} . n = (1 / (n !)) * (z #N n)

for b_{1}, b_{2} being sequence of X st ( for n being Nat holds b_{1} . n = (1 / (n !)) * (z #N n) ) & ( for n being Nat holds b_{2} . n = (1 / (n !)) * (z #N n) ) holds

b_{1} = b_{2}

end;
let z be Element of X;

func z rExpSeq -> sequence of X means :Def2: :: LOPBAN_4:def 2

for n being Nat holds it . n = (1 / (n !)) * (z #N n);

existence for n being Nat holds it . n = (1 / (n !)) * (z #N n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines rExpSeq LOPBAN_4:def 2 :

for X being Banach_Algebra

for z being Element of X

for b_{3} being sequence of X holds

( b_{3} = z rExpSeq iff for n being Nat holds b_{3} . n = (1 / (n !)) * (z #N n) );

for X being Banach_Algebra

for z being Element of X

for b

( b

theorem Th13: :: LOPBAN_4:13

( ( for k being Nat st 0 < k holds

((k -' 1) !) * k = k ! ) & ( for m, k being Nat st k <= m holds

((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )

((k -' 1) !) * k = k ! ) & ( for m, k being Nat st k <= m holds

((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )

proof end;

definition

let n be Nat;

ex b_{1} being Real_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Real_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
func Coef n -> Real_Sequence means :Def3: :: LOPBAN_4:def 3

for k being Nat holds

( ( k <= n implies it . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );

existence for k being Nat holds

( ( k <= n implies it . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def3 defines Coef LOPBAN_4:def 3 :

for n being Nat

for b_{2} being Real_Sequence holds

( b_{2} = Coef n iff for k being Nat holds

( ( k <= n implies b_{2} . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{2} . k = 0 ) ) );

for n being Nat

for b

( b

( ( k <= n implies b

definition

let n be Nat;

ex b_{1} being Real_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Real_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
func Coef_e n -> Real_Sequence means :Def4: :: LOPBAN_4:def 4

for k being Nat holds

( ( k <= n implies it . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );

existence for k being Nat holds

( ( k <= n implies it . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def4 defines Coef_e LOPBAN_4:def 4 :

for n being Nat

for b_{2} being Real_Sequence holds

( b_{2} = Coef_e n iff for k being Nat holds

( ( k <= n implies b_{2} . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{2} . k = 0 ) ) );

for n being Nat

for b

( b

( ( k <= n implies b

definition

let X be non empty ZeroStr ;

let seq be sequence of X;

ex b_{1} being sequence of X st

( b_{1} . 0 = 0. X & ( for k being Nat holds b_{1} . (k + 1) = seq . k ) )

for b_{1}, b_{2} being sequence of X st b_{1} . 0 = 0. X & ( for k being Nat holds b_{1} . (k + 1) = seq . k ) & b_{2} . 0 = 0. X & ( for k being Nat holds b_{2} . (k + 1) = seq . k ) holds

b_{1} = b_{2}

end;
let seq be sequence of X;

func Shift seq -> sequence of X means :Def5: :: LOPBAN_4:def 5

( it . 0 = 0. X & ( for k being Nat holds it . (k + 1) = seq . k ) );

existence ( it . 0 = 0. X & ( for k being Nat holds it . (k + 1) = seq . k ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines Shift LOPBAN_4:def 5 :

for X being non empty ZeroStr

for seq, b_{3} being sequence of X holds

( b_{3} = Shift seq iff ( b_{3} . 0 = 0. X & ( for k being Nat holds b_{3} . (k + 1) = seq . k ) ) );

for X being non empty ZeroStr

for seq, b

( b

definition

let n be Nat;

let X be Banach_Algebra;

let z, w be Element of X;

ex b_{1} being sequence of X st

for k being Nat holds

( ( k <= n implies b_{1} . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b_{1} . k = 0. X ) )

for b_{1}, b_{2} being sequence of X st ( for k being Nat holds

( ( k <= n implies b_{1} . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b_{1} . k = 0. X ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b_{2} . k = 0. X ) ) ) holds

b_{1} = b_{2}

end;
let X be Banach_Algebra;

let z, w be Element of X;

func Expan (n,z,w) -> sequence of X means :Def6: :: LOPBAN_4:def 6

for k being 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 for k being Nat holds

( ( k <= n implies it . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies it . k = 0. X ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def6 defines Expan LOPBAN_4:def 6 :

for n being Nat

for X being Banach_Algebra

for z, w being Element of X

for b_{5} being sequence of X holds

( b_{5} = Expan (n,z,w) iff for k being Nat holds

( ( k <= n implies b_{5} . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b_{5} . k = 0. X ) ) );

for n being Nat

for X being Banach_Algebra

for z, w being Element of X

for b

( b

( ( k <= n implies b

definition

let n be Nat;

let X be Banach_Algebra;

let z, w be Element of X;

ex b_{1} being sequence of X st

for k being Nat holds

( ( k <= n implies b_{1} . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b_{1} . k = 0. X ) )

for b_{1}, b_{2} being sequence of X st ( for k being Nat holds

( ( k <= n implies b_{1} . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b_{1} . k = 0. X ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b_{2} . k = 0. X ) ) ) holds

b_{1} = b_{2}

end;
let X be Banach_Algebra;

let z, w be Element of X;

func Expan_e (n,z,w) -> sequence of X means :Def7: :: LOPBAN_4:def 7

for k being 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 for k being 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 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def7 defines Expan_e LOPBAN_4:def 7 :

for n being Nat

for X being Banach_Algebra

for z, w being Element of X

for b_{5} being sequence of X holds

( b_{5} = Expan_e (n,z,w) iff for k being Nat holds

( ( k <= n implies b_{5} . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b_{5} . k = 0. X ) ) );

for n being Nat

for X being Banach_Algebra

for z, w being Element of X

for b

( b

( ( k <= n implies b

definition

let n be Nat;

let X be Banach_Algebra;

let z, w be Element of X;

ex b_{1} being sequence of X st

for k being Nat holds

( ( k <= n implies b_{1} . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b_{1} . k = 0. X ) )

for b_{1}, b_{2} being sequence of X st ( for k being Nat holds

( ( k <= n implies b_{1} . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b_{1} . k = 0. X ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b_{2} . k = 0. X ) ) ) holds

b_{1} = b_{2}

end;
let X be Banach_Algebra;

let z, w be Element of X;

func Alfa (n,z,w) -> sequence of X means :Def8: :: LOPBAN_4:def 8

for k being Nat holds

( ( k <= n implies it . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies it . k = 0. X ) );

existence for k being Nat holds

( ( k <= n implies it . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies it . k = 0. X ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def8 defines Alfa LOPBAN_4:def 8 :

for n being Nat

for X being Banach_Algebra

for z, w being Element of X

for b_{5} being sequence of X holds

( b_{5} = Alfa (n,z,w) iff for k being Nat holds

( ( k <= n implies b_{5} . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b_{5} . k = 0. X ) ) );

for n being Nat

for X being Banach_Algebra

for z, w being Element of X

for b

( b

( ( k <= n implies b

definition

let X be Banach_Algebra;

let z, w be Element of X;

let n be Nat;

ex b_{1} being sequence of X st

for k being Nat holds

( ( k <= n implies b_{1} . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b_{1} . k = 0. X ) )

for b_{1}, b_{2} being sequence of X st ( for k being Nat holds

( ( k <= n implies b_{1} . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b_{1} . k = 0. X ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b_{2} . k = 0. X ) ) ) holds

b_{1} = b_{2}

end;
let z, w be Element of X;

let n be Nat;

func Conj (n,z,w) -> sequence of X means :Def9: :: LOPBAN_4:def 9

for k being 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 for k being 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 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def9 defines Conj LOPBAN_4:def 9 :

for X being Banach_Algebra

for z, w being Element of X

for n being Nat

for b_{5} being sequence of X holds

( b_{5} = Conj (n,z,w) iff for k being Nat holds

( ( k <= n implies b_{5} . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b_{5} . k = 0. X ) ) );

for X being Banach_Algebra

for z, w being Element of X

for n being Nat

for b

( b

( ( k <= n implies b

theorem Th14: :: LOPBAN_4:14

for X being Banach_Algebra

for z being Element of X

for n being Nat holds

( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )

for z being Element of X

for n being Nat holds

( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )

proof end;

theorem Th15: :: LOPBAN_4:15

for k being Nat

for X being non empty ZeroStr

for seq being sequence of X st 0 < k holds

(Shift seq) . k = seq . (k -' 1)

for X being non empty ZeroStr

for seq being sequence of X st 0 < k holds

(Shift seq) . k = seq . (k -' 1)

proof end;

theorem Th16: :: LOPBAN_4:16

for X being Banach_Algebra

for k being Nat

for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)

for k being Nat

for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)

proof end;

theorem Th17: :: LOPBAN_4:17

for X being Banach_Algebra

for n being Nat

for z, w being Element of X st z,w are_commutative holds

(z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n

for n being Nat

for z, w being Element of X st z,w are_commutative holds

(z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n

proof end;

theorem Th18: :: LOPBAN_4:18

for X being Banach_Algebra

for w, z being Element of X

for n being Nat holds Expan_e (n,z,w) = (1 / (n !)) * (Expan (n,z,w))

for w, z being Element of X

for n being Nat holds Expan_e (n,z,w) = (1 / (n !)) * (Expan (n,z,w))

proof end;

theorem Th19: :: LOPBAN_4:19

for X being Banach_Algebra

for n being Nat

for z, w being Element of X st z,w are_commutative holds

(1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n

for n being Nat

for z, w being Element of X st z,w are_commutative holds

(1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n

proof end;

registration
end;

theorem Th21: :: LOPBAN_4:21

for X being Banach_Algebra

for w, z being Element of X holds

( (z rExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X )

for w, z being Element of X holds

( (z rExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X )

proof end;

theorem Th22: :: LOPBAN_4:22

for X being Banach_Algebra

for w, z being Element of X

for k, l being Nat st l <= k holds

(Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l)

for w, z being Element of X

for k, l being Nat st l <= k holds

(Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l)

proof end;

theorem Th23: :: LOPBAN_4:23

for X being Banach_Algebra

for w, z being Element of X

for k being Nat holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k)

for w, z being Element of X

for k being Nat holds (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 end;

theorem Th24: :: LOPBAN_4:24

for X being Banach_Algebra

for w, z being Element of X

for k being Nat holds (z rExpSeq) . k = (Expan_e (k,z,w)) . k

for w, z being Element of X

for k being Nat holds (z rExpSeq) . k = (Expan_e (k,z,w)) . k

proof end;

theorem Th25: :: LOPBAN_4:25

for X being Banach_Algebra

for n being Nat

for z, w being Element of X st z,w are_commutative holds

(Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n

for n being Nat

for z, w being Element of X st z,w are_commutative holds

(Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n

proof end;

theorem Th26: :: LOPBAN_4:26

for X being Banach_Algebra

for k being Nat

for z, w being Element of X 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

for k being Nat

for z, w being Element of X 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 end;

theorem Th27: :: LOPBAN_4:27

for X being Banach_Algebra

for z being Element of X

for n being Nat holds 0 <= (||.z.|| rExpSeq) . n

for z being Element of X

for n being Nat holds 0 <= (||.z.|| rExpSeq) . n

proof end;

theorem Th28: :: LOPBAN_4:28

for X being Banach_Algebra

for z being Element of X

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) )

for z being Element of X

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 end;

theorem Th30: :: LOPBAN_4:30

for X being Banach_Algebra

for z being Element of X

for m, n being Nat holds

( |.((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) ) )

for z being Element of X

for m, n being Nat holds

( |.((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 end;

theorem Th31: :: LOPBAN_4:31

for X being Banach_Algebra

for w, z being Element of X

for k, n being Nat holds |.((Partial_Sums ||.(Conj (k,z,w)).||) . n).| = (Partial_Sums ||.(Conj (k,z,w)).||) . n

for w, z being Element of X

for k, n being Nat holds |.((Partial_Sums ||.(Conj (k,z,w)).||) . n).| = (Partial_Sums ||.(Conj (k,z,w)).||) . n

proof end;

theorem Th32: :: LOPBAN_4:32

for X being Banach_Algebra

for w, z being Element of X

for p being Real st p > 0 holds

ex n being Nat st

for k being Nat st n <= k holds

|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p

for w, z being Element of X

for p being Real st p > 0 holds

ex n being Nat st

for k being Nat st n <= k holds

|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p

proof end;

theorem Th33: :: LOPBAN_4:33

for X being Banach_Algebra

for w, z being Element of X

for seq being sequence of X st ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds

( seq is convergent & lim seq = 0. X )

for w, z being Element of X

for seq being sequence of X st ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds

( seq is convergent & lim seq = 0. X )

proof end;

Lm3: for X being Banach_Algebra

for z, w being Element of X st z,w are_commutative holds

(Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq)

proof end;

definition

let X be Banach_Algebra;

ex b_{1} being Function of the carrier of X, the carrier of X st

for z being Element of X holds b_{1} . z = Sum (z rExpSeq)

for b_{1}, b_{2} being Function of the carrier of X, the carrier of X st ( for z being Element of X holds b_{1} . z = Sum (z rExpSeq) ) & ( for z being Element of X holds b_{2} . z = Sum (z rExpSeq) ) holds

b_{1} = b_{2}

end;
func exp_ X -> Function of the carrier of X, the carrier of X means :Def10: :: LOPBAN_4:def 10

for z being Element of X holds it . z = Sum (z rExpSeq);

existence for z being Element of X holds it . z = Sum (z rExpSeq);

ex b

for z being Element of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines exp_ LOPBAN_4:def 10 :

for X being Banach_Algebra

for b_{2} being Function of the carrier of X, the carrier of X holds

( b_{2} = exp_ X iff for z being Element of X holds b_{2} . z = Sum (z rExpSeq) );

for X being Banach_Algebra

for b

( b

definition
end;

:: deftheorem defines exp LOPBAN_4:def 11 :

for X being Banach_Algebra

for z being Element of X holds exp z = (exp_ X) . z;

for X being Banach_Algebra

for z being Element of X holds exp z = (exp_ X) . z;

theorem :: LOPBAN_4:34

theorem Th35: :: LOPBAN_4:35

for X being Banach_Algebra

for z1, z2 being Element of X 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 )

for z1, z2 being Element of X 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 end;

theorem :: LOPBAN_4:36

for X being Banach_Algebra

for z1, z2 being Element of X st z1,z2 are_commutative holds

z1 * (exp z2) = (exp z2) * z1

for z1, z2 being Element of X st z1,z2 are_commutative holds

z1 * (exp z2) = (exp z2) * z1

proof end;

theorem Th38: :: LOPBAN_4:38

for X being Banach_Algebra

for z being Element of X holds

( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X )

for z being Element of X holds

( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X )

proof end;

theorem :: LOPBAN_4:39

for X being Banach_Algebra

for z being Element of X holds

( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z )

for z being Element of X holds

( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z )

proof end;

theorem Th40: :: LOPBAN_4:40

for X being Banach_Algebra

for z being Element of X

for s, t being Real holds s * z,t * z are_commutative

for z being Element of X

for s, t being Real holds s * z,t * z are_commutative

proof end;

theorem :: LOPBAN_4:41

for X being Banach_Algebra

for z being Element of X

for s, t being 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 )

for z being Element of X

for s, t being 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 end;