:: The Lebesgue Monotone Convergence Theorem
:: by Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received March 18, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: MESFUNC9:1
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & g is V120() holds
dom (f + g) = (dom f) /\ (dom g)
proof end;

theorem Th2: :: MESFUNC9:2
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & g is V119() holds
dom (f - g) = (dom f) /\ (dom g)
proof end;

theorem Th3: :: MESFUNC9:3
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V119() & g is V119() holds
f + g is V119()
proof end;

theorem Th4: :: MESFUNC9:4
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & g is V120() holds
f + g is V120()
proof end;

theorem :: MESFUNC9:5
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V119() & g is V120() holds
f - g is V119()
proof end;

theorem :: MESFUNC9:6
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & g is V119() holds
f - g is V120()
proof end;

theorem Th7: :: MESFUNC9:7
for seq being ExtREAL_sequence holds
( ( seq is convergent_to_finite_number implies ex g being real number st
( lim seq = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) ) ) & ( seq is convergent_to_+infty implies lim seq = +infty ) & ( seq is convergent_to_-infty implies lim seq = -infty ) )
proof end;

theorem Th8: :: MESFUNC9:8
for seq being ExtREAL_sequence st seq is V111() holds
not seq is convergent_to_-infty
proof end;

theorem Th9: :: MESFUNC9:9
for seq being ExtREAL_sequence
for p being ext-real number st seq is convergent & ( for k being Nat holds seq . k <= p ) holds
lim seq <= p
proof end;

theorem Th10: :: MESFUNC9:10
for seq being ExtREAL_sequence
for p being ext-real number st seq is convergent & ( for k being Nat holds p <= seq . k ) holds
p <= lim seq
proof end;

theorem Th11: :: MESFUNC9:11
for seq1, seq2, seq being ExtREAL_sequence st seq1 is convergent & seq2 is convergent & seq1 is V111() & seq2 is V111() & ( for k being Nat holds seq . k = (seq1 . k) + (seq2 . k) ) holds
( seq is V111() & seq is convergent & lim seq = (lim seq1) + (lim seq2) )
proof end;

theorem Th12: :: MESFUNC9:12
for X being non empty set
for G, F being Functional_Sequence of X,ExtREAL
for x being Element of X
for D being set st ( for n being Nat holds G . n = (F . n) | D ) & x in D holds
( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )
proof end;

theorem Th13: :: MESFUNC9:13
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 PartFunc of X,ExtREAL st E = dom f & f is_measurable_on E & f is nonnegative & M . (E /\ (eq_dom (f,+infty))) <> 0 holds
Integral (M,f) = +infty
proof end;

theorem :: MESFUNC9:14
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 holds
( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
proof end;

theorem Th15: :: MESFUNC9:15
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, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is_measurable_on E & g is_measurable_on E & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral (M,(f | E)) <= Integral (M,(g | E))
proof end;

begin

definition
let f be ext-real-valued Function;
let x be set ;
:: original: .
redefine func f . x -> Element of ExtREAL ;
coherence
f . x is Element of ExtREAL
by XXREAL_0:def 1;
end;

definition
let s be ext-real-valued Function;
func Partial_Sums s -> ExtREAL_sequence means :Def1: :: MESFUNC9:def 1
( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (s . (n + 1)) ) );
existence
ex b1 being ExtREAL_sequence st
( b1 . 0 = s . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being ExtREAL_sequence st b1 . 0 = s . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) & b2 . 0 = s . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Partial_Sums MESFUNC9:def 1 :
for s being ext-real-valued Function
for b2 being ExtREAL_sequence holds
( b2 = Partial_Sums s iff ( b2 . 0 = s . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) ) );

definition
let s be ext-real-valued Function;
attr s is summable means :Def2: :: MESFUNC9:def 2
Partial_Sums s is convergent ;
end;

:: deftheorem Def2 defines summable MESFUNC9:def 2 :
for s being ext-real-valued Function holds
( s is summable iff Partial_Sums s is convergent );

definition
let s be ext-real-valued Function;
func Sum s -> R_eal equals :: MESFUNC9:def 3
lim (Partial_Sums s);
correctness
coherence
lim (Partial_Sums s) is R_eal
;
;
end;

:: deftheorem defines Sum MESFUNC9:def 3 :
for s being ext-real-valued Function holds Sum s = lim (Partial_Sums s);

theorem Th16: :: MESFUNC9:16
for seq being ExtREAL_sequence st seq is V111() holds
( Partial_Sums seq is V111() & Partial_Sums seq is non-decreasing )
proof end;

theorem :: MESFUNC9:17
for seq being ExtREAL_sequence st ( for n being Nat holds 0 < seq . n ) holds
for m being Nat holds 0 < (Partial_Sums seq) . m
proof end;

theorem Th18: :: MESFUNC9:18
for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for D being set st F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | D ) holds
G is with_the_same_dom
proof end;

theorem Th19: :: MESFUNC9:19
for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for D being set st D c= dom (F . 0) & ( for n being Nat holds G . n = (F . n) | D ) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim G
proof end;

