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

definition
func R2-to-C -> Function of ,COMPLEX means :Def1: :: INTEGR1C:def 1
for p being Element of
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 ,COMPLEX st
for p being Element of
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 ,COMPLEX st ( for p being Element of
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
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 ,COMPLEX holds
( b1 = R2-to-C iff for p being Element of
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 + ()) | [.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 + ()) | [.a,b.] ) );

registration
existence
ex b1 being PartFunc of REAL,COMPLEX st b1 is C1-curve-like
proof end;
end;

definition 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 + ()) | [.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 + ()) | [.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 + ()) | [.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 + ()) | [.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 + ()) | [.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 + ()) | [.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 + ()) | [.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 + ()) | [.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 + ()) | [.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 + ()) | [.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;