:: 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 RLSUBDef0 defines multi-closed LPSPACE1:def 1 :
theorem :: LPSPACE1:1
:: deftheorem defines Mult_ LPSPACE1:def 2 :
theorem RLSUB132: :: 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 RSSPACE13: :: 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 RLSUB121: :: LPSPACE1:4
theorem RLSUB122: :: 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 Th10: :: LPSPACE1:6
theorem Th11: :: LPSPACE1:7
theorem :: LPSPACE1:8
theorem Th15: :: LPSPACE1:9
theorem Th16: :: LPSPACE1:10
theorem Th17: :: LPSPACE1:11
theorem :: LPSPACE1:12
theorem :: LPSPACE1:13
theorem :: LPSPACE1:14
theorem Th21: :: LPSPACE1:15
theorem Th22: :: LPSPACE1:16
theorem Th23: :: LPSPACE1:17
theorem Th24: :: LPSPACE1:18
theorem Th25: :: LPSPACE1:19
Lm2:
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 Lm1: :: 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 :
LmDef1:
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 )
MLm01:
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 Th01a: :: LPSPACE1:23
theorem Th01b: :: LPSPACE1:24
Th01:
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 ThB10: :: LPSPACE1:25
theorem ThB11: :: LPSPACE1:26
:: deftheorem Def2 defines a.e.= LPSPACE1:def 10 :
theorem ThB11Z: :: LPSPACE1:27
theorem Th04: :: LPSPACE1:28
theorem Th05: :: LPSPACE1:29
theorem Th06: :: LPSPACE1:30
theorem Th07: :: LPSPACE1:31
theorem Th08: :: LPSPACE1:32
:: deftheorem defines AlmostZeroFunctions LPSPACE1:def 11 :
theorem HSATZE: :: LPSPACE1:33
Th09:
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 Th09a: :: 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 EQC00: :: LPSPACE1:37
theorem EQC01: :: LPSPACE1:38
theorem EQC02: :: LPSPACE1:39
theorem :: LPSPACE1:40
theorem EQC03: :: 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 EQC04: :: 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 :
VSPDef3X:
:: 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 VSPDef3X defines addCoset LPSPACE1:def 15 :
:: deftheorem VSPDef4X 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 :
VSPDef5X:
:: 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 VSPDef5X defines lmultCoset LPSPACE1:def 17 :
:: deftheorem VSPDef6X defines Pre-L-Space LPSPACE1:def 18 :
theorem Th14a: :: LPSPACE1:43
theorem Lm15: :: LPSPACE1:44
theorem Th14: :: LPSPACE1:45
theorem Lm10: :: LPSPACE1:46
theorem Th15: :: LPSPACE1:47
theorem Lm16: :: LPSPACE1:48
theorem Lm17: :: 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 :
Def20:
:: 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 Th15;
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 Def20 defines L-1-Norm LPSPACE1:def 19 :
:: deftheorem defines L-1-Space LPSPACE1:def 20 :
theorem Lm17x: :: LPSPACE1:50
theorem Lm17z: :: LPSPACE1:51
theorem Lm17Y: :: LPSPACE1:52
theorem Lm261a: :: LPSPACE1:53
theorem Lm261: :: LPSPACE1:54
theorem Lm262: :: LPSPACE1:55
theorem Lm263: :: LPSPACE1:56
Th26:
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 )