:: Complex Integral
:: by Masahiko Yamazaki , Hiroshi Yamazaki , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 10, 2009
:: Copyright (c) 2009-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, FDIFF_1, SEQ_1, FUNCT_1, ZFMISC_1, MCART_1, ARYTM_3, RELAT_1, XCMPLX_0, REAL_1, PARTFUN1, INTEGRA1, COMPLEX1, VALUED_1, ARYTM_1, XBOOLE_0, TARSKI, XXREAL_0, XXREAL_1, RCOMP_1, ORDINAL2, SIN_COS, CARD_1, FDIFF_3, FUNCT_2, SEQ_2, TOPMETR, INTEGRA5, VFUNCT_1, XXREAL_2, INTEGR1C, MEASURE5, VALUED_0, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, VALUED_0, FUNCT_3, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, REAL_1, BINOP_1, RCOMP_1, SEQ_1, SEQ_2, FCONT_1, FDIFF_1, COMSEQ_3, TOPMETR, MCART_1, MEASURE5, INTEGRA5, SIN_COS, VALUED_1, PRE_TOPC, FDIFF_3, STRUCT_0, XXREAL_2;
definitions TARSKI;
theorems ZFMISC_1, XCMPLX_0, TOPMETR, SEQ_4, INTEGRA1, RFUNCT_1, FUNCT_1, SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, COMPLEX1, FUNCT_3, TARSKI, RCOMP_1, FCONT_1, RFUNCT_2, FDIFF_2, RELAT_1, XXREAL_1, FUNCT_2, NUMBERS, XBOOLE_0, XBOOLE_1, XREAL_1, INTEGRA5, SIN_COS, INTEGRA6, CFUNCT_1, VALUED_1, MESFUN6C, TOPS_1, FDIFF_3, RELSET_1, XXREAL_2, MCART_1, BORSUK_5, COMSEQ_3, MEASURE5, XREAL_0, ORDINAL1;
schemes FUNCT_2, FUNCT_7;
registrations XREAL_0, FUNCT_2, NUMBERS, ORDINAL1, MEMBERED, SIN_COS, FDIFF_1, SUBSET_1, XCMPLX_0, RELAT_1, XXREAL_0, XBOOLE_0, VALUED_0, VALUED_1, RELSET_1, MEASURE5, XTUPLE_0;
constructors HIDDEN, REAL_1, FDIFF_1, RFUNCT_3, FCONT_1, INTEGRA5, SIN_COS, TOPMETR, FDIFF_3, MESFUN6C, SEQ_2, RVSUM_1, COMSEQ_3, INTEGRA1, COMSEQ_2, XTUPLE_0, BINOP_2, BINOP_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities INTEGRA5, VALUED_1, ORDINAL1;
expansions TARSKI;


definition
func R2-to-C -> Function of [:REAL,REAL:],COMPLEX means :Def1: :: INTEGR1C:def 1
 for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
it . [a,b] = a + (b * <i>);
existence
ex b1 being Function of [:REAL,REAL:],COMPLEX st
for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b1 . [a,b] = a + (b * <i>)
proof end;
uniqueness
for b1, b2 being Function of [:REAL,REAL:],COMPLEX st ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b1 . [a,b] = a + (b * <i>) ) & ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b2 . [a,b] = a + (b * <i>) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines R2-to-C INTEGR1C:def 1 :
for b1 being Function of [:REAL,REAL:],COMPLEX holds
( b1 = R2-to-C iff for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b1 . [a,b] = a + (b * <i>) );

definition
let a, b be Real;
let x, y be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let f be PartFunc of COMPLEX,COMPLEX;
func integral (f,x,y,a,b,Z) -> Complex means :Def2: :: INTEGR1C:def 2
 ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & it = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) );
existence
ex b1 being Complex ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b1 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) )
proof end;
uniqueness
for b1, b2 being Complex st ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b1 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) & ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b2 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines integral INTEGR1C:def 2 :
for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for f being PartFunc of COMPLEX,COMPLEX
for b7 being Complex holds
( b7 = integral (f,x,y,a,b,Z) iff ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b7 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) );

definition
let C be PartFunc of REAL,COMPLEX;
attr C is C1-curve-like means :Def3: :: INTEGR1C:def 3
 ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] );
end;

:: deftheorem Def3 defines C1-curve-like INTEGR1C:def 3 :
for C being PartFunc of REAL,COMPLEX holds
( C is C1-curve-like iff ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] ) );

