:: Integral of Complex-Valued Measurable Function
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: MESFUN6C:1
:: deftheorem Def1 defines Re MESFUN6C:def 1 :
:: deftheorem Def2 defines Im MESFUN6C:def 2 :
:: deftheorem Def3 defines is_measurable_on MESFUN6C:def 3 :
theorem Th2: :: MESFUN6C:2
theorem Th3: :: MESFUN6C:3
theorem Th4: :: MESFUN6C:4
theorem Th5: :: MESFUN6C:5
theorem Th6: :: MESFUN6C:6
theorem Th7: :: MESFUN6C:7
theorem Th8: :: MESFUN6C:8
theorem :: MESFUN6C:9
theorem :: MESFUN6C:10
theorem :: MESFUN6C:11
theorem :: MESFUN6C:12
theorem :: MESFUN6C:13
theorem :: MESFUN6C:14
theorem :: MESFUN6C:15
theorem :: MESFUN6C:16
theorem Th17: :: MESFUN6C:17
theorem :: MESFUN6C:18
:: deftheorem Def4 defines is_integrable_on MESFUN6C:def 4 :
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
let f be
PartFunc of
X,
COMPLEX ;
assume A1:
f is_integrable_on M
;
func Integral M,
f -> complex number means :
Def5:
:: MESFUN6C:def 5
ex
R,
I being
Real st
(
R = Integral M,
(Re f) &
I = Integral M,
(Im f) &
it = R + (I * <i> ) );
existence
ex b1 being complex number ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & b1 = R + (I * <i> ) )
uniqueness
for b1, b2 being complex number st ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & b1 = R + (I * <i> ) ) & ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & b2 = R + (I * <i> ) ) holds
b1 = b2
;
end;
:: deftheorem Def5 defines Integral MESFUN6C:def 5 :
Lm1:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( max+ f is nonnegative & max- f is nonnegative )
theorem Th19: :: MESFUN6C:19
theorem Th20: :: MESFUN6C:20
theorem :: MESFUN6C:21
theorem :: MESFUN6C:22
theorem Th23: :: MESFUN6C:23
theorem :: MESFUN6C:24
theorem :: MESFUN6C:25
:: deftheorem Def6 defines to_power MESFUN6C:def 6 :
theorem Th26: :: MESFUN6C:26
theorem Th27: :: MESFUN6C:27
theorem Th28: :: MESFUN6C:28
theorem Th29: :: MESFUN6C:29
theorem Th30: :: MESFUN6C:30
theorem Th31: :: MESFUN6C:31
theorem :: MESFUN6C:32
theorem Th33: :: MESFUN6C:33
theorem Th34: :: MESFUN6C:34
theorem :: MESFUN6C:35
theorem Th36: :: MESFUN6C:36
theorem :: MESFUN6C:37
theorem Th38: :: MESFUN6C:38
theorem Th39: :: MESFUN6C:39
theorem Th40: :: MESFUN6C:40
Lm2:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral M,f = 0 holds
|.(Integral M,f).| <= Integral M,|.f.|
theorem Th41: :: MESFUN6C:41
theorem Th42: :: MESFUN6C:42
Lm3:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral M,f <> 0 holds
|.(Integral M,f).| <= Integral M,|.f.|
theorem :: MESFUN6C:43
:: deftheorem defines Integral_on MESFUN6C:def 7 :
theorem :: MESFUN6C:44
theorem :: MESFUN6C:45
theorem :: MESFUN6C:46
theorem :: MESFUN6C:47
theorem :: MESFUN6C:48
theorem :: MESFUN6C:49