begin
definition
func R2-to-C -> Function of
[:REAL ,REAL :],
COMPLEX means :
Def1:
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> )
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
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:
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> ) )
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> ) ) );
:: deftheorem Def3 defines C1-curve-like INTEGR1C:def 3 :
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
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
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:
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 )
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
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 :
Def5:
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 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 &
[.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 :
Def6:
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 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 &
[.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 ) );
begin
theorem
theorem
begin
theorem
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)