environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, REAL_1, INTEGRA5, TARSKI, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0, MEASURE6, MESFUNC5, FUNCT_3, VALUED_1, MESFUNC1, ARYTM_1, SUPINF_2, MESFUNC2, FINSEQ_1, NAT_1, CARD_3, CARD_1, MESFUNC3, INTEGRA1, ZFMISC_1, XXREAL_2, VALUED_0, RPR_1, FINSET_1, UPROOTS, RFUNCT_3, PROB_4, COMPLEX1, EQREL_1, SEQ_2, ORDINAL2, POWER, RANDOM_1, BSPACE, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, NUMBERS, XXREAL_3, XREAL_0, XXREAL_0, XCMPLX_0, COMPLEX1, XXREAL_2, FUNCT_1, REAL_1, SUPINF_2, RELSET_1, PARTFUN1, VALUED_1, FINSEQ_1, RFUNCT_3, NAT_1, FUNCT_2, SEQ_2, RPR_1, PROB_1, PROB_4, MEASURE1, EXTREAL1, MESFUNC1, MESFUNC3, MEASURE6, MESFUNC5, MESFUNC6, MESFUNC2, RVSUM_1, UPROOTS, MESFUN6C;
definitions TARSKI, FINSEQ_1, XBOOLE_0;
theorems ABSVALUE, TARSKI, PARTFUN1, FUNCT_1, NUMBERS, SUPINF_2, EXTREAL1, RPR_1, MESFUNC1, FINSEQ_1, XBOOLE_0, SEQM_3, RVSUM_1, XBOOLE_1, XCMPLX_1, MESFUNC2, MESFUNC3, XREAL_1, COMPLEX1, XXREAL_0, RFUNCT_3, MESFUNC5, PROB_1, NAT_1, RELAT_1, FUNCT_3, ZFMISC_1, FUNCT_2, MEASURE1, INTEGRA5, MESFUNC4, MESFUNC6, ORDINAL1, SEQ_2, MESFUNC7, VALUED_0, VALUED_1, ABCMIZ_1, RCOMP_1, MESFUN6C, FINSEQ_3, XXREAL_3, XREAL_0, CARD_2;
schemes FINSEQ_1, FUNCT_2, FINSEQ_2;
registrations SUBSET_1, NAT_1, XREAL_0, XXREAL_0, MEMBERED, ORDINAL1, FINSEQ_1, MEASURE1, FUNCT_2, RELAT_1, SEQ_4, FINSET_1, NUMBERS, XCMPLX_0, VALUED_0, VALUED_1, RELSET_1, JORDAN5A, XXREAL_3;
constructors HIDDEN, REAL_1, RPR_1, NAT_3, EXTREAL1, POWER, RVSUM_1, MESFUNC6, MESFUNC3, MESFUNC5, MEASURE6, MESFUNC2, BINOP_2, INTEGRA2, PROB_4, SUPINF_1, UPROOTS, MESFUN6C, MESFUNC1, DOMAIN_1, RELSET_1, COMSEQ_2, FUNCT_7;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities RPR_1, SUBSET_1, MESFUNC1, MESFUNC5, MESFUNC6, PROB_4, VALUED_1, XBOOLE_0, XXREAL_3, SUPINF_2;
expansions TARSKI, MESFUNC6, XBOOLE_0;
Lm1:
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S
for a being FinSequence of REAL
for x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) holds
Integral (M,f) = Sum x
Lm2:
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of REAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )
Lm3:
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL st f is_simple_func_in S holds
rng f is real-bounded
Lm4:
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 dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is_measurable_on E ) holds
f is_integrable_on M
Lm5:
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 f is_simple_func_in S & dom f <> {} & dom f in S & M . (dom f) < +infty holds
f is_integrable_on M
Lm6:
for Omega being non empty finite set
for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st
( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being Nat st k in dom F holds
F . k = {((canFS (dom f)) . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )
Lm7:
for Omega being non empty set
for Sigma being SigmaField of Omega
for M being sigma_Measure of Sigma
for A, B being set st A in Sigma & B in Sigma & A c= B & M . B < +infty holds
M . A in REAL
Lm8:
for Omega being non empty finite set
for f being PartFunc of Omega,REAL holds f * (canFS (dom f)) is FinSequence of REAL
Lm9:
for Omega being non empty finite set
for f being PartFunc of Omega,REAL holds dom (f * (canFS (dom f))) = dom (canFS (dom f))
reconsider jj = 1 as Real ;
Lm10:
for Omega being non empty finite set
for M being sigma_Measure of (Trivial-SigmaField Omega)
for f being Function of Omega,REAL st M . Omega < +infty holds
ex x being FinSequence of ExtREAL st
( len x = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . ((canFS Omega) . n)) * (M . {((canFS Omega) . n)}) ) & Integral (M,f) = Sum x )
Lm11:
for Omega being non empty finite set
for P being Probability of Trivial-SigmaField Omega
for f being Function of Omega,REAL ex F being FinSequence of REAL st
( len F = card Omega & ( for n being Nat st n in dom F holds
F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) ) & Integral ((P2M P),f) = Sum F )
Lm12:
for X being non empty set
for f being PartFunc of X,REAL holds abs f is nonnegative