:: Partial Differentiation of Real Binary Functions
:: by Bing Xie , Xiquan Liang , Hongwei Li and Yanping Zhuang
::
:: Received August 5, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: PDIFF_2:1
( dom (proj (1,2)) = REAL 2 &amp; rng (proj (1,2)) = REAL &amp; ( for x, y being Element of REAL holds (proj (1,2)) . <*x,y*> = x ) )
proofend;

theorem Th2: :: PDIFF_2:2
( dom (proj (2,2)) = REAL 2 &amp; rng (proj (2,2)) = REAL &amp; ( for x, y being Element of REAL holds (proj (2,2)) . <*x,y*> = y ) )
proofend;

begin

definition
let n, i be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let z be Element of REAL n;
func SVF1 (i,f,z) ->  PartFunc of REAL,REAL equals :: PDIFF_2:def 1
f * (reproj (i,z));
coherence
 f * (reproj (i,z)) is PartFunc of REAL,REAL ;
end;

:: deftheorem  defines SVF1 PDIFF_2:def_1_:_
 for n, i being Element of NAT
for f being PartFunc of (REAL n),REAL
for z being Element of REAL n holds SVF1 (i,f,z) = f * (reproj (i,z));

theorem Th3: :: 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*> &amp; f is_partial_differentiable_in z,1 holds
SVF1 (1,f,z) is_differentiable_in x
proofend;

theorem Th4: :: 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*> &amp; f is_partial_differentiable_in z,2 holds
SVF1 (2,f,z) is_differentiable_in y
proofend;

theorem Th5: :: PDIFF_2:5
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( ex x0, y0 being Real st
( z = <*x0,y0*> &amp; SVF1 (1,f,z) is_differentiable_in x0 ) iff f is_partial_differentiable_in z,1 )
proofend;

theorem Th6: :: PDIFF_2:6
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( ex x0, y0 being Real st
( z = <*x0,y0*> &amp; SVF1 (2,f,z) is_differentiable_in y0 ) iff f is_partial_differentiable_in z,2 )
proofend;

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*> &amp; f is_partial_differentiable_in z,1 holds
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) &amp; 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)) )
proofend;

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*> &amp; f is_partial_differentiable_in z,2 holds
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) &amp; 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)) )
proofend;

theorem Th9: :: 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*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) &amp; 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)) ) ) )
proofend;

theorem Th10: :: 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*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) &amp; 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)) ) ) )
proofend;

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*> &amp; 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*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) &amp; ex L being LinearFunc ex R being RestFunc st
( r = L . 1 &amp; ( 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)) ) ) ) ) )
proofend;

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*> &amp; 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*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) &amp; ex L being LinearFunc ex R being RestFunc st
( r = L . 1 &amp; ( 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)) ) ) ) ) )
proofend;

theorem Th11: :: 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*> &amp; f is_partial_differentiable_in z,1 holds
( r = partdiff (f,z,1) iff ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) &amp; ex L being LinearFunc ex R being RestFunc st
( r = L . 1 &amp; ( 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)) ) ) ) ) )
proofend;

theorem Th12: :: 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*> &amp; f is_partial_differentiable_in z,2 holds
( r = partdiff (f,z,2) iff ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) &amp; ex L being LinearFunc ex R being RestFunc st
( r = L . 1 &amp; ( 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)) ) ) ) ) )
proofend;

theorem :: PDIFF_2:13
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> &amp; f is_partial_differentiable_in z,1 holds
partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
proofend;

theorem :: PDIFF_2:14
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> &amp; f is_partial_differentiable_in z,2 holds
partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0)
proofend;

definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
predf is_partial_differentiable`1_on Z means :Def2: :: PDIFF_2:def 2
( Z c= dom f &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable_in z,1 ) );
predf is_partial_differentiable`2_on Z means :Def3: :: PDIFF_2:def 3
( Z c= dom f &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable_in z,2 ) );
end;

:: deftheorem Def2 defines is_partial_differentiable`1_on PDIFF_2:def_2_:_
 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 &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable_in z,1 ) ) );

:: deftheorem Def3 defines is_partial_differentiable`2_on PDIFF_2:def_3_:_
 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 &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable_in z,2 ) ) );

theorem :: PDIFF_2:15
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 &amp; ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1 ) )
proofend;

theorem :: PDIFF_2:16
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 &amp; ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) )
proofend;

definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_partial_differentiable`1_on Z ;
funcf `partial1| Z ->  PartFunc of (REAL 2),REAL means :: PDIFF_2:def 4
( dom it = Z &amp; ( 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 &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,1) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,1) ) &amp; dom b2 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b2 . z = partdiff (f,z,1) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines `partial1| PDIFF_2:def_4_:_
 for f being PartFunc of (REAL 2),REAL
for Z being set st f is_partial_differentiable`1_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `partial1| Z iff ( dom b3 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b3 . z = partdiff (f,z,1) ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_partial_differentiable`2_on Z ;
funcf `partial2| Z ->  PartFunc of (REAL 2),REAL means :: PDIFF_2:def 5
( dom it = Z &amp; ( 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 &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,2) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,2) ) &amp; dom b2 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b2 . z = partdiff (f,z,2) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines `partial2| PDIFF_2:def_5_:_
 for f being PartFunc of (REAL 2),REAL
for Z being set st f is_partial_differentiable`2_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `partial2| Z iff ( dom b3 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b3 . z = partdiff (f,z,2) ) ) );

begin

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 &amp; 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)} &amp; rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent &amp; partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )
proofend;

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 &amp; 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)} &amp; rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent &amp; partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) )
proofend;

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_in z0,1 &amp; f2 is_partial_differentiable_in z0,1 holds
f1 (#) f2 is_partial_differentiable_in z0,1
proofend;

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_in z0,2 &amp; f2 is_partial_differentiable_in z0,2 holds
f1 (#) f2 is_partial_differentiable_in z0,2
proofend;

theorem :: PDIFF_2:21
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2 st f is_partial_differentiable_in z0,1 holds
SVF1 (1,f,z0) is_continuous_in (proj (1,2)) . z0
proofend;

theorem :: PDIFF_2:22
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2 st f is_partial_differentiable_in z0,2 holds
SVF1 (2,f,z0) is_continuous_in (proj (2,2)) . z0
proofend;