:: 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

( dom (proj 1,2) = REAL 2 & rng (proj 1,2) = REAL & ( for x, y being Element of REAL holds (proj 1,2) . <*x,y*> = x ) )

proof end;

theorem Th2: :: PDIFF_2:2

( dom (proj 2,2) = REAL 2 & rng (proj 2,2) = REAL & ( for x, y being Element of REAL holds (proj 2,2) . <*x,y*> = y ) )

proof end;

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 :

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds SVF1 f,z = f * (reproj 1,z);

:: deftheorem defines SVF2 PDIFF_2:def 2 :

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds SVF2 f,z = f * (reproj 2,z);

theorem Lem1: :: PDIFF_2:3

for x, y being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x,y*> & f is_partial_differentiable_in z,1 holds
SVF1 f,z is_differentiable_in x

proof end;

theorem Lem2: :: PDIFF_2:4

for x, y being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x,y*> & f is_partial_differentiable_in z,2 holds
SVF2 f,z is_differentiable_in y

proof end;

definition

let f be PartFunc of REAL 2, REAL ;
let z be Element of REAL 2;
pred f is_partial_differentiable`1_in z means :Def6: :: PDIFF_2:def 3
ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 f,z is_differentiable_in x0 );
pred f is_partial_differentiable`2_in z means :Def7: :: PDIFF_2:def 4
ex x0, y0 being Real st
( z = <*x0,y0*> & SVF2 f,z is_differentiable_in y0 );

end;

:: deftheorem Def6 defines is_partial_differentiable`1_in PDIFF_2:def 3 :

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds
( f is_partial_differentiable`1_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 f,z is_differentiable_in x0 ) );

:: deftheorem Def7 defines is_partial_differentiable`2_in PDIFF_2:def 4 :

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds
( f is_partial_differentiable`2_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> & SVF2 f,z is_differentiable_in y0 ) );

theorem :: PDIFF_2:5

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`1_in z holds
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)) )

proof end;

theorem :: PDIFF_2:6

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`2_in z holds
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)) )

proof end;

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)) ) ) )

proof end;

end;

:: deftheorem Def10 defines is_partial_differentiable`1_in PDIFF_2:def 5 :

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds
( 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)) ) ) );

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)) ) ) )

proof end;

end;

:: deftheorem Def11 defines is_partial_differentiable`2_in PDIFF_2:def 6 :

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds
( 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)) ) ) );

theorem Lem3: :: PDIFF_2:7

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds
( f is_partial_differentiable`1_in z iff f is_partial_differentiable_in z,1 )

proof end;

theorem Lem4: :: PDIFF_2:8

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds
( f is_partial_differentiable`2_in z iff f is_partial_differentiable_in z,2 )

proof end;

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 :

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds partdiff1 f,z = partdiff f,z,1;

:: deftheorem defines partdiff2 PDIFF_2:def 8 :

for f being PartFunc of REAL 2, REAL
for z being Element of REAL 2 holds partdiff2 f,z = partdiff f,z,2;

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)) ) ) ) ) )

proof end;

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)) ) ) ) ) )

proof end;

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)) ) ) ) ) )

proof end;

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)) ) ) ) ) )

proof end;

theorem :: PDIFF_2:11

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`1_in z holds
partdiff1 f,z = diff (SVF1 f,z),x0

proof end;

theorem :: PDIFF_2:12

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`2_in z holds
partdiff2 f,z = diff (SVF2 f,z),y0

proof end;

definition

let f be PartFunc of REAL 2, REAL ;
let Z be set ;
pred f is_partial_differentiable`1_on Z means :Def16: :: PDIFF_2:def 9
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable`1_in z ) );
pred f is_partial_differentiable`2_on Z means :Def17: :: PDIFF_2:def 10
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable`2_in z ) );

end;

:: deftheorem Def16 defines is_partial_differentiable`1_on PDIFF_2:def 9 :

for f being PartFunc of REAL 2, REAL
for Z being set holds
( f is_partial_differentiable`1_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable`1_in z ) ) );

:: deftheorem Def17 defines is_partial_differentiable`2_on PDIFF_2:def 10 :

for f being PartFunc of REAL 2, REAL
for Z being set holds
( f is_partial_differentiable`2_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable`2_in z ) ) );

theorem :: PDIFF_2:13

for Z being Subset of (REAL 2)
for f being PartFunc of REAL 2, REAL st f is_partial_differentiable`1_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable`1_in z ) )

proof end;

theorem :: PDIFF_2:14

for Z being Subset of (REAL 2)
for f being PartFunc of REAL 2, REAL st f is_partial_differentiable`2_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable`2_in z ) )

