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

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

:: 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) & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) 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 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)

proof end;

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)

proof end;

theorem Th10: :: 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 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) & F1 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;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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

proof end;

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 & 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 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) & lim_sup seq2 = - (lim_inf seq1) )

proof end;

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) & F1 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 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) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( 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;

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) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & 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;

:: 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) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & 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: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) & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( 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 :: MESFUN10:def 1
ex K being Real st
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K;

end;

:: deftheorem 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 st
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K );

:: 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 & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & 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 :: MESFUN10:def 2
( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being Real 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 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 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 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 & lim (F1 # x) = f . x )

proof end;

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 & 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;