:: Riemann Integral of Functions $\mathbbbR$ into $\mathbbbC$
:: by Keiichi Miyajima , Takahiro Kato and Yasunari Shidama
::
:: Received February 23, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

theorem Th1: :: INTEGR16:1
for z being complex number
for r being real number holds
( Re (r * z) = r * (Re z) & Im (r * z) = r * (Im z) )
proofend;

Lm1: now__::_thesis:_for_f_being_FinSequence
for_g_being_Function_st_dom_f_=_dom_g_holds_
g_is_FinSequence
let f be FinSequence; ::_thesis: for g being Function st dom f = dom g holds
g is FinSequence
let g be Function; ::_thesis: ( dom f = dom g implies g is FinSequence )
 ex n being Nat st dom f = Seg n by FINSEQ_1:def_2;
hence  ( dom f = dom g implies g is FinSequence ) by FINSEQ_1:def_2; ::_thesis: verum
end;

registration
let S be FinSequence of COMPLEX ;
cluster Re S ->  FinSequence-like ;
coherence
 Re S is FinSequence-like
proofend;
cluster Im S ->  FinSequence-like ;
coherence
 Im S is FinSequence-like
proofend;
end;

definition
let S be FinSequence of COMPLEX ;
:: original:Re
redefine func Re S ->  FinSequence of REAL ;
coherence
 Re S is FinSequence of REAL
proofend;
:: original:Im
redefine func Im S ->  FinSequence of REAL ;
coherence
 Im S is FinSequence of REAL
proofend;
end;

definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,COMPLEX;
let D be Division of A;
mode middle_volume of f,D ->  FinSequence of COMPLEX  means :Def1: :: INTEGR16:def 1
( len it = len D & ( for i being Nat st i in dom D holds
ex c being Element of COMPLEX st
( c in rng (f | (divset (D,i))) & it . i = c * (vol (divset (D,i))) ) ) );
correctness
existence
ex b1 being FinSequence of COMPLEX st
( len b1 = len D & ( for i being Nat st i in dom D holds
ex c being Element of COMPLEX st
( c in rng (f | (divset (D,i))) & b1 . i = c * (vol (divset (D,i))) ) ) );
proofend;
end;

:: deftheorem Def1 defines middle_volume INTEGR16:def_1_:_
 for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for D being Division of A
for b4 being FinSequence of COMPLEX holds
( b4 is middle_volume of f,D iff ( len b4 = len D & ( for i being Nat st i in dom D holds
ex c being Element of COMPLEX st
( c in rng (f | (divset (D,i))) & b4 . i = c * (vol (divset (D,i))) ) ) ) );

definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,COMPLEX;
let D be Division of A;
let F be middle_volume of f,D;
func middle_sum (f,F) ->  Element of COMPLEX  equals :: INTEGR16:def 2
 Sum F;
coherence
 Sum F is Element of COMPLEX ;
end;

:: deftheorem  defines middle_sum INTEGR16:def_2_:_
 for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for D being Division of A
for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;

definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,COMPLEX;
let T be DivSequence of A;
mode middle_volume_Sequence of f,T ->  Function of NAT,(COMPLEX *) means :Def3: :: INTEGR16:def 3
 for k being Element of NAT holds it . k is middle_volume of f,T . k;