proof end;

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 11
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = partdiff1 f,z ) );
existence
ex b₁ being PartFunc of REAL 2, REAL st
( dom b₁ = Z & ( for z being Element of REAL 2 st z in Z holds
b₁ . z = partdiff1 f,z ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of REAL 2, REAL st dom b₁ = Z & ( for z being Element of REAL 2 st z in Z holds
b₁ . z = partdiff1 f,z ) & dom b₂ = Z & ( for z being Element of REAL 2 st z in Z holds
b₂ . z = partdiff1 f,z ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines `partial1| PDIFF_2:def 11 :

for f being PartFunc of REAL 2, REAL
for Z being set st f is_partial_differentiable`1_on Z holds
for b<sub>3</sub> being PartFunc of REAL 2, REAL holds
( b<sub>3</sub> = f `partial1| Z iff ( dom b₃ = Z & ( for z being Element of REAL 2 st z in Z holds
b₃ . z = partdiff1 f,z ) ) );

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 12
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = partdiff2 f,z ) );
existence
ex b₁ being PartFunc of REAL 2, REAL st
( dom b₁ = Z & ( for z being Element of REAL 2 st z in Z holds
b₁ . z = partdiff2 f,z ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of REAL 2, REAL st dom b₁ = Z & ( for z being Element of REAL 2 st z in Z holds
b₁ . z = partdiff2 f,z ) & dom b₂ = Z & ( for z being Element of REAL 2 st z in Z holds
b₂ . z = partdiff2 f,z ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines `partial2| PDIFF_2:def 12 :

for f being PartFunc of REAL 2, REAL
for Z being set st f is_partial_differentiable`2_on Z holds
for b<sub>3</sub> being PartFunc of REAL 2, REAL holds
( b<sub>3</sub> = f `partial2| Z iff ( dom b₃ = Z & ( for z being Element of REAL 2 st z in Z holds
b₃ . z = partdiff2 f,z ) ) );

theorem :: PDIFF_2:15

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`1_in z0 & N c= dom (SVF1 f,z0) holds
for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {((proj 1,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 f,z0) /* (h + c)) - ((SVF1 f,z0) /* c)) is convergent & partdiff1 f,z0 = lim ((h " ) (#) (((SVF1 f,z0) /* (h + c)) - ((SVF1 f,z0) /* c))) )

proof end;

theorem :: PDIFF_2:16

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`2_in z0 & N c= dom (SVF2 f,z0) holds
for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {((proj 2,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF2 f,z0) /* (h + c)) - ((SVF2 f,z0) /* c)) is convergent & partdiff2 f,z0 = lim ((h " ) (#) (((SVF2 f,z0) /* (h + c)) - ((SVF2 f,z0) /* c))) )

proof end;

theorem :: PDIFF_2:17

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_partial_differentiable`1_in z0 & f2 is_partial_differentiable`1_in z0 holds
( f1 + f2 is_partial_differentiable`1_in z0 & partdiff1 (f1 + f2),z0 = (partdiff1 f1,z0) + (partdiff1 f2,z0) )

proof end;

theorem :: PDIFF_2:18

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_partial_differentiable`2_in z0 & f2 is_partial_differentiable`2_in z0 holds
( f1 + f2 is_partial_differentiable`2_in z0 & partdiff2 (f1 + f2),z0 = (partdiff2 f1,z0) + (partdiff2 f2,z0) )

proof end;

theorem :: PDIFF_2:19

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_partial_differentiable`1_in z0 & f2 is_partial_differentiable`1_in z0 holds
( f1 - f2 is_partial_differentiable`1_in z0 & partdiff1 (f1 - f2),z0 = (partdiff1 f1,z0) - (partdiff1 f2,z0) )

proof end;

theorem :: PDIFF_2:20

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_partial_differentiable`2_in z0 & f2 is_partial_differentiable`2_in z0 holds
( f1 - f2 is_partial_differentiable`2_in z0 & partdiff2 (f1 - f2),z0 = (partdiff2 f1,z0) - (partdiff2 f2,z0) )

proof end;

theorem :: PDIFF_2:21

for r being Real
for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_partial_differentiable`1_in z0 holds
( r (#) f is_partial_differentiable`1_in z0 & partdiff1 (r (#) f),z0 = r * (partdiff1 f,z0) )

proof end;

theorem :: PDIFF_2:22

for r being Real
for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_partial_differentiable`2_in z0 holds
( r (#) f is_partial_differentiable`2_in z0 & partdiff2 (r (#) f),z0 = r * (partdiff2 f,z0) )

proof end;

theorem :: PDIFF_2:23

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_partial_differentiable`1_in z0 & f2 is_partial_differentiable`1_in z0 holds
f1 (#) f2 is_partial_differentiable`1_in z0

proof end;

theorem :: PDIFF_2:24

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_partial_differentiable`2_in z0 & f2 is_partial_differentiable`2_in z0 holds
f1 (#) f2 is_partial_differentiable`2_in z0

proof end;

theorem :: PDIFF_2:25

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2 st f is_partial_differentiable`1_in z0 holds
SVF1 f,z0 is_continuous_in (proj 1,2) . z0

proof end;

theorem :: PDIFF_2:26

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2 st f is_partial_differentiable`2_in z0 holds
SVF2 f,z0 is_continuous_in (proj 2,2) . z0

proof end;

theorem :: PDIFF_2:27

for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_partial_differentiable`1_in z0 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;

theorem :: PDIFF_2:28

for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_partial_differentiable`2_in z0 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;