:: On $L^1$ Space Formed by Real-valued Partial Functions
:: by Yasushige Watase , Noboru Endou and Yasunari Shidama
::
:: Received August 26, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem Def1 defines multi-closed LPSPACE1:def 1 :
theorem :: LPSPACE1:1
:: deftheorem defines Mult_ LPSPACE1:def 2 :
theorem Th2: :: LPSPACE1:2
for
V being non
empty Abelian add-associative right_zeroed RealLinearSpace-like RLSStruct for
V1 being non
empty Subset of
V for
d1 being
Element of
V1 for
A being
BinOp of
V1 for
M being
Function of
[:REAL ,V1:],
V1 st
d1 = 0. V &
A = the
addF of
V || V1 &
M = the
Mult of
V | [:REAL ,V1:] holds
(
RLSStruct(#
V1,
d1,
A,
M #) is
Abelian &
RLSStruct(#
V1,
d1,
A,
M #) is
add-associative &
RLSStruct(#
V1,
d1,
A,
M #) is
right_zeroed &
RLSStruct(#
V1,
d1,
A,
M #) is
RealLinearSpace-like )
theorem Th3: :: LPSPACE1:3
for
V being non
empty Abelian add-associative right_zeroed RealLinearSpace-like RLSStruct for
V1 being non
empty add-closed multi-closed Subset of
V st
0. V in V1 holds
(
RLSStruct(#
V1,
(In (0. V),V1),
(add| V1,V),
(Mult_ V1) #) is
Abelian &
RLSStruct(#
V1,
(In (0. V),V1),
(add| V1,V),
(Mult_ V1) #) is
add-associative &
RLSStruct(#
V1,
(In (0. V),V1),
(add| V1,V),
(Mult_ V1) #) is
right_zeroed &
RLSStruct(#
V1,
(In (0. V),V1),
(add| V1,V),
(Mult_ V1) #) is
RealLinearSpace-like )
theorem Th4: :: LPSPACE1:4
theorem Th5: :: LPSPACE1:5
definition
let A be non
empty set ;
func multpfunc A -> BinOp of
(PFuncs A,REAL ) means :
Def3:
:: LPSPACE1:def 3
for
f,
g being
Element of
PFuncs A,
REAL holds
it . f,
g = f (#) g;
existence
ex b1 being BinOp of (PFuncs A,REAL ) st
for f, g being Element of PFuncs A,REAL holds b1 . f,g = f (#) g
uniqueness
for b1, b2 being BinOp of (PFuncs A,REAL ) st ( for f, g being Element of PFuncs A,REAL holds b1 . f,g = f (#) g ) & ( for f, g being Element of PFuncs A,REAL holds b2 . f,g = f (#) g ) holds
b1 = b2
end;
:: deftheorem Def3 defines multpfunc LPSPACE1:def 3 :
definition
let A be non
empty set ;
func multrealpfunc A -> Function of
[:REAL ,(PFuncs A,REAL ):],
(PFuncs A,REAL ) means :
Def4:
:: LPSPACE1:def 4
for
a being
Real for
f being
Element of
PFuncs A,
REAL holds
it . a,
f = a (#) f;
existence
ex b1 being Function of [:REAL ,(PFuncs A,REAL ):],(PFuncs A,REAL ) st
for a being Real
for f being Element of PFuncs A,REAL holds b1 . a,f = a (#) f
uniqueness
for b1, b2 being Function of [:REAL ,(PFuncs A,REAL ):],(PFuncs A,REAL ) st ( for a being Real
for f being Element of PFuncs A,REAL holds b1 . a,f = a (#) f ) & ( for a being Real
for f being Element of PFuncs A,REAL holds b2 . a,f = a (#) f ) holds
b1 = b2
end;
:: deftheorem Def4 defines multrealpfunc LPSPACE1:def 4 :
:: deftheorem defines RealPFuncZero LPSPACE1:def 5 :
:: deftheorem defines RealPFuncUnit LPSPACE1:def 6 :
theorem Th6: :: LPSPACE1:6
theorem Th7: :: LPSPACE1:7
theorem :: LPSPACE1:8
theorem Th9: :: LPSPACE1:9
theorem Th10: :: LPSPACE1:10
theorem Th11: :: LPSPACE1:11
theorem :: LPSPACE1:12
theorem :: LPSPACE1:13
theorem :: LPSPACE1:14
theorem Th15: :: LPSPACE1:15
theorem Th16: :: LPSPACE1:16
theorem Th17: :: LPSPACE1:17
theorem Th18: :: LPSPACE1:18
theorem Th19: :: LPSPACE1:19
Lm1:
for a being Real
for A being non empty set
for f, g being Element of PFuncs A,REAL holds (addpfunc A) . ((multrealpfunc A) . a,f),((multrealpfunc A) . a,g) = (multrealpfunc A) . a,((addpfunc A) . f,g)
theorem :: LPSPACE1:20
theorem :: LPSPACE1:21
:: deftheorem defines RLSp_PFunct LPSPACE1:def 7 :
theorem Th22: :: LPSPACE1:22
Lm2:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st X = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral M,f = 0 )
:: deftheorem defines L1_Functions LPSPACE1:def 8 :
Lm3:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )
Lm4:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0
theorem Th23: :: LPSPACE1:23
theorem Th24: :: LPSPACE1:24
Lm5:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L1_Functions M is add-closed & L1_Functions M is multi-closed )
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
func RLSp_L1Funct M -> non
empty RLSStruct equals :: LPSPACE1:def 9
RLSStruct(#
(L1_Functions M),
(In (0. (RLSp_PFunct X)),(L1_Functions M)),
(add| (L1_Functions M),(RLSp_PFunct X)),
(Mult_ (L1_Functions M)) #);
coherence
RLSStruct(# (L1_Functions M),(In (0. (RLSp_PFunct X)),(L1_Functions M)),(add| (L1_Functions M),(RLSp_PFunct X)),(Mult_ (L1_Functions M)) #) is non empty RLSStruct
;
end;
:: deftheorem defines RLSp_L1Funct LPSPACE1:def 9 :
theorem Th25: :: LPSPACE1:25
theorem Th26: :: LPSPACE1:26
:: deftheorem Def10 defines a.e.= LPSPACE1:def 10 :
theorem Th27: :: LPSPACE1:27
theorem Th28: :: LPSPACE1:28
theorem Th29: :: LPSPACE1:29
theorem Th30: :: LPSPACE1:30
theorem Th31: :: LPSPACE1:31
theorem Th32: :: LPSPACE1:32
:: deftheorem defines AlmostZeroFunctions LPSPACE1:def 11 :
theorem Th33: :: LPSPACE1:33
Lm6:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed )
theorem Th34: :: LPSPACE1:34
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
func RLSp_AlmostZeroFunct M -> non
empty RLSStruct equals :: LPSPACE1:def 12
RLSStruct(#
(AlmostZeroFunctions M),
(In (0. (RLSp_L1Funct M)),(AlmostZeroFunctions M)),
(add| (AlmostZeroFunctions M),(RLSp_L1Funct M)),
(Mult_ (AlmostZeroFunctions M)) #);
coherence
RLSStruct(# (AlmostZeroFunctions M),(In (0. (RLSp_L1Funct M)),(AlmostZeroFunctions M)),(add| (AlmostZeroFunctions M),(RLSp_L1Funct M)),(Mult_ (AlmostZeroFunctions M)) #) is non empty RLSStruct
;
end;
:: deftheorem defines RLSp_AlmostZeroFunct LPSPACE1:def 12 :
theorem :: LPSPACE1:35
theorem :: LPSPACE1:36
:: deftheorem defines a.e-eq-class LPSPACE1:def 13 :
theorem Th37: :: LPSPACE1:37
theorem Th38: :: LPSPACE1:38
theorem Th39: :: LPSPACE1:39
theorem :: LPSPACE1:40
theorem Th41: :: LPSPACE1:41
for
X being non
empty set for
S being
SigmaField of
X for
M being
sigma_Measure of
S for
f,
f1,
g,
g1 being
PartFunc of
X,
REAL st
f in L1_Functions M &
f1 in L1_Functions M &
g in L1_Functions M &
g1 in L1_Functions M &
a.e-eq-class f,
M = a.e-eq-class f1,
M &
a.e-eq-class g,
M = a.e-eq-class g1,
M holds
a.e-eq-class (f + g),
M = a.e-eq-class (f1 + g1),
M
theorem Th42: :: LPSPACE1:42
:: deftheorem defines CosetSet LPSPACE1:def 14 :
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
func addCoset M -> BinOp of
(CosetSet M) means :
Def15:
:: LPSPACE1:def 15
for
A,
B being
Element of
CosetSet M for
a,
b being
PartFunc of
X,
REAL st
a in A &
b in B holds
it . A,
B = a.e-eq-class (a + b),
M;
existence
ex b1 being BinOp of (CosetSet M) st
for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b1 . A,B = a.e-eq-class (a + b),M
uniqueness
for b1, b2 being BinOp of (CosetSet M) st ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b1 . A,B = a.e-eq-class (a + b),M ) & ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b2 . A,B = a.e-eq-class (a + b),M ) holds
b1 = b2
end;
:: deftheorem Def15 defines addCoset LPSPACE1:def 15 :
:: deftheorem Def16 defines zeroCoset LPSPACE1:def 16 :
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
func lmultCoset M -> Function of
[:REAL ,(CosetSet M):],
(CosetSet M) means :
Def17:
:: LPSPACE1:def 17
for
z being
Element of
REAL for
A being
Element of
CosetSet M for
f being
PartFunc of
X,
REAL st
f in A holds
it . z,
A = a.e-eq-class (z (#) f),
M;
existence
ex b1 being Function of [:REAL ,(CosetSet M):],(CosetSet M) st
for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b1 . z,A = a.e-eq-class (z (#) f),M
uniqueness
for b1, b2 being Function of [:REAL ,(CosetSet M):],(CosetSet M) st ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b1 . z,A = a.e-eq-class (z (#) f),M ) & ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b2 . z,A = a.e-eq-class (z (#) f),M ) holds
b1 = b2
end;
:: deftheorem Def17 defines lmultCoset LPSPACE1:def 17 :
:: deftheorem Def18 defines Pre-L-Space LPSPACE1:def 18 :
theorem Th43: :: LPSPACE1:43
theorem Th44: :: LPSPACE1:44
theorem Th45: :: LPSPACE1:45
theorem Th46: :: LPSPACE1:46
theorem Th47: :: LPSPACE1:47
theorem Th48: :: LPSPACE1:48
theorem Th49: :: LPSPACE1:49
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
func L-1-Norm M -> Function of the
carrier of
(Pre-L-Space M),
REAL means :
Def19:
:: LPSPACE1:def 19
for
x being
Point of
(Pre-L-Space M) ex
f being
PartFunc of
X,
REAL st
(
f in x &
it . x = Integral M,
(abs f) );
existence
ex b1 being Function of the carrier of (Pre-L-Space M),REAL st
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b1 . x = Integral M,(abs f) )
by Th47;
uniqueness
for b1, b2 being Function of the carrier of (Pre-L-Space M),REAL st ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b1 . x = Integral M,(abs f) ) ) & ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b2 . x = Integral M,(abs f) ) ) holds
b1 = b2
end;
:: deftheorem Def19 defines L-1-Norm LPSPACE1:def 19 :
:: deftheorem defines L-1-Space LPSPACE1:def 20 :
theorem Th50: :: LPSPACE1:50
theorem Th51: :: LPSPACE1:51
theorem Th52: :: LPSPACE1:52
theorem Th53: :: LPSPACE1:53
theorem Th54: :: LPSPACE1:54
theorem Th55: :: LPSPACE1:55
theorem Th56: :: LPSPACE1:56
Lm7:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is RealLinearSpace-like & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )