:: Partial Differentiation of Real Binary Functions
:: by Bing Xie , Xiquan Liang , Hongwei Li and Yanping Zhuang
::
:: Received August 5, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: PDIFF_2:1
theorem Th2: :: PDIFF_2:2
:: deftheorem defines SVF1 PDIFF_2:def 1 :
theorem Lem1: :: PDIFF_2:3
theorem Lem2: :: PDIFF_2:4
theorem Def6: :: PDIFF_2:5
theorem Def7: :: PDIFF_2:6
theorem :: PDIFF_2:7
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
LINEAR ex
R being
REST 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 :: PDIFF_2:8
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
LINEAR ex
R being
REST 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 Def10: :: PDIFF_2:9
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
LINEAR ex
R being
REST 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 Def11: :: PDIFF_2:10
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
LINEAR ex
R being
REST 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)) ) ) )
def12:
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 LINEAR ex R being REST 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)) ) ) ) ) )
def13:
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 LINEAR ex R being REST 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 Def12: :: PDIFF_2:11
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
LINEAR ex
R being
REST 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 Def13: :: PDIFF_2:12
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
LINEAR ex
R being
REST 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 :: PDIFF_2:13
theorem :: PDIFF_2:14
:: deftheorem Def16 defines is_partial_differentiable`1_on PDIFF_2:def 2 :
:: deftheorem Def17 defines is_partial_differentiable`2_on PDIFF_2:def 3 :
theorem :: PDIFF_2:15
theorem :: PDIFF_2:16
definition
let f be
PartFunc of
(REAL 2),
REAL ;
let Z be
set ;
assume A1:
f is_partial_differentiable`1_on Z
;
func f `partial1| Z -> PartFunc of
(REAL 2),
REAL means :: PDIFF_2:def 4
(
dom it = Z & ( for
z being
Element of
REAL 2 st
z in Z holds
it . z = partdiff f,
z,1 ) );
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;
:: deftheorem defines `partial1| PDIFF_2:def 4 :
definition
let f be
PartFunc of
(REAL 2),
REAL ;
let Z be
set ;
assume A1:
f is_partial_differentiable`2_on Z
;
func f `partial2| Z -> PartFunc of
(REAL 2),
REAL means :: PDIFF_2:def 5
(
dom it = Z & ( for
z being
Element of
REAL 2 st
z in Z holds
it . z = partdiff f,
z,2 ) );
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;
:: deftheorem defines `partial2| PDIFF_2:def 5 :
theorem :: PDIFF_2:17
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
convergent_to_0 Real_Sequence for
c being
V8()
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 :: PDIFF_2:18
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
convergent_to_0 Real_Sequence for
c being
V8()
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))) )
theorem :: PDIFF_2:19
theorem :: PDIFF_2:20
theorem :: PDIFF_2:21
theorem :: PDIFF_2:22
theorem :: PDIFF_2:23
theorem :: PDIFF_2:24