begin
theorem Th1:
theorem Th2:
theorem Th3:
begin
theorem Lem1:
theorem Lem2:
theorem Lem3:
theorem BXXLXSDef6:
theorem BXXLXSDef7:
theorem BXXLXSDef7ForZ:
theorem
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_partial_differentiable_in u,1 holds
ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,f,u) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,f,u) . x) - ((SVF1 1,f,u) . x0) = (L . (x - x0)) + (R . (x - x0)) )
theorem
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_partial_differentiable_in u,2 holds
ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,f,u) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,f,u) . y) - ((SVF1 2,f,u) . y0) = (L . (y - y0)) + (R . (y - y0)) )
theorem
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_partial_differentiable_in u,3 holds
ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,f,u) & ex
L being
LINEAR ex
R being
REST st
for
z being
Real st
z in N holds
((SVF1 3,f,u) . z) - ((SVF1 3,f,u) . z0) = (L . (z - z0)) + (R . (z - z0)) )
theorem BXXLXSDef10:
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_partial_differentiable_in u,1 iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,f,u) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,f,u) . x) - ((SVF1 1,f,u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
theorem BXXLXSDef11:
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_partial_differentiable_in u,2 iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,f,u) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,f,u) . y) - ((SVF1 2,f,u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
theorem BXXLXSDef11ForZ:
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_partial_differentiable_in u,3 iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,f,u) & ex
L being
LINEAR ex
R being
REST st
for
z being
Real st
z in N holds
((SVF1 3,f,u) . z) - ((SVF1 3,f,u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) )
BXXLXSdef12:
for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = diff (SVF1 1,f,u),x0 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 1,f,u) . x) - ((SVF1 1,f,u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
BXXLXSdef13:
for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = diff (SVF1 2,f,u),y0 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 2,f,u) . y) - ((SVF1 2,f,u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
BXXLXSdef13ForZ:
for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = diff (SVF1 3,f,u),z0 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 3,f,u) . z) - ((SVF1 3,f,u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
theorem BXXLXSDef12:
for
x0,
y0,
z0,
r being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_partial_differentiable_in u,1 holds
(
r = partdiff f,
u,1 iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,f,u) & ex
L being
LINEAR ex
R being
REST st
(
r = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 1,f,u) . x) - ((SVF1 1,f,u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
theorem BXXLXSDef13:
for
x0,
y0,
z0,
r being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_partial_differentiable_in u,2 holds
(
r = partdiff f,
u,2 iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,f,u) & ex
L being
LINEAR ex
R being
REST st
(
r = L . 1 & ( for
y being
Real st
y in N holds
((SVF1 2,f,u) . y) - ((SVF1 2,f,u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
theorem BXXLXSDef13ForZ:
for
x0,
y0,
z0,
r being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_partial_differentiable_in u,3 holds
(
r = partdiff f,
u,3 iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,f,u) & ex
L being
LINEAR ex
R being
REST st
(
r = L . 1 & ( for
z being
Real st
z in N holds
((SVF1 3,f,u) . z) - ((SVF1 3,f,u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
theorem
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> holds
partdiff f,
u,1
= diff (SVF1 1,f,u),
x0 by Th1;
theorem
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> holds
partdiff f,
u,2
= diff (SVF1 2,f,u),
y0 by Th2;
theorem
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> holds
partdiff f,
u,3
= diff (SVF1 3,f,u),
z0 by Th3;
:: deftheorem Def16 defines is_partial_differentiable`1_on PDIFF_4:def 1 :
:: deftheorem Def17 defines is_partial_differentiable`2_on PDIFF_4:def 2 :
:: deftheorem Def17ForZ defines is_partial_differentiable`3_on PDIFF_4:def 3 :
theorem
theorem
theorem
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let D be
set ;
assume A1:
f is_partial_differentiable`1_on D
;
func f `partial1| D -> PartFunc of
(REAL 3),
REAL means
(
dom it = D & ( for
u being
Element of
REAL 3 st
u in D holds
it . u = partdiff f,
u,1 ) );
existence
ex b1 being PartFunc of (REAL 3),REAL st
( dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff f,u,1 ) )
uniqueness
for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff f,u,1 ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds
b2 . u = partdiff f,u,1 ) holds
b1 = b2
end;
:: deftheorem defines `partial1| PDIFF_4:def 4 :
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let D be
set ;
assume A1:
f is_partial_differentiable`2_on D
;
func f `partial2| D -> PartFunc of
(REAL 3),
REAL means
(
dom it = D & ( for
u being
Element of
REAL 3 st
u in D holds
it . u = partdiff f,
u,2 ) );
existence
ex b1 being PartFunc of (REAL 3),REAL st
( dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff f,u,2 ) )
uniqueness
for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff f,u,2 ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds
b2 . u = partdiff f,u,2 ) holds
b1 = b2
end;
:: deftheorem defines `partial2| PDIFF_4:def 5 :
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let D be
set ;
assume A1:
f is_partial_differentiable`3_on D
;
func f `partial3| D -> PartFunc of
(REAL 3),
REAL means
(
dom it = D & ( for
u being
Element of
REAL 3 st
u in D holds
it . u = partdiff f,
u,3 ) );
existence
ex b1 being PartFunc of (REAL 3),REAL st
( dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff f,u,3 ) )
uniqueness
for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff f,u,3 ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds
b2 . u = partdiff f,u,3 ) holds
b1 = b2
end;
:: deftheorem defines `partial3| PDIFF_4:def 6 :
begin
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 1,3) . u0 st
f is_partial_differentiable_in u0,1 &
N c= dom (SVF1 1,f,u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 1,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 1,f,u0) /* (h + c)) - ((SVF1 1,f,u0) /* c)) is
convergent &
partdiff f,
u0,1
= lim ((h " ) (#) (((SVF1 1,f,u0) /* (h + c)) - ((SVF1 1,f,u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 2,3) . u0 st
f is_partial_differentiable_in u0,2 &
N c= dom (SVF1 2,f,u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 2,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c)) is
convergent &
partdiff f,
u0,2
= lim ((h " ) (#) (((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 3,3) . u0 st
f is_partial_differentiable_in u0,3 &
N c= dom (SVF1 3,f,u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 3,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 3,f,u0) /* (h + c)) - ((SVF1 3,f,u0) /* c)) is
convergent &
partdiff f,
u0,3
= lim ((h " ) (#) (((SVF1 3,f,u0) /* (h + c)) - ((SVF1 3,f,u0) /* c))) )
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
Lm6:
for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let p be
Element of
REAL 3;
func grad f,
p -> Element of
REAL 3
equals
(((partdiff f,p,1) * <e1> ) + ((partdiff f,p,2) * <e2> )) + ((partdiff f,p,3) * <e3> );
coherence
(((partdiff f,p,1) * <e1> ) + ((partdiff f,p,2) * <e2> )) + ((partdiff f,p,3) * <e3> ) is Element of REAL 3
;
end;
:: deftheorem defines grad PDIFF_4:def 7 :
theorem Th43:
for
p being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL holds
grad f,
p = |[(partdiff f,p,1),(partdiff f,p,2),(partdiff f,p,3)]|
theorem Th45:
for
p being
Element of
REAL 3
for
f,
g being
PartFunc of
(REAL 3),
REAL st
f is_partial_differentiable_in p,1 &
f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 &
g is_partial_differentiable_in p,1 &
g is_partial_differentiable_in p,2 &
g is_partial_differentiable_in p,3 holds
grad (f + g),
p = (grad f,p) + (grad g,p)
theorem Th46:
for
p being
Element of
REAL 3
for
f,
g being
PartFunc of
(REAL 3),
REAL st
f is_partial_differentiable_in p,1 &
f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 &
g is_partial_differentiable_in p,1 &
g is_partial_differentiable_in p,2 &
g is_partial_differentiable_in p,3 holds
grad (f - g),
p = (grad f,p) - (grad g,p)
theorem Th47:
theorem
for
s,
t being
Real for
p being
Element of
REAL 3
for
f,
g being
PartFunc of
(REAL 3),
REAL st
f is_partial_differentiable_in p,1 &
f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 &
g is_partial_differentiable_in p,1 &
g is_partial_differentiable_in p,2 &
g is_partial_differentiable_in p,3 holds
grad ((s (#) f) + (t (#) g)),
p = (s * (grad f,p)) + (t * (grad g,p))
theorem
for
s,
t being
Real for
p being
Element of
REAL 3
for
f,
g being
PartFunc of
(REAL 3),
REAL st
f is_partial_differentiable_in p,1 &
f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 &
g is_partial_differentiable_in p,1 &
g is_partial_differentiable_in p,2 &
g is_partial_differentiable_in p,3 holds
grad ((s (#) f) - (t (#) g)),
p = (s * (grad f,p)) - (t * (grad g,p))
theorem
:: deftheorem defines unitvector PDIFF_4:def 8 :
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let p,
a be
Element of
REAL 3;
func Directiondiff f,
p,
a -> Real equals
(((partdiff f,p,1) * ((unitvector a) . 1)) + ((partdiff f,p,2) * ((unitvector a) . 2))) + ((partdiff f,p,3) * ((unitvector a) . 3));
coherence
(((partdiff f,p,1) * ((unitvector a) . 1)) + ((partdiff f,p,2) * ((unitvector a) . 2))) + ((partdiff f,p,3) * ((unitvector a) . 3)) is Real
;
end;
:: deftheorem defines Directiondiff PDIFF_4:def 9 :
for
f being
PartFunc of
(REAL 3),
REAL for
p,
a being
Element of
REAL 3 holds
Directiondiff f,
p,
a = (((partdiff f,p,1) * ((unitvector a) . 1)) + ((partdiff f,p,2) * ((unitvector a) . 2))) + ((partdiff f,p,3) * ((unitvector a) . 3));
theorem
for
x0,
y0,
z0 being
Real for
a,
p being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
a = <*x0,y0,z0*> holds
Directiondiff f,
p,
a = ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * z0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))
theorem
definition
let f1,
f2,
f3 be
PartFunc of
(REAL 3),
REAL ;
let p be
Element of
REAL 3;
func curl f1,
f2,
f3,
p -> Element of
REAL 3
equals
((((partdiff f3,p,2) - (partdiff f2,p,3)) * <e1> ) + (((partdiff f1,p,3) - (partdiff f3,p,1)) * <e2> )) + (((partdiff f2,p,1) - (partdiff f1,p,2)) * <e3> );
coherence
((((partdiff f3,p,2) - (partdiff f2,p,3)) * <e1> ) + (((partdiff f1,p,3) - (partdiff f3,p,1)) * <e2> )) + (((partdiff f2,p,1) - (partdiff f1,p,2)) * <e3> ) is Element of REAL 3
;
end;
:: deftheorem defines curl PDIFF_4:def 10 :
for
f1,
f2,
f3 being
PartFunc of
(REAL 3),
REAL for
p being
Element of
REAL 3 holds
curl f1,
f2,
f3,
p = ((((partdiff f3,p,2) - (partdiff f2,p,3)) * <e1> ) + (((partdiff f1,p,3) - (partdiff f3,p,1)) * <e2> )) + (((partdiff f2,p,1) - (partdiff f1,p,2)) * <e3> );
theorem
for
p being
Element of
REAL 3
for
f1,
f2,
f3 being
PartFunc of
(REAL 3),
REAL holds
curl f1,
f2,
f3,
p = |[((partdiff f3,p,2) - (partdiff f2,p,3)),((partdiff f1,p,3) - (partdiff f3,p,1)),((partdiff f2,p,1) - (partdiff f1,p,2))]|