:: 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 Th1: :: MESFUN9C:1
theorem Th2: :: MESFUN9C:2
theorem Th3: :: MESFUN9C:3
theorem Th4: :: MESFUN9C:4
theorem Th5: :: MESFUN9C:5
theorem Th6: :: MESFUN9C:6
:: deftheorem Def2 defines Partial_Sums MESFUN9C:def 2 :
theorem Th7: :: MESFUN9C:7
theorem Th8: :: MESFUN9C:8
theorem Th9: :: MESFUN9C:9
theorem Th10: :: MESFUN9C:10
theorem Th11: :: MESFUN9C:11
theorem Th12: :: MESFUN9C:12
theorem Th13: :: MESFUN9C:13
theorem Th14: :: MESFUN9C:14
theorem Th15: :: MESFUN9C:15
theorem Th16: :: MESFUN9C:16
theorem Th17: :: MESFUN9C:17
theorem Th18: :: MESFUN9C:18
theorem Th19: :: MESFUN9C:19
theorem Th20: :: MESFUN9C:20
Lm1:
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 Th21: :: MESFUN9C:21
theorem Th22: :: MESFUN9C:22
theorem Th23: :: MESFUN9C:23
theorem Th24: :: MESFUN9C:24
theorem Th25: :: MESFUN9C:25
theorem :: MESFUN9C:26
theorem :: MESFUN9C:27
theorem :: MESFUN9C:28
:: deftheorem Def3 defines Partial_Sums MESFUN9C:def 3 :
theorem Th29: :: MESFUN9C:29
theorem :: MESFUN9C:30
theorem :: MESFUN9C:31
theorem Th32: :: MESFUN9C:32
theorem :: MESFUN9C:33
theorem Th34: :: MESFUN9C:34
theorem Th35: :: MESFUN9C:35
theorem :: MESFUN9C:36
theorem :: MESFUN9C:37
Lm2:
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 Th46: :: MESFUN9C:46
theorem Th47: :: MESFUN9C:47
theorem Th48: :: MESFUN9C:48
:: deftheorem Def4 defines uniformly_bounded MESFUN9C:def 4 :
theorem Th49: :: MESFUN9C:49
:: deftheorem Def5 defines is_uniformly_convergent_to MESFUN9C:def 5 :
theorem Th50: :: MESFUN9C:50
theorem Th51: :: MESFUN9C:51
theorem :: MESFUN9C:52
:: deftheorem Def6 defines uniformly_bounded MESFUN9C:def 6 :
theorem :: MESFUN9C:53
:: deftheorem Def7 defines is_uniformly_convergent_to MESFUN9C:def 7 :
theorem :: MESFUN9C:54