:: 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 Th1: :: MESFUN10:1
theorem Th2: :: MESFUN10:2
theorem Th3: :: MESFUN10:3
theorem Th4: :: MESFUN10:4
theorem Th5: :: MESFUN10:5
theorem Th6: :: MESFUN10:6
theorem Th7: :: MESFUN10:7
theorem Th8: :: MESFUN10:8
theorem Th9: :: MESFUN10:9
theorem Th10: :: MESFUN10:10
theorem Th11: :: MESFUN10:11
theorem :: MESFUN10:12
canceled;
theorem Th13: :: MESFUN10:13
theorem Th14: :: MESFUN10:14
theorem Th15: :: MESFUN10:15
theorem Th16: :: MESFUN10:16
theorem Th17: :: MESFUN10:17
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_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) ) ) )
theorem Th18: :: MESFUN10:18
theorem :: MESFUN10:19
:: deftheorem Def1 defines uniformly_bounded MESFUN10:def 1 :
theorem :: MESFUN10:20
:: deftheorem Def2 defines is_uniformly_convergent_to MESFUN10:def 2 :
theorem Th21: :: MESFUN10:21
theorem :: MESFUN10:22