registration
cluster Relation-like REAL -defined COMPLEX -valued Function-like complex-valued C1-curve-like for Element of bool [:REAL,COMPLEX:];
existence
ex b1 being PartFunc of REAL,COMPLEX st b1 is C1-curve-like
proof end;
end;

definition
mode C1-curve is C1-curve-like PartFunc of REAL,COMPLEX;
end;

Lm1: for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z1, Z2 being Subset of REAL
for f being PartFunc of COMPLEX,COMPLEX st a <= b & [.a,b.] c= dom x & [.a,b.] c= dom y & Z1 is open & Z2 is open & [.a,b.] c= Z1 & Z1 c= Z2 & x is_differentiable_on Z2 & y is_differentiable_on Z2 & rng ((x + (<i> (#) y)) | [.a,b.]) c= dom f holds
integral (f,x,y,a,b,Z1) = integral (f,x,y,a,b,Z2)
proof end;

Lm2: for a, b being Real
for x1, y1, x2, y2 being PartFunc of REAL,REAL
for Z being Subset of REAL
for f being PartFunc of COMPLEX,COMPLEX st a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
proof end;

definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
assume A1: rng C c= dom f ;
func integral (f,C) -> Complex means :Def4: :: INTEGR1C:def 4
 ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & it = integral (f,x,y,a,b,Z) );
existence
ex b1 being Complex ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b1 = integral (f,x,y,a,b,Z) )
proof end;
uniqueness
for b1, b2 being Complex st ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b1 = integral (f,x,y,a,b,Z) ) & ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b2 = integral (f,x,y,a,b,Z) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines integral INTEGR1C:def 4 :
for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve st rng C c= dom f holds
for b3 being Complex holds
( b3 = integral (f,C) iff ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b3 = integral (f,x,y,a,b,Z) ) );

definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
pred f is_integrable_on C means :: INTEGR1C:def 5
 for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for u0, v0 being PartFunc of REAL,REAL st a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] holds
( (u0 (#) (x `| Z)) - (v0 (#) (y `| Z)) is_integrable_on ['a,b'] & (v0 (#) (x `| Z)) + (u0 (#) (y `| Z)) is_integrable_on ['a,b'] );
end;

:: deftheorem defines is_integrable_on INTEGR1C:def 5 :
for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve holds
( f is_integrable_on C iff for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for u0, v0 being PartFunc of REAL,REAL st a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] holds
( (u0 (#) (x `| Z)) - (v0 (#) (y `| Z)) is_integrable_on ['a,b'] & (v0 (#) (x `| Z)) + (u0 (#) (y `| Z)) is_integrable_on ['a,b'] ) );

definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
pred f is_bounded_on C means :: INTEGR1C:def 6
 for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for u0, v0 being PartFunc of REAL,REAL st a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] holds
( ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is bounded & ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is bounded );
end;

:: deftheorem defines is_bounded_on INTEGR1C:def 6 :
for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve holds
( f is_bounded_on C iff for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for u0, v0 being PartFunc of REAL,REAL st a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] holds
( ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is bounded & ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is bounded ) );

theorem :: INTEGR1C:1
for f, g being PartFunc of COMPLEX,COMPLEX
for C being C1-curve st rng C c= dom f & rng C c= dom g & f is_integrable_on C & g is_integrable_on C & f is_bounded_on C & g is_bounded_on C holds
integral ((f + g),C) = (integral (f,C)) + (integral (g,C))
proof end;

theorem :: INTEGR1C:2
for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve st rng C c= dom f & f is_integrable_on C & f is_bounded_on C holds
for r being Real holds integral ((r (#) f),C) = r * (integral (f,C))
proof end;

theorem :: INTEGR1C:3
for f being PartFunc of COMPLEX,COMPLEX
for C, C1, C2 being C1-curve
for a, b, d being Real st rng C c= dom f & f is_integrable_on C & f is_bounded_on C & a <= b & dom C = [.a,b.] & d in [.a,b.] & dom C1 = [.a,d.] & dom C2 = [.d,b.] & ( for t being Real st t in dom C1 holds
C . t = C1 . t ) & ( for t being Real st t in dom C2 holds
C . t = C2 . t ) holds
integral (f,C) = (integral (f,C1)) + (integral (f,C2))
proof end;