INTEGR1C: Complex Integral

:: Complex Integral
:: by Masahiko Yamazaki , Hiroshi Yamazaki , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 10, 2009
:: Copyright (c) 2009 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 ,;
let Z be Subset of ;
let f be PartFunc of ,;
func integral f,x,y,a,b,Z -> Complex means :Def2: :: INTEGR1C:def 2
ex u0, v0 being PartFunc of , 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 ,;
attr C is C1-curve-like means :Def3: :: INTEGR1C:def 3
ex a, b being Real ex x, y being PartFunc of , ex Z being Subset of 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 C1-curve-like Element of bool [:REAL ,COMPLEX :];
existence

proof end;

end;

definition

mode C1-curve is C1-curve-like PartFunc of ,;

end;

Lm1: for a, b being Real
for x, y being PartFunc of ,
for Z1, Z2 being Subset of
for f being PartFunc of , 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 ,
for Z being Subset of
for f being PartFunc of , 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 ,;
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 , ex Z being Subset of 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 ,;
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 ,
for Z being Subset of
for u0, v0 being PartFunc of , 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 ,;
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 ,
for Z being Subset of
for u0, v0 being PartFunc of , 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 ,
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 ,
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 ,
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;