:: 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
definition
let f be
PartFunc of
REAL 2,
REAL ;
let z be
Element of
REAL 2;
func SVF1 f,
z -> PartFunc of
REAL ,
REAL equals :: PDIFF_2:def 1
f * (reproj 1,z);
coherence
f * (reproj 1,z) is PartFunc of REAL , REAL
;
func SVF2 f,
z -> PartFunc of
REAL ,
REAL equals :: PDIFF_2:def 2
f * (reproj 2,z);
coherence
f * (reproj 2,z) is PartFunc of REAL , REAL
;
end;
:: deftheorem defines SVF1 PDIFF_2:def 1 :
:: deftheorem defines SVF2 PDIFF_2:def 2 :
theorem Lem1: :: PDIFF_2:3
theorem Lem2: :: PDIFF_2:4
:: deftheorem Def6 defines is_partial_differentiable`1_in PDIFF_2:def 3 :
:: deftheorem Def7 defines is_partial_differentiable`2_in PDIFF_2:def 4 :
theorem :: PDIFF_2:5
theorem :: PDIFF_2:6
definition
let f be
PartFunc of
REAL 2,
REAL ;
let z be
Element of
REAL 2;
redefine pred f is_partial_differentiable`1_in z means :
Def10:
:: PDIFF_2:def 5
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 f,z) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 f,z) . x) - ((SVF1 f,z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
compatibility
( f is_partial_differentiable`1_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 f,z) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 f,z) . x) - ((SVF1 f,z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
end;
:: deftheorem Def10 defines is_partial_differentiable`1_in PDIFF_2:def 5 :
definition
let f be
PartFunc of
REAL 2,
REAL ;
let z be
Element of
REAL 2;
redefine pred f is_partial_differentiable`2_in z means :
Def11:
:: PDIFF_2:def 6
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF2 f,z) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF2 f,z) . y) - ((SVF2 f,z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
compatibility
( f is_partial_differentiable`2_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF2 f,z) & ex L being LINEAR ex R being REST st
for y being Real st y in N holds
((SVF2 f,z) . y) - ((SVF2 f,z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
end;
:: deftheorem Def11 defines is_partial_differentiable`2_in PDIFF_2:def 6 :
theorem Lem3: :: PDIFF_2:7
theorem Lem4: :: PDIFF_2:8
definition
let f be
PartFunc of
REAL 2,
REAL ;
let z be
Element of
REAL 2;
func partdiff1 f,
z -> Real equals :: PDIFF_2:def 7
partdiff f,
z,1;
coherence
partdiff f,z,1 is Real
;
func partdiff2 f,
z -> Real equals :: PDIFF_2:def 8
partdiff f,
z,2;
coherence
partdiff f,z,2 is Real
;
end;
:: deftheorem defines partdiff1 PDIFF_2:def 7 :
:: deftheorem defines partdiff2 PDIFF_2:def 8 :
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`1_in z holds
( r = diff (SVF1 f,z),x0 iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 f,z) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 f,z) . x) - ((SVF1 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`2_in z holds
( r = diff (SVF2 f,z),y0 iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF2 f,z) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for y being Real st y in N holds
((SVF2 f,z) . y) - ((SVF2 f,z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
theorem Def12: :: PDIFF_2:9
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`1_in z holds
(
r = partdiff1 f,
z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 f,z) & ex
L being
LINEAR ex
R being
REST st
(
r = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 f,z) . x) - ((SVF1 f,z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
theorem Def13: :: PDIFF_2:10
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`2_in z holds
(
r = partdiff2 f,
z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF2 f,z) & ex
L being
LINEAR ex
R being
REST st
(
r = L . 1 & ( for
y being
Real st
y in N holds
((SVF2 f,z) . y) - ((SVF2 f,z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
theorem :: PDIFF_2:11
theorem :: PDIFF_2:12
:: deftheorem Def16 defines is_partial_differentiable`1_on PDIFF_2:def 9 :
:: deftheorem Def17 defines is_partial_differentiable`2_on PDIFF_2:def 10 :
theorem :: PDIFF_2:13
theorem :: PDIFF_2:14
:: deftheorem defines `partial1| PDIFF_2:def 11 :
:: deftheorem defines `partial2| PDIFF_2:def 12 :
theorem :: PDIFF_2:15
theorem :: PDIFF_2:16
theorem :: PDIFF_2:17
theorem :: PDIFF_2:18
theorem :: PDIFF_2:19
theorem :: PDIFF_2:20
theorem :: PDIFF_2:21
theorem :: PDIFF_2:22
theorem :: PDIFF_2:23
theorem :: PDIFF_2:24
theorem :: PDIFF_2:25
theorem :: PDIFF_2:26
theorem :: PDIFF_2:27
theorem :: PDIFF_2:28