correctness
existence
ex b1 being Function of NAT,(COMPLEX *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k;
proofend;
end;

:: deftheorem Def3 defines middle_volume_Sequence INTEGR16:def_3_:_
 for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for T being DivSequence of A
for b4 being Function of NAT,(COMPLEX *) holds
( b4 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b4 . k is middle_volume of f,T . k );

definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,COMPLEX;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original:.
redefine funcS . k ->  middle_volume of f,T . k;
coherence
 S . k is middle_volume of f,T . k by Def3;
end;

definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,COMPLEX;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
func middle_sum (f,S) ->  Complex_Sequence means :Def4: :: INTEGR16:def 4
 for i being Element of NAT holds it . i = middle_sum (f,(S . i));
existence
 ex b1 being Complex_Sequence st
for i being Element of NAT holds b1 . i = middle_sum (f,(S . i))
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines middle_sum INTEGR16:def_4_:_
 for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b5 being Complex_Sequence holds
( b5 = middle_sum (f,S) iff for i being Element of NAT holds b5 . i = middle_sum (f,(S . i)) );

begin

theorem :: INTEGR16:2
for f being PartFunc of REAL,COMPLEX
for A being Subset of REAL holds Re (f | A) = (Re f) | A
proofend;

theorem :: INTEGR16:3
for f being PartFunc of REAL,COMPLEX
for A being Subset of REAL holds Im (f | A) = (Im f) | A
proofend;

registration
let A be non empty closed_interval Subset of REAL;
let f be Function of A,COMPLEX;
cluster Re f ->  quasi_total for PartFunc of A,REAL;
correctness
coherence
for b1 being PartFunc of A,REAL st b1 = Re f holds
b1 is quasi_total ;
proofend;
cluster Im f ->  quasi_total for PartFunc of A,REAL;
correctness
coherence
for b1 being PartFunc of A,REAL st b1 = Im f holds
b1 is quasi_total ;
proofend;
end;

theorem Th4: :: INTEGR16:4
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for D being Division of A
for S being middle_volume of f,D holds
( Re S is middle_volume of Re f,D & Im S is middle_volume of Im f,D )
proofend;

Lm2:  Sum (<*> COMPLEX) = 0
by BINOP_2:1, FINSOP_1:10;

Lm3:  for F being FinSequence of COMPLEX
for x being Element of COMPLEX holds Sum (F ^ <*x*>) = (Sum F) + x
proofend;

theorem Th5: :: INTEGR16:5
for F being FinSequence of COMPLEX
for x being Element of COMPLEX holds Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*>
proofend;

theorem Th6: :: INTEGR16:6
for F being FinSequence of COMPLEX
for x being Element of COMPLEX holds Im (F ^ <*x*>) = (Im F) ^ <*(Im x)*>
proofend;

theorem Th7: :: INTEGR16:7
for F being FinSequence of COMPLEX
for Fr being FinSequence of REAL st Fr = Re F holds
Sum Fr = Re (Sum F)
proofend;

theorem Th8: :: INTEGR16:8
for F being FinSequence of COMPLEX
for Fi being FinSequence of REAL st Fi = Im F holds
Sum Fi = Im (Sum F)
proofend;

theorem :: INTEGR16:9
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for D being Division of A
for F being middle_volume of f,D
for Fr being middle_volume of Re f,D st Fr = Re F holds
Re (middle_sum (f,F)) = middle_sum ((Re f),Fr) by Th7;

theorem :: INTEGR16:10
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for D being Division of A
for F being middle_volume of f,D
for Fi being middle_volume of Im f,D st Fi = Im F holds
Im (middle_sum (f,F)) = middle_sum ((Im f),Fi) by Th8;

definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,COMPLEX;
attrf is integrable  means :Def5: :: INTEGR16:def 5
( Re f is integrable &amp; Im f is integrable );
end;

:: deftheorem Def5 defines integrable INTEGR16:def_5_:_
 for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX holds
( f is integrable iff ( Re f is integrable &amp; Im f is integrable ) );

theorem Th11: :: INTEGR16:11
for f being PartFunc of REAL,COMPLEX holds
( f is bounded iff ( Re f is bounded &amp; Im f is bounded ) )
proofend;

theorem :: INTEGR16:12
for A being non empty Subset of REAL
for f being PartFunc of REAL,COMPLEX
for g being Function of A,COMPLEX st f = g holds
( Re f = Re g &amp; Im f = Im g ) ;

theorem Th13: :: INTEGR16:13
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX holds
( f is bounded iff ( Re f is bounded &amp; Im f is bounded ) )
proofend;

definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,COMPLEX;
func integral f ->  Element of COMPLEX  equals :: INTEGR16:def 6
(integral (Re f)) + ((integral (Im f)) * <i>);
correctness
coherence
(integral (Re f)) + ((integral (Im f)) * <i>) is Element of COMPLEX ;
;
end;

:: deftheorem  defines integral INTEGR16:def_6_:_
 for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX holds integral f = (integral (Re f)) + ((integral (Im f)) * <i>);

theorem Th14: :: INTEGR16:14
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded &amp; f is integrable &amp; delta T is convergent &amp; lim (delta T) = 0 holds
( middle_sum (f,S) is convergent &amp; lim (middle_sum (f,S)) = integral f )
proofend;

theorem :: INTEGR16:15
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX st f is bounded holds
( f is integrable iff ex I being Element of COMPLEX st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent &amp; lim (delta T) = 0 holds
( middle_sum (f,S) is convergent &amp; lim (middle_sum (f,S)) = I ) )
proofend;

definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,COMPLEX;
predf is_integrable_on A means :Def7: :: INTEGR16:def 7
( Re f is_integrable_on A &amp; Im f is_integrable_on A );
end;

:: deftheorem Def7 defines is_integrable_on INTEGR16:def_7_:_
 for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,COMPLEX holds
( f is_integrable_on A iff ( Re f is_integrable_on A &amp; Im f is_integrable_on A ) );

definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,COMPLEX;
func integral (f,A) ->  Element of COMPLEX  equals :: INTEGR16:def 8
(integral ((Re f),A)) + ((integral ((Im f),A)) * <i>);
correctness
coherence
(integral ((Re f),A)) + ((integral ((Im f),A)) * <i>) is Element of COMPLEX ;
;
end;

:: deftheorem  defines integral INTEGR16:def_8_:_
 for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,COMPLEX holds integral (f,A) = (integral ((Re f),A)) + ((integral ((Im f),A)) * <i>);

Lm4:  for f being PartFunc of REAL,COMPLEX
for A being Subset of REAL holds
( Re (f | A) = (Re f) | A &amp; Im (f | A) = (Im f) | A )
proofend;

theorem :: INTEGR16:16
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,COMPLEX
for g being Function of A,COMPLEX st f | A = g holds
( f is_integrable_on A iff g is integrable )
proofend;

theorem :: INTEGR16:17
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,COMPLEX
for g being Function of A,COMPLEX st f | A = g holds
integral (f,A) = integral g
proofend;

definition
let a, b be real number ;
let f be PartFunc of REAL,COMPLEX;
func integral (f,a,b) ->  Element of COMPLEX  equals :: INTEGR16:def 9
(integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>);
correctness
coherence
(integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>) is Element of COMPLEX ;
;
end;

:: deftheorem  defines integral INTEGR16:def_9_:_
 for a, b being real number
for f being PartFunc of REAL,COMPLEX holds integral (f,a,b) = (integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>);

begin

theorem Th18: :: INTEGR16:18
for c being complex number
for f being PartFunc of REAL,COMPLEX holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) &amp; Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) )
proofend;

theorem :: INTEGR16:19
for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL,COMPLEX st f1 is_integrable_on A &amp; f2 is_integrable_on A &amp; A c= dom f1 &amp; A c= dom f2 &amp; f1 | A is bounded &amp; f2 | A is bounded holds
( f1 + f2 is_integrable_on A &amp; f1 - f2 is_integrable_on A &amp; integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) &amp; integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
proofend;

theorem :: INTEGR16:20
for r being Real
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,COMPLEX st A c= dom f &amp; f is_integrable_on A &amp; f | A is bounded holds
( r (#) f is_integrable_on A &amp; integral ((r (#) f),A) = r * (integral (f,A)) )
proofend;

theorem :: INTEGR16:21
for c being complex number
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,COMPLEX st A c= dom f &amp; f is_integrable_on A &amp; f | A is bounded holds
( c (#) f is_integrable_on A &amp; integral ((c (#) f),A) = c * (integral (f,A)) )
proofend;

theorem :: INTEGR16:22
for f being PartFunc of REAL,COMPLEX
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
proofend;

theorem :: INTEGR16:23
for f being PartFunc of REAL,COMPLEX
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
proofend;