MESFUN6C: Integral of Complex-Valued Measurable Function

:: 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

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 )

proof end;

definition

let X be non empty set ;
let f be PartFunc of X,COMPLEX ;
func Re f -> PartFunc of X,REAL means :Def1: :: MESFUN6C:def 1
( dom it = dom f & ( for x being Element of X st x in dom it holds
it . x = Re (f . x) ) );
existence

proof end;

uniqueness

proof end;

func Im f -> PartFunc of X,REAL means :Def2: :: MESFUN6C:def 2
( dom it = dom f & ( for x being Element of X st x in dom it holds
it . x = Im (f . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Re MESFUN6C:def 1 :

:: deftheorem Def2 defines Im MESFUN6C:def 2 :

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;
pred f is_measurable_on E means :Def3: :: MESFUN6C:def 3
( Re f is_measurable_on E & Im f is_measurable_on E );

end;

:: deftheorem Def3 defines is_measurable_on MESFUN6C:def 3 :

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) )

proof end;

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)) )

proof end;

theorem Th4: :: MESFUN6C:4

for X being non empty set
for f being PartFunc of X,COMPLEX holds
( - (Im f) = Re ( (#) f) & Re f = Im ( (#) f) )

proof end;

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) & Im (f + g) = (Im f) + (Im g) )

proof end;

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) & Im (f - g) = (Im f) - (Im g) )

proof end;

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) & (Im f) | A = Im (f | A) )

proof end;

theorem Th8: :: MESFUN6C:8

for X being non empty set
for f being PartFunc of X,COMPLEX holds f = (Re f) + ( (#) (Im f))

proof end;

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 & f is_measurable_on A holds
f is_measurable_on B

proof end;

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 & f is_measurable_on B holds
f is_measurable_on A \/ B

proof end;

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 & g is_measurable_on A holds
f + g is_measurable_on A

proof end;

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 & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A

proof end;

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 & (f + g) | Y = (f | Y) + (g | Y) )

proof end;

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 & A = (dom f) /\ B holds
f | B is_measurable_on A

proof end;

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 & dom g in S holds
dom (f + g) in S

proof end;

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 )

proof end;

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 & A c= dom f holds
c (#) f is_measurable_on A

proof end;

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

proof end;

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 ;
pred f is_integrable_on M means :Def4: :: MESFUN6C:def 4
( Re f is_integrable_on M & Im f is_integrable_on M );

end;

:: 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 * ) );
existence

proof end;

uniqueness ;

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 )

proof end;

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 & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M

proof end;

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 & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M

proof end;

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

proof end;

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 & f is_integrable_on M & M . A = 0 holds
Integral M,(f | (E \ A)) = Integral M,f

proof end;

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

proof end;

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 & A misses B holds
Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B))

proof end;

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 & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral M,f = (Integral M,(f | A)) + (Integral M,(f | B)) )

proof end;

definition

let k be real number ;
let X be non empty set ;
let f be PartFunc of X,REAL ;
func f to_power k -> PartFunc of X,REAL means :Def6: :: MESFUN6C:def 6
( dom it = dom f & ( for x being Element of X st x in dom it holds
it . x = (f . x) to_power k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines to_power MESFUN6C:def 6 :

registration

let X be non empty set ;
cluster nonnegative Element of K21(K22(X,REAL ));
existence

proof end;

end;

registration

let k be real non negative number ;
let X be non empty set ;
let f be nonnegative PartFunc of X,REAL ;
cluster f to_power k -> nonnegative ;
coherence

proof end;

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 & 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)

proof end;

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))

proof end;

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 & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E

proof end;

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 & A c= dom f holds
|.f.| is_measurable_on A

proof end;

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 & f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )

proof end;

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 & g is_integrable_on M holds
dom (f + g) in S

proof end;

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 & g is_integrable_on M holds
f + g is_integrable_on M

proof end;

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 & g is_integrable_on M holds
f - g is_integrable_on M

proof end;

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 & g is_integrable_on M holds
f - g is_integrable_on M

proof end;

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 & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )

proof end;

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 & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f - g) = (Integral M,(f | E)) + (Integral M,((- g) | E)) )

proof end;

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 & Integral M,(r (#) f) = r * (Integral M,f) )

proof end;

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
( (#) f is_integrable_on M & Integral M,( (#) f) = * (Integral M,f) )

proof end;

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 & Integral M,(c (#) f) = c * (Integral M,f) )

proof end;

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.|

proof end;

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)

proof end;

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) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f | E) <= Integral M,(g | E) )

proof end;

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.|

proof end;

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

proof end;

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 7
Integral M,(f | B);
coherence ;

end;

:: deftheorem defines Integral_on MESFUN6C:def 7 :

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 & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on M,B,(f + g) = (Integral_on M,B,f) + (Integral_on M,B,g) )

proof end;

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)

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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)

proof end;