begin
:: deftheorem Def1 defines multi-closed LPSPACE1:def 1 :
for V being non empty RLSStruct
for V1 being Subset of V holds
( V1 is multi-closed iff for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1 );
theorem
:: deftheorem defines Mult_ LPSPACE1:def 2 :
for X being non empty RLSStruct
for X1 being non empty multi-closed Subset of X holds Mult_ X1 = the Mult of X | [:REAL ,X1:];
theorem Th2:
for
V being non
empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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
vector-distributive &
RLSStruct(#
V1,
d1,
A,
M #) is
scalar-distributive &
RLSStruct(#
V1,
d1,
A,
M #) is
scalar-associative &
RLSStruct(#
V1,
d1,
A,
M #) is
scalar-unital )
theorem Th3:
for
V being non
empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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
vector-distributive &
RLSStruct(#
V1,
(In (0. V),V1),
(add| V1,V),
(Mult_ V1) #) is
scalar-distributive &
RLSStruct(#
V1,
(In (0. V),V1),
(add| V1,V),
(Mult_ V1) #) is
scalar-associative &
RLSStruct(#
V1,
(In (0. V),V1),
(add| V1,V),
(Mult_ V1) #) is
scalar-unital )
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 :
for A being non empty set
for b2 being BinOp of (PFuncs A,REAL ) holds
( b2 = multpfunc A iff for f, g being Element of PFuncs A,REAL holds b2 . f,g = f (#) g );
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 :
for A being non empty set
for b2 being Function of [:REAL ,(PFuncs A,REAL ):],(PFuncs A,REAL ) holds
( b2 = multrealpfunc A iff for a being Real
for f being Element of PFuncs A,REAL holds b2 . a,f = a (#) f );
:: deftheorem defines RealPFuncZero LPSPACE1:def 5 :
for A being non empty set holds RealPFuncZero A = A --> 0 ;
:: deftheorem defines RealPFuncUnit LPSPACE1:def 6 :
for A being non empty set holds RealPFuncUnit A = A --> 1;
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 :
for A being non empty set holds RLSp_PFunct A = RLSStruct(# (PFuncs A,REAL ),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #);
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 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L1_Functions M = { f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } ;
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 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_L1Funct M = RLSStruct(# (L1_Functions M),(In (0. (RLSp_PFunct X)),(L1_Functions M)),(add| (L1_Functions M),(RLSp_PFunct X)),(Mult_ (L1_Functions M)) #);
begin
theorem Th25:
theorem Th26:
:: deftheorem Def10 defines a.e.= LPSPACE1:def 10 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL holds
( f a.e.= g,M iff ex E being Element of S st
( M . E = 0 & f | (E ` ) = g | (E ` ) ) );
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem defines AlmostZeroFunctions LPSPACE1:def 11 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds AlmostZeroFunctions M = { f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0 ,M ) } ;
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 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_AlmostZeroFunct M = RLSStruct(# (AlmostZeroFunctions M),(In (0. (RLSp_L1Funct M)),(AlmostZeroFunctions M)),(add| (AlmostZeroFunctions M),(RLSp_L1Funct M)),(Mult_ (AlmostZeroFunctions M)) #);
theorem
theorem
:: deftheorem defines a.e-eq-class LPSPACE1:def 13 :
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 holds a.e-eq-class f,M = { g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) } ;
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 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CosetSet M = { (a.e-eq-class f,M) where f is PartFunc of X,REAL : f in L1_Functions M } ;
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 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being BinOp of (CosetSet M) holds
( b4 = addCoset M iff for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b4 . A,B = a.e-eq-class (a + b),M );
:: deftheorem Def16 defines zeroCoset LPSPACE1:def 16 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Element of CosetSet M holds
( b4 = zeroCoset M iff ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b4 = a.e-eq-class f,M ) );
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 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Function of [:REAL ,(CosetSet M):],(CosetSet M) holds
( b4 = lmultCoset M iff 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
b4 . z,A = a.e-eq-class (z (#) f),M );
:: deftheorem Def18 defines Pre-L-Space LPSPACE1:def 18 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds
( b4 = Pre-L-Space M iff ( the carrier of b4 = CosetSet M & the addF of b4 = addCoset M & 0. b4 = zeroCoset M & the Mult of b4 = lmultCoset M ) );
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 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Function of the carrier of (Pre-L-Space M),REAL holds
( b4 = L-1-Norm M iff for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b4 . x = Integral M,(abs f) ) );
:: deftheorem defines L-1-Space LPSPACE1:def 20 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L-1-Space M = NORMSTR(# the carrier of (Pre-L-Space M),the ZeroF of (Pre-L-Space M),the addF of (Pre-L-Space M),the Mult of (Pre-L-Space M),(L-1-Norm M) #);
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 vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & 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 )