:: 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 Association of Mizar Users

theorem Th61a: :: 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)

proof end;

theorem limseq1b: :: 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 & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k )

proof end;

theorem limseq1: :: 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 & lim_sup seq1 <= lim_sup seq2 )

proof end;

theorem Th63a: :: 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

proof end;

theorem Th63b: :: 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

proof end;

theorem inferiorf1a: :: 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)

proof end;

theorem Th135: :: 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 ) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & Integral M,(lim_inf F) <= lim_inf I )

proof end;

theorem SUPINF226a: :: MESFUN10:8

for X, Y being non empty Subset of ExtREAL
for r being R_eal st X = {r} & r in REAL holds
sup (X + Y) = (sup X) + (sup Y)

proof end;

theorem SUPINF227a: :: MESFUN10:9

for X, Y being non empty Subset of ExtREAL
for r being R_eal st X = {r} & r in REAL holds
inf (X + Y) = (inf X) + (inf Y)

proof end;

theorem limseq2: :: MESFUN10:10

for seq1, seq2 being ExtREAL_sequence
for r being R_eal st r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) holds
( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) )

proof end;

theorem limfunc2: :: 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 ) & F1 is with_the_same_dom & F2 is with_the_same_dom & f " {+infty } = {} & f " {-infty } = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds
( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) )

proof end;

theorem :: MESFUN10:12

canceled;

theorem Th114a: :: 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 & g is_integrable_on M holds
f - g is_integrable_on M

proof end;

theorem Th115a: :: MESFUN10:14

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 & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f - g) = (Integral M,(f | E)) + (Integral M,((- g) | E)) )

proof end;

theorem supinfa: :: MESFUN10:15

for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n = - (seq2 . n) ) holds
( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) )

proof end;

theorem supinfb: :: MESFUN10:16

for X being non empty set
for F1, F2 being Functional_Sequence of X,ExtREAL st dom (F1 . 0 ) = dom (F2 . 0 ) & F1 is with_the_same_dom & F2 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) holds
( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) )

proof end;

theorem Th136z: :: 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 ) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( 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 ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )

proof end;

Th136: 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 ) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom P,+infty = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & lim_inf I >= Integral M,(lim_inf F) & lim_sup I <= Integral M,(lim_sup F) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral M,(lim F) ) ) )

proof end;

theorem Th136x: :: 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
for P being PartFunc of X, ExtREAL st E = dom (F . 0 ) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( 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) ) & lim_inf I >= Integral M,(lim_inf F) & lim_sup I <= Integral M,(lim_sup F) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral M,(lim F) ) ) )

proof end;

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 E = dom (F . 0 ) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral M,((F . 0 ) | E) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & lim I = Integral M,(lim F) )

proof end;

definition

let X be set ;
let F be Functional_Sequence of X,ExtREAL ;
attr F is uniformly_bounded means :DefUB: :: 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 DefUB 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 );

theorem :: MESFUN10:20

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 & E = dom (F . 0 ) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( 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 ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & lim I = Integral M,(lim F) ) )

proof end;

definition

let X be set ;
let F be Functional_Sequence of X,ExtREAL ;
let f be PartFunc of X, ExtREAL ;
pred F is_uniformly_convergent_to f means :DefUC: :: MESFUN10:def 2
( F is with_the_same_dom & dom (F . 0 ) = dom f & ( 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 & x in dom (F . 0 ) holds
|.(((F . n) . x) - (f . x)).| < e ) );

end;

:: deftheorem DefUC 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 & dom (F . 0 ) = dom f & ( 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 & x in dom (F . 0 ) holds
|.(((F . n) . x) - (f . x)).| < e ) ) );

theorem UCONV: :: MESFUN10:21

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 & lim (F1 # x) = f . x )

proof end;

theorem :: MESFUN10:22

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 & E = dom (F . 0 ) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & lim I = Integral M,f ) )

proof end;