:: The Lebesgue Monotone Convergence Theorem
:: by Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: MESFUNC9:1
theorem Th2: :: MESFUNC9:2
theorem Th3: :: MESFUNC9:3
theorem Th4: :: MESFUNC9:4
theorem :: MESFUNC9:5
theorem :: MESFUNC9:6
theorem Th7: :: MESFUNC9:7
theorem Th8: :: MESFUNC9:8
theorem Th9: :: MESFUNC9:9
theorem Th10: :: MESFUNC9:10
theorem Th11: :: MESFUNC9:11
theorem Th12: :: MESFUNC9:12
theorem Th13: :: MESFUNC9:13
theorem :: MESFUNC9:14
theorem Th15: :: MESFUNC9:15
:: deftheorem Def1 defines Partial_Sums MESFUNC9:def 1 :
:: deftheorem Def2 defines summable MESFUNC9:def 2 :
:: deftheorem defines Sum MESFUNC9:def 3 :
theorem Th16: :: MESFUNC9:16
theorem :: MESFUNC9:17
theorem Th18: :: MESFUNC9:18
theorem Th19: :: MESFUNC9:19
theorem Th20: :: MESFUNC9:20
theorem Th21: :: MESFUNC9:21
:: 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: :: MESFUNC9:22
theorem Th23: :: MESFUNC9:23
theorem :: MESFUNC9:24
theorem Th25: :: MESFUNC9:25
theorem :: MESFUNC9:26
theorem Th27: :: MESFUNC9:27
theorem Th28: :: MESFUNC9:28
theorem Th29: :: MESFUNC9:29
theorem Th30: :: MESFUNC9:30
theorem Th31: :: MESFUNC9:31
theorem Th32: :: MESFUNC9:32
theorem Th33: :: MESFUNC9:33
theorem Th34: :: MESFUNC9:34
theorem Th35: :: MESFUNC9:35
theorem Th36: :: MESFUNC9:36
theorem Th37: :: MESFUNC9:37
theorem Th38: :: MESFUNC9:38
theorem Th39: :: MESFUNC9:39
theorem :: MESFUNC9:40
theorem Th41: :: MESFUNC9:41
theorem Th42: :: MESFUNC9:42
theorem Th43: :: MESFUNC9:43
theorem Th44: :: MESFUNC9:44
theorem :: MESFUNC9:45
theorem Th46: :: MESFUNC9:46
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 :: MESFUNC9:47
theorem :: MESFUNC9:48
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 :: MESFUNC9:def 6
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 :: MESFUNC9:def 7
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:
:: MESFUNC9:def 8
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:
:: MESFUNC9:def 9
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: :: MESFUNC9:49
theorem Th50: :: MESFUNC9:50
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: :: MESFUNC9:51
theorem :: MESFUNC9:52