:: Integral of Complex-Valued Measurable Function
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: MESFUN6C:1
for a, b being real number holds
( (R_EAL a) + (R_EAL b) = a + b & - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b )
proofend;

begin

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,COMPLEX;
let E be Element of S;
predf is_measurable_on E means :Def1: :: MESFUN6C:def 1
( Re f is_measurable_on E & Im f is_measurable_on E );
end;

:: deftheorem Def1 defines is_measurable_on MESFUN6C:def_1_:_
 for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for E being Element of S holds
( f is_measurable_on E iff ( Re f is_measurable_on E & Im f is_measurable_on E ) );

theorem Th2: :: MESFUN6C:2
for X being non empty set
for f being PartFunc of X,COMPLEX
for r being Real holds
( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
proofend;

theorem Th3: :: MESFUN6C:3
for X being non empty set
for f being PartFunc of X,COMPLEX
for c being complex number holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
proofend;

theorem Th4: :: MESFUN6C:4
for X being non empty set
for f being PartFunc of X,COMPLEX holds
( - (Im f) = Re (<i> (#) f) &amp; Re f = Im (<i> (#) f) )
proofend;

theorem Th5: :: MESFUN6C:5
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( Re (f + g) = (Re f) + (Re g) &amp; Im (f + g) = (Im f) + (Im g) )
proofend;

theorem Th6: :: MESFUN6C:6
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( Re (f - g) = (Re f) - (Re g) &amp; Im (f - g) = (Im f) - (Im g) )
proofend;

theorem Th7: :: MESFUN6C:7
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S holds
( (Re f) | A = Re (f | A) &amp; (Im f) | A = Im (f | A) )
proofend;

theorem Th8: :: MESFUN6C:8
for X being non empty set
for f being PartFunc of X,COMPLEX holds f = (Re f) + (<i> (#) (Im f))
proofend;

theorem :: MESFUN6C:9
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for B, A being Element of S st B c= A &amp; f is_measurable_on A holds
f is_measurable_on B
proofend;

theorem :: MESFUN6C:10
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A, B being Element of S st f is_measurable_on A &amp; f is_measurable_on B holds
f is_measurable_on A \/ B
proofend;

theorem :: MESFUN6C:11
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A &amp; g is_measurable_on A holds
f + g is_measurable_on A
proofend;

theorem :: MESFUN6C:12
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A &amp; g is_measurable_on A &amp; A c= dom g holds
f - g is_measurable_on A
proofend;

theorem :: MESFUN6C:13
for X being non empty set
for Y being set
for f, g being PartFunc of X,COMPLEX st Y c= dom (f + g) holds
( dom ((f | Y) + (g | Y)) = Y &amp; (f + g) | Y = (f | Y) + (g | Y) )
proofend;

theorem :: MESFUN6C:14
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for B, A being Element of S st f is_measurable_on B &amp; A = (dom f) /\ B holds
f | B is_measurable_on A
proofend;

theorem :: MESFUN6C:15
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX st dom f in S &amp; dom g in S holds
dom (f + g) in S
proofend;

theorem :: MESFUN6C:16
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
proofend;

theorem Th17: :: MESFUN6C:17
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being complex number
for A being Element of S st f is_measurable_on A &amp; A c= dom f holds
c (#) f is_measurable_on A
proofend;

theorem :: MESFUN6C:18
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds
for c being complex number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
proofend;

begin

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;
predf is_integrable_on M means :Def2: :: MESFUN6C:def 2
( Re f is_integrable_on M &amp; Im f is_integrable_on M );
end;

:: deftheorem Def2 defines is_integrable_on MESFUN6C:def_2_:_
 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 holds
( f is_integrable_on M iff ( Re f is_integrable_on M &amp; Im f is_integrable_on M ) );

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 :Def3: :: MESFUN6C:def 3
 ex R, I being Real st
( R = Integral (M,(Re f)) &amp; I = Integral (M,(Im f)) &amp; it = R + (I * <i>) );
existence
 ex b1 being complex number ex R, I being Real st
( R = Integral (M,(Re f)) &amp; I = Integral (M,(Im f)) &amp; b1 = R + (I * <i>) )
proofend;
uniqueness
 for b1, b2 being complex number st ex R, I being Real st
( R = Integral (M,(Re f)) &amp; I = Integral (M,(Im f)) &amp; b1 = R + (I * <i>) ) &amp; ex R, I being Real st
( R = Integral (M,(Re f)) &amp; I = Integral (M,(Im f)) &amp; b2 = R + (I * <i>) ) holds
b1 = b2 ;
end;

:: deftheorem Def3 defines Integral MESFUN6C:def_3_:_
 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 f is_integrable_on M holds
for b5 being complex number holds
( b5 = Integral (M,f) iff ex R, I being Real st
( R = Integral (M,(Re f)) &amp; I = Integral (M,(Im f)) &amp; b5 = R + (I * <i>) ) );

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 &amp; max- f is nonnegative )
proofend;

theorem Th19: :: MESFUN6C:19
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
for A being Element of S st ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; M . A = 0 holds
f | A is_integrable_on M
proofend;

theorem Th20: :: MESFUN6C:20
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,REAL
for E, A being Element of S st ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; M . A = 0 holds
f | A is_integrable_on M
proofend;

theorem :: MESFUN6C:21
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
for A being Element of S st ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; M . A = 0 holds
( f | A is_integrable_on M &amp; Integral (M,(f | A)) = 0 )
proofend;

theorem :: MESFUN6C:22
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
for E, A being Element of S st E = dom f &amp; f is_integrable_on M &amp; M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
proofend;

theorem Th23: :: MESFUN6C:23
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
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
proofend;

theorem :: MESFUN6C:24
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
for A, B being Element of S st f is_integrable_on M &amp; A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
proofend;

theorem :: MESFUN6C:25
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
for B, A being Element of S st f is_integrable_on M &amp; B = (dom f) \ A holds
( f | A is_integrable_on M &amp; Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
proofend;

definition
let k be real number ;
let X be non empty set ;
let f be PartFunc of X,REAL;
funcf to_power k ->  PartFunc of X,REAL means :Def4: :: MESFUN6C:def 4
( dom it = dom f &amp; ( for x being Element of X st x in dom it holds
it . x = (f . x) to_power k ) );
existence
 ex b1 being PartFunc of X,REAL st
( dom b1 = dom f &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = (f . x) to_power k ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of X,REAL st dom b1 = dom f &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = (f . x) to_power k ) &amp; dom b2 = dom f &amp; ( for x being Element of X st x in dom b2 holds
b2 . x = (f . x) to_power k ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines to_power MESFUN6C:def_4_:_
 for k being real number
for X being non empty set
for f, b4 being PartFunc of X,REAL holds
( b4 = f to_power k iff ( dom b4 = dom f &amp; ( for x being Element of X st x in dom b4 holds
b4 . x = (f . x) to_power k ) ) );

registration
let X be non empty set ;
cluster Relation-like X -defined REAL -valued Function-like V33() V34() V35() nonnegative for Element of K6(K7(X,REAL));
existence
 ex b1 being PartFunc of X,REAL st b1 is nonnegative
proofend;
end;

registration
let k be real non negative number ;
let X be non empty set ;
let f be nonnegative PartFunc of X,REAL;
clusterf to_power k ->  nonnegative ;
coherence
 f to_power k is nonnegative
proofend;
end;

theorem Th26: :: MESFUN6C:26
for k being real number
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative &amp; 0 <= k holds
f to_power k is nonnegative ;

theorem Th27: :: MESFUN6C:27
for x being set
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
proofend;

theorem Th28: :: MESFUN6C:28
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))
proofend;

theorem Th29: :: MESFUN6C:29
for k being real number
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative &amp; 0 <= k &amp; E c= dom f &amp; f is_measurable_on E holds
f to_power k is_measurable_on E
proofend;

theorem Th30: :: MESFUN6C:30
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A &amp; A c= dom f holds
|.f.| is_measurable_on A
proofend;

theorem Th31: :: MESFUN6C:31
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 &amp; f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
proofend;

theorem :: MESFUN6C:32
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M &amp; g is_integrable_on M holds
dom (f + g) in S
proofend;

theorem Th33: :: MESFUN6C:33
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M &amp; g is_integrable_on M holds
f + g is_integrable_on M
proofend;

theorem Th34: :: MESFUN6C:34
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M &amp; g is_integrable_on M holds
f - g is_integrable_on M
proofend;

theorem :: MESFUN6C:35
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M &amp; g is_integrable_on M holds
f - g is_integrable_on M
proofend;

theorem Th36: :: MESFUN6C:36
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M &amp; g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) &amp; Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
proofend;

theorem :: MESFUN6C:37
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M &amp; g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) &amp; Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
proofend;

theorem Th38: :: MESFUN6C:38
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
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M &amp; Integral (M,(r (#) f)) = r * (Integral (M,f)) )
proofend;

theorem Th39: :: MESFUN6C:39
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 f is_integrable_on M holds
( <i> (#) f is_integrable_on M &amp; Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) )
proofend;

theorem Th40: :: MESFUN6C:40
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
for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M &amp; Integral (M,(c (#) f)) = c * (Integral (M,f)) )
proofend;

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 &amp; f is_measurable_on A ) &amp; f is_integrable_on M &amp; Integral (M,f) = 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
proofend;

theorem Th41: :: MESFUN6C:41
for X being non empty set
for f being PartFunc of X,REAL
for Y being set
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
proofend;

theorem Th42: :: MESFUN6C:42
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = (dom f) /\ (dom g) &amp; f is_measurable_on A &amp; g is_measurable_on A ) &amp; f is_integrable_on M &amp; g is_integrable_on M &amp; g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) &amp; Integral (M,(f | E)) <= Integral (M,(g | E)) )
proofend;

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 &amp; f is_measurable_on A ) &amp; f is_integrable_on M &amp; Integral (M,f) <> 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
proofend;

theorem :: MESFUN6C:43
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 &amp; f is_measurable_on A ) &amp; f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
proofend;

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;
let B be Element of S;
func Integral_on (M,B,f) ->  complex number  equals :: MESFUN6C:def 5
 Integral (M,(f | B));
coherence
 Integral (M,(f | B)) is complex number ;
end;

:: deftheorem  defines Integral_on MESFUN6C:def_5_:_
 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
for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));

theorem :: MESFUN6C:44
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX
for B being Element of S st f is_integrable_on M &amp; g is_integrable_on M &amp; B c= dom (f + g) holds
( f + g is_integrable_on M &amp; Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
proofend;

theorem :: MESFUN6C:45
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
for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))
proofend;

begin

theorem :: MESFUN6C:46
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
proofend;

theorem :: MESFUN6C:47
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))
proofend;

theorem :: MESFUN6C:48
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
proofend;

theorem :: MESFUN6C:49
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
proofend;