:: Lebesgue's Convergence Theorem of Complex-Valued Function
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received March 17, 2009
:: Copyright (c) 2009 Association of Mizar Users
:: deftheorem Def1 defines || MESFUN9C:def 1 :
theorem Th4: :: MESFUN9C:1
theorem Th8a: :: MESFUN9C:2
theorem Th919r: :: MESFUN9C:3
theorem Th9: :: MESFUN9C:4
theorem Lm10a: :: MESFUN9C:5
theorem Th10: :: MESFUN9C:6
:: deftheorem Def0 defines Partial_Sums MESFUN9C:def 2 :
theorem Lm11: :: MESFUN9C:7
theorem Th11: :: MESFUN9C:8
theorem Lem20: :: MESFUN9C:9
theorem Lem07: :: MESFUN9C:10
theorem ADD0: :: MESFUN9C:11
theorem Cor00: :: MESFUN9C:12
theorem Cor01: :: MESFUN9C:13
theorem Th934r: :: MESFUN9C:14
theorem Th16: :: MESFUN9C:15
theorem ADD1: :: MESFUN9C:16
theorem ADD5: :: MESFUN9C:17
theorem Th22: :: MESFUN9C:18
theorem Th23: :: MESFUN9C:19
theorem MES6C7: :: MESFUN9C:20
Lem30:
for X being non empty set
for D being set
for F being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
theorem Lm31: :: MESFUN9C:21
theorem Lm32: :: MESFUN9C:22
theorem M9C32c: :: MESFUN9C:23
theorem Lm33a: :: MESFUN9C:24
theorem Lm33b: :: MESFUN9C:25
theorem :: MESFUN9C:26
theorem :: MESFUN9C:27
theorem :: MESFUN9C:28
:: deftheorem Def0c defines Partial_Sums MESFUN9C:def 3 :
theorem Lm326: :: MESFUN9C:29
theorem :: MESFUN9C:30
theorem :: MESFUN9C:31
theorem ADD0c: :: MESFUN9C:32
theorem :: MESFUN9C:33
theorem ADD5c: :: MESFUN9C:34
theorem Cor01c: :: MESFUN9C:35
theorem :: MESFUN9C:36
theorem :: MESFUN9C:37
Lm1:
for X being non empty set
for S being SigmaField of X
for E being Element of S
for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
theorem :: MESFUN9C:38
theorem :: MESFUN9C:39
theorem :: MESFUN9C:40
theorem :: MESFUN9C:41
theorem :: MESFUN9C:42
theorem :: MESFUN9C:43
theorem :: MESFUN9C:44
theorem :: MESFUN9C:45
theorem MES1017e: :: MESFUN9C:46
theorem MES1017r: :: MESFUN9C:47
theorem MES1018r: :: MESFUN9C:48
:: deftheorem DefUBr defines uniformly_bounded MESFUN9C:def 4 :
theorem MES1020r: :: MESFUN9C:49
:: deftheorem DefUCr defines is_uniformly_convergent_to MESFUN9C:def 5 :
theorem MES1022r: :: MESFUN9C:50
theorem MES1017c: :: MESFUN9C:51
theorem :: MESFUN9C:52
:: deftheorem DefUBc defines uniformly_bounded MESFUN9C:def 6 :
theorem :: MESFUN9C:53
:: deftheorem DefUCc defines is_uniformly_convergent_to MESFUN9C:def 7 :
theorem :: MESFUN9C:54