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


begin

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 &amp; b = p `2 holds
b1 . [a,b] = a + (b * <i>)
proofend;
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 &amp; b = p `2 holds
b1 . [a,b] = a + (b * <i>) ) &amp; ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 &amp; b = p `2 holds
b2 . [a,b] = a + (b * <i>) ) holds
b1 = b2
proofend;
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 &amp; 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:> &amp; v0 = ((Im f) * R2-to-C) * <:x,y:> &amp; 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:> &amp; v0 = ((Im f) * R2-to-C) * <:x,y:> &amp; b1 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) )
proofend;
uniqueness
 for b1, b2 being Complex st ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> &amp; v0 = ((Im f) * R2-to-C) * <:x,y:> &amp; b1 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) &amp; ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> &amp; v0 = ((Im f) * R2-to-C) * <:x,y:> &amp; 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:> &amp; v0 = ((Im f) * R2-to-C) * <:x,y:> &amp; 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;
attrC 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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; 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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; 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
proofend;
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 &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z1 is open &amp; Z2 is open &amp; [.a,b.] c= Z1 &amp; Z1 c= Z2 &amp; x is_differentiable_on Z2 &amp; y is_differentiable_on Z2 &amp; rng ((x + (<i> (#) y)) | [.a,b.]) c= dom f holds
integral (f,x,y,a,b,Z1) = integral (f,x,y,a,b,Z2)
proofend;

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 &amp; [.a,b.] c= dom x1 &amp; [.a,b.] c= dom y1 &amp; [.a,b.] c= dom x2 &amp; [.a,b.] c= dom y2 &amp; x1 | [.a,b.] = x2 | [.a,b.] &amp; y1 | [.a,b.] = y2 | [.a,b.] &amp; Z is open &amp; [.a,b.] c= Z &amp; x1 is_differentiable_on Z &amp; y1 is_differentiable_on Z &amp; rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f &amp; x2 is_differentiable_on Z &amp; y2 is_differentiable_on Z &amp; rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
proofend;

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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] &amp; 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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] &amp; b1 = integral (f,x,y,a,b,Z) )
proofend;
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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] &amp; b1 = integral (f,x,y,a,b,Z) ) &amp; ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] &amp; b2 = integral (f,x,y,a,b,Z) ) holds
b1 = b2
proofend;
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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] &amp; b3 = integral (f,x,y,a,b,Z) ) );

definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
predf is_integrable_on C means :Def5: :: 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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] holds
( (u0 (#) (x `| Z)) - (v0 (#) (y `| Z)) is_integrable_on ['a,b'] &amp; (v0 (#) (x `| Z)) + (u0 (#) (y `| Z)) is_integrable_on ['a,b'] );
end;

:: deftheorem Def5 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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] holds
( (u0 (#) (x `| Z)) - (v0 (#) (y `| Z)) is_integrable_on ['a,b'] &amp; (v0 (#) (x `| Z)) + (u0 (#) (y `| Z)) is_integrable_on ['a,b'] ) );

definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
predf is_bounded_on C means :Def6: :: 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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] holds
( ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is bounded &amp; ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is bounded );
end;

:: deftheorem Def6 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 &amp; [.a,b.] = dom C &amp; [.a,b.] c= dom x &amp; [.a,b.] c= dom y &amp; Z is open &amp; [.a,b.] c= Z &amp; x is_differentiable_on Z &amp; y is_differentiable_on Z &amp; x `| Z is continuous &amp; y `| Z is continuous &amp; C = (x + (<i> (#) y)) | [.a,b.] holds
( ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is bounded &amp; ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is bounded ) );

begin

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

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

begin

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 &amp; f is_integrable_on C &amp; f is_bounded_on C &amp; a <= b &amp; dom C = [.a,b.] &amp; d in [.a,b.] &amp; dom C1 = [.a,d.] &amp; dom C2 = [.d,b.] &amp; ( for t being Element of REAL st t in dom C1 holds
C . t = C1 . t ) &amp; ( for t being Element of REAL st t in dom C2 holds
C . t = C2 . t ) holds
integral (f,C) = (integral (f,C1)) + (integral (f,C2))
proofend;