:: CLOPBAN4 semantic presentation

definition

let c₁ be non empty Normed_Complex_AlgebraStr ;
let c₂, c₃ be Element of c₁;
pred c₂,c₃ are_commutative means :Def1: :: CLOPBAN4:def 1
a₂ * a₃ = a₃ * a₂;
symmetry ;

end;

:: deftheorem Def1 defines are_commutative CLOPBAN4:def 1 :

Lemma2: for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being Nat holds
( b₂ * (b₂ #N b₃) = b₂ #N (b₃ + 1) & (b₂ #N b₃) * b₂ = b₂ #N (b₃ + 1) & b₂ * (b₂ #N b₃) = (b₂ #N b₃) * b₂ )

proof end;

Lemma3: for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃, b₄ being Element of b₁ st b₃,b₄ are_commutative holds
( b₄ * (b₃ #N b₂) = (b₃ #N b₂) * b₄ & b₃ * (b₄ #N b₂) = (b₄ #N b₂) * b₃ )

proof end;

theorem Th1: :: CLOPBAN4:1

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent & lim (b₂ - b₃) = 0. b₁ holds
lim b₂ = lim b₃

proof end;

theorem Th2: :: CLOPBAN4:2

for b₁ being Complex_Banach_Algebra
for b₂ being sequence of b₁
for b₃ being Element of b₁ st ( for b₄ being Nat holds b₂ . b₄ = b₃ ) holds
lim b₂ = b₃

proof end;

theorem Th3: :: CLOPBAN4:3

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ * b₃ is convergent

proof end;

theorem Th4: :: CLOPBAN4:4

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
b₂ * b₃ is convergent

proof end;

theorem Th5: :: CLOPBAN4:5

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
b₃ * b₂ is convergent

proof end;

theorem Th6: :: CLOPBAN4:6

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₂ * b₃) = b₂ * (lim b₃)

proof end;

theorem Th7: :: CLOPBAN4:7

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₃ * b₂) = (lim b₃) * b₂

proof end;

theorem Th8: :: CLOPBAN4:8

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ * b₃) = (lim b₂) * (lim b₃)

proof end;

theorem Th9: :: CLOPBAN4:9

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being sequence of b₁ holds
( Partial_Sums (b₂ * b₃) = b₂ * (Partial_Sums b₃) & Partial_Sums (b₃ * b₂) = (Partial_Sums b₃) * b₂ )

proof end;

theorem Th10: :: CLOPBAN4:10

for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃ being sequence of b₁ holds ||.((Partial_Sums b₃) . b₂).|| <= (Partial_Sums ||.b₃.||) . b₂

proof end;

theorem Th11: :: CLOPBAN4:11

for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃, b₄ being sequence of b₁ st ( for b₅ being Nat st b₅ <= b₂ holds
b₃ . b₅ = b₄ . b₅ ) holds
(Partial_Sums b₃) . b₂ = (Partial_Sums b₄) . b₂

proof end;

theorem Th12: :: CLOPBAN4:12

for b₁ being Complex_Banach_Algebra
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds ||.(b₂ . b₄).|| <= b₃ . b₄ ) & b₃ is convergent & lim b₃ = 0 holds
( b₂ is convergent & lim b₂ = 0. b₁ )

proof end;

definition

