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

:: 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) & ( 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 );

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