:: 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 b₁ being FinSequence of COMPLEX st
( len b₁ = 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))) & b₁ . 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 b₄ being FinSequence of COMPLEX holds
( b₄ is middle_volume of f,D iff ( len b₄ = 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))) & b₄ . 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 b₁ being sequence of (COMPLEX *) st
for k being Element of NAT holds b₁ . 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 b₄ being sequence of (COMPLEX *) holds
( b₄ is middle_volume_Sequence of f,T iff for k being Element of NAT holds b₄ . 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 b₁ being Complex_Sequence st
for i being Element of NAT holds b₁ . i = middle_sum (f,(S . i))

proof end;

uniqueness
for b₁, b₂ being Complex_Sequence st ( for i being Element of NAT holds b₁ . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b₂ . i = middle_sum (f,(S . i)) ) holds
b₁ = b₂

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 b₅ being Complex_Sequence holds
( b₅ = middle_sum (f,S) iff for i being Element of NAT holds b₅ . 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 b₁ being PartFunc of A,REAL st b₁ = Re f holds
b₁ is quasi_total ;

proof end;

cluster Im f -> quasi_total for PartFunc of A,REAL;

correctness
coherence
for b₁ being PartFunc of A,REAL st b₁ = Im f holds
b₁ 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;