CC0SP1: Banach Algebra of Bounded Complex-Valued Functionals

:: Banach Algebra of Bounded Complex-Valued Functionals
:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 20, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users

begin

definition

let V be ComplexAlgebra;
mode ComplexSubAlgebra of V -> ComplexAlgebra means :DefComplexAlgebra: :: CC0SP1:def 1
( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & the Mult of it = the Mult of V | [:COMPLEX, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );
existence

proof end;

end;

:: deftheorem DefComplexAlgebra defines ComplexSubAlgebra CC0SP1:def 1 :

theorem Th1: :: CC0SP1:1

for X being non empty set
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

proof end;

registration

let V be ComplexAlgebra;
cluster non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative strict vector-associative ComplexSubAlgebra of V;
existence

proof end;

end;

definition

let V be ComplexAlgebra;
let V1 be Subset of V;
attr V1 is Cadditively-linearly-closed means :Def10: :: CC0SP1:def 2
( V1 is add-closed & V1 is having-inverse & ( for a being Complex
for v being Element of V st v in V1 holds
a * v in V1 ) );

end;

:: deftheorem Def10 defines Cadditively-linearly-closed CC0SP1:def 2 :

definition

let V be ComplexAlgebra;
let V1 be Subset of V;
assume A1: ( V1 is Cadditively-linearly-closed & not V1 is empty ) ;
func Mult_ (V1,V) -> Function of [:COMPLEX,V1:],V1 equals :Def11: :: CC0SP1:def 3
the Mult of V | [:COMPLEX,V1:];
correctness

proof end;

end;

:: deftheorem Def11 defines Mult_ CC0SP1:def 3 :

definition

let X be non empty set ;
func ComplexBoundedFunctions X -> non empty Subset of (CAlgebra X) equals :: CC0SP1:def 4
{ f where f is Function of X,COMPLEX : f | X is bounded } ;
correctness

proof end;

end;

:: deftheorem defines ComplexBoundedFunctions CC0SP1:def 4 :

registration

let X be non empty set ;
cluster CAlgebra X -> scalar-unital ;
coherence

proof end;

end;

registration

let X be non empty set ;
cluster ComplexBoundedFunctions X -> non empty multiplicatively-closed Cadditively-linearly-closed ;
coherence

proof end;

end;

registration

let V be ComplexAlgebra;
cluster non empty multiplicatively-closed Cadditively-linearly-closed Element of bool the carrier of V;
existence

proof end;

end;

definition

let V be non empty CLSStruct ;
attr V is scalar-mult-cancelable means :: CC0SP1:def 5
for a being Complex
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V );

end;

:: deftheorem defines scalar-mult-cancelable CC0SP1:def 5 :

theorem Th2: :: CC0SP1:2

for V being ComplexAlgebra
for V1 being non empty multiplicatively-closed Cadditively-linearly-closed Subset of V holds ComplexAlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is ComplexSubAlgebra of V

proof end;

theorem Th4: :: CC0SP1:3

for V being ComplexAlgebra
for V1 being ComplexSubAlgebra of V holds
( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Complex st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

proof end;

definition

let X be non empty set ;
func C_Algebra_of_BoundedFunctions X -> ComplexAlgebra equals :: CC0SP1:def 6
ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #);
coherence by Th2;

end;

:: deftheorem defines C_Algebra_of_BoundedFunctions CC0SP1:def 6 :

theorem :: CC0SP1:4

for X being non empty set holds C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;

registration

let X be non empty set ;
cluster C_Algebra_of_BoundedFunctions X -> scalar-unital ;
coherence

proof end;

end;

theorem Th8: :: CC0SP1:5

for X being non empty set
for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th9: :: CC0SP1:6

for X being non empty set
for a being Complex
for F, G being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g being Function of X,COMPLEX st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem Th10: :: CC0SP1:7

for X being non empty set
for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

theorem Th11: :: CC0SP1:8

for X being non empty set holds 0. (C_Algebra_of_BoundedFunctions X) = X --> 0

proof end;

theorem Th12: :: CC0SP1:9

for X being non empty set holds 1_ (C_Algebra_of_BoundedFunctions X) = X --> 1r

proof end;

definition

let X be non empty set ;
let F be set ;
assume A1: F in ComplexBoundedFunctions X ;
func modetrans (F,X) -> Function of X,COMPLEX means :DefB7: :: CC0SP1:def 7
( it = F & it | X is bounded );
correctness by A1;

end;

:: deftheorem DefB7 defines modetrans CC0SP1:def 7 :

definition

let X be non empty set ;
let f be Function of X,COMPLEX;
func PreNorms f -> non empty Subset of REAL equals :: CC0SP1:def 8
{ |.(f . x).| where x is Element of X : verum } ;
coherence

proof end;

end;

:: deftheorem defines PreNorms CC0SP1:def 8 :

Lm1: for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )

