:: LOPBAN_4 semantic presentation

definition

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

end;

:: deftheorem Def1 defines are_commutative LOPBAN_4:def 1 :

Lemma2: for b₁ being 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 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: :: LOPBAN_4:1

for b₁ being 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: :: LOPBAN_4:2

for b₁ being 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: :: LOPBAN_4:3

for b₁ being 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: :: LOPBAN_4:4

for b₁ being 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: :: LOPBAN_4:5

for b₁ being 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: :: LOPBAN_4:6

for b₁ being 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: :: LOPBAN_4:7

for b₁ being 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: :: LOPBAN_4:8

for b₁ being 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: :: LOPBAN_4:9

for b₁ being 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: :: LOPBAN_4:10

for b₁ being 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: :: LOPBAN_4:11

for b₁ being 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: :: LOPBAN_4:12

for b₁ being 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 Banach_Algebra;
let c₂ be Element of c₁;
func c₂ ExpSeq -> sequence of a₁ means :Def2: :: LOPBAN_4:def 2
for b₁ being Nat holds a₃ . b₁ = (1 / (b₁ ! )) * (a₂ #N b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ExpSeq LOPBAN_4:def 2 :

scheme :: LOPBAN_4:sch 1
s1{ F₁() -> non empty 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;

theorem Th13: :: LOPBAN_4:13

( ( for b₁ being Nat st 0 < b₁ holds
((b₁ -' 1) ! ) * b₁ = b₁ ! ) & ( for b₁, b₂ being Nat st b₂ <= b₁ holds
((b₁ -' b₂) ! ) * ((b₁ + 1) - b₂) = ((b₁ + 1) -' b₂) ! ) )

proof end;

definition

let c₁ be Nat;
func Coef c₁ -> Real_Sequence means :Def3: :: LOPBAN_4:def 3
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₂ . b₁ = (a₁ ! ) / ((b₁ ! ) * ((a₁ -' b₁) ! )) ) & ( b₁ > a₁ implies a₂ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Coef LOPBAN_4:def 3 :

definition

let c₁ be Nat;
func Coef_e c₁ -> Real_Sequence means :Def4: :: LOPBAN_4:def 4
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₂ . b₁ = 1 / ((b₁ ! ) * ((a₁ -' b₁) ! )) ) & ( b₁ > a₁ implies a₂ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Coef_e LOPBAN_4:def 4 :

definition

let c₁ be Banach_Algebra;
let c₂ be sequence of c₁;
func Sift c₂ -> sequence of a₁ means :Def5: :: LOPBAN_4:def 5
( a₃ . 0 = 0. a₁ & ( for b₁ being Nat holds a₃ . (b₁ + 1) = a₂ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Sift LOPBAN_4:def 5 :

definition

let c₁ be Nat;
let c₂ be Banach_Algebra;
let c₃, c₄ be Element of c₂;
func Expan c₁,c₃,c₄ -> sequence of a₂ means :Def6: :: LOPBAN_4:def 6
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 Def6 defines Expan LOPBAN_4:def 6 :

definition

let c₁ be Nat;
let c₂ be Banach_Algebra;
let c₃, c₄ be Element of c₂;
func Expan_e c₁,c₃,c₄ -> sequence of a₂ means :Def7: :: LOPBAN_4:def 7
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 Def7 defines Expan_e LOPBAN_4:def 7 :

definition

let c₁ be Nat;
let c₂ be Banach_Algebra;
let c₃, c₄ be Element of c₂;
func Alfa c₁,c₃,c₄ -> sequence of a₂ means :Def8: :: LOPBAN_4:def 8
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 Def8 defines Alfa LOPBAN_4:def 8 :

definition

let c₁ be Banach_Algebra;
let c₂, c₃ be Element of c₁;
let c₄ be Nat;
func Conj c₄,c₂,c₃ -> sequence of a₁ means :Def9: :: LOPBAN_4:def 9
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 Def9 defines Conj LOPBAN_4:def 9 :

theorem Th14: :: LOPBAN_4:14

for b₁ being Banach_Algebra
for b₂ being Element of b₁
for b₃ being Nat holds
( (b₂ ExpSeq ) . (b₃ + 1) = ((1 / (b₃ + 1)) * b₂) * ((b₂ ExpSeq ) . b₃) & (b₂ ExpSeq ) . 0 = 1. b₁ & ||.((b₂ ExpSeq ) . b₃).|| <= (||.b₂.|| ExpSeq ) . b₃ )

proof end;

theorem Th15: :: LOPBAN_4:15

for b₁ being 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 Th16: :: LOPBAN_4:16

for b₁ being 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 Th17: :: LOPBAN_4:17

for b₁ being 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 Th18: :: LOPBAN_4:18

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

proof end;

theorem Th19: :: LOPBAN_4:19

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

proof end;

theorem Th20: :: LOPBAN_4:20

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

proof end;

registration

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

proof end;

end;

theorem Th21: :: LOPBAN_4:21

for b₁ being 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 Th22: :: LOPBAN_4:22

for b₁ being 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 Th23: :: LOPBAN_4:23

for b₁ being 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 Th24: :: LOPBAN_4:24

for b₁ being 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 Th25: :: LOPBAN_4:25

for b₁ being 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 Th26: :: LOPBAN_4:26

for b₁ being 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 Th27: :: LOPBAN_4:27

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

proof end;

theorem Th28: :: LOPBAN_4:28

for b₁ being 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 Th29: :: LOPBAN_4:29

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

proof end;

theorem Th30: :: LOPBAN_4:30

for b₁ being 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 Th31: :: LOPBAN_4:31

for b₁ being 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 Th32: :: LOPBAN_4:32

for b₁ being 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 Th33: :: LOPBAN_4:33

for b₁ being 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;

Lemma45: for b₁ being 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 Banach_Algebra;
func exp_ c₁ -> Function of the carrier of a₁,the carrier of a₁ means :Def10: :: LOPBAN_4:def 10
for b₁ being Element of a₁ holds a₂ . b₁ = Sum (b₁ ExpSeq );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines exp_ LOPBAN_4:def 10 :

definition

let c₁ be Banach_Algebra;
let c₂ be Element of c₁;
func exp c₂ -> Element of a₁ equals :: LOPBAN_4:def 11
(exp_ a₁) . a₂;
correctness ;

end;

:: deftheorem Def11 defines exp LOPBAN_4:def 11 :

theorem Th34: :: LOPBAN_4:34

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

theorem Th35: :: LOPBAN_4:35

for b₁ being 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 Th36: :: LOPBAN_4:36

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

proof end;

theorem Th37: :: LOPBAN_4:37

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

proof end;

theorem Th38: :: LOPBAN_4:38

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

proof end;

theorem Th39: :: LOPBAN_4:39

for b₁ being 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 Th40: :: LOPBAN_4:40

for b₁ being Banach_Algebra
for b₂ being Element of b₁
for b₃, b₄ being Real holds b₃ * b₂,b₄ * b₂ are_commutative

proof end;

theorem Th41: :: LOPBAN_4:41

for b₁ being Banach_Algebra
for b₂ being Element of b₁
for b₃, b₄ being Real 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;