:: by Bing Xie , Xiquan Liang , Hongwei Li and Yanping Zhuang

::

:: Received August 5, 2008

:: Copyright (c) 2008-2021 Association of Mizar Users

theorem Th1: :: PDIFF_2:1

( dom (proj (1,2)) = REAL 2 & rng (proj (1,2)) = REAL & ( for x, y being 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 Real holds (proj (2,2)) . <*x,y*> = y ) )

proof end;

definition

let n, i be Element of NAT ;

let f be PartFunc of (REAL n),REAL;

let z be Element of REAL n;

coherence

f * (reproj (i,z)) is PartFunc of REAL,REAL ;

end;
let f be PartFunc of (REAL n),REAL;

let z be Element of REAL n;

coherence

f * (reproj (i,z)) is PartFunc of REAL,REAL ;

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

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 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*> & SVF1 (1,f,z) is_differentiable_in x0 ) iff f is_partial_differentiable_in z,1 )

for z being Element of REAL 2 holds

( ex x0, y0 being Real st

( z = <*x0,y0*> & SVF1 (1,f,z) is_differentiable_in x0 ) iff f is_partial_differentiable_in z,1 )

proof end;

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*> & SVF1 (2,f,z) is_differentiable_in y0 ) iff f is_partial_differentiable_in z,2 )

for z being Element of REAL 2 holds

( ex x0, y0 being Real st

( z = <*x0,y0*> & SVF1 (2,f,z) is_differentiable_in y0 ) iff f is_partial_differentiable_in z,2 )

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

proof end;

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

proof end;

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

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

proof end;

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

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

proof end;

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*> & f is_partial_differentiable_in z,1 holds

partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)

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

partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)

proof end;

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*> & f is_partial_differentiable_in z,2 holds

partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0)

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

partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0)

proof end;

definition

let f be PartFunc of (REAL 2),REAL;

let Z be set ;

end;
let Z be set ;

pred f is_partial_differentiable`1_on Z means :: PDIFF_2:def 2

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_partial_differentiable_in z,1 ) );

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_partial_differentiable_in z,1 ) );

pred f is_partial_differentiable`2_on Z means :: PDIFF_2:def 3

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_partial_differentiable_in z,2 ) );

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_partial_differentiable_in z,2 ) );

:: deftheorem 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 & ( for z being Element of REAL 2 st z in Z holds

f | Z is_partial_differentiable_in z,1 ) ) );

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_in z,1 ) ) );

:: deftheorem 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 & ( for z being Element of REAL 2 st z in Z holds

f | Z is_partial_differentiable_in z,2 ) ) );

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_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 & ( for z being Element of REAL 2 st z in Z holds

f is_partial_differentiable_in z,1 ) )

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

proof end;

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 & ( for z being Element of REAL 2 st z in Z holds

f is_partial_differentiable_in z,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_in z,2 ) )

proof end;

definition

let f be PartFunc of (REAL 2),REAL;

let Z be set ;

assume A1: f is_partial_differentiable`1_on Z ;

ex b_{1} being PartFunc of (REAL 2),REAL st

( dom b_{1} = Z & ( for z being Element of REAL 2 st z in Z holds

b_{1} . z = partdiff (f,z,1) ) )

for b_{1}, b_{2} being PartFunc of (REAL 2),REAL st dom b_{1} = Z & ( for z being Element of REAL 2 st z in Z holds

b_{1} . z = partdiff (f,z,1) ) & dom b_{2} = Z & ( for z being Element of REAL 2 st z in Z holds

b_{2} . z = partdiff (f,z,1) ) holds

b_{1} = b_{2}

end;
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 ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

it . z = partdiff (f,z,1) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 2),REAL holds

( b_{3} = f `partial1| Z iff ( dom b_{3} = Z & ( for z being Element of REAL 2 st z in Z holds

b_{3} . z = partdiff (f,z,1) ) ) );

for f being PartFunc of (REAL 2),REAL

for Z being set st f is_partial_differentiable`1_on Z holds

for b

( b

b

definition

let f be PartFunc of (REAL 2),REAL;

let Z be set ;

assume A1: f is_partial_differentiable`2_on Z ;

ex b_{1} being PartFunc of (REAL 2),REAL st

( dom b_{1} = Z & ( for z being Element of REAL 2 st z in Z holds

b_{1} . z = partdiff (f,z,2) ) )

for b_{1}, b_{2} being PartFunc of (REAL 2),REAL st dom b_{1} = Z & ( for z being Element of REAL 2 st z in Z holds

b_{1} . z = partdiff (f,z,2) ) & dom b_{2} = Z & ( for z being Element of REAL 2 st z in Z holds

b_{2} . z = partdiff (f,z,2) ) holds

b_{1} = b_{2}

end;
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 ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

it . z = partdiff (f,z,2) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 2),REAL holds

( b_{3} = f `partial2| Z iff ( dom b_{3} = Z & ( for z being Element of REAL 2 st z in Z holds

b_{3} . z = partdiff (f,z,2) ) ) );

for f being PartFunc of (REAL 2),REAL

for Z being set st f is_partial_differentiable`2_on Z holds

for b

( b

b

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

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

proof end;

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

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

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_in z0,1 & f2 is_partial_differentiable_in z0,1 holds

f1 (#) f2 is_partial_differentiable_in z0,1

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_partial_differentiable_in z0,1 & f2 is_partial_differentiable_in z0,1 holds

f1 (#) f2 is_partial_differentiable_in z0,1

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_in z0,2 & f2 is_partial_differentiable_in z0,2 holds

f1 (#) f2 is_partial_differentiable_in z0,2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_partial_differentiable_in z0,2 & f2 is_partial_differentiable_in z0,2 holds

f1 (#) f2 is_partial_differentiable_in z0,2

proof end;

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 by FDIFF_1:24;

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 by FDIFF_1:24;

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 by FDIFF_1:24;

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 by FDIFF_1:24;