begin
:: deftheorem Def1 defines multi-closed LPSPACE1:def 1 :
theorem
:: deftheorem defines Mult_ LPSPACE1:def 2 :
theorem Th2:
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:
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:
theorem Th5:
begin
definition
let A be non
empty set ;
func multpfunc A -> BinOp of
(PFuncs A,REAL ) means :
Def3:
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:
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:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
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
theorem
:: deftheorem defines RLSp_PFunct LPSPACE1:def 7 :
begin
theorem Th22:
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:
theorem Th24:
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
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 :
begin
theorem Th25:
theorem Th26:
:: deftheorem Def10 defines a.e.= LPSPACE1:def 10 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem defines AlmostZeroFunctions LPSPACE1:def 11 :
theorem Th33:
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:
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
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
theorem
:: deftheorem defines a.e-eq-class LPSPACE1:def 13 :
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem Th41:
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:
:: 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:
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:
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 :
begin
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
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:
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:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
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 )