proof end;

theorem Th13: :: CC0SP1:10

for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
PreNorms f is bounded_above

proof end;

theorem Th14: :: CC0SP1:11

for X being non empty set
for f being Function of X,COMPLEX holds
( f | X is bounded iff PreNorms f is bounded_above )

proof end;

theorem Th15: :: CC0SP1:12

for X being non empty set ex NORM being Function of (ComplexBoundedFunctions X),REAL st
for F being set st F in ComplexBoundedFunctions X holds
NORM . F = upper_bound (PreNorms (modetrans (F,X)))

proof end;

definition

let X be non empty set ;
func ComplexBoundedFunctionsNorm X -> Function of (ComplexBoundedFunctions X),REAL means :DefB9C: :: CC0SP1:def 9
for x being set st x in ComplexBoundedFunctions X holds
it . x = upper_bound (PreNorms (modetrans (x,X)));
existence by Th15;
uniqueness

proof end;

end;

:: deftheorem DefB9C defines ComplexBoundedFunctionsNorm CC0SP1:def 9 :

theorem Th16: :: CC0SP1:13

for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
modetrans (f,X) = f

proof end;

theorem Th17: :: CC0SP1:14

for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

proof end;

definition

let X be non empty set ;
func C_Normed_Algebra_of_BoundedFunctions X -> Normed_Complex_AlgebraStr equals :: CC0SP1:def 10
Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #);
correctness ;

end;

:: deftheorem defines C_Normed_Algebra_of_BoundedFunctions CC0SP1:def 10 :

registration

let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X -> non empty ;
correctness ;

end;

Lm2: now

end;

registration

let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X -> unital ;
correctness

proof end;

end;

theorem Th18: :: CC0SP1:15

for W being Normed_Complex_AlgebraStr
for V being ComplexAlgebra st ComplexAlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds
W is ComplexAlgebra

proof end;

theorem Th19: :: CC0SP1:16

for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is ComplexAlgebra

proof end;

theorem :: CC0SP1:17

for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F

proof end;

theorem Th21: :: CC0SP1:18

for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is ComplexLinearSpace

proof end;

theorem Th22: :: CC0SP1:19

for X being non empty set holds X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X)

proof end;

theorem Th23: :: CC0SP1:20

for X being non empty set
for x being Element of X
for f being Function of X,COMPLEX
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||

proof end;

theorem :: CC0SP1:21

for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||

proof end;

theorem Th25: :: CC0SP1:22

for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st F = 0. (C_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||

proof end;

theorem Th26: :: CC0SP1:23

for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th27: :: CC0SP1:24

for X being non empty set
for a being Complex
for f, g being Function of X,COMPLEX
for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem Th28: :: CC0SP1:25

for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

theorem Th29: :: CC0SP1:26

for X being non empty set
for a being Complex
for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof end;

Th30: for X being non empty set holds
( C_Normed_Algebra_of_BoundedFunctions X is reflexive & C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like )

proof end;

registration

let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence by Th21, Th30;

end;

theorem Th31: :: CC0SP1:27

for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )

proof end;

theorem Th32: :: CC0SP1:28

for X being non empty set
for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent

proof end;

registration

let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X -> complete ;
coherence

proof end;

end;

theorem :: CC0SP1:29

for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is Complex_Banach_Algebra

proof end;