environ
vocabularies HIDDEN, NUMBERS, SUPINF_1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3, MEASURE6, NAT_1, CARD_1, NEWTON, RELAT_1, REAL_1, SUBSET_1, INT_1, PARTFUN1, FUNCT_1, SUPINF_2, XBOOLE_0, PROB_1, MESFUNC2, VALUED_0, RAT_1, MESFUNC1, TARSKI, MEASURE1, VALUED_1, RFUNCT_3, FINSEQ_1, MESFUNC3, CARD_3, ZFMISC_1, SEQ_2, ORDINAL2, XCMPLX_0, XXREAL_2, SEQFUNC, PBOOLE, INTEGRA1, FINSET_1, MEMBERED, SETLIM_1, INTEGRA5, FUNCT_3, MESFUNC5, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, XXREAL_2, XXREAL_3, REAL_1, RELAT_1, FUNCT_1, FINSEQ_1, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, INT_1, NAT_D, RAT_1, MEMBERED, SUPINF_1, SUPINF_2, MEASURE1, EXTREAL1, NAT_1, MESFUNC1, MESFUNC2, MESFUNC3, FINSEQOP, RFUNCT_3, PROB_1, MEASURE6, NEWTON, SEQFUNC, SETLIM_1, VALUED_0;
definitions TARSKI, XBOOLE_0, FINSEQ_1, SUPINF_2;
theorems MEASURE1, MEASURE2, TARSKI, PARTFUN1, FUNCT_1, FUNCT_2, MEASURE6, NAT_1, SUPINF_2, RELSET_1, EXTREAL1, INT_1, MESFUNC1, FINSEQ_1, XREAL_0, PROB_1, PROB_2, XBOOLE_0, NAT_2, XBOOLE_1, XCMPLX_1, MESFUNC2, MESFUNC3, NEWTON, XREAL_1, PREPOWER, XXREAL_0, MESFUNC4, ZFMISC_1, SETLIM_1, FINSEQ_3, RAT_1, FUNCT_3, RELAT_1, FINSUB_1, GRFUNC_1, FINSEQ_2, ORDINAL1, NAT_D, NUMBERS, CARD_1, XXREAL_2, VALUED_0, XXREAL_3, KURATO_0;
schemes CLASSES1, FUNCT_2, FINSEQ_1, FINSEQ_2, NAT_1, SEQFUNC, PARTFUN1;
registrations SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, RAT_1, MEMBERED, COMPLEX1, FINSEQ_1, MEASURE1, VALUED_0, XXREAL_2, XXREAL_3, XCMPLX_0, NEWTON, EXTREAL1, SUPINF_2;
constructors HIDDEN, WELLORD2, REAL_1, SQUARE_1, NAT_D, FINSEQOP, LIMFUNC1, SEQFUNC, NEWTON, RFUNCT_3, MEASURE6, EXTREAL1, MESFUNC1, BINARITH, MESFUNC2, KURATO_0, MESFUNC3, SETLIM_1, SUPINF_1, RELSET_1, XREAL_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, FINSEQ_1, CARD_3, XXREAL_3, SUPINF_2;
expansions TARSKI, XBOOLE_0, SUPINF_2;
reconsider jj = 1 as Real ;
Lm1:
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,ExtREAL holds
( max+ f is nonnegative & max- f is nonnegative & |.f.| is nonnegative )
Lm2:
for Y being set
for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in Y ) holds
p is FinSequence of Y
Lm3:
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,ExtREAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
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,ExtREAL
for r being Real st dom f in S & ( for x being object st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
Lm5:
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,ExtREAL
for r being Real holds A /\ (less_dom (f,r)) = less_dom ((f | A),r)
Lm6:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for f being PartFunc of X,ExtREAL holds
( f | A is_measurable_on A iff f is_measurable_on A )
Lm7:
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,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) & dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG )
Lm8:
for J being ExtREAL_sequence holds
( not J is () or sup (rng J) in REAL or sup (rng J) = +infty )
Lm9:
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,ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative & ( for x being set st x in dom f holds
g . x <= f . x ) holds
( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
let f be
PartFunc of
X,
ExtREAL;
assume that A1:
ex
A being
Element of
S st
(
A = dom f &
f is_measurable_on A )
and A2:
f is
nonnegative
;
existence
ex b1 being Element of ExtREAL ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b1 = lim K )
uniqueness
for b1, b2 being Element of ExtREAL st ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b1 = lim K ) & ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b2 = lim K ) holds
b1 = b2
end;
Lm10:
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,ExtREAL st ex A being Element of S st
( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) & f is nonnegative & g is nonnegative holds
integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))
Lm11:
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,ExtREAL st ex E0 being Element of S st
( dom (f + g) = E0 & f + g is_measurable_on E0 ) & f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
Lm12:
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,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds
ex E, NFG, NFPG being Element of S st
( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is_measurable_on E & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is_measurable_on E & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is_measurable_on E & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
Lm13:
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,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds
( f + g is_integrable_on M & Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g)) )