begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
begin
:: deftheorem Def1 defines Partial_Sums MESFUNC9:def 1 :
:: deftheorem Def2 defines summable MESFUNC9:def 2 :
:: deftheorem defines Sum MESFUNC9:def 3 :
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
:: deftheorem Def4 defines Partial_Sums MESFUNC9:def 4 :
:: deftheorem Def5 defines additive MESFUNC9:def 5 :
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)
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem Th46:
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 )
theorem
theorem
definition
let C,
D,
X be non
empty set ;
let F be
Function of
[:C,D:],
X;
let c be
Element of
C;
func ProjMap1 F,
c -> Function of
D,
X means
for
d being
Element of
D holds
it . d = F . c,
d;
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;
:: deftheorem defines ProjMap1 MESFUNC9:def 6 :
definition
let C,
D,
X be non
empty set ;
let F be
Function of
[:C,D:],
X;
let d be
Element of
D;
func ProjMap2 F,
d -> Function of
C,
X means
for
c being
Element of
C holds
it . c = F . c,
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;
:: deftheorem defines ProjMap2 MESFUNC9:def 7 :
definition
let X,
Y be
set ;
let F be
Function of
[:NAT ,NAT :],
(PFuncs X,Y);
let n be
Nat;
func ProjMap1 F,
n -> Functional_Sequence of
X,
Y means :
Def8:
for
m being
Nat holds
it . m = F . n,
m;
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
func ProjMap2 F,
n -> Functional_Sequence of
X,
Y means :
Def9:
for
m being
Nat holds
it . m = F . m,
n;
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;
:: deftheorem Def8 defines ProjMap1 MESFUNC9:def 8 :
:: deftheorem Def9 defines ProjMap2 MESFUNC9:def 9 :
theorem Th49:
theorem Th50:
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 )
theorem Th51:
theorem