:: 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
theorem limseq1b: :: MESFUN10:2
theorem limseq1: :: MESFUN10:3
theorem Th63a: :: MESFUN10:4
theorem Th63b: :: MESFUN10:5
theorem inferiorf1a: :: MESFUN10:6
theorem Th135: :: MESFUN10:7
theorem SUPINF226a: :: MESFUN10:8
theorem SUPINF227a: :: MESFUN10:9
theorem limseq2: :: MESFUN10:10
theorem limfunc2: :: MESFUN10:11
theorem :: MESFUN10:12
canceled;
theorem Th114a: :: MESFUN10:13
theorem Th115a: :: MESFUN10:14
theorem supinfa: :: MESFUN10:15
theorem supinfb: :: MESFUN10:16
theorem Th136z: :: MESFUN10:17
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) ) ) )
theorem Th136x: :: MESFUN10:18
theorem :: MESFUN10:19
:: deftheorem DefUB defines uniformly_bounded MESFUN10:def 1 :
theorem :: MESFUN10:20
:: deftheorem DefUC defines is_uniformly_convergent_to MESFUN10:def 2 :
theorem UCONV: :: MESFUN10:21
theorem :: MESFUN10:22