:: by Keiichi Miyajima , Takahiro Kato and Yasunari Shidama

::

:: Received February 23, 2010

:: Copyright (c) 2010-2017 Association of Mizar Users

Lm1: now :: thesis: for f being FinSequence

for g being Function st dom f = dom g holds

g is 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;
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

registration

let S be FinSequence of COMPLEX ;

coherence

Re S is FinSequence-like

Im S is FinSequence-like

end;
coherence

Re S is FinSequence-like

proof end;

coherence Im S is FinSequence-like

proof end;

definition

let S be FinSequence of COMPLEX ;

:: original: Re

redefine func Re S -> FinSequence of REAL ;

coherence

Re S is FinSequence of REAL

redefine func Im S -> FinSequence of REAL ;

coherence

Im S is FinSequence of REAL

end;
:: original: Re

redefine func Re S -> FinSequence of REAL ;

coherence

Re S is FinSequence of REAL

proof end;

:: original: Imredefine func Im S -> FinSequence of REAL ;

coherence

Im S is FinSequence of REAL

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

existence

ex b_{1} being FinSequence of COMPLEX st

( len b_{1} = 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_{1} . i = c * (vol (divset (D,i))) ) ) );

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

existence

ex b

( len b

ex c being Element of COMPLEX st

( c in rng (f | (divset (D,i))) & b

proof 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_{4} being FinSequence of COMPLEX holds

( b_{4} is middle_volume of f,D iff ( len b_{4} = 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_{4} . i = c * (vol (divset (D,i))) ) ) ) );

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

( b

ex c being Element of COMPLEX st

( c in rng (f | (divset (D,i))) & b

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;

coherence

Sum F is Element of COMPLEX ;

end;
let f be Function of A,COMPLEX;

let D be Division of A;

let F be middle_volume of f,D;

coherence

Sum F is Element of COMPLEX ;

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

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;

existence

ex b_{1} being sequence of (COMPLEX *) st

for k being Element of NAT holds b_{1} . k is middle_volume of f,T . k;

end;
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 for k being Element of NAT holds it . k is middle_volume of f,T . k;

existence

ex b

for k being Element of NAT holds b

proof 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_{4} being sequence of (COMPLEX *) holds

( b_{4} is middle_volume_Sequence of f,T iff for k being Element of NAT holds b_{4} . k is middle_volume of f,T . k );

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

( b

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

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;

ex b_{1} being Complex_Sequence st

for i being Element of NAT holds b_{1} . i = middle_sum (f,(S . i))

for b_{1}, b_{2} being Complex_Sequence st ( for i being Element of NAT holds b_{1} . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b_{2} . i = middle_sum (f,(S . i)) ) holds

b_{1} = b_{2}

end;
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 for i being Element of NAT holds it . i = middle_sum (f,(S . i));

ex b

for i being Element of NAT holds b

proof end;

uniqueness for b

b

proof 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_{5} being Complex_Sequence holds

( b_{5} = middle_sum (f,S) iff for i being Element of NAT holds b_{5} . i = middle_sum (f,(S . i)) );

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

( b

registration

let A be non empty closed_interval Subset of REAL;

let f be Function of A,COMPLEX;

correctness

coherence

for b_{1} being PartFunc of A,REAL st b_{1} = Re f holds

b_{1} is quasi_total ;

coherence

for b_{1} being PartFunc of A,REAL st b_{1} = Im f holds

b_{1} is quasi_total ;

end;
let f be Function of A,COMPLEX;

correctness

coherence

for b

b

proof end;

correctness coherence

for b

b

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

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

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

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)

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)

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;

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;

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;

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

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

( f is bounded iff ( Re f is bounded & Im f is bounded ) )

proof end;

theorem :: INTEGR16:12

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

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;

coherence

(integral (Re f)) + ((integral (Im f)) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

end;
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 (integral (Re f)) + ((integral (Im f)) * <i>);

coherence

(integral (Re f)) + ((integral (Im f)) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

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

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 )

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

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;

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

( Re f is_integrable_on A & Im f is_integrable_on A );

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

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;

coherence

(integral ((Re f),A)) + ((integral ((Im f),A)) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

end;
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 (integral ((Re f),A)) + ((integral ((Im f),A)) * <i>);

coherence

(integral ((Re f),A)) + ((integral ((Im f),A)) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

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

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 )

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

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;

coherence

(integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

end;
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 (integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>);

coherence

(integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

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

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

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

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

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

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)

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)

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;