INTEGR1C: Complex Integral

:: Complex Integral
:: by Masahiko Yamazaki , Hiroshi Yamazaki , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 10, 2009
:: Copyright (c) 2009-2011 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 * );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines R2-to-C INTEGR1C:def 1 :

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

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines integral INTEGR1C:def 2 :

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 + ( (#) y)) | [.a,b.] );

end;

:: deftheorem Def3 defines C1-curve-like INTEGR1C:def 3 :

registration

cluster Relation-like Function-like V43() C1-curve-like Element of bool [:REAL,COMPLEX:];
existence

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 + ( (#) 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 + ( (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + ( (#) 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 + ( (#) y)) | [.a,b.] & it = integral (f,x,y,a,b,Z) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines integral INTEGR1C:def 4 :

definition

let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
pred f 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 & [.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 + ( (#) 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 Def5 defines is_integrable_on INTEGR1C:def 5 :

definition

let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
pred f 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 & [.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 + ( (#) 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 Def6 defines is_bounded_on INTEGR1C:def 6 :

begin

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;

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 & 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 Element of REAL st t in dom C1 holds
C . t = C1 . t ) & ( 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))

proof end;