begin
begin
begin
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)
begin
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