:: Riemann Integral of Functions $\mathbbbR$ into $\mathbbbC$
:: by Keiichi Miyajima , Takahiro Kato and Yasunari Shidama
::
:: Received February 23, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies INTEGRA1, INTEGRA2, FINSEQ_1, SEQ_1, SEQ_2, ORDINAL2, ARYTM_1,
RELAT_1, FUNCT_1, PARTFUN1, XBOOLE_0, FUNCT_3, INTEGR15, REALSET1,
XCMPLX_0, COMPLEX1, COMSEQ_1, SETWISEO, SUBSET_1, NUMBERS, CARD_1,
ORDINAL4, NAT_1, TARSKI, CARD_3, MEASURE7, ARYTM_3, BINOP_2, XXREAL_0,
XXREAL_2, INTEGRA5, VALUED_1, REAL_1, XXREAL_1, FUNCT_2, MEASURE5;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, REAL_1, RCOMP_1, VALUED_1,
RELSET_1, PARTFUN1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, BINOP_2, BINOP_1,
SETWOP_2, RVSUM_1, XXREAL_0, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3,
INTEGRA5, INTEGR15, MESFUN6C, COMSEQ_1, COMSEQ_2, COMSEQ_3;
constructors REAL_1, MONOID_0, MEASURE6, BINOP_2, INTEGRA5, RELSET_1,
INTEGR15, FINSOP_1, SETWISEO, COMSEQ_2, COMSEQ_3, MESFUN6C, SQUARE_1,
SEQ_2, INTEGRA3, BINOP_1;
registrations NUMBERS, XREAL_0, INTEGRA1, FUNCT_2, BINOP_2, MEMBERED,
ORDINAL1, VALUED_0, RELSET_1, FINSEQ_1, MEASURE5, XCMPLX_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, INTEGRA5, INTEGR15, FINSEQ_1, COMPLEX1, RVSUM_1;
expansions XBOOLE_0, INTEGRA5, COMPLEX1;
theorems XBOOLE_0, XBOOLE_1, XCMPLX_0, XREAL_0, INTEGRA1, COMSEQ_3, RFUNCT_1,
COMPLEX1, RELSET_1, BINOP_2, FINSOP_1, NAT_1, XXREAL_0, RELAT_1,
ORDINAL1, XREAL_1, FINSEQ_1, RVSUM_1, FUNCT_1, FUNCT_2, INTEGRA5,
FINSEQ_3, INTEGRA6, INTEGR15, VALUED_1, MESFUN6C, COMSEQ_2;
schemes FUNCT_2, FINSEQ_1, NAT_1;
begin :: Preliminaries
theorem Th1:
for z being Complex, r be Real holds Re(r * z) = r* Re (z)
& Im(r * z) = r* Im (z)
proof
let z be Complex, r be Real;
A2: Re(r) = r by COMPLEX1:def 1;
hence Re(r * z) = r * Re(z) - Im(r) * Im(z) by COMPLEX1:9
.= r * Re(z) - 0 * Im(z) by COMPLEX1:def 2
.= r * Re(z);
thus Im(r * z) = r * Im(z) + Re(z) * Im(r) by A2,COMPLEX1:9
.= r * Im(z) + 0 * Re(z) by COMPLEX1:def 2
.= r * Im(z);
end;
Lm1:now
let f be FinSequence, g be Function;
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;
end;
registration
let S be FinSequence of COMPLEX;
cluster Re S -> FinSequence-like;
coherence
proof
dom Re S = dom S by COMSEQ_3:def 3;
hence thesis by Lm1;
end;
cluster Im S -> FinSequence-like;
coherence
proof
dom Im S = dom S by COMSEQ_3:def 4;
hence thesis by Lm1;
end;
end;
definition
let S be FinSequence of COMPLEX;
redefine func Re S -> FinSequence of REAL; :: redefines Re (COMSEQ_3, definition)
coherence
proof
rng Re S c= REAL;
hence thesis by FINSEQ_1:def 4;
end;
redefine func Im S -> FinSequence of REAL; :: redefines Im (COMSEQ_3, definition)
coherence
proof
rng Im S c= REAL;
hence thesis by FINSEQ_1:def 4;
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:
len it = len D & for i be Nat st i in dom D holds
ex c be Element of COMPLEX st c in rng (f|divset(D,i))
& it.i = c * vol divset(D,i);
correctness
proof
defpred P1[ Nat, set] means
ex c be Element of COMPLEX st c in rng (f|divset(D,$1))
& $2= c *vol divset(D,$1);
A1: Seg len D = dom D by FINSEQ_1:def 3;
A2: for k being Nat st k in Seg len D holds ex x being Element of COMPLEX st
P1[k,x]
proof
let k be Nat;
assume k in Seg len D; then
A3: k in dom D by FINSEQ_1:def 3;
dom f = A by FUNCT_2:def 1; then
dom (f|divset(D,k)) = divset(D,k) by A3,INTEGRA1:8,RELAT_1:62; then
rng (f|divset(D,k)) is non empty by RELAT_1:42; then
consider c be object such that
A4: c in rng (f|divset(D,k));
reconsider c as Element of COMPLEX by A4;
c*vol divset(D,k) is Element of COMPLEX by XCMPLX_0:def 2;
hence thesis by A4;
end;
consider p being FinSequence of COMPLEX such that
A5: dom p = Seg len D & for k being Nat st k in Seg len D holds P1[k,p.k]
from FINSEQ_1:sch 5(A2);
len p = len D by A5,FINSEQ_1:def 3;
hence thesis by A5,A1;
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;
let F be middle_volume of f,D;
func middle_sum(f,F) -> Element of COMPLEX equals
Sum(F);
coherence;
end;
definition
let A be non empty closed_interval Subset of REAL,
f be Function of A,COMPLEX,
T be DivSequence of A;
mode middle_volume_Sequence of f,T -> sequence of (COMPLEX)* means
:Def3:
for k be Element of NAT holds it.k is middle_volume of f,T.k;
correctness
proof
defpred P[Element of NAT,set] means $2 is middle_volume of f,T.$1;
A1: for x being Element of NAT ex y being Element of (COMPLEX)* st P[x, y]
proof
let x be Element of NAT;
set y = the middle_volume of f,T.x;
reconsider y as Element of (COMPLEX)* by FINSEQ_1:def 11;
y is middle_volume of f,T.x;
hence thesis;
end;
ex f being sequence of (COMPLEX)* st for x being Element of NAT holds
P[x, f.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
end;
definition
let A be non empty closed_interval Subset of REAL,
f be Function of A,COMPLEX,
T be DivSequence of A,
S be middle_volume_Sequence of f,T,
k be Element of NAT;
redefine func S.k -> middle_volume of f,T.k; :: redefines . (FUNCT_1, definition)
coherence by Def3;
end;
definition
let A be non empty closed_interval Subset of REAL,
f be Function of A,COMPLEX,
T be DivSequence of A,
S be middle_volume_Sequence of f,T;
func middle_sum(f,S) -> Complex_Sequence means :Def4:
for i be Element of NAT holds it.i = middle_sum(f,S.i);
existence
proof
deffunc H1(Element of NAT) = middle_sum(f,S.$1);
thus ex IT being Complex_Sequence st for i being Element of NAT
holds IT.i = H1(i) from FUNCT_2:sch 4;
end;
uniqueness
proof
let F1, F2 be Complex_Sequence;
assume that
A1: for i being Element of NAT holds F1.i = middle_sum(f,S.i) and
A2: for i being Element of NAT holds F2.i = middle_sum(f,S.i);
for i being Element of NAT holds F1.i = F2.i
proof
let i be Element of NAT;
F1.i = middle_sum(f,S.i) by A1
.= F2.i by A2;
hence F1.i = F2.i;
end;
hence F1 = F2 by FUNCT_2:63;
end;
end;
begin :: Definition of Riemann Integral on Functions $\mathbbbR$ into $\mathbbbC$
theorem
for f be PartFunc of REAL,COMPLEX,
A be Subset of REAL holds Re (f|A) = (Re f)|A
proof
let f be PartFunc of REAL,COMPLEX,
A be Subset of REAL;
A1: now
let c be object;
assume
A2: c in dom ((Re f)|A); then
A3: c in dom (Re f) /\ A by RELAT_1:61; then
A4: c in A by XBOOLE_0:def 4;
A5: c in dom (Re f) by A3,XBOOLE_0:def 4;then
c in dom f by COMSEQ_3:def 3; then
c in dom f /\ A by A4,XBOOLE_0:def 4; then
A6: c in dom (f|A) by RELAT_1:61; then
c in dom (Re (f|A)) by COMSEQ_3:def 3; then
(Re (f|A)).c = Re ((f|A).c) by COMSEQ_3:def 3
.= Re (f.c) by A6,FUNCT_1:47
.= (Re f).c by A5,COMSEQ_3:def 3;
hence ((Re f)|A).c = (Re (f|A)).c by A2,FUNCT_1:47;
end;
dom ((Re f)|A) = dom (Re f) /\ A by RELAT_1:61
.= dom f /\ A by COMSEQ_3:def 3
.= dom (f|A) by RELAT_1:61
.= dom (Re (f|A)) by COMSEQ_3:def 3;
hence thesis by A1,FUNCT_1:2;
end;
theorem
for f be PartFunc of REAL,COMPLEX,
A be Subset of REAL holds Im (f|A) = (Im f)|A
proof
let f be PartFunc of REAL,COMPLEX,
A be Subset of REAL;
A1: now
let c be object;
assume
A2: c in dom ((Im f)|A); then
A3: c in dom (Im f) /\ A by RELAT_1:61; then
A4: c in A by XBOOLE_0:def 4;
A5: c in dom (Im f) by A3,XBOOLE_0:def 4; then
c in dom f by COMSEQ_3:def 4; then
c in dom f /\ A by A4,XBOOLE_0:def 4; then
A6: c in dom (f|A) by RELAT_1:61; then
c in dom (Im (f|A)) by COMSEQ_3:def 4; then
(Im (f|A)).c = Im ((f|A).c) by COMSEQ_3:def 4
.= Im (f.c) by A6,FUNCT_1:47
.= (Im f).c by A5,COMSEQ_3:def 4;
hence ((Im f)|A).c = (Im (f|A)).c by A2,FUNCT_1:47;
end;
dom ((Im f)|A) = dom (Im f) /\ A by RELAT_1:61
.= dom f /\ A by COMSEQ_3:def 4
.= dom (f|A) by RELAT_1:61
.= dom (Im (f|A)) by COMSEQ_3:def 4;
hence thesis by A1,FUNCT_1:2;
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
proof
dom f = A by FUNCT_2:def 1; then
dom (Re f) = A by COMSEQ_3:def 3;
hence thesis by FUNCT_2:def 1;
end;
cluster Im f -> quasi_total for PartFunc of A,REAL;
correctness
proof
dom f = A by FUNCT_2:def 1; then
dom (Im f) = A by COMSEQ_3:def 4;
hence thesis by FUNCT_2:def 1;
end;
end;
theorem Th4:
for A be non empty closed_interval Subset of REAL, f be Function of A,COMPLEX,
D be Division of A,
S be 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
let A be non empty closed_interval Subset of REAL,
f be Function of A,COMPLEX,
D be Division of A,
S be middle_volume of f,D;
A1: dom S = dom (Re S) by COMSEQ_3:def 3;
set RS = Re S;
len S = len D by Def1; then
A2: dom S = Seg len D by FINSEQ_1:def 3; then
A3: len (RS) = len D by A1,FINSEQ_1:def 3;
for i be Nat st i in dom D holds
ex r be Element of REAL st r in rng ( (Re f)|divset(D,i))
& (RS).i=r*vol divset(D,i)
proof
let i be Nat such that A4: i in dom D;
consider c be Element of COMPLEX such that
A5: c in rng (f|divset(D,i)) & S.i= c * vol divset(D,i) by A4,Def1;
A6: i in dom (Re S) by A4,A1,A2,FINSEQ_1:def 3;
set r =Re c;
take r;
consider t be object such that
A7: t in dom (f|divset(D,i)) and
A8: c = (f|divset(D,i)).t by A5,FUNCT_1:def 3;
t in dom(f) /\ divset(D,i) by A7,RELAT_1:61; then
t in dom(f) by XBOOLE_0:def 4; then
A9: t in dom (Re f) by COMSEQ_3:def 3;
A10: dom (f|divset(D,i)) =dom (f) /\ divset(D,i) by RELAT_1:61
.=dom (Re f) /\ divset(D,i) by COMSEQ_3:def 3
.=dom ((Re f)|divset(D,i)) by RELAT_1:61;
r = Re (f.t) by A7,A8,FUNCT_1:47
.= (Re f).t by A9,COMSEQ_3:def 3
.= ((Re f)|divset(D,i)).t by A7,A10,FUNCT_1:47;
hence r in rng ( (Re f)|divset(D,i)) by A7,A10,FUNCT_1:def 3;
thus (RS).i = Re (S.i) by A6,COMSEQ_3:def 3
.= r*vol divset(D,i) by A5,Th1;
end;
hence Re S is middle_volume of (Re f),D by A3,INTEGR15:def 1;
A11: dom S = dom (Im S) by COMSEQ_3:def 4;
set IS = Im S;
A12: len (IS) = len D by A2,A11,FINSEQ_1:def 3;
for i be Nat st i in dom D holds
ex r be Element of REAL st r in rng ( (Im f)|divset(D,i))
& (IS).i=r*vol divset(D,i)
proof
let i be Nat such that A13: i in dom D;
consider c be Element of COMPLEX such that
A14: c in rng (f|divset(D,i)) & S.i= c * vol divset(D,i) by A13,Def1;
A15: i in dom (Im S) by A13,A2,A11,FINSEQ_1:def 3;
set r = Im c;
take r;
consider t be object such that
A16: t in dom (f|divset(D,i)) and
A17: c = (f|divset(D,i)).t by A14,FUNCT_1:def 3;
t in dom(f) /\ divset(D,i) by A16,RELAT_1:61; then
t in dom(f) by XBOOLE_0:def 4; then
A18: t in dom (Im f) by COMSEQ_3:def 4;
A19: dom (f|divset(D,i)) =dom (f) /\ divset(D,i) by RELAT_1:61
.=dom (Im f) /\ divset(D,i) by COMSEQ_3:def 4
.=dom ((Im f)|divset(D,i)) by RELAT_1:61;
r = Im (f.t) by A16,A17,FUNCT_1:47
.= (Im f).t by A18,COMSEQ_3:def 4
.= ((Im f)|divset(D,i)).t by A16,A19,FUNCT_1:47;
hence r in rng ((Im f)|divset(D,i)) by A16,A19,FUNCT_1:def 3;
thus (IS).i = Im (S.i) by A15,COMSEQ_3:def 4
.= r*vol divset(D,i) by A14,Th1;
end;
hence Im S is middle_volume of (Im f),D by A12,INTEGR15:def 1;
end;
Lm2:
Sum(<*> COMPLEX) = 0 by BINOP_2:1,FINSOP_1:10;
Lm3:
for F be FinSequence of COMPLEX, x be Element of COMPLEX holds
Sum(F^<* x *>) = Sum F + x
proof
let F be FinSequence of COMPLEX,
x be Element of COMPLEX;
thus Sum(F^<*x*>) = addcomplex.(addcomplex $$ F,x) by FINSOP_1:4
.= (Sum F) + x by BINOP_2:def 3;
end;
theorem Th5:
for F be FinSequence of COMPLEX, x be Element of COMPLEX holds
Re (F^<* x *>) = (Re F)^<* Re x *>
proof
let F be FinSequence of COMPLEX,
x be Element of COMPLEX;
set F1=Re (F^<* x *>);
set F2=(Re F)^<* Re x *>;
A1: dom F = dom (Re F) by COMSEQ_3:def 3;
A2: Seg len F = dom F by FINSEQ_1:def 3;
A3: len <* Re x *> = 1 by FINSEQ_1:39;
A4: dom F1 = dom (F^<* x *>) by COMSEQ_3:def 3
.= Seg (len F + len <* x *>) by FINSEQ_1:def 7
.= Seg (len (Re F) + len <* x *>) by A1,A2,FINSEQ_1:def 3
.= Seg (len (Re F) + len <* Re x *>) by A3,FINSEQ_1:39
.= dom F2 by FINSEQ_1:def 7;
now let k be Nat;
assume A5: k in dom F1; then
k in dom (F^<*x*>) by COMSEQ_3:def 3; then
A6:k in Seg len((F^<*x*>)) by FINSEQ_1:def 3; then
k in Seg (len F + len <*x*>) by FINSEQ_1:22; then
A7:1 <=k & k <= len F + len <*x*> by FINSEQ_1:1;
now per cases;
suppose A8: k = len F + 1;
thus F1.k = Re( (F^<* x *>).k ) by A5,COMSEQ_3:def 3
.= Re x by A8,FINSEQ_1:42
.= F2.(len (Re F) + 1) by FINSEQ_1:42
.= F2.k by A8,A1,A2,FINSEQ_1:def 3;
end;
suppose A9: k <> len F + 1;
k <= len F + 1 by A7,FINSEQ_1:39; then
k < len F + 1 by A9,XXREAL_0:1; then
1 <= k & k <= len F by A6,FINSEQ_1:1,NAT_1:13; then
k in Seg (len F); then
A10:k in dom F by FINSEQ_1:def 3; then
A11:k in dom (Re F) by COMSEQ_3:def 3;
thus F1.k = Re( (F^<* x *>).k ) by A5,COMSEQ_3:def 3
.= Re (F.k) by A10,FINSEQ_1:def 7
.=(Re F).k by A11,COMSEQ_3:def 3
.=F2.k by A11,FINSEQ_1:def 7;
end;
end;
hence F1.k = F2.k;
end;
hence Re (F^<* x *>) = (Re F)^<* Re x *> by A4,FINSEQ_1:13;
end;
theorem Th6:
for F be FinSequence of COMPLEX, x be Element of COMPLEX holds
Im (F^<* x *>) = (Im F)^<* Im x *>
proof
let F be FinSequence of COMPLEX,
x be Element of COMPLEX;
set F1=Im (F^<* x *>);
set F2=(Im F)^<* Im x *>;
A1: dom F = dom (Im F) by COMSEQ_3:def 4;
A2: Seg len F = dom F by FINSEQ_1:def 3;
A3: len <* Im x *> = 1 by FINSEQ_1:39;
A4: dom F1 = dom (F^<* x *>) by COMSEQ_3:def 4
.= Seg (len F + len <* x *>) by FINSEQ_1:def 7
.= Seg (len (Im F) + len <* x *>) by A1,A2,FINSEQ_1:def 3
.= Seg (len (Im F) + len <* Im x *>) by A3,FINSEQ_1:39
.= dom F2 by FINSEQ_1:def 7;
now let k be Nat;
assume A5: k in dom F1; then
k in dom (F^<*x*>) by COMSEQ_3:def 4; then
A6: k in Seg len((F^<*x*>)) by FINSEQ_1:def 3; then
k in Seg (len F + len <*x*>) by FINSEQ_1:22; then
A7: 1 <=k & k <= len F + len <*x*> by FINSEQ_1:1;
now per cases;
suppose A8: k = len F + 1;
thus F1.k = Im((F^<* x *>).k) by A5,COMSEQ_3:def 4
.= Im x by A8,FINSEQ_1:42
.= F2.(len (Im F) + 1) by FINSEQ_1:42
.= F2.k by A8,A1,A2,FINSEQ_1:def 3;
end;
suppose A9: k <> len F + 1;
k <= len F + 1 by A7,FINSEQ_1:39; then
k < len F + 1 by A9,XXREAL_0:1; then
1<=k & k <= len F by A6,FINSEQ_1:1,NAT_1:13; then
k in Seg (len F); then
A10: k in dom F by FINSEQ_1:def 3; then
A11: k in dom (Im F) by COMSEQ_3:def 4;
thus F1.k = Im((F^<* x *>).k) by A5,COMSEQ_3:def 4
.= Im (F.k) by A10,FINSEQ_1:def 7
.=(Im F).k by A11,COMSEQ_3:def 4
.= F2.k by A11,FINSEQ_1:def 7;
end;
end;
hence F1.k = F2.k;
end;
hence Im (F^<* x *>) = (Im F)^<* Im x *> by A4,FINSEQ_1:13;
end;
theorem Th7:
for F be FinSequence of COMPLEX, Fr be FinSequence of REAL st Fr=Re F
holds Sum(Fr) = Re Sum(F)
proof
defpred P[Nat] means
for F be FinSequence of COMPLEX,
Fr be FinSequence of REAL
st len F = $1 & Fr=Re F
holds Sum(Fr) = Re Sum(F);
A1: P[0]
proof
let F be FinSequence of COMPLEX,
Fr be FinSequence of REAL;
assume A2: len F = 0 & Fr=Re F;
then dom Fr = dom F by COMSEQ_3:def 3
.= Seg len F by FINSEQ_1:def 3; then
A3: len Fr = 0 by A2,FINSEQ_1:def 3;
thus Re (Sum (F)) = Re (0) by A2,Lm2,FINSEQ_1:20
.= Sum Fr by A3,COMPLEX1:4,FINSEQ_1:20,RVSUM_1:72;
end;
A4:now let k be Nat;
assume A5:P[k];
now let F be FinSequence of COMPLEX,
Fr be FinSequence of REAL;
assume A6:len F = k+1 & Fr=Re F;
reconsider F1= F|k as FinSequence of COMPLEX;
A7: len F1 = k by A6,FINSEQ_1:59,NAT_1:11;
reconsider F1r= Re F1 as FinSequence of REAL;
reconsider x=F.(k+1) as Element of COMPLEX by XCMPLX_0:def 2;
A8: F = F1^ <* x *> by A6,FINSEQ_3:55;
hence Re (Sum(F)) = Re (Sum(F1)+ x ) by Lm3
.=Re (Sum(F1)) + Re x by COMPLEX1:8
.=Sum (F1r) + Re x by A5,A7
.=Sum(F1r^<* Re x *> ) by RVSUM_1:74
.=Sum(Fr) by A6,A8,Th5;
end;
hence P[k+1];
end;
A9:for k be Nat holds P[k] from NAT_1:sch 2(A1,A4);
let F be FinSequence of COMPLEX,
Fr be FinSequence of REAL;
assume A10: Fr=Re F;
len F is Element of NAT;
hence Sum(Fr) = Re Sum(F) by A9,A10;
end;
theorem Th8:
for F be FinSequence of COMPLEX, Fi be FinSequence of REAL st Fi=Im F
holds Sum(Fi) = Im Sum(F)
proof
defpred P[Nat] means
for F be FinSequence of COMPLEX,
Fi be FinSequence of REAL
st len F = $1 & Fi=Im F
holds Sum(Fi) = Im Sum(F);
A1: P[0]
proof
let F be FinSequence of COMPLEX,
Fi be FinSequence of REAL;
assume A2: len F = 0 & Fi=Im F;
then dom Fi = dom F by COMSEQ_3:def 4
.= Seg len F by FINSEQ_1:def 3; then
A3:len Fi = 0 by A2,FINSEQ_1:def 3;
thus Im (Sum (F)) = Im (0) by A2,Lm2,FINSEQ_1:20
.= Sum Fi by A3,COMPLEX1:4,FINSEQ_1:20,RVSUM_1:72;
end;
A4:now let k be Nat;
assume A5:P[k];
now let F be FinSequence of COMPLEX,
Fi be FinSequence of REAL;
assume A6:len F = k+1 & Fi=Im F;
reconsider F1= F|k as FinSequence of COMPLEX;
A7: len F1 = k by A6,FINSEQ_1:59,NAT_1:11;
reconsider F1i= Im F1 as FinSequence of REAL;
reconsider x=F.(k+1) as Element of COMPLEX by XCMPLX_0:def 2;
A8: F = F1^ <* x *> by A6,FINSEQ_3:55;
hence Im (Sum(F)) = Im (Sum(F1)+ x ) by Lm3
.= Im (Sum(F1)) + Im x by COMPLEX1:8
.= Sum (F1i) + Im x by A5,A7
.= Sum(F1i^<* Im x *> ) by RVSUM_1:74
.= Sum(Fi) by A6,A8,Th6;
end;
hence P[k+1];
end;
A9:for k be Nat holds P[k] from NAT_1:sch 2(A1,A4);
let F be FinSequence of COMPLEX,
Fi be FinSequence of REAL;
assume A10: Fi=Im F;
len F is Element of NAT;
hence Sum(Fi) = Im Sum(F) by A9,A10;
end;
theorem
for A be non empty closed_interval Subset of REAL, f be Function of A,COMPLEX,
D be Division of A,
F be middle_volume of f,D,
Fr be middle_volume of (Re f),D
st Fr=Re F
holds Re middle_sum(f,F) = middle_sum((Re f),Fr) by Th7;
theorem
for A be non empty closed_interval Subset of REAL, f be Function of A,COMPLEX,
D be Division of A,
F be middle_volume of f,D,
Fi be 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
(Re f) is integrable & (Im f) is integrable;
end;
theorem Th11:
for f be PartFunc of REAL,COMPLEX holds
f is bounded iff (Re f is bounded & Im f is bounded)
proof
let f be PartFunc of REAL,COMPLEX;
thus f is bounded implies (Re f is bounded & Im f is bounded)
proof
assume f is bounded; then
consider r being Real such that
A1: for y be set st y in dom f holds |.f.y.| < r by COMSEQ_2:def 3;
now
let y be set;
assume A2:y in dom (Re f); then
A3:y in dom f by COMSEQ_3:def 3;
|.Re (f.y).| <= |.f.y.| by COMPLEX1:79; then
|.Re (f.y).| < r by A1,A3,XXREAL_0:2;
hence |.(Re f).y.| < r by A2,COMSEQ_3:def 3;
end;
hence Re f is bounded by COMSEQ_2:def 3;
now
let y be set;
assume A4:y in dom (Im f); then
A5:y in dom f by COMSEQ_3:def 4;
|.Im (f.y).| <= |.f.y.| by COMPLEX1:79; then
|.Im (f.y).| < r by A1,A5,XXREAL_0:2;
hence |.(Im f).y.| < r by A4,COMSEQ_3:def 4;
end;
hence Im f is bounded by COMSEQ_2:def 3;
end;
thus (Re f is bounded & Im f is bounded) implies f is bounded
proof
assume A6: Re f is bounded & Im f is bounded; then
consider r1 being Real such that
A7: for y be set st y in dom (Re f) holds |.(Re f).y.| < r1 by
COMSEQ_2:def 3;
consider r2 being Real such that
A8: for y be set st y in dom (Im f)
holds |.(Im f).y.| < r2 by A6,COMSEQ_2:def 3;
now let y be set;
assume A9:y in dom f; then
A10: y in dom (Re f) by COMSEQ_3:def 3; then
|.(Re f).y.| < r1 by A7; then
A11: |.Re (f.y).| < r1 by A10,COMSEQ_3:def 3;
A12: y in dom (Im f) by A9,COMSEQ_3:def 4; then
|.(Im f).y.| < r2 by A8; then
A13: |.Im (f.y).| < r2 by A12,COMSEQ_3:def 4;
A14: |.f.y.| <= |.Re (f.y).| + |.Im(f.y).| by COMPLEX1:78;
|.Re (f.y).| + |.Im(f.y).| < r1+r2 by A11,A13,XREAL_1:8;
hence |.f.y.| < r1+r2 by A14,XXREAL_0:2;
end;
hence f is bounded by COMSEQ_2:def 3;
end;
end;
theorem
for A be non empty Subset of REAL, f be PartFunc of REAL,COMPLEX,
g be Function of A,COMPLEX
st f = g
holds Re f = Re g & Im f = Im g;
theorem Th13:
for A be non empty closed_interval Subset of REAL,
f be Function of A,COMPLEX holds
f is bounded iff (Re f is bounded & Im f is bounded)
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,COMPLEX;
dom f = A by FUNCT_2:def 1; then
reconsider f0=f as PartFunc of REAL,COMPLEX by RELSET_1:5;
f0 is bounded iff Re f0 is bounded & Im f0 is bounded by Th11;
hence thesis;
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
integral(Re f) + integral(Im f) *<i>;
correctness by XCMPLX_0:def 2;
end;
theorem Th14:
for A be non empty closed_interval Subset of REAL,
f being Function of A,COMPLEX,
T being DivSequence of A,
S be 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
let A be non empty closed_interval Subset of REAL,
f be Function of A,COMPLEX,
T be DivSequence of A,
S be middle_volume_Sequence of f,T;
assume that
A1: f is bounded & f is integrable and
A2: delta(T) is convergent & lim delta(T)=0;
set seq=middle_sum(f,S);
set xs=integral(f);
A3: Re f is bounded & Re f is integrable by A1,Th13;
A4: Im f is bounded & Im f is integrable by A1,Th13;
reconsider xseq=seq as sequence of COMPLEX;
ex rseqi be Real_Sequence st for k be Nat holds
rseqi.k = Re (xseq.k) & rseqi is convergent & Re xs = lim rseqi
proof
reconsider pjinf= Re f as Function of A,REAL;
defpred P[Element of NAT,set] means $2= Re (S.$1);
A5:for x being Element of NAT ex y being Element of (REAL)* st P[x, y]
proof
let x be Element of NAT;
Re (S.x) is Element of (REAL)* by FINSEQ_1:def 11;
hence thesis;
end;
consider F being sequence of (REAL)* such that
A6:for x being Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A5);
A7:for x being Element of NAT holds dom(Re (S.x)) = Seg len(S.x)
proof
let x be Element of NAT;
thus dom(Re (S.x)) = dom (S.x) by COMSEQ_3:def 3
.= Seg len(S.x) by FINSEQ_1:def 3;
end;
for k be Element of NAT holds F.k is middle_volume of pjinf,T.k
proof
let k be Element of NAT;
set Tk=T.k;
reconsider Fk=F.k as FinSequence of REAL;
A8:F.k= Re (S.k) by A6; then
A9:dom (Fk) = Seg len(S.k) by A7
.= Seg len(Tk) by Def1; then
A10:dom (Fk) = dom (Tk) by FINSEQ_1:def 3;
A11:now
let j be Nat;
assume A12:j in dom (Tk); then
consider r be Element of COMPLEX such that
A13:r in rng (f|divset((T.k),j)) and
A14:(S.k).j=r * vol divset((T.k),j) by Def1;
reconsider v=Re r as Element of REAL;
take v;
consider t be object such that
A15:t in dom (f|divset((T.k),j)) and
A16:r=(f|divset((T.k),j)).t by A13,FUNCT_1:def 3;
t in dom(f) /\ divset((T.k),j) by A15,RELAT_1:61; then
t in dom(f) by XBOOLE_0:def 4; then
A17:t in dom (Re f) by COMSEQ_3:def 3;
A18:dom (f|divset((T.k),j)) =dom (f) /\ divset((T.k),j) by RELAT_1:61
.=dom (pjinf) /\ divset((T.k),j) by COMSEQ_3:def 3
.=dom (pjinf|divset((T.k),j)) by RELAT_1:61;
Re r = Re (f.t) by A15,A16,FUNCT_1:47
.=(Re f).t by A17,COMSEQ_3:def 3
.=(pjinf|divset((T.k),j)).t by A15,A18,FUNCT_1:47;
hence v in rng (pjinf|divset((T.k),j)) by A15,A18,FUNCT_1:3;
thus (Fk).j = Re ((S.k).j) by A8,A10,A12,COMSEQ_3:def 3
.= v*vol divset((T.k),j) by A14,Th1;
end;
len (Fk) = len(Tk) by A9,FINSEQ_1:def 3;
hence thesis by A11,INTEGR15:def 1;
end; then
reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def 3;
reconsider rseqi = middle_sum(pjinf,pjis) as Real_Sequence;
A19:for k be Nat holds rseqi.k =Re (xseq.k)
proof
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
A20: Re (S.kk) is middle_volume of Re f,T.kk by Th4;
thus rseqi.k = middle_sum(pjinf,pjis.kk) by INTEGR15:def 4
.= Re (middle_sum(f,S.kk)) by A6,A20,Th7
.= Re (xseq.k) by Def4;
end;
take rseqi;
lim (middle_sum(pjinf,pjis))=integral(pjinf) by A2,A3,INTEGR15:9;
hence thesis by A2,A3,A19,COMPLEX1:12,INTEGR15:9;
end; then
consider rseqi be Real_Sequence such that
A21:for k be Nat holds
rseqi.k = Re (xseq.k) & rseqi is convergent & Re xs = lim rseqi;
ex iseqi be Real_Sequence st for k be Nat holds
iseqi.k = Im (xseq.k) & iseqi is convergent & Im xs = lim iseqi
proof
reconsider pjinf= Im f as Function of A,REAL;
defpred P[Element of NAT,set] means $2= Im (S.$1);
A22:for x being Element of NAT ex y being Element of (REAL)* st P[x, y]
proof
let x be Element of NAT;
Im (S.x) is Element of (REAL)* by FINSEQ_1:def 11;
hence thesis;
end;
consider F being sequence of (REAL)* such that
A23:for x being Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A22);
A24:for x being Element of NAT holds dom(Im (S.x)) = Seg len(S.x)
proof
let x be Element of NAT;
dom(Im (S.x)) = dom (S.x) by COMSEQ_3:def 4
.= Seg len(S.x) by FINSEQ_1:def 3;
hence thesis;
end;
for k be Element of NAT holds F.k is middle_volume of pjinf,T.k
proof
let k be Element of NAT;
reconsider Tk=T.k as FinSequence;
reconsider Fk=F.k as FinSequence of REAL;
A25:F.k= Im (S.k) by A23; then
A26:dom (Fk) = Seg len(S.k) by A24
.= Seg len(Tk) by Def1; then
A27:dom (Fk) = dom (Tk) by FINSEQ_1:def 3;
A28:now let j be Nat;
assume A29: j in dom (Tk); then
consider r be Element of COMPLEX such that
A30:r in rng (f|divset((T.k),j)) and
A31:(S.k).j=r * vol divset((T.k),j) by Def1;
reconsider v=Im r as Element of REAL;
take v;
consider t be object such that
A32:t in dom (f|divset((T.k),j)) and
A33:r=(f|divset((T.k),j)).t by A30,FUNCT_1:def 3;
t in dom(f) /\ divset((T.k),j) by A32,RELAT_1:61; then
t in dom(f) by XBOOLE_0:def 4; then
A34:t in dom (Im f) by COMSEQ_3:def 4;
A35:dom (f|divset((T.k),j)) =dom (f) /\ divset((T.k),j) by RELAT_1:61
.=dom (pjinf) /\ divset((T.k),j) by COMSEQ_3:def 4
.=dom (pjinf|divset((T.k),j)) by RELAT_1:61;
Im r = Im (f.t) by A32,A33,FUNCT_1:47
.= (Im f).t by A34,COMSEQ_3:def 4
.= (pjinf|divset((T.k),j)).t by A32,A35,FUNCT_1:47;
hence v in rng (pjinf|divset((T.k),j)) by A32,A35,FUNCT_1:3;
thus (Fk).j = Im ((S.k).j) by A25,A27,A29,COMSEQ_3:def 4
.= v*vol divset((T.k),j) by A31,Th1;
end;
len (Fk) = len(Tk) by A26,FINSEQ_1:def 3;
hence thesis by A28,INTEGR15:def 1;
end; then
reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def 3;
reconsider iseqi = middle_sum(pjinf,pjis) as Real_Sequence;
A36:for k be Nat holds iseqi.k =Im (xseq.k)
proof
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
A37:Im (S.kk) is middle_volume of Im f,T.kk by Th4;
thus iseqi.k = middle_sum(pjinf,pjis.kk) by INTEGR15:def 4
.= Im (middle_sum(f,S.kk)) by A23,A37,Th8
.= Im (xseq.k) by Def4;
end;
take iseqi;
lim (middle_sum(pjinf,pjis))=integral(pjinf) by A2,A4,INTEGR15:9;
hence thesis by A2,A4,A36,COMPLEX1:12,INTEGR15:9;
end; then
consider iseqi be Real_Sequence such that
A38:for k be Nat holds
iseqi.k = Im (xseq.k) & iseqi is convergent & Im xs = lim iseqi;
thus middle_sum(f,S) is convergent by A21,A38,COMSEQ_3:38;
thus lim middle_sum(f,S) = lim(rseqi) + lim(iseqi)*<i> by A21,A38,COMSEQ_3:39
.= integral(f) by A21,A38,COMPLEX1:13;
end;
theorem
for A be non empty closed_interval Subset of REAL,
f being Function of A,COMPLEX
st f is bounded
holds
f is integrable iff
ex I be Element of COMPLEX
st for T being DivSequence of A,
S be 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
let A be non empty closed_interval Subset of REAL,
f be Function of A,COMPLEX;
assume A1: f is bounded;
hereby
reconsider I=integral(f) as Element of COMPLEX;
assume A2: f is integrable;
take I;
thus for T being DivSequence of A, S be 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 by A1,A2,Th14;
end;
now
assume ex I be Element of COMPLEX st for T being DivSequence of A,
S be 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; then
consider I be Element of COMPLEX such that
A3:for T being DivSequence of A, S be 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;
reconsider Ii=Re I as Element of REAL;
reconsider Ic=Im I as Element of REAL;
A4:now
set x=I;
let T be DivSequence of A,
Si be middle_volume_Sequence of (Re f) ,T;
defpred P[Element of NAT,set] means
ex H be FinSequence,
z be FinSequence st H=T.$1 & z = $2 & len z = len H &
for j be Element of NAT st j in dom H holds
ex rji be Element of COMPLEX,
tji be Element of REAL st
tji in dom (f|divset((T.$1),j))
& (Si.$1).j = vol divset((T.$1),j) * ((Re f)|divset((T.$1),j).tji)
& rji=(f|divset((T.$1),j)).tji
& z.j =(vol divset((T.$1) ,j))* rji;
reconsider xs=x as Element of COMPLEX;
A5:for k being Element of NAT ex y being Element of (COMPLEX)* st P[k,y]
proof
let k be Element of NAT;
reconsider Tk=T.k as FinSequence;
defpred P1[Nat, set] means
ex j be Element of NAT st $1 = j
& ex rji be Element of COMPLEX,
tji be Element of REAL
st tji in dom (f|divset((T.k),j))
& ((Si.k)).j = vol divset((T.k),j) * (((Re f)|divset((T.k),j)).tji)
& rji=(f|divset((T.k),j)).tji & $2=vol divset((T.k),j)*rji;
A6:for j be Nat st j in Seg len Tk
ex x being Element of COMPLEX st P1[j,x]
proof
let j0 be Nat;
assume A7: j0 in Seg len Tk; then
reconsider j = j0 as Element of NAT;
j in dom (Tk) by A7,FINSEQ_1:def 3; then
consider r be Element of REAL such that
A8:r in rng ((Re f)|divset((T.k),j)) and
A9:(Si.k).j= r* vol divset((T.k),j) by INTEGR15:def 1;
consider tji be object such that
A10:tji in dom ((Re f)|divset((T.k),j)) and
A11:r=((Re f)|divset((T.k),j)).tji by A8,FUNCT_1:def 3;
tji in dom(Re f) /\ divset((T.k),j) by A10,RELAT_1:61; then
reconsider tji as Element of REAL;
A12:dom (f|divset((T.k),j)) = dom (f) /\ divset((T.k),j) by RELAT_1:61
.= dom (Re f) /\ divset((T.k),j) by COMSEQ_3:def 3
.= dom ((Re f)|divset((T.k),j)) by RELAT_1:61; then
(f|divset((T.k),j)).tji in rng (f|divset((T.k),j)) by A10,FUNCT_1:3;
then
reconsider rji=(f|divset((T.k),j)).tji as Element of COMPLEX;
reconsider x=vol divset((T.k),j)*rji as Element of COMPLEX
by XCMPLX_0:def 2;
take x;
thus P1[j0,x] by A9,A10,A11,A12;
end;
consider p being FinSequence of COMPLEX such that
A13:dom p = Seg len Tk & for j be Nat st j in Seg len Tk holds P1[j,p.j]
from FINSEQ_1:sch 5(A6);
reconsider x=p as Element of (COMPLEX)* by FINSEQ_1:def 11;
take x;
A14:now
let jj0 be Element of NAT;
reconsider j0=jj0 as Nat;
A15:dom Tk = Seg len Tk by FINSEQ_1:def 3;
assume jj0 in dom Tk; then
P1[j0,p.j0] by A13,A15;
hence ex rji be Element of COMPLEX, tji be Element of REAL st
tji in dom (f|divset((T.k),jj0))
&(Si.k).jj0 = vol divset((T.k),jj0) * ((Re f)|divset((T.k),jj0).tji)
& rji=(f|divset((T.k),jj0)).tji
& p.jj0 =(vol divset ((T.k),jj0))* rji;
end;
len p = len Tk by A13,FINSEQ_1:def 3;
hence P[k,x] by A14;
end;
consider S being sequence of (COMPLEX)* such that
A16:for x being Element of NAT holds P[x, S.x] from FUNCT_2:sch 3(A5);
for k be Element of NAT holds S.k is middle_volume of f,T.k
proof
let k be Element of NAT;
consider H be FinSequence,z be FinSequence such that
A17:H=T.k & z = S.k & len H = len z and
A18:for j be Element of NAT st j in dom H holds
ex rji be Element of COMPLEX,
tji be Element of REAL st
tji in dom ( f|divset((T.k),j) )
& (Si.k).j = vol divset((T.k),j)* ((Re f)|divset((T.k),j).tji)
& rji=(f|divset((T.k ),j)).tji
& z.j =(vol divset((T.k),j))* rji by A16;
A19:now
let x be Nat;
assume A20: x in dom H; then
reconsider j=x as Element of NAT;
consider rji be Element of COMPLEX,
tji be Element of REAL such that
A21:tji in dom ( f|divset((T.k),j) ) and
(Si.k).j = vol divset((T.k),j) * (((Re f)|divset((T.k),j)). tji)
and
A22:rji=(f|divset((T.k),j)).tji and
A23:z.j =(vol divset((T.k),j))* rji by A18,A20;
take rji;
thus rji in rng (f|divset((T.k),x)) by A21,A22,FUNCT_1:3;
thus z.x =rji*(vol divset((T.k),x)) by A23;
end;
thus thesis by A17,A19,Def1;
end; then
reconsider S as middle_volume_Sequence of f,T by Def3;
set seq=middle_sum(f,S);
reconsider xseq=seq as sequence of COMPLEX;
assume delta(T) is convergent & lim delta(T)=0; then
A24:seq is convergent & lim seq = x by A3;
reconsider rseqi = Re seq as Real_Sequence;
A25:for k be Element of NAT holds
rseqi.k = Re (xseq.k) & rseqi is convergent & Re xs = lim rseqi
by A24,COMSEQ_3:41,def 5;
for k be Element of NAT holds rseqi.k = (middle_sum((Re f),Si)).k
proof
let k be Element of NAT;
consider H be FinSequence,z be FinSequence such that
A26:H=T.k and
A27:z = S.k and
A28:len H = len z and
A29:for j be Element of NAT st j in dom H holds
ex rji be Element of COMPLEX,
tji be Element of REAL st
tji in dom (f|divset((T.k),j))
& (Si.k).j = vol divset((T.k),j) * ((Re f)|divset((T.k),j).tji)
& rji=(f|divset((T.k ),j)).tji
& z.j =(vol divset((T.k),j))* rji by A16;
A30:dom(Re (S.k)) = dom (S.k) by COMSEQ_3:def 3
.=Seg len(H) by A27,A28,FINSEQ_1:def 3
.=Seg len(Si.k) by A26,INTEGR15:def 1
.=dom (Si.k) by FINSEQ_1:def 3;
A31:for j be Nat st j in dom(Re (S.k)) holds (Re (S.k)).j = (Si.k).j
proof
let j0 be Nat;
reconsider j=j0 as Element of NAT by ORDINAL1:def 12;
assume A32: j0 in dom(Re (S.k)); then
j0 in Seg len(Si.k) by A30,FINSEQ_1:def 3; then
j0 in Seg len(H) by A26,INTEGR15:def 1; then
j in dom H by FINSEQ_1:def 3; then
consider rji be Element of COMPLEX,
tji be Element of REAL such that
A33:tji in dom (f|divset((T.k),j)) and
A34:(Si.k).j = vol divset((T.k),j) * (((Re f)|divset((T.k),j)).tji)
and
A35:rji=(f|divset((T.k),j)).tji and
A36:z.j =(vol divset((T.k),j)) * rji by A29;
A37:dom(f|divset((T.k),j)) =dom(f) /\ divset((T.k),j) by RELAT_1:61
.=dom ((Re f)) /\ divset((T.k),j) by COMSEQ_3:def 3
.=dom ((Re f)|divset((T.k),j)) by RELAT_1:61; then
tji in dom((Re f)) /\ divset((T.k),j) by A33,RELAT_1:61; then
A38:tji in dom((Re f)) by XBOOLE_0:def 4;
A39:((Re f)|divset((T.k),j)).tji =(Re f).tji by A33,A37,FUNCT_1:47
.= Re (f.tji) by A38,COMSEQ_3:def 3
.= Re rji by A33,A35,FUNCT_1:47;
(Re (S.k)).j = Re ((S.k).j) by A32,COMSEQ_3:def 3
.= (Si.k).j by A34,A39,Th1,A27,A36;
hence thesis;
end;
A40:for j0 be object st j0 in dom (Re (S.k))
holds (Re (S.k)).j0 = (Si.k).j0 by A31;
thus rseqi.k = Re (xseq.k) by COMSEQ_3:def 5
.=Re (middle_sum(f,S.k)) by Def4
.=(middle_sum((Re f),Si.k)) by A30,A40,Th7,FUNCT_1:2
.=(middle_sum((Re f),Si)).k by INTEGR15:def 4;
end;
hence middle_sum((Re f),Si) is convergent
& lim (middle_sum((Re f),Si))=Ii by A25,FUNCT_2:63;
end;
Re f is bounded by A1,Th13; then
A41:(Re f) is integrable by A4,INTEGR15:10;
A42:now
set x=I;
let T be DivSequence of A,
Si be middle_volume_Sequence of (Im f), T;
defpred P[Element of NAT,set] means
ex H be FinSequence,z be FinSequence st
H=T.$1 & z = $2 & len z = len H &
for j be Element of NAT st j in dom H holds
ex rji be Element of COMPLEX,
tji be Element of REAL st
tji in dom (f|divset((T.$1),j))
& (Si.$1).j = vol divset((T.$1),j) * ((Im f)|divset((T.$1),j).tji)
& rji=(f|divset((T.$1),j)).tji
& z.j =(vol divset((T.$1),j))* rji;
reconsider xs=x as Element of COMPLEX;
A43:for k being Element of NAT ex y being Element of (COMPLEX)* st P[k,y]
proof
let k be Element of NAT;
reconsider Tk=T.k as FinSequence;
defpred P1[Nat, set] means
ex j be Element of NAT st $1 = j &
ex rji be Element of COMPLEX,
tji be Element of REAL st
tji in dom (f|divset((T.k),j))
& ((Si.k)).j = vol divset((T.k),j) * (((Im f)|divset((T.k),j)).tji)
& rji=(f|divset((T.k),j)).tji
& $2=vol divset((T.k),j)*rji;
A44
:for j be Nat st j in Seg len Tk ex x being Element of COMPLEX st P1[j,x]
proof
let j0 be Nat;
assume A45: j0 in Seg len Tk; then
reconsider j = j0 as Element of NAT;
j in dom (Tk) by A45,FINSEQ_1:def 3; then
consider r be Element of REAL such that
A46:r in rng ((Im f)|divset((T.k),j)) and
A47:(Si.k).j= r* vol divset((T.k),j) by INTEGR15:def 1;
consider tji be object such that
A48:tji in dom ((Im f)|divset((T.k),j)) and
A49:r=((Im f)|divset((T.k),j)).tji by A46,FUNCT_1:def 3;
tji in dom(Im f) /\ divset((T.k),j) by A48,RELAT_1:61; then
reconsider tji as Element of REAL;
A50:dom (f|divset((T.k),j)) = dom (f) /\ divset((T.k),j) by RELAT_1:61
.= dom (Im f) /\ divset((T.k),j) by COMSEQ_3:def 4
.= dom ((Im f)|divset((T.k),j)) by RELAT_1:61; then
(f|divset((T.k),j)).tji in rng (f|divset((T.k),j)) by A48,FUNCT_1:3;
then
reconsider rji=(f|divset((T.k),j)).tji as Element of COMPLEX;
reconsider x=vol divset((T.k),j)*rji as Element of COMPLEX
by XCMPLX_0:def 2;
take x;
thus P1[j0,x] by A47,A48,A49,A50;
end;
consider p being FinSequence of COMPLEX such that
A51:dom p = Seg len Tk &
for j be Nat st j in Seg len Tk holds P1[j,p.j] from FINSEQ_1:sch 5(A44);
reconsider x=p as Element of (COMPLEX)* by FINSEQ_1:def 11;
take x;
A52:now
let jj0 be Element of NAT;
reconsider j0=jj0 as Nat;
A53:dom Tk = Seg len Tk by FINSEQ_1:def 3;
assume jj0 in dom Tk; then
P1[j0,p.j0] by A51,A53;
hence
ex rji be Element of COMPLEX, tji be Element of REAL st
tji in dom (f|divset((T.k),jj0))
& (Si.k).jj0 = vol divset((T.k),jj0) * ((Im f)|divset((T.k),jj0).tji)
& rji=(f|divset((T.k),jj0)).tji
& p.jj0 =(vol divset ((T.k),jj0)) * rji;
end;
len p = len Tk by A51,FINSEQ_1:def 3;
hence P[k,x] by A52;
end;
consider S being sequence of (COMPLEX) * such that
A54:for x being Element of NAT holds P[x, S.x] from FUNCT_2:sch 3(A43);
for k be Element of NAT holds S.k is middle_volume of f,T.k
proof
let k be Element of NAT;
consider H be FinSequence,z be FinSequence such that
A55:H=T.k & z = S.k & len H = len z and
A56:for j be Element of NAT st j in dom H holds
ex rji be Element of COMPLEX,
tji be Element of REAL st
tji in dom (f|divset((T.k),j))
& (Si.k).j = vol divset((T.k),j) * ((Im f)|divset((T.k),j).tji)
& rji=(f|divset((T.k ),j)).tji
& z.j =(vol divset((T.k),j))* rji by A54;
A57:now
let x be Nat;
assume A58: x in dom H; then
reconsider j=x as Element of NAT;
consider rji be Element of COMPLEX,
tji be Element of REAL such that
A59:tji in dom (f|divset((T.k),j)) and
(Si.k).j = vol divset((T.k),j) * (((Im f)|divset((T.k),j)).tji) and
A60:rji=(f|divset((T.k),j)).tji and
A61:z.j =(vol divset((T.k),j))* rji by A56,A58;
take rji;
thus rji in rng (f|divset((T.k),x)) by A59,A60,FUNCT_1:3;
thus z.x =rji*(vol divset((T.k),x)) by A61;
end;
thus thesis by A55,A57,Def1;
end; then
reconsider S as middle_volume_Sequence of f,T by Def3;
set seq=middle_sum(f,S);
reconsider xseq=seq as sequence of COMPLEX;
assume delta(T) is convergent & lim delta(T)=0; then
A62:seq is convergent & lim seq = x by A3;
reconsider rseqi = Im seq as Real_Sequence;
A63:for k be Element of NAT holds rseqi.k = Im (xseq.k) & rseqi is convergent
& Im xs = lim rseqi by A62,COMSEQ_3:41,def 6;
for k be Element of NAT holds rseqi.k = (middle_sum((Im f),Si)).k
proof
let k be Element of NAT;
consider H be FinSequence,z be FinSequence such that
A64:H=T.k and
A65:z = S.k and
A66:len H = len z and
A67:for j be Element of NAT st j in dom H holds
ex rji be Element of COMPLEX,
tji be Element of REAL st
tji in dom (f|divset((T.k),j))
& (Si.k).j = vol divset((T.k),j) * ((Im f)|divset((T.k),j).tji)
& rji=(f|divset((T.k ),j)).tji
& z.j =(vol divset((T.k),j)) * rji by A54;
A68:dom(Im (S.k)) =dom (S.k) by COMSEQ_3:def 4
.=Seg len(H) by A65,A66,FINSEQ_1:def 3
.=Seg len(Si.k) by A64,INTEGR15:def 1
.=dom (Si.k) by FINSEQ_1:def 3;
A69:for j be Nat st j in dom(Im (S.k)) holds (Im (S.k)).j = (Si.k).j
proof
let j0 be Nat;
reconsider j=j0 as Element of NAT by ORDINAL1:def 12;
assume A70: j0 in dom(Im (S.k)); then
j0 in Seg len(Si.k) by A68,FINSEQ_1:def 3; then
j0 in Seg len(H) by A64,INTEGR15:def 1; then
j in dom H by FINSEQ_1:def 3; then
consider rji be Element of COMPLEX,
tji be Element of REAL such that
A71:tji in dom (f|divset((T.k),j)) and
A72:(Si.k).j = vol divset((T.k),j) * (((Im f)|divset((T.k),j)).tji)
and
A73:rji=(f|divset((T.k),j)).tji and
A74:z.j =(vol divset((T.k),j))* rji by A67;
A75:dom (f|divset((T.k),j)) = dom (f) /\ divset((T.k),j)
by RELAT_1:61
.=dom ((Im f)) /\ divset((T.k),j) by COMSEQ_3:def 4
.=dom ((Im f)|divset((T.k),j)) by RELAT_1:61; then
tji in dom((Im f)) /\ divset((T.k),j) by A71,RELAT_1:61; then
A76:tji in dom((Im f)) by XBOOLE_0:def 4;
A77:((Im f)|divset((T.k),j)).tji =(Im f).tji by A71,A75,FUNCT_1:47
.= Im (f.tji) by A76,COMSEQ_3:def 4
.= Im rji by A71,A73,FUNCT_1:47;
(Im (S.k)).j = Im ((S.k).j) by A70,COMSEQ_3:def 4
.= (Si.k).j by A72,A77,A65,A74,Th1;
hence thesis;
end;
A78:for j0 be object st j0 in dom (Im (S.k))
holds (Im (S.k)).j0 = (Si.k).j0 by A69;
thus rseqi.k = Im (xseq.k) by COMSEQ_3:def 6
.=Im (middle_sum(f,S.k)) by Def4
.=(middle_sum((Im f),Si.k)) by A78,A68,Th8,FUNCT_1:2
.=(middle_sum((Im f),Si)).k by INTEGR15:def 4;
end;
hence middle_sum((Im f),Si) is convergent
& lim (middle_sum((Im f),Si))=Ic by A63,FUNCT_2:63;
end;
Im f is bounded by A1,Th13; then
(Im f) is integrable by A42,INTEGR15:10;
hence f is integrable by A41;
end;
hence thesis;
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
(Re f) is_integrable_on A & (Im f) is_integrable_on A;
end;
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
integral((Re f),A) + integral((Im f),A)*<i>;
correctness by XCMPLX_0:def 2;
end;
Lm4:
for f be PartFunc of REAL,COMPLEX, A be Subset of REAL holds
Re (f|A) = (Re f)|A & Im (f|A) = (Im f)|A
proof
let f be PartFunc of REAL,COMPLEX,
A be Subset of REAL;
dom((Re f)|A) = (dom Re f) /\ A by RELAT_1:61
.= dom f /\ A by COMSEQ_3:def 3; then
A1: dom((Re f)|A) = dom(f|A) by RELAT_1:61
.= dom Re(f|A) by COMSEQ_3:def 3;
now
let x be object;
assume A2: x in dom(Re(f)|A); then
A3: x in dom Re(f) /\ A by RELAT_1:61; then
A4: x in dom Re f by XBOOLE_0:def 4;
A5: x in A by A3,XBOOLE_0:def 4;
thus Re(f|A).x = Re((f|A).x) by A1,A2,COMSEQ_3:def 3
.= Re(f.x) by A5,FUNCT_1:49
.= (Re f).x by A4,COMSEQ_3:def 3
.= ((Re f)|A).x by A5,FUNCT_1:49;
end;
hence Re(f)|A = Re(f|A) by A1,FUNCT_1:2;
dom((Im f)|A) = (dom Im f) /\ A by RELAT_1:61
.= dom f /\ A by COMSEQ_3:def 4; then
A6: dom((Im f)|A) = dom(f|A) by RELAT_1:61
.= dom Im(f|A) by COMSEQ_3:def 4;
now
let x be object;
assume A7: x in dom(Im(f)|A); then
A8: x in dom Im(f) /\ A by RELAT_1:61; then
A9: x in dom Im f by XBOOLE_0:def 4;
A10: x in A by A8,XBOOLE_0:def 4;
thus Im(f|A).x = Im((f|A).x) by A6,A7,COMSEQ_3:def 4
.= Im(f.x) by A10,FUNCT_1:49
.= (Im f).x by A9,COMSEQ_3:def 4
.= ((Im f)|A).x by A10,FUNCT_1:49;
end;
hence thesis by A6,FUNCT_1:2;
end;
theorem
for A be non empty closed_interval Subset of REAL,
f be PartFunc of REAL,COMPLEX,
g be Function of A,COMPLEX st f|A = g
holds f is_integrable_on A iff g is integrable
proof
let A be non empty closed_interval Subset of REAL,
f be PartFunc of REAL,COMPLEX,
g be Function of A,COMPLEX;
assume A1: f|A = g;
thus f is_integrable_on A implies g is integrable
proof
assume A2: f is_integrable_on A;
(Re g) is integrable & (Im g) is integrable
proof
A3:A = dom g by FUNCT_2:def 1
.= dom f /\ A by A1,RELAT_1:61;
then A = dom (Re f) /\ A by COMSEQ_3:def 3; then
(Re f)||A is total by INTEGRA5:6,XBOOLE_1:17; then
reconsider F = (Re f)|A as Function of A,REAL;
A4:(Re f) is_integrable_on A by A2;
dom g = A by FUNCT_2:def 1; then
reconsider g0=g as PartFunc of REAL,COMPLEX by RELSET_1:5;
Re g = Re g0
.= F by A1,Lm4;
hence (Re g) is integrable by A4;
A = dom (Im f) /\ A by A3,COMSEQ_3:def 4; then
(Im f)||A is total by INTEGRA5:6,XBOOLE_1:17; then
reconsider G = (Im f)|A as Function of A,REAL;
A5:(Im f) is_integrable_on A by A2;
Im g = Im g0
.= G by A1,Lm4;
hence (Im g) is integrable by A5;
end;
hence thesis;
end;
assume A6: g is integrable;
(Re f) is_integrable_on A & (Im f) is_integrable_on A
by A1,Lm4,A6;
hence thesis;
end;
theorem
for A be non empty closed_interval Subset of REAL,
f be PartFunc of REAL,COMPLEX,
g be Function of A,COMPLEX st f|A = g holds
integral(f,A) = integral(g)
proof
let A be non empty closed_interval Subset of REAL,
f be PartFunc of REAL,COMPLEX,
g be Function of A,COMPLEX;
assume A1: f|A = g;
A2: A = dom g by FUNCT_2:def 1
.= dom f /\ A by A1,RELAT_1:61; then
A = dom (Re f) /\ A by COMSEQ_3:def 3; then
(Re f)||A is total by INTEGRA5:6,XBOOLE_1:17; then
reconsider F = (Re f)|A as Function of A,REAL;
dom g = A by FUNCT_2:def 1; then
reconsider g0=g as PartFunc of REAL,COMPLEX by RELSET_1:5;
A3: Re g = Re g0
.= F by A1,Lm4;
A = dom (Im f) /\ A by A2,COMSEQ_3:def 4; then
(Im f)||A is total by INTEGRA5:6,XBOOLE_1:17; then
reconsider G = (Im f)|A as Function of A,REAL;
Im g = Im g0
.= G by A1,Lm4;
hence integral(f,A) = integral(g) by A3;
end;
definition
let a,b be Real;
let f be PartFunc of REAL, COMPLEX;
func integral(f,a,b) -> Element of COMPLEX equals
integral((Re f),a,b) + integral((Im f),a,b) *<i>;
correctness by XCMPLX_0:def 2;
end;
begin :: Linearity of the Integration Operator
theorem Th18:
for c be Complex, f be 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
let c be Complex,
f be PartFunc of REAL, COMPLEX;
A1:dom (Re (c(#)f)) = dom (c(#)f) by COMSEQ_3:def 3
.= dom f by VALUED_1:def 5;
A2:dom (Im (c(#)f)) = dom (c(#)f) by COMSEQ_3:def 4
.= dom f by VALUED_1:def 5;
A3:dom ((Re c)(#)(Re f)) = dom (Re f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 3;
A4:dom ((Im c)(#)(Im f)) = dom (Im f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 4;
A5:dom ((Im c)(#)(Re f)) = dom (Re f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 3;
A6:dom ((Re c)(#)(Im f)) = dom (Im f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 4;
A7: dom (Re (c(#)f)) = (dom f) /\ (dom f) by A1
.=dom ((Re c)(#)(Re f) - (Im c)(#)(Im f)) by A3,A4,VALUED_1:12;
A8: dom (Im (c(#)f)) = (dom f) /\ (dom f) by A2
.=dom ((Re c)(#)(Im f) + (Im c)(#)(Re f)) by A5,A6,VALUED_1:def 1;
now let x be object;
assume A9: x in dom (Re (c(#)f)); then
A10: x in dom (Re f) & x in dom (Im f) by A1,COMSEQ_3:def 3,def 4;
thus (Re (c(#)f)).x = Re ((c(#)f).x) by A9,COMSEQ_3:def 3
.=Re (c*(f.x)) by VALUED_1:6
.=Re c * Re (f.x) - Im c * Im (f.x) by COMPLEX1:9
.=Re c * (Re f).x - Im c * Im (f.x) by A10,COMSEQ_3:def 3
.=Re c * (Re f).x - Im c * (Im f).x by A10,COMSEQ_3:def 4
.=((Re c)(#)(Re f)).x - Im c * (Im f).x by VALUED_1:6
.=((Re c)(#)(Re f)).x - ((Im c)(#)(Im f)).x by VALUED_1:6
.=((Re c)(#)(Re f) - (Im c)(#)(Im f)).x by A9,A7,VALUED_1:13;
end;
hence Re (c(#)f) = (Re c)(#)(Re f) - (Im c)(#)(Im f) by A7,FUNCT_1:2;
now let x be object;
assume A11: x in dom (Im (c(#)f)); then
A12: x in dom (Re f) & x in dom (Im f) by A2,COMSEQ_3:def 3,def 4;
thus (Im (c(#)f)).x = Im ((c(#)f).x) by A11,COMSEQ_3:def 4
.=Im (c*(f.x)) by VALUED_1:6
.=Re c * Im (f.x) + Im c * Re (f.x) by COMPLEX1:9
.=Re c * (Im f).x + Im c * Re (f.x) by A12,COMSEQ_3:def 4
.=Re c * (Im f).x + Im c * (Re f).x by A12,COMSEQ_3:def 3
.=((Re c)(#)(Im f)).x + Im c * (Re f).x by VALUED_1:6
.=((Re c)(#)(Im f)).x + ((Im c)(#)(Re f)).x by VALUED_1:6
.=((Re c)(#)(Im f) + (Im c)(#)(Re f)).x by A11,A8,VALUED_1:def 1;
end;
hence Im (c(#)f) = (Re c)(#)(Im f) + (Im c)(#)(Re f) by A8,FUNCT_1:2;
end;
theorem
for A be non empty closed_interval Subset of REAL,
f1,f2 be 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
let A be non empty closed_interval Subset of REAL;
let f1,f2 be PartFunc of REAL, COMPLEX;
assume that
A1: f1 is_integrable_on A & f2 is_integrable_on A and
A2: A c= dom f1 & A c= dom f2 and
A3: f1|A is bounded and
A4: f2|A is bounded;
A5: (Re f1) + (Re f2) is_integrable_on A & (Im f1) + (Im f2) is_integrable_on A
& integral((Re f1) + (Re f2),A) = integral((Re f1),A) + integral((Re f2),A)
& integral((Im f1) + (Im f2),A) = integral((Im f1),A) + integral((Im f2),A)
& (Re f1) - (Re f2) is_integrable_on A
& (Im f1) - (Im f2) is_integrable_on A
& integral((Re f1) - (Re f2),A) = integral((Re f1),A) - integral((Re f2),A)
& integral((Im f1) - (Im f2),A) = integral((Im f1),A) - integral((Im f2),A)
proof
A6:A c= dom (Re f1) & A c= dom (Re f2) &
A c= dom (Im f1) & A c= dom (Im f2) by A2,COMSEQ_3:def 3,def 4;
Re (f2|A) is bounded & Im (f2|A) is bounded by A4,Th11; then
A7:(Re f2)|A is bounded & (Im f2)|A is bounded by Lm4;
Re (f1|A) is bounded & Im (f1|A) is bounded by A3,Th11; then
A8:(Re f1)|A is bounded & (Im f1)|A is bounded by Lm4;
A9:Re f1 is_integrable_on A & Im f1 is_integrable_on A
& Re f2 is_integrable_on A & Im f2 is_integrable_on A by A1;
hence (Re f1) + (Re f2) is_integrable_on A
& (Im f1) + (Im f2) is_integrable_on A
& integral((Re f1)+(Re f2),A)=integral((Re f1),A)+integral((Re f2),A)
& integral((Im f1)+(Im f2),A)=integral((Im f1),A)+integral((Im f2),A)
by A6,A7,A8,INTEGRA6:11;
thus (Re f1) - (Re f2) is_integrable_on A
& (Im f1) - (Im f2) is_integrable_on A
& integral((Re f1)-(Re f2),A)=integral((Re f1),A)-integral((Re f2),A)
& integral((Im f1)-(Im f2),A)=integral((Im f1),A)-integral((Im f2),A)
by A6,A7,A8,A9,INTEGRA6:11;
end;
then Re (f1+f2) is_integrable_on A & Im (f1+f2) is_integrable_on A
& Re (f1-f2) is_integrable_on A & Im (f1-f2) is_integrable_on A
by MESFUN6C:5,6;
hence f1+f2 is_integrable_on A & f1-f2 is_integrable_on A;
Re(integral(f1,A)) + Re(integral(f2,A))
=integral((Re f1),A) + integral((Re f2),A)
& Im(integral(f1,A)) + Im(integral(f2,A))
=integral((Im f1),A) + integral((Im f2),A)
& Re(integral(f1,A)) - Re(integral(f2,A))
=integral((Re f1),A) - integral((Re f2),A)
& Im(integral(f1,A)) - Im(integral(f2,A))
=integral((Im f1),A) - integral((Im f2),A)
proof
Re (integral(f1,A)) = integral((Re f1),A)
& Im (integral(f1,A)) = integral((Im f1),A)
& Re (integral(f2,A)) = integral((Re f2),A)
& Im (integral(f2,A)) = integral((Im f2),A) by COMPLEX1:12;
hence thesis;
end; then
Re (integral(f1,A)) + Re (integral(f2,A)) = integral(Re (f1+f2),A)
& Im (integral(f1,A)) + Im (integral(f2,A))
= integral(Im (f1+f2),A)
& Re (integral(f1,A)) - Re (integral(f2,A))
= integral(Re (f1-f2),A)
& Im (integral(f1,A)) - Im (integral(f2,A))
= integral(Im (f1-f2),A) by A5,MESFUN6C:5,6; then
A10: Re (integral(f1+f2,A)) = Re (integral(f1,A)) + Re (integral(f2,A))
& Im (integral(f1+f2,A)) = Im (integral(f1,A)) + Im (integral(f2,A))
& Re (integral(f1-f2,A)) = Re (integral(f1,A)) - Re (integral(f2,A))
& Im (integral(f1-f2,A)) = Im (integral(f1,A)) - Im (integral(f2,A))
by COMPLEX1:12; then
Re (integral(f1+f2,A)) = Re (integral(f1,A) + integral(f2,A))
& Im (integral(f1+f2,A)) = Im (integral(f1,A) + integral(f2,A))
by COMPLEX1:8;
hence integral(f1+f2,A)=integral(f1,A)+integral(f2,A);
Re (integral(f1-f2,A)) = Re (integral(f1,A) - integral(f2,A))
& Im (integral(f1-f2,A)) = Im (integral(f1,A) - integral(f2,A))
by A10,COMPLEX1:19;
hence integral(f1-f2,A)=integral(f1,A)-integral(f2,A);
end;
theorem
for r be Real for A be non empty closed_interval Subset of REAL
for f be 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
let r be Real;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL, COMPLEX;
assume that A1: A c= dom f and
A2: f is_integrable_on A and
A3: f|A is bounded;
A4: (Re f) is_integrable_on A & (Im f) is_integrable_on A by A2;
A5: integral(r(#)(Re f), A)=r*integral((Re f), A)
& integral(r(#)(Im f), A)=r*integral((Im f), A)
proof
Re (f|A) is bounded & Im (f|A) is bounded by A3,Th11; then
A6: (Re f)|A is bounded & (Im f)|A is bounded by Lm4;
A7: A c= dom (Re f) & A c= dom (Im f) by A1,COMSEQ_3:def 3,def 4;
hence integral(r(#)(Re f),A)=r*integral((Re f),A) by A4,A6,INTEGRA6:9;
thus integral(r(#)(Im f),A)=r*integral((Im f),A) by A4,A6,A7,INTEGRA6:9;
end;
A8: Re (integral((r(#)f), A)) = r * Re (integral(f,A))
& Im (integral((r(#)f), A)) = r * Im (integral(f,A))
proof
Re (integral((r(#)f),A)) = integral((Re (r(#)f)),A)
& r*Re (integral(f,A)) = r*integral((Re f),A)
& Im (integral((r(#)f),A)) = integral((Im (r(#)f)),A)
& r*Im (integral(f,A)) = r*integral((Im f),A) by COMPLEX1:12;
hence thesis by A5,MESFUN6C:2;
end;
(Re (r(#)f)) is_integrable_on A & (Im (r(#)f)) is_integrable_on A
proof
(Re f)|A = Re (f|A) & (Im f)|A = Im (f|A) by Lm4; then
A9:(Re f)|A is bounded & (Im f)|A is bounded by A3,Th11;
A10:A c= dom (Re f) & A c= dom (Im f) by A1,COMSEQ_3:def 3,def 4;
(Re f) is_integrable_on A & (Im f) is_integrable_on A by A2; then
r(#)(Re f) is_integrable_on A & r(#)(Im f ) is_integrable_on A
by A9,A10,INTEGRA6:9;
hence thesis by MESFUN6C:2;
end;
hence r(#)f is_integrable_on A;
Re (integral((r(#)f), A)) = Re (r*integral(f,A))
& Im (integral((r(#)f), A)) = Im (r*integral(f,A)) by A8,Th1;
hence thesis;
end;
theorem
for c be Complex, A be non empty closed_interval Subset of REAL,
f be 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
let c be Complex;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL, COMPLEX;
assume that A1: A c= dom f and
A2: f is_integrable_on A and
A3: f|A is bounded;
A4: Re(c*integral(f,A)) = (Re c)*integral((Re f),A)-(Im c)*integral((Im f),A)
& Im(c*integral(f,A)) = (Re c)*integral((Im f),A)+(Im c)*integral((Re f),A)
proof
A5: Re (integral(f,A)) = integral((Re f),A) by COMPLEX1:12;
A6: Im (integral(f,A)) = integral((Im f),A) by COMPLEX1:12;
hence Re(c*integral(f,A))
= (Re c)*integral((Re f),A) - (Im c)*integral((Im f),A)
by A5,COMPLEX1:9;
thus Im(c*integral(f,A))
= (Re c)*integral((Im f),A) + (Im c)*integral((Re f),A)
by A5,A6,COMPLEX1:9;
end;
(Re f)|A = Re (f|A) & (Im f)|A = Im (f|A) by Lm4; then
A7: (Re f)|A is bounded & (Im f)|A is bounded by A3,Th11;
A8: A c= dom (Re f) & A c= dom (Im f) by A1,COMSEQ_3:def 3,def 4;
A9: (Re f) is_integrable_on A & (Im f) is_integrable_on A by A2; then
A10: (Re c)(#)(Re f) is_integrable_on A & (Re c)(#)(Im f) is_integrable_on A
& (Im c)(#)(Re f) is_integrable_on A
& (Im c)(#)(Im f) is_integrable_on A by A7,A8,INTEGRA6:9;
A11: Re (c(#)f) = (Re c)(#)(Re f) - (Im c)(#)(Im f)
& Im (c(#)f) = (Re c)(#)(Im f) + (Im c)(#)(Re f) by Th18;
A12: ((Re c)(#)(Re f))|A is bounded & ((Re c)(#)(Im f))|A is bounded
& ((Im c)(#)(Re f))|A is bounded
& ((Im c)(#)(Im f))|A is bounded by A7,RFUNCT_1:80;
dom (Re f) = dom f & dom (Im f) = dom f by COMSEQ_3:def 3,def 4; then
A13: A c= dom ((Re c)(#)(Re f)) & A c= dom ((Re c)(#)(Im f))
& A c= dom ((Im c)(#)(Re f))
& A c= dom ((Im c)(#)(Im f)) by A1,VALUED_1:def 5; then
A14: Re (c(#)f) is_integrable_on A by A10,A11,A12,INTEGRA6:11;
Im (c(#)f) is_integrable_on A by A10,A11,A12,A13,INTEGRA6:11;
hence c(#)f is_integrable_on A by A14;
A15: Re (integral((c(#)f), A)) = integral(Re (c(#)f),A) by COMPLEX1:12
.= integral((Re c)(#)(Re f),A) - integral((Im c)(#)(Im f),A)
by A10,A11,A12,A13,INTEGRA6:11
.= (Re c)*integral((Re f),A) - integral((Im c)(#)(Im f),A)
by A9,A7,A8,INTEGRA6:9
.= Re (c*integral(f,A)) by A4,A9,A7,A8,INTEGRA6:9;
Im (integral((c(#)f), A)) = integral( Im (c(#)f),A) by COMPLEX1:12
.= integral((Re c)(#)(Im f),A) + integral((Im c)(#)(Re f),A)
by A10,A11,A12,A13,INTEGRA6:11
.= (Re c)*integral((Im f),A) + integral((Im c)(#)(Re f),A)
by A9,A7,A8,INTEGRA6:9
.= Im (c*integral(f,A)) by A4,A9,A7,A8,INTEGRA6:9;
hence thesis by A15;
end;
theorem
for f being PartFunc of REAL,COMPLEX,
A being non empty closed_interval Subset of REAL,
a,b be Real st A=[.a,b.]
holds integral(f,A) = integral(f,a,b)
proof
let f be PartFunc of REAL,COMPLEX,
A be non empty closed_interval Subset of REAL, a,b be Real;
assume A1: A=[.a,b.];
Re (integral(f,A)) = integral((Re f),A)
& Im (integral(f,A)) = integral((Im f),A)
& Re (integral(f,a,b)) =integral((Re f), a,b)
& Im (integral(f,a,b)) =integral((Im f), a,b) by COMPLEX1:12; then
Re (integral(f,A)) = Re (integral(f,a,b))
& Im (integral(f,A)) = Im (integral(f,a,b)) by A1,INTEGRA5:19;
hence integral(f,A)=integral(f,a,b);
end;
theorem
for f being PartFunc of REAL,COMPLEX,
A being non empty closed_interval Subset of REAL,
a,b be Real st A=[.b,a.]
holds -integral(f,A) = integral(f,a,b)
proof
let f be PartFunc of REAL,COMPLEX,
A be non empty closed_interval Subset of REAL, a,b be Real;
assume A1: A=[.b,a.];
A2: Re (integral(f,a,b)) = integral((Re f), a,b)
& Im (integral(f,a,b)) = integral((Im f), a,b) by COMPLEX1:12;
A3: Re (-integral(f,A)) = -(Re (integral(f,A))) by COMPLEX1:17
.= -integral((Re f),A) by COMPLEX1:12;
A4: Im (-integral(f,A)) = -(Im (integral(f,A))) by COMPLEX1:17
.=-integral((Im f),A) by COMPLEX1:12;
A5: Re (-integral(f,A)) = Re (integral(f,a,b)) by A3,A1,A2,INTEGRA5:20;
Im (-integral(f,A)) = Im (integral(f,a,b)) by A4,A1,A2,INTEGRA5:20;
hence thesis by A5;
end;