environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PROB_1, MEASURE1, SUBSET_1, SEQFUNC, MESFUNC5, PARTFUN1, XXREAL_0, NAT_1, RELAT_1, ARYTM_3, ARYTM_1, FUNCT_1, ORDINAL2, CARD_1, COMPLEX1, SEQ_2, SUPINF_2, XXREAL_2, RINFSUP1, TARSKI, REAL_1, PBOOLE, MESFUNC1, VALUED_1, FUNCT_3, MESFUNC2, SUPINF_1, VALUED_0, RFUNCT_3, SERIES_1, CARD_3, MESFUNC8, MSSUBFAM, SETFAM_1, INTEGRA5, FUNCOP_1, ZFMISC_1, FUNCT_2, MEASURE2, MESFUNC9, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, VALUED_0, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, FUNCT_2, PARTFUN1, NAT_1, PROB_1, SETFAM_1, SUPINF_1, SUPINF_2, XXREAL_2, MEASURE1, MEASURE2, EXTREAL1, MESFUNC1, MEASURE6, MESFUNC2, SEQFUNC, MESFUNC5, MESFUNC8, RINFSUP2, FUNCOP_1;
definitions MESFUNC5, MESFUNC8, TARSKI, VALUED_0;
theorems TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, MESFUNC1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, MESFUNC2, XREAL_1, XXREAL_0, MESFUNC5, PROB_1, NAT_1, RELAT_1, FUNCT_3, ZFMISC_1, FUNCT_2, MEASURE1, MESFUNC6, SEQFUNC, ORDINAL1, SETFAM_1, MESFUNC8, RINFSUP2, MESFUNC7, SEQ_4, RELSET_1, MEASURE2, XXREAL_2, VALUED_0, FUNCOP_1, XXREAL_3;
schemes FUNCT_2, NAT_1, BINOP_1, RECDEF_1, SEQFUNC, FUNCT_1;
registrations SUBSET_1, NAT_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, MEASURE1, FUNCT_2, RELAT_1, XBOOLE_0, NUMBERS, XXREAL_0, XCMPLX_0, MESFUNC8, FUNCT_1, VALUED_0, XXREAL_3, RELSET_1;
constructors HIDDEN, REAL_1, EXTREAL1, BINOP_1, NEWTON, MESFUNC1, MEASURE2, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC8, RINFSUP2, SUPINF_1, SEQFUNC, RELSET_1, BINOP_2, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities MESFUNC1, MESFUNC5, BINOP_1, RINFSUP2, XXREAL_3, SUPINF_2;
expansions MESFUNC5, MESFUNC8, TARSKI, FUNCT_2;
reconsider zz = 0 as ExtReal ;
reconsider jj = 1 as Real ;
Lm1:
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
z in dom ((Partial_Sums F) . m)
Lm2:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is_measurable_on E & E = {} & ( for n being Nat holds F . n is_simple_func_in S ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
Lm3:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is_measurable_on E & F is additive & E common_on_dom F & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
definition
let C,
D,
X be non
empty set ;
let F be
Function of
[:C,D:],
X;
let c be
Element of
C;
existence
ex b1 being Function of D,X st
for d being Element of D holds b1 . d = F . (c,d)
uniqueness
for b1, b2 being Function of D,X st ( for d being Element of D holds b1 . d = F . (c,d) ) & ( for d being Element of D holds b2 . d = F . (c,d) ) holds
b1 = b2
end;
definition
let C,
D,
X be non
empty set ;
let F be
Function of
[:C,D:],
X;
let d be
Element of
D;
existence
ex b1 being Function of C,X st
for c being Element of C holds b1 . c = F . (c,d)
uniqueness
for b1, b2 being Function of C,X st ( for c being Element of C holds b1 . c = F . (c,d) ) & ( for c being Element of C holds b2 . c = F . (c,d) ) holds
b1 = b2
end;
definition
let X,
Y be
set ;
let F be
Function of
[:NAT,NAT:],
(PFuncs (X,Y));
let n be
Nat;
existence
ex b1 being Functional_Sequence of X,Y st
for m being Nat holds b1 . m = F . (n,m)
uniqueness
for b1, b2 being Functional_Sequence of X,Y st ( for m being Nat holds b1 . m = F . (n,m) ) & ( for m being Nat holds b2 . m = F . (n,m) ) holds
b1 = b2
existence
ex b1 being Functional_Sequence of X,Y st
for m being Nat holds b1 . m = F . (m,n)
uniqueness
for b1, b2 being Functional_Sequence of X,Y st ( for m being Nat holds b1 . m = F . (m,n) ) & ( for m being Nat holds b2 . m = F . (m,n) ) holds
b1 = b2
end;
Lm4:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
:: Lebesgue's Monotone Convergence Theorem