:: The Lebesgue Monotone Convergence Theorem
:: by Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received March 18, 2008
:: Copyright (c) 2008-2011 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 without+infty & g is without+infty 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 without+infty & g is without-infty 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 without-infty & g is without-infty holds
f + g is without-infty

proof end;

theorem Th4: :: MESFUNC9:4

for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is without+infty & g is without+infty holds
f + g is without+infty

proof end;

theorem :: MESFUNC9:5

for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is without-infty & g is without+infty holds
f - g is without-infty

proof end;

theorem :: MESFUNC9:6

for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is without+infty & g is without-infty holds
f - g is without+infty

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 nonnegative 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 nonnegative & seq2 is nonnegative & ( for k being Nat holds seq . k = (seq1 . k) + (seq2 . k) ) holds
( seq is nonnegative & 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 b₁ being ExtREAL_sequence st
( b₁ . 0 = s . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) + (s . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being ExtREAL_sequence st b₁ . 0 = s . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) + (s . (n + 1)) ) & b₂ . 0 = s . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) + (s . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Partial_Sums MESFUNC9:def 1 :
for s being ext-real-valued Function
for b₂ being ExtREAL_sequence holds
( b₂ = Partial_Sums s iff ( b₂ . 0 = s . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . 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 nonnegative holds
( Partial_Sums seq is nonnegative & 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 b₁ being Functional_Sequence of X,ExtREAL st
( b₁ . 0 = F . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) + (F . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being Functional_Sequence of X,ExtREAL st b₁ . 0 = F . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) + (F . (n + 1)) ) & b₂ . 0 = F . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) + (F . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Partial_Sums MESFUNC9:def 4 :
for X being non empty set
for F, b₃ being Functional_Sequence of X,ExtREAL holds
( b₃ = Partial_Sums F iff ( b₃ . 0 = F . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . 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 without-infty ) holds
(Partial_Sums F) . n is without-infty

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 without+infty ) holds
(Partial_Sums F) . n is without+infty

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 without-infty ) ) 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 Element of bool [:NAT,(PFuncs (X,ExtREAL)):];
existence
ex b₁ being Functional_Sequence of X,ExtREAL st
( b₁ is additive & b₁ 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 b₁ being Function of D,X st
for d being Element of D holds b₁ . d = F . (c,d)

proof end;

uniqueness
for b₁, b₂ being Function of D,X st ( for d being Element of D holds b₁ . d = F . (c,d) ) & ( for d being Element of D holds b₂ . d = F . (c,d) ) holds
b₁ = b₂

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 b₆ being Function of D,X holds
( b₆ = ProjMap1 (F,c) iff for d being Element of D holds b₆ . 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 b₁ being Function of C,X st
for c being Element of C holds b₁ . c = F . (c,d)

proof end;

uniqueness
for b₁, b₂ being Function of C,X st ( for c being Element of C holds b₁ . c = F . (c,d) ) & ( for c being Element of C holds b₂ . c = F . (c,d) ) holds
b₁ = b₂

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 b₆ being Function of C,X holds
( b₆ = ProjMap2 (F,d) iff for c being Element of C holds b₆ . 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 b₁ being Functional_Sequence of X,Y st
for m being Nat holds b₁ . m = F . (n,m)

proof end;

uniqueness
for b₁, b₂ being Functional_Sequence of X,Y st ( for m being Nat holds b₁ . m = F . (n,m) ) & ( for m being Nat holds b₂ . m = F . (n,m) ) holds
b₁ = b₂

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 b₁ being Functional_Sequence of X,Y st
for m being Nat holds b₁ . m = F . (m,n)

proof end;

uniqueness
for b₁, b₂ being Functional_Sequence of X,Y st ( for m being Nat holds b₁ . m = F . (m,n) ) & ( for m being Nat holds b₂ . m = F . (m,n) ) holds
b₁ = b₂

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 b₅ being Functional_Sequence of X,Y holds
( b₅ = ProjMap1 (F,n) iff for m being Nat holds b₅ . 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 b₅ being Functional_Sequence of X,Y holds
( b₅ = ProjMap2 (F,n) iff for m being Nat holds b₅ . 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;

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;