:: Fatou's Lemma and the {L}ebesgue's Convergence Theorem
:: by Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received July 22, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: MESFUN10:1
for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n <= seq2 . n ) holds
inf (rng seq1) <= inf (rng seq2)
proofend;

theorem Th2: :: MESFUN10:2
for seq1, seq2 being ExtREAL_sequence
for k being Nat st ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k &amp; (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k )
proofend;

theorem Th3: :: MESFUN10:3
for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( lim_inf seq1 <= lim_inf seq2 &amp; lim_sup seq1 <= lim_sup seq2 )
proofend;

theorem Th4: :: MESFUN10:4
for seq being ExtREAL_sequence
for a being R_eal st ( for n being Nat holds seq . n >= a ) holds
inf seq >= a
proofend;

theorem Th5: :: MESFUN10:5
for seq being ExtREAL_sequence
for a being R_eal st ( for n being Nat holds seq . n <= a ) holds
sup seq <= a
proofend;

theorem Th6: :: MESFUN10:6
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for x being Element of X
for n being Element of NAT st x in dom (inf (F ^\ n)) holds
(inf (F ^\ n)) . x = inf ((F # x) ^\ n)
proofend;

:: [WP: ] Fatou's_Lemma
theorem Th7: :: MESFUN10:7
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S st E = dom (F . 0) &amp; ( for n being Nat holds
( F . n is nonnegative &amp; F . n is_measurable_on E ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; Integral (M,(lim_inf F)) <= lim_inf I )
proofend;

begin

theorem Th8: :: MESFUN10:8
for Y being non empty Subset of ExtREAL
for r being R_eal st r in REAL holds
sup ({r} + Y) = (sup {r}) + (sup Y)
proofend;

theorem Th9: :: MESFUN10:9
for Y being non empty Subset of ExtREAL
for r being R_eal st r in REAL holds
inf ({r} + Y) = (inf {r}) + (inf Y)
proofend;

theorem Th10: :: MESFUN10:10
for seq1, seq2 being ExtREAL_sequence
for r being R_eal st r in REAL &amp; ( for n being Nat holds seq1 . n = r + (seq2 . n) ) holds
( lim_inf seq1 = r + (lim_inf seq2) &amp; lim_sup seq1 = r + (lim_sup seq2) )
proofend;

theorem Th11: :: MESFUN10:11
for X being non empty set
for F1, F2 being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) &amp; F1 is with_the_same_dom &amp; f " {+infty} = {} &amp; f " {-infty} = {} &amp; ( for n being Nat holds F1 . n = f + (F2 . n) ) holds
( lim_inf F1 = f + (lim_inf F2) &amp; lim_sup F1 = f + (lim_sup F2) )
proofend;

theorem Th12: :: MESFUN10:12
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M &amp; g is_integrable_on M holds
f - g is_integrable_on M
proofend;

theorem Th13: :: MESFUN10:13
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M &amp; g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) &amp; Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
proofend;

theorem Th14: :: MESFUN10:14
for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n = - (seq2 . n) ) holds
( lim_inf seq2 = - (lim_sup seq1) &amp; lim_sup seq2 = - (lim_inf seq1) )
proofend;

theorem Th15: :: MESFUN10:15
for X being non empty set
for F1, F2 being Functional_Sequence of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) &amp; F1 is with_the_same_dom &amp; ( for n being Nat holds F1 . n = - (F2 . n) ) holds
( lim_inf F1 = - (lim_sup F2) &amp; lim_sup F1 = - (lim_inf F2) )
proofend;

theorem Th16: :: MESFUN10:16
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) &amp; E = dom P &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; P is_integrable_on M &amp; ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) &amp; |.(lim_inf F).| is_integrable_on M &amp; |.(lim_sup F).| is_integrable_on M )
proofend;

Lm1:  for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) &amp; E = dom P &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; P is_integrable_on M &amp; P is nonnegative &amp; ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) &amp; eq_dom (P,+infty) = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; lim_inf I >= Integral (M,(lim_inf F)) &amp; lim_sup I <= Integral (M,(lim_sup F)) &amp; ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent &amp; lim I = Integral (M,(lim F)) ) ) )
proofend;

:: Lebesgue's Convergence theorem
theorem Th17: :: MESFUN10:17
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) &amp; E = dom P &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; P is_integrable_on M &amp; P is nonnegative &amp; ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; lim_inf I >= Integral (M,(lim_inf F)) &amp; lim_sup I <= Integral (M,(lim_sup F)) &amp; ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent &amp; lim I = Integral (M,(lim F)) ) ) )
proofend;

theorem :: MESFUN10:18
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S st E = dom (F . 0) &amp; ( for n being Nat holds
( F . n is nonnegative &amp; F . n is_measurable_on E ) ) &amp; ( for x being Element of X
for n, m being Nat st x in E &amp; n <= m holds
(F . n) . x >= (F . m) . x ) &amp; Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; I is convergent &amp; lim I = Integral (M,(lim F)) )
proofend;

definition
let X be set ;
let F be Functional_Sequence of X,ExtREAL;
attrF is uniformly_bounded  means :Def1: :: MESFUN10:def 1
 ex K being real number st
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K;
end;

:: deftheorem Def1 defines uniformly_bounded MESFUN10:def_1_:_
 for X being set
for F being Functional_Sequence of X,ExtREAL holds
( F is uniformly_bounded iff ex K being real number st
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K );

:: [WP: ] Lebesgue's_Bounded_Convergence_Theorem
theorem :: MESFUN10:19
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S st M . E < +infty &amp; E = dom (F . 0) &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; F is uniformly_bounded &amp; ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) &amp; lim F is_integrable_on M &amp; ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; I is convergent &amp; lim I = Integral (M,(lim F)) ) )
proofend;

definition
let X be set ;
let F be Functional_Sequence of X,ExtREAL;
let f be PartFunc of X,ExtREAL;
predF is_uniformly_convergent_to f means :Def2: :: MESFUN10:def 2
( F is with_the_same_dom &amp; dom (F . 0) = dom f &amp; ( for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being set st n >= N &amp; x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) );
end;

:: deftheorem Def2 defines is_uniformly_convergent_to MESFUN10:def_2_:_
 for X being set
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL holds
( F is_uniformly_convergent_to f iff ( F is with_the_same_dom &amp; dom (F . 0) = dom f &amp; ( for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being set st n >= N &amp; x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) ) );

theorem Th20: :: MESFUN10:20
for X being non empty set
for F1 being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds
for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent &amp; lim (F1 # x) = f . x )
proofend;

theorem :: MESFUN10:21
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
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 M . E < +infty &amp; E = dom (F . 0) &amp; ( for n being Nat holds F . n is_integrable_on M ) &amp; F is_uniformly_convergent_to f holds
( f is_integrable_on M &amp; ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; I is convergent &amp; lim I = Integral (M,f) ) )
proofend;