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


theorem Th1: :: INTEGR16:1
for z being Complex
for r being Real holds
( Re (r * z) = r * (Re z) & Im (r * z) = r * (Im z) )
proof end;

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
proof end;
cluster Im S -> FinSequence-like ;
coherence
Im S is FinSequence-like
proof end;
end;

definition
let S be FinSequence of COMPLEX ;
:: original: Re
redefine func Re S -> FinSequence of REAL ;
coherence
Re S is FinSequence of REAL
proof end;
:: original: Im
redefine func Im S -> FinSequence of REAL ;
coherence
Im S is FinSequence of REAL
proof end;
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))) ) ) )
;
proof end;
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 -> sequence of (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 sequence of (COMPLEX *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k
;
proof end;
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 sequence of (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 func S . 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))
proof end;
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
proof end;
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)) );

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

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

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
;
proof end;
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
;
proof end;
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 )
proof end;

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

proof end;

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

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

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)
proof end;

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)
proof end;

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;
attr f is integrable means :: INTEGR16:def 5
( Re f is integrable & Im f is integrable );
end;

:: deftheorem 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 & Im f is integrable ) );

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

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 & 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 & Im f is bounded ) )
proof end;

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
;
by XCMPLX_0:def 2;
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 & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
proof end;

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 & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
proof end;

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

:: deftheorem 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 & 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
;
by XCMPLX_0:def 2;
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 & Im (f | A) = (Im f) | A )

proof end;

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 )
proof end;

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
proof end;

definition
let a, b be Real;
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
;
by XCMPLX_0:def 2;
end;

:: deftheorem defines integral INTEGR16:def 9 :
for a, b being Real
for f being PartFunc of REAL,COMPLEX holds integral (f,a,b) = (integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>);

theorem Th18: :: INTEGR16:18
for c being Complex
for f being PartFunc of REAL,COMPLEX holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) )
proof end;

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 & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds
( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
proof end;

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 & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
proof end;

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

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)
proof end;

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)
proof end;