environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, RLVECT_1, SUBSET_1, REAL_1, RELAT_1, RLSUB_1, IDEAL_1, ARYTM_3, STRUCT_0, RSSPACE, FUNCT_1, ZFMISC_1, TARSKI, BINOP_1, SUPINF_2, ALGSTR_0, REALSET1, FUNCT_7, PARTFUN1, VALUED_1, FUNCOP_1, CARD_1, RFUNCT_3, ARYTM_1, PROB_1, MEASURE1, NAT_1, INTEGRA5, MESFUNC5, MESFUNC2, XXREAL_0, MESFUNC1, SUPINF_1, MEASURE6, VECTSP10, SETFAM_1, COMPLEX1, PRE_TOPC, NORMSP_1, LPSPACE1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XXREAL_3, XCMPLX_0, NUMBERS, COMPLEX1, XXREAL_0, XREAL_0, SUPINF_1, SUPINF_2, EXTREAL1, REALSET1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1, RFUNCT_3, BINOP_1, NAT_1, FUNCOP_1, REAL_1, STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1, IDEAL_1, SETFAM_1, DOMAIN_1, PRE_TOPC, NORMSP_0, NORMSP_1, PROB_1, MEASURE1, MEASURE2, MEASURE3, MEASURE6, MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC6, FUNCT_7;
definitions TARSKI, SUPINF_2, ALGSTR_0, RLVECT_1;
theorems FUNCT_1, FUNCT_2, PARTFUN1, COMPLEX1, XBOOLE_0, TARSKI, RELAT_1, VALUED_1, RLSUB_1, ZFMISC_1, RLVECT_1, FUNCOP_1, XBOOLE_1, BINOP_1, SUPINF_2, RFUNCT_3, MESFUNC5, MESFUNC2, EXTREAL1, MEASURE1, MESFUNC6, PROB_1, RFUNCT_1, XXREAL_0, NUMBERS, ABSVALUE, MESFUNC1, MEASURE2, MESFUNC7, RSSPACE3, NORMSP_1, VALUED_0, RELSET_1, XXREAL_3, XREAL_0, SUBSET_1;
schemes BINOP_1, FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, NAT_1, SUBSET_1, PARTFUN1, XXREAL_0, RLVECT_1, STRUCT_0, NORMSP_1, MEASURE1, MESFUNC7, XXREAL_3;
constructors HIDDEN, COMPLEX1, EXTREAL1, BINOP_1, REAL_1, RLSUB_1, IDEAL_1, NORMSP_1, MEASURE3, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6, SUPINF_1, FUNCT_7, REALSET1, MESFUNC1, RELSET_1, BINOP_2, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, IDEAL_1, MESFUNC5, MESFUNC6, SUBSET_1, XXREAL_3, NORMSP_0;
expansions TARSKI, BINOP_1, RLVECT_1, IDEAL_1, MESFUNC5, MESFUNC6;
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 )
definition
let A be non
empty set ;
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;
definition
let A be non
empty set ;
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;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
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)))
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 )
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
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 )
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 Th41:
for
X being non
empty set for
S being
SigmaField of
X for
M being
sigma_Measure of
S for
f,
g,
f1,
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)
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
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;
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
existence
ex b1 being Function of [:REAL,(CosetSet M):],(CosetSet M) st
for z being 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 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 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;
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 )