environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, RLVECT_1, SUBSET_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_0, VALUED_1, FUNCOP_1, CARD_1, ARYTM_1, PROB_1, MEASURE1, MEMBERED, INTEGRA5, MESFUNC5, REAL_1, XXREAL_0, MESFUNC1, MEASURE6, SETFAM_1, COMPLEX1, PRE_TOPC, NORMSP_1, LPSPACE1, CLVECT_1, LPSPACC1, XCMPLX_0, SQUARE_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_3, XREAL_0, SQUARE_1, MEMBERED, VALUED_0, COMPLEX1, COMSEQ_3, VALUED_1, CFUNCT_1, SUPINF_2, PROB_1, MEASURE1, RFUNCT_3, MEASURE6, EXTREAL1, MESFUNC1, MESFUNC5, MESFUNC6, MESFUN6C, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, IDEAL_1, CLVECT_1, LPSPACE1;
definitions TARSKI, BINOP_1, ALGSTR_0, RLVECT_1, CLVECT_1;
theorems FUNCT_1, FUNCT_2, PARTFUN1, COMPLEX1, XBOOLE_0, TARSKI, RELAT_1, VALUED_1, ZFMISC_1, RLVECT_1, FUNCOP_1, XBOOLE_1, BINOP_1, VALUED_0, MEASURE1, MESFUNC6, RFUNCT_1, CLVECT_1, XCMPLX_0, MESFUN6C, MESFUN7C, LPSPACE1, CFUNCT_1, SQUARE_1, XREAL_1, CSSPACE3, SUBSET_1, COMSEQ_3;
schemes BINOP_1, FUNCT_2;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, PARTFUN1, SQUARE_1, VALUED_0, SUBSET_1, XCMPLX_0, STRUCT_0, MEASURE1, XXREAL_3, CLVECT_1;
constructors HIDDEN, COMPLEX1, EXTREAL1, CLVECT_1, CFUNCT_1, IDEAL_1, SQUARE_1, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6, SUPINF_1, REALSET1, MESFUNC1, RELSET_1, BINOP_2, MESFUN6C, LPSPACE2, COMSEQ_3;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, IDEAL_1, MESFUNC5, MESFUNC6, SUBSET_1, SQUARE_1, CLVECT_1, LPSPACE1, NORMSP_0;
expansions TARSKI, BINOP_1, RLVECT_1, IDEAL_1, MESFUNC5, MESFUNC6, CLVECT_1;
definition
let D be non
empty set ;
let E be
complex-membered set ;
let F1,
F2 be
Element of
PFuncs (
D,
E);
+redefine func F1 + F2 -> Element of
PFuncs (
D,
COMPLEX);
coherence
F1 + F2 is Element of PFuncs (D,COMPLEX)
-redefine func F1 - F2 -> Element of
PFuncs (
D,
COMPLEX);
coherence
F1 - F2 is Element of PFuncs (D,COMPLEX)
(#)redefine func F1 (#) F2 -> Element of
PFuncs (
D,
COMPLEX);
coherence
F1 (#) F2 is Element of PFuncs (D,COMPLEX)
/"redefine func F1 /" F2 -> Element of
PFuncs (
D,
COMPLEX);
coherence
F1 /" F2 is Element of PFuncs (D,COMPLEX)
end;
theorem Th2:
for
V being non
empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct 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
[:COMPLEX,V1:],
V1 st
d1 = 0. V &
A = the
addF of
V || V1 &
M = the
Mult of
V | [:COMPLEX,V1:] holds
(
CLSStruct(#
V1,
d1,
A,
M #) is
Abelian &
CLSStruct(#
V1,
d1,
A,
M #) is
add-associative &
CLSStruct(#
V1,
d1,
A,
M #) is
right_zeroed &
CLSStruct(#
V1,
d1,
A,
M #) is
vector-distributive &
CLSStruct(#
V1,
d1,
A,
M #) is
scalar-distributive &
CLSStruct(#
V1,
d1,
A,
M #) is
scalar-associative &
CLSStruct(#
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 CLSStruct for
V1 being non
empty add-closed multi-closed Subset of
V st
0. V in V1 holds
(
CLSStruct(#
V1,
(In ((0. V),V1)),
(add| (V1,V)),
(Mult_ V1) #) is
Abelian &
CLSStruct(#
V1,
(In ((0. V),V1)),
(add| (V1,V)),
(Mult_ V1) #) is
add-associative &
CLSStruct(#
V1,
(In ((0. V),V1)),
(add| (V1,V)),
(Mult_ V1) #) is
right_zeroed &
CLSStruct(#
V1,
(In ((0. V),V1)),
(add| (V1,V)),
(Mult_ V1) #) is
vector-distributive &
CLSStruct(#
V1,
(In ((0. V),V1)),
(add| (V1,V)),
(Mult_ V1) #) is
scalar-distributive &
CLSStruct(#
V1,
(In ((0. V),V1)),
(add| (V1,V)),
(Mult_ V1) #) is
scalar-associative &
CLSStruct(#
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,COMPLEX)) st
for f, g being Element of PFuncs (A,COMPLEX) holds b1 . (f,g) = f (#) g
uniqueness
for b1, b2 being BinOp of (PFuncs (A,COMPLEX)) st ( for f, g being Element of PFuncs (A,COMPLEX) holds b1 . (f,g) = f (#) g ) & ( for f, g being Element of PFuncs (A,COMPLEX) holds b2 . (f,g) = f (#) g ) holds
b1 = b2
end;
definition
let A be non
empty set ;
existence
ex b1 being Function of [:COMPLEX,(PFuncs (A,COMPLEX)):],(PFuncs (A,COMPLEX)) st
for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds b1 . (a,f) = a (#) f
uniqueness
for b1, b2 being Function of [:COMPLEX,(PFuncs (A,COMPLEX)):],(PFuncs (A,COMPLEX)) st ( for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds b1 . (a,f) = a (#) f ) & ( for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds b2 . (a,f) = a (#) f ) holds
b1 = b2
end;
definition
let D be non
empty set ;
existence
ex b1 being BinOp of (PFuncs (D,COMPLEX)) st
for F1, F2 being Element of PFuncs (D,COMPLEX) holds b1 . (F1,F2) = F1 + F2
uniqueness
for b1, b2 being BinOp of (PFuncs (D,COMPLEX)) st ( for F1, F2 being Element of PFuncs (D,COMPLEX) holds b1 . (F1,F2) = F1 + F2 ) & ( for F1, F2 being Element of PFuncs (D,COMPLEX) holds b2 . (F1,F2) = F1 + F2 ) holds
b1 = b2
end;
reconsider R = - 1r as Element of COMPLEX by XCMPLX_0:def 2;
Lm1:
for a being Complex
for A being non empty set
for f, g being Element of PFuncs (A,COMPLEX) holds (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (a,g))) = (multcomplexcpfunc A) . (a,((addcpfunc 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,COMPLEX 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 in L1_CFunctions 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_CFunctions M is add-closed & L1_CFunctions 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
( AlmostZeroCFunctions M is add-closed & AlmostZeroCFunctions M is multi-closed )
theorem Th34:
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,
COMPLEX st
f in L1_CFunctions M &
f1 in L1_CFunctions M &
g in L1_CFunctions M &
g1 in L1_CFunctions M &
a.e-Ceq-class (
f,
M)
= a.e-Ceq-class (
f1,
M) &
a.e-Ceq-class (
g,
M)
= a.e-Ceq-class (
g1,
M) holds
a.e-Ceq-class (
(f + g),
M)
= a.e-Ceq-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 (CCosetSet M) st
for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
b1 . (A,B) = a.e-Ceq-class ((a + b),M)
uniqueness
for b1, b2 being BinOp of (CCosetSet M) st ( for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
b1 . (A,B) = a.e-Ceq-class ((a + b),M) ) & ( for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
b2 . (A,B) = a.e-Ceq-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 [:COMPLEX,(CCosetSet M):],(CCosetSet M) st
for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
b1 . (z,A) = a.e-Ceq-class ((z (#) f),M)
uniqueness
for b1, b2 being Function of [:COMPLEX,(CCosetSet M):],(CCosetSet M) st ( for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
b1 . (z,A) = a.e-Ceq-class ((z (#) f),M) ) & ( for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
b2 . (z,A) = a.e-Ceq-class ((z (#) f),M) ) holds
b1 = b2
end;