let c₁ be Complex_Banach_Algebra;
let c₂ be Element of c₁;
func c₂ ExpSeq -> sequence of a₁ means :Def2: :: CLOPBAN4:def 2
for b₁ being Nat holds a₃ . b₁ = (1r / (b₁ !c )) * (a₂ #N b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ExpSeq CLOPBAN4:def 2 :

scheme :: CLOPBAN4:sch 1
s1{ F₁() -> non empty Complex_Banach_Algebra, F₂( Nat, Nat) -> Point of F₁() } :

for b₁ being Nat ex b₂ being sequence of F₁() st
for b₃ being Nat holds
( ( b₃ <= b₁ implies b₂ . b₃ = F₂(b₁,b₃) ) & ( b₃ > b₁ implies b₂ . b₃ = 0. F₁() ) )

proof end;

definition

let c₁ be Complex_Banach_Algebra;
let c₂ be sequence of c₁;
func Sift c₂ -> sequence of a₁ means :Def3: :: CLOPBAN4:def 3
( a₃ . 0 = 0. a₁ & ( for b₁ being Nat holds a₃ . (b₁ + 1) = a₂ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Sift CLOPBAN4:def 3 :

definition

let c₁ be Nat;
let c₂ be Complex_Banach_Algebra;
let c₃, c₄ be Element of c₂;
func Expan c₁,c₃,c₄ -> sequence of a₂ means :Def4: :: CLOPBAN4:def 4
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₅ . b₁ = (((Coef a₁) . b₁) * (a₃ #N b₁)) * (a₄ #N (a₁ -' b₁)) ) & ( a₁ < b₁ implies a₅ . b₁ = 0. a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Expan CLOPBAN4:def 4 :

definition

let c₁ be Nat;
let c₂ be Complex_Banach_Algebra;
let c₃, c₄ be Element of c₂;
func Expan_e c₁,c₃,c₄ -> sequence of a₂ means :Def5: :: CLOPBAN4:def 5
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₅ . b₁ = (((Coef_e a₁) . b₁) * (a₃ #N b₁)) * (a₄ #N (a₁ -' b₁)) ) & ( a₁ < b₁ implies a₅ . b₁ = 0. a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Expan_e CLOPBAN4:def 5 :

definition

let c₁ be Nat;
let c₂ be Complex_Banach_Algebra;
let c₃, c₄ be Element of c₂;
func Alfa c₁,c₃,c₄ -> sequence of a₂ means :Def6: :: CLOPBAN4:def 6
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₅ . b₁ = ((a₃ ExpSeq ) . b₁) * ((Partial_Sums (a₄ ExpSeq )) . (a₁ -' b₁)) ) & ( a₁ < b₁ implies a₅ . b₁ = 0. a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Alfa CLOPBAN4:def 6 :

definition

let c₁ be Complex_Banach_Algebra;
let c₂, c₃ be Element of c₁;
let c₄ be Nat;
func Conj c₄,c₂,c₃ -> sequence of a₁ means :Def7: :: CLOPBAN4:def 7
for b₁ being Nat holds
( ( b₁ <= a₄ implies a₅ . b₁ = ((a₂ ExpSeq ) . b₁) * (((Partial_Sums (a₃ ExpSeq )) . a₄) - ((Partial_Sums (a₃ ExpSeq )) . (a₄ -' b₁))) ) & ( a₄ < b₁ implies a₅ . b₁ = 0. a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Conj CLOPBAN4:def 7 :

theorem Th13: :: CLOPBAN4:13

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being Nat holds
( (b₂ ExpSeq ) . (b₃ + 1) = ((1r / [*(b₃ + 1),0*]) * b₂) * ((b₂ ExpSeq ) . b₃) & (b₂ ExpSeq ) . 0 = 1. b₁ & ||.((b₂ ExpSeq ) . b₃).|| <= (||.b₂.|| ExpSeq ) . b₃ )

proof end;

theorem Th14: :: CLOPBAN4:14

for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃ being sequence of b₁ st 0 < b₂ holds
(Sift b₃) . b₂ = b₃ . (b₂ -' 1)

proof end;

theorem Th15: :: CLOPBAN4:15

for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃ being sequence of b₁ holds (Partial_Sums b₃) . b₂ = ((Partial_Sums (Sift b₃)) . b₂) + (b₃ . b₂)

proof end;

theorem Th16: :: CLOPBAN4:16

for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃, b₄ being Element of b₁ st b₃,b₄ are_commutative holds
(b₃ + b₄) #N b₂ = (Partial_Sums (Expan b₂,b₃,b₄)) . b₂

proof end;

theorem Th17: :: CLOPBAN4:17

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁
for b₄ being Nat holds Expan_e b₄,b₂,b₃ = (1r / (b₄ !c )) * (Expan b₄,b₂,b₃)

proof end;

theorem Th18: :: CLOPBAN4:18

for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃, b₄ being Element of b₁ st b₃,b₄ are_commutative holds
(1r / (b₂ !c )) * ((b₃ + b₄) #N b₂) = (Partial_Sums (Expan_e b₂,b₃,b₄)) . b₂

proof end;

theorem Th19: :: CLOPBAN4:19

for b₁ being Complex_Banach_Algebra holds
( (0. b₁) ExpSeq is norm_summable & Sum ((0. b₁) ExpSeq ) = 1. b₁ )

proof end;

registration

let c₁ be Complex_Banach_Algebra;
let c₂ be Element of c₁;
cluster a₂ ExpSeq -> norm_summable ;
coherence

proof end;

end;

theorem Th20: :: CLOPBAN4:20

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁ holds
( (b₂ ExpSeq ) . 0 = 1. b₁ & (Expan 0,b₂,b₃) . 0 = 1. b₁ )

proof end;

theorem Th21: :: CLOPBAN4:21

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁
for b₄, b₅ being Nat st b₄ <= b₅ holds
(Alfa (b₅ + 1),b₂,b₃) . b₄ = ((Alfa b₅,b₂,b₃) . b₄) + ((Expan_e (b₅ + 1),b₂,b₃) . b₄)

proof end;

theorem Th22: :: CLOPBAN4:22

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (Partial_Sums (Alfa (b₄ + 1),b₂,b₃)) . b₄ = ((Partial_Sums (Alfa b₄,b₂,b₃)) . b₄) + ((Partial_Sums (Expan_e (b₄ + 1),b₂,b₃)) . b₄)

proof end;

theorem Th23: :: CLOPBAN4:23

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (b₂ ExpSeq ) . b₄ = (Expan_e b₄,b₂,b₃) . b₄

proof end;

theorem Th24: :: CLOPBAN4:24

for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃, b₄ being Element of b₁ st b₃,b₄ are_commutative holds
(Partial_Sums ((b₃ + b₄) ExpSeq )) . b₂ = (Partial_Sums (Alfa b₂,b₃,b₄)) . b₂

proof end;

theorem Th25: :: CLOPBAN4:25

for b₁ being Complex_Banach_Algebra
for b₂ being Nat
for b₃, b₄ being Element of b₁ st b₃,b₄ are_commutative holds
(((Partial_Sums (b₃ ExpSeq )) . b₂) * ((Partial_Sums (b₄ ExpSeq )) . b₂)) - ((Partial_Sums ((b₃ + b₄) ExpSeq )) . b₂) = (Partial_Sums (Conj b₂,b₃,b₄)) . b₂

proof end;

theorem Th26: :: CLOPBAN4:26

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being Nat holds 0 <= (||.b₂.|| ExpSeq ) . b₃

proof end;

theorem Th27: :: CLOPBAN4:27

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃ being Nat holds
( ||.((Partial_Sums (b₂ ExpSeq )) . b₃).|| <= (Partial_Sums (||.b₂.|| ExpSeq )) . b₃ & (Partial_Sums (||.b₂.|| ExpSeq )) . b₃ <= Sum (||.b₂.|| ExpSeq ) & ||.((Partial_Sums (b₂ ExpSeq )) . b₃).|| <= Sum (||.b₂.|| ExpSeq ) )

proof end;

theorem Th28: :: CLOPBAN4:28

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁ holds 1 <= Sum (||.b₂.|| ExpSeq )

proof end;

theorem Th29: :: CLOPBAN4:29

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃, b₄ being Nat holds
( abs ((Partial_Sums (||.b₂.|| ExpSeq )) . b₃) = (Partial_Sums (||.b₂.|| ExpSeq )) . b₃ & ( b₃ <= b₄ implies abs (((Partial_Sums (||.b₂.|| ExpSeq )) . b₄) - ((Partial_Sums (||.b₂.|| ExpSeq )) . b₃)) = ((Partial_Sums (||.b₂.|| ExpSeq )) . b₄) - ((Partial_Sums (||.b₂.|| ExpSeq )) . b₃) ) )

proof end;

theorem Th30: :: CLOPBAN4:30

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁
for b₄, b₅ being Nat holds abs ((Partial_Sums ||.(Conj b₄,b₂,b₃).||) . b₅) = (Partial_Sums ||.(Conj b₄,b₂,b₃).||) . b₅

proof end;

theorem Th31: :: CLOPBAN4:31

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁
for b₄ being real number st b₄ > 0 holds
ex b₅ being Nat st
for b₆ being Nat st b₅ <= b₆ holds
abs ((Partial_Sums ||.(Conj b₆,b₂,b₃).||) . b₆) < b₄

proof end;

theorem Th32: :: CLOPBAN4:32

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁
for b₄ being sequence of b₁ st ( for b₅ being Nat holds b₄ . b₅ = (Partial_Sums (Conj b₅,b₂,b₃)) . b₅ ) holds
( b₄ is convergent & lim b₄ = 0. b₁ )

proof end;

Lemma42: for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁ st b₂,b₃ are_commutative holds
(Sum (b₂ ExpSeq )) * (Sum (b₃ ExpSeq )) = Sum ((b₂ + b₃) ExpSeq )

proof end;

definition

let c₁ be Complex_Banach_Algebra;
func exp_ c₁ -> Function of the carrier of a₁,the carrier of a₁ means :Def8: :: CLOPBAN4:def 8
for b₁ being Element of a₁ holds a₂ . b₁ = Sum (b₁ ExpSeq );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines exp_ CLOPBAN4:def 8 :

definition

let c₁ be Complex_Banach_Algebra;
let c₂ be Element of c₁;
func exp c₂ -> Element of a₁ equals :: CLOPBAN4:def 9
(exp_ a₁) . a₂;
correctness ;

end;

:: deftheorem Def9 defines exp CLOPBAN4:def 9 :

theorem Th33: :: CLOPBAN4:33

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁ holds exp b₂ = Sum (b₂ ExpSeq ) by Def8;

theorem Th34: :: CLOPBAN4:34

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁ st b₂,b₃ are_commutative holds
( exp (b₂ + b₃) = (exp b₂) * (exp b₃) & exp (b₃ + b₂) = (exp b₃) * (exp b₂) & exp (b₂ + b₃) = exp (b₃ + b₂) & exp b₂, exp b₃ are_commutative )

proof end;

theorem Th35: :: CLOPBAN4:35

for b₁ being Complex_Banach_Algebra
for b₂, b₃ being Element of b₁ st b₂,b₃ are_commutative holds
b₂ * (exp b₃) = (exp b₃) * b₂

proof end;

theorem Th36: :: CLOPBAN4:36

for b₁ being Complex_Banach_Algebra holds exp (0. b₁) = 1. b₁

proof end;

theorem Th37: :: CLOPBAN4:37

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁ holds
( (exp b₂) * (exp (- b₂)) = 1. b₁ & (exp (- b₂)) * (exp b₂) = 1. b₁ )

proof end;

theorem Th38: :: CLOPBAN4:38

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁ holds
( exp b₂ is invertible & (exp b₂) " = exp (- b₂) & exp (- b₂) is invertible & (exp (- b₂)) " = exp b₂ )

proof end;

theorem Th39: :: CLOPBAN4:39

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃, b₄ being Complex holds b₃ * b₂,b₄ * b₂ are_commutative

proof end;

theorem Th40: :: CLOPBAN4:40

for b₁ being Complex_Banach_Algebra
for b₂ being Element of b₁
for b₃, b₄ being Complex holds
( (exp (b₃ * b₂)) * (exp (b₄ * b₂)) = exp ((b₃ + b₄) * b₂) & (exp (b₄ * b₂)) * (exp (b₃ * b₂)) = exp ((b₄ + b₃) * b₂) & exp ((b₃ + b₄) * b₂) = exp ((b₄ + b₃) * b₂) & exp (b₃ * b₂), exp (b₄ * b₂) are_commutative )

proof end;