theorem Th20: :: MESFUNC9:20
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F, G being Functional_Sequence of X,ExtREAL
for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds
( F . m is_measurable_on E & G . m = (F . m) | E ) ) holds
G . n is_measurable_on E
proof end;

theorem Th21: :: MESFUNC9:21
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F, G being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & G is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) & ( for n being Nat holds G . n = (F . n) | E ) holds
for x being Element of X st x in E holds
G # x is summable
proof end;

begin

definition
let X be non empty set ;
let F be Functional_Sequence of X,ExtREAL;
func Partial_Sums F -> Functional_Sequence of X,ExtREAL means :Def4: :: MESFUNC9:def 4
( it . 0 = F . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (F . (n + 1)) ) );
existence
ex b1 being Functional_Sequence of X,ExtREAL st
( b1 . 0 = F . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of X,ExtREAL st b1 . 0 = F . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) & b2 . 0 = F . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (F . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Partial_Sums MESFUNC9:def 4 :
for X being non empty set
for F, b3 being Functional_Sequence of X,ExtREAL holds
( b3 = Partial_Sums F iff ( b3 . 0 = F . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . n) + (F . (n + 1)) ) ) );

definition
let X be set ;
let F be Functional_Sequence of X,ExtREAL;
attr F is additive means :Def5: :: MESFUNC9:def 5
for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty );
end;

:: deftheorem Def5 defines additive MESFUNC9:def 5 :
for X being set
for F being Functional_Sequence of X,ExtREAL holds
( F is additive iff for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) );

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)

proof end;

theorem Th22: :: MESFUNC9:22
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) & z in dom (F . m) )
proof end;

theorem Th23: :: MESFUNC9:23
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat
for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty holds
ex m being Nat st
( m <= n & (F . m) . z = +infty )
proof end;

theorem :: MESFUNC9:24
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty & m <= n holds
(F . m) . z <> -infty
proof end;

theorem Th25: :: MESFUNC9:25
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat
for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty holds
ex m being Nat st
( m <= n & (F . m) . z = -infty )
proof end;

theorem :: MESFUNC9:26
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty & m <= n holds
(F . m) . z <> +infty
proof end;

theorem Th27: :: MESFUNC9:27
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive holds
( (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} & (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} )
proof end;

theorem Th28: :: MESFUNC9:28
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive holds
dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
proof end;

theorem Th29: :: MESFUNC9:29
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive & F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)
proof end;

theorem Th30: :: MESFUNC9:30
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is nonnegative ) holds
F is additive
proof end;

theorem Th31: :: MESFUNC9:31
for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for D being set st F is additive & ( for n being Nat holds G . n = (F . n) | D ) holds
G is additive
proof end;

theorem Th32: :: MESFUNC9:32
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat
for x being Element of X
for D being set st F is additive & F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
proof end;

theorem Th33: :: MESFUNC9:33
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X
for D being set st F is additive & F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( ( Partial_Sums (F # x) is convergent_to_finite_number implies (Partial_Sums F) # x is convergent_to_finite_number ) & ( (Partial_Sums F) # x is convergent_to_finite_number implies Partial_Sums (F # x) is convergent_to_finite_number ) & ( Partial_Sums (F # x) is convergent_to_+infty implies (Partial_Sums F) # x is convergent_to_+infty ) & ( (Partial_Sums F) # x is convergent_to_+infty implies Partial_Sums (F # x) is convergent_to_+infty ) & ( Partial_Sums (F # x) is convergent_to_-infty implies (Partial_Sums F) # x is convergent_to_-infty ) & ( (Partial_Sums F) # x is convergent_to_-infty implies Partial_Sums (F # x) is convergent_to_-infty ) & ( Partial_Sums (F # x) is convergent implies (Partial_Sums F) # x is convergent ) & ( (Partial_Sums F) # x is convergent implies Partial_Sums (F # x) is convergent ) )
proof end;

theorem Th34: :: MESFUNC9:34
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL
for x being Element of X st F is additive & F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
proof end;

theorem Th35: :: MESFUNC9:35
for X being non empty set
for S being SigmaField of X
for F being Functional_Sequence of X,ExtREAL
for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
( F is additive & (Partial_Sums F) . n is_simple_func_in S )
proof end;

theorem Th36: :: MESFUNC9:36
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st ( for m being Nat holds F . m is nonnegative ) holds
(Partial_Sums F) . n is nonnegative
proof end;

theorem Th37: :: MESFUNC9:37
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for k being Nat holds F . k is nonnegative ) & n <= m holds
((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x
proof end;

theorem Th38: :: MESFUNC9:38
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for m being Nat holds F . m is nonnegative ) holds
( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent )
proof end;

theorem Th39: :: MESFUNC9:39
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st ( for m being Nat holds F . m is V119() ) holds
(Partial_Sums F) . n is V119()
proof end;

theorem :: MESFUNC9:40
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st ( for m being Nat holds F . m is V120() ) holds
(Partial_Sums F) . n is V120()
proof end;

theorem Th41: :: MESFUNC9:41
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for m being Nat st ( for n being Nat holds
( F . n is_measurable_on E & F . n is V119() ) ) holds
(Partial_Sums F) . m is_measurable_on E
proof end;

theorem Th42: :: MESFUNC9:42
for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for n being Nat
for x being Element of X st F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in (dom (F . 0)) /\ (dom (G . 0)) & ( for k being Nat
for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds
(F . k) . y <= (G . k) . y ) holds
((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
proof end;

theorem Th43: :: MESFUNC9:43
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom holds
Partial_Sums F is with_the_same_dom
proof end;

theorem Th44: :: MESFUNC9:44
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st dom (F . 0) = E & F is additive & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
proof end;

theorem :: MESFUNC9:45
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
proof end;

theorem Th46: :: MESFUNC9:46
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 I being ExtREAL_sequence
for m being Nat st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral (M,(F . n)) ) ) holds
Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m
proof end;

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 )

proof end;

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 )

proof end;

theorem :: MESFUNC9:47
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 & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( 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 )
proof end;

theorem :: MESFUNC9:48
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 PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is_measurable_on E holds
ex g being Functional_Sequence of X,ExtREAL st
( g is additive & ( for n being Nat holds
( g . n is_simple_func_in S & g . n is nonnegative & g . n is_measurable_on E ) ) & ( for x being Element of X st x in E holds
( g # x is summable & f . x = Sum (g # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((g . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
proof end;

registration
let X be non empty set ;
cluster non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total with_the_same_dom additive for Element of bool [:NAT,(PFuncs (X,ExtREAL)):];
existence
ex b1 being Functional_Sequence of X,ExtREAL st
( b1 is additive & b1 is with_the_same_dom )
proof end;
end;

definition
let C, D, X be non empty set ;
let F be Function of [:C,D:],(PFuncs (X,ExtREAL));
let c be Element of C;
let d be Element of D;
:: original: .
redefine func F . (c,d) -> PartFunc of X,ExtREAL;
correctness
coherence
F . (c,d) is PartFunc of X,ExtREAL
;
proof end;
end;

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)
proof end;
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
proof end;
end;

:: deftheorem defines ProjMap1 MESFUNC9:def 6 :
for C, D, X being non empty set
for F being Function of [:C,D:],X
for c being Element of C
for b6 being Function of D,X holds
( b6 = ProjMap1 (F,c) iff for d being Element of D holds b6 . d = F . (c,d) );

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)
proof end;
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
proof end;
end;

:: deftheorem defines ProjMap2 MESFUNC9:def 7 :
for C, D, X being non empty set
for F being Function of [:C,D:],X
for d being Element of D
for b6 being Function of C,X holds
( b6 = ProjMap2 (F,d) iff for c being Element of C holds b6 . c = F . (c,d) );

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)
proof end;
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
proof end;
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)
proof end;
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
proof end;
end;

:: deftheorem Def8 defines ProjMap1 MESFUNC9:def 8 :
for X, Y being set
for F being Function of [:NAT,NAT:],(PFuncs (X,Y))
for n being Nat
for b5 being Functional_Sequence of X,Y holds
( b5 = ProjMap1 (F,n) iff for m being Nat holds b5 . m = F . (n,m) );

:: deftheorem Def9 defines ProjMap2 MESFUNC9:def 9 :
for X, Y being set
for F being Function of [:NAT,NAT:],(PFuncs (X,Y))
for n being Nat
for b5 being Functional_Sequence of X,Y holds
( b5 = ProjMap2 (F,n) iff for m being Nat holds b5 . m = F . (m,n) );

definition
let X be non empty set ;
let F be Function of NAT,(Funcs (NAT,(PFuncs (X,ExtREAL))));
let n be Nat;
:: original: .
redefine func F . n -> Functional_Sequence of X,ExtREAL;
correctness
coherence
F . n is Functional_Sequence of X,ExtREAL
;
proof end;
end;

theorem Th49: :: MESFUNC9:49
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) holds
ex FF being Function of NAT,(Funcs (NAT,(PFuncs (X,ExtREAL)))) st
for n being Nat holds
( ( for m being Nat holds
( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonnegative ) & ( for j, k being Nat st j <= k holds
for x being Element of X st x in dom (F . n) holds
((FF . n) . j) . x <= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds
( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )
proof end;

theorem Th50: :: MESFUNC9:50
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_measurable_on E & F . n is nonnegative ) ) holds
ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )
proof 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 )

proof end;

theorem Th51: :: MESFUNC9:51
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 c= 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 )
proof end;

:: Lebesgue Monotone Convergence Theorem
:: WP: Lebesgue's Monotone Convergence Theorem
theorem :: MESFUNC9:52
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 . 0 is nonnegative & F is with_the_same_dom & ( for n being Nat holds F . n is_measurable_on E ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )
proof end;