:: 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 M5th22: :: MESFUNC9:1
theorem M5th23: :: MESFUNC9:2
theorem ADD1a: :: MESFUNC9:3
theorem ADD1b: :: MESFUNC9:4
theorem :: MESFUNC9:5
theorem :: MESFUNC9:6
theorem LIM: :: MESFUNC9:7
theorem LIM2a: :: MESFUNC9:8
theorem LIM3: :: MESFUNC9:9
theorem LIM3a: :: MESFUNC9:10
theorem LIM2: :: MESFUNC9:11
theorem Lm16: :: MESFUNC9:12
theorem Lem13: :: MESFUNC9:13
theorem :: MESFUNC9:14
theorem Prop3: :: MESFUNC9:15
:: deftheorem Def1 defines Partial_Sums MESFUNC9:def 1 :
:: deftheorem Def2 defines summable MESFUNC9:def 2 :
:: deftheorem defines Sum MESFUNC9:def 3 :
theorem ADD3a: :: MESFUNC9:16
theorem :: MESFUNC9:17
theorem Lm17: :: MESFUNC9:18
theorem Lm15: :: MESFUNC9:19
theorem Prop1: :: MESFUNC9:20
theorem Prop2: :: MESFUNC9:21
:: deftheorem Def0 defines Partial_Sums MESFUNC9:def 4 :
:: deftheorem Def1a defines additive MESFUNC9:def 5 :
Lem01:
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 Lem02: :: MESFUNC9:22
theorem Lem03: :: MESFUNC9:23
theorem :: MESFUNC9:24
theorem Lem05: :: MESFUNC9:25
theorem :: MESFUNC9:26
theorem Lem07b: :: MESFUNC9:27
theorem Lem07: :: MESFUNC9:28
theorem ADD0: :: MESFUNC9:29
theorem LIM4: :: MESFUNC9:30
theorem Lem09: :: MESFUNC9:31
theorem Cor00: :: MESFUNC9:32
theorem Cor01: :: MESFUNC9:33
theorem Cor02: :: MESFUNC9:34
theorem Lem10: :: MESFUNC9:35
theorem ADD3C: :: MESFUNC9:36
theorem ADD3D: :: MESFUNC9:37
theorem ADD3: :: MESFUNC9:38
theorem ADD1e: :: MESFUNC9:39
theorem :: MESFUNC9:40
theorem ADD1: :: MESFUNC9:41
theorem ADD4: :: MESFUNC9:42
theorem ADD5: :: MESFUNC9:43
theorem ADD2: :: MESFUNC9:44
theorem :: MESFUNC9:45
theorem FSUM3: :: MESFUNC9:46
Cor131a:
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 )
Cor131b:
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 :
defproj1:
:: 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 :
defproj2:
:: 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 defproj1 defines ProjMap1 MESFUNC9:def 8 :
:: deftheorem defproj2 defines ProjMap2 MESFUNC9:def 9 :
theorem Th131z: :: MESFUNC9:49
theorem FSUM2: :: MESFUNC9:50
Th131x:
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 Th131: :: MESFUNC9:51
theorem :: MESFUNC9:52