:: 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 Th7a: :: 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 COM21r: :: MESFUN6C:2
theorem COM21: :: MESFUN6C:3
theorem COM21c: :: MESFUN6C:4
theorem COM19: :: MESFUN6C:5
theorem COM48: :: MESFUN6C:6
theorem COM91: :: MESFUN6C:7
theorem COM99: :: 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 Th21: :: 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 AS:
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 Th100a: :: MESFUN6C:19
theorem Th88a: :: MESFUN6C:20
theorem :: MESFUN6C:21
theorem :: MESFUN6C:22
theorem Th91: :: MESFUN6C:23
theorem :: MESFUN6C:24
theorem :: MESFUN6C:25
:: deftheorem Def7 defines to_power MESFUN6C:def 6 :
theorem Lm648: :: MESFUN6C:26
theorem Lm648a: :: MESFUN6C:27
theorem MES121: :: MESFUN6C:28
theorem MES714: :: MESFUN6C:29
theorem MES648: :: MESFUN6C:30
theorem Th94: :: MESFUN6C:31
theorem :: MESFUN6C:32
theorem Th100: :: MESFUN6C:33
theorem Th100x: :: MESFUN6C:34
theorem :: MESFUN6C:35
theorem Th101: :: MESFUN6C:36
theorem :: MESFUN6C:37
theorem Th102r: :: MESFUN6C:38
theorem Th102c: :: MESFUN6C:39
theorem Th102: :: MESFUN6C:40
Th95a:
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 MES72: :: MESFUN6C:41
theorem MES73: :: MESFUN6C:42
Th95b:
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