begin
begin
theorem
for
x0,
y0 being
Real for
z being
Element of
REAL 2
for
f being
PartFunc of
(REAL 2),
REAL st
z = <*x0,y0*> &
f is_partial_differentiable_in z,1 holds
ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 (1,f,z)) & ex
L being
LinearFunc ex
R being
RestFunc st
for
x being
Real st
x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
theorem
for
x0,
y0 being
Real for
z being
Element of
REAL 2
for
f being
PartFunc of
(REAL 2),
REAL st
z = <*x0,y0*> &
f is_partial_differentiable_in z,2 holds
ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 (2,f,z)) & ex
L being
LinearFunc ex
R being
RestFunc st
for
y being
Real st
y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
theorem Th9:
for
f being
PartFunc of
(REAL 2),
REAL for
z being
Element of
REAL 2 holds
(
f is_partial_differentiable_in z,1 iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 (1,f,z)) & ex
L being
LinearFunc ex
R being
RestFunc st
for
x being
Real st
x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
theorem Th10:
for
f being
PartFunc of
(REAL 2),
REAL for
z being
Element of
REAL 2 holds
(
f is_partial_differentiable_in z,2 iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 (2,f,z)) & ex
L being
LinearFunc ex
R being
RestFunc st
for
y being
Real st
y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
Lm1:
for x0, y0, r being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
( r = diff ((SVF1 (1,f,z)),x0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
Lm2:
for x0, y0, r being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
( r = diff ((SVF1 (2,f,z)),y0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
theorem Th11:
for
x0,
y0,
r being
Real for
z being
Element of
REAL 2
for
f being
PartFunc of
(REAL 2),
REAL st
z = <*x0,y0*> &
f is_partial_differentiable_in z,1 holds
(
r = partdiff (
f,
z,1) iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 (1,f,z)) & ex
L being
LinearFunc ex
R being
RestFunc st
(
r = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
theorem Th12:
for
x0,
y0,
r being
Real for
z being
Element of
REAL 2
for
f being
PartFunc of
(REAL 2),
REAL st
z = <*x0,y0*> &
f is_partial_differentiable_in z,2 holds
(
r = partdiff (
f,
z,2) iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 (2,f,z)) & ex
L being
LinearFunc ex
R being
RestFunc st
(
r = L . 1 & ( for
y being
Real st
y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
definition
let f be
PartFunc of
(REAL 2),
REAL;
let Z be
set ;
assume A1:
f is_partial_differentiable`1_on Z
;
existence
ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,1) ) )
uniqueness
for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,1) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds
b2 . z = partdiff (f,z,1) ) holds
b1 = b2
end;
definition
let f be
PartFunc of
(REAL 2),
REAL;
let Z be
set ;
assume A1:
f is_partial_differentiable`2_on Z
;
existence
ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,2) ) )
uniqueness
for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,2) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds
b2 . z = partdiff (f,z,2) ) holds
b1 = b2
end;
begin
theorem
for
f being
PartFunc of
(REAL 2),
REAL for
z0 being
Element of
REAL 2
for
N being
Neighbourhood of
(proj (1,2)) . z0 st
f is_partial_differentiable_in z0,1 &
N c= dom (SVF1 (1,f,z0)) holds
for
h being
non-zero 0 -convergent Real_Sequence for
c being
constant Real_Sequence st
rng c = {((proj (1,2)) . z0)} &
rng (h + c) c= N holds
(
(h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is
convergent &
partdiff (
f,
z0,1)
= lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )
theorem
for
f being
PartFunc of
(REAL 2),
REAL for
z0 being
Element of
REAL 2
for
N being
Neighbourhood of
(proj (2,2)) . z0 st
f is_partial_differentiable_in z0,2 &
N c= dom (SVF1 (2,f,z0)) holds
for
h being
non-zero 0 -convergent Real_Sequence for
c being
constant Real_Sequence st
rng c = {((proj (2,2)) . z0)} &
rng (h + c) c= N holds
(
(h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is
convergent &
partdiff (
f,
z0,2)
= lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) )