:: Partial Differentiation of Real Binary Functions :: by Bing Xie , Xiquan Liang , Hongwei Li and Yanping Zhuang :: :: Received August 5, 2008 :: Copyright (c) 2008-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, REAL_1, SEQ_1, PARTFUN1, FDIFF_1, RELAT_1, CARD_3, FUNCT_1, FINSEQ_1, FINSEQ_2, PDIFF_1, RCOMP_1, TARSKI, ARYTM_1, ARYTM_3, CARD_1, XXREAL_1, VALUED_0, SEQ_2, ORDINAL2, XXREAL_0, NAT_1, FUNCT_2, VALUED_1, XBOOLE_0, COMPLEX1, FCONT_1, PDIFF_2, FUNCT_7; notations TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XCMPLX_0, XREAL_0, COMPLEX1, ORDINAL1, NUMBERS, REAL_1, NAT_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, RCOMP_1, EUCLID, FDIFF_1, XXREAL_0, FCONT_1, PDIFF_1; constructors REAL_1, SEQ_2, COMPLEX1, RCOMP_1, FDIFF_1, FCONT_1, PDIFF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2; registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS, XBOOLE_0, FINSEQ_1, VALUED_0, VALUED_1, ORDINAL1, EUCLID, SEQ_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Preliminaries reserve x,x0,x1,x2,y,y0,y1,y2,r,r1,s,p,p1 for Real; reserve z,z0 for Element of REAL 2; reserve n,m,k for Element of NAT; reserve Z for Subset of REAL 2; reserve s1 for Real_Sequence; reserve f,f1,f2 for PartFunc of REAL 2,REAL; reserve R,R1,R2 for RestFunc; reserve L,L1,L2 for LinearFunc; theorem :: PDIFF_2:1 dom proj(1,2) = REAL 2 & rng proj(1,2) = REAL & for x,y be Real holds proj(1,2).<*x,y*> = x; theorem :: PDIFF_2:2 dom proj(2,2) = REAL 2 & rng proj(2,2) = REAL & for x,y be Real holds proj(2,2).<*x,y*> = y; begin :: Partial Differentiation of Real Binary Functions 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); end; theorem :: PDIFF_2:3 z = <*x,y*> & f is_partial_differentiable_in z,1 implies SVF1(1,f ,z) is_differentiable_in x; theorem :: PDIFF_2:4 z = <*x,y*> & f is_partial_differentiable_in z,2 implies SVF1(2,f ,z) is_differentiable_in y; theorem :: PDIFF_2:5 for f be PartFunc of REAL 2,REAL for z be 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; theorem :: PDIFF_2:6 for f be PartFunc of REAL 2,REAL for z be 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; theorem :: PDIFF_2:7 z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,z) & ex L,R st for x 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 z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,z) & ex L,R st for y st y in N holds SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0); theorem :: PDIFF_2:9 for f be PartFunc of REAL 2,REAL for z be 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,R st for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0); theorem :: PDIFF_2:10 for f be PartFunc of REAL 2,REAL for z be 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,R st for y st y in N holds SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0); theorem :: PDIFF_2:11 z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies (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,R st r = L.1 & for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0)); theorem :: PDIFF_2:12 z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies (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,R st r = L.1 & for y 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 z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies partdiff(f, z,1) = diff(SVF1(1,f,z),x0); theorem :: PDIFF_2:14 z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies partdiff(f, z,2) = diff(SVF1(2,f,z),y0); definition let f be PartFunc of REAL 2,REAL; let Z be set; pred f is_partial_differentiable`1_on Z means :: PDIFF_2:def 2 Z c= dom f & for z be 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 be Element of REAL 2 st z in Z holds f|Z is_partial_differentiable_in z,2; end; theorem :: PDIFF_2:15 f is_partial_differentiable`1_on Z implies Z c= dom f & for z st z in Z holds f is_partial_differentiable_in z,1; theorem :: PDIFF_2:16 f is_partial_differentiable`2_on Z implies Z c= dom f & for z st z in Z holds f is_partial_differentiable_in z,2; definition let f be PartFunc of REAL 2,REAL; let Z be set; assume 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 be Element of REAL 2 st z in Z holds it.z = partdiff(f,z,1); end; definition let f be PartFunc of REAL 2,REAL; let Z be set; assume 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 be Element of REAL 2 st z in Z holds it.z = partdiff(f,z,2); end; begin :: Main Properties of Partial Differentiation of Real Binary Functions theorem :: PDIFF_2:17 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 be 0-convergent non-zero Real_Sequence, c be 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)); theorem :: PDIFF_2:18 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 be 0-convergent non-zero Real_Sequence, c be 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)); theorem :: PDIFF_2:19 f1 is_partial_differentiable_in z0,1 & f2 is_partial_differentiable_in z0,1 implies f1(#)f2 is_partial_differentiable_in z0,1; theorem :: PDIFF_2:20 f1 is_partial_differentiable_in z0,2 & f2 is_partial_differentiable_in z0,2 implies f1(#)f2 is_partial_differentiable_in z0,2; theorem :: PDIFF_2:21 for z0 being Element of REAL 2 holds f is_partial_differentiable_in z0 ,1 implies SVF1(1,f,z0) is_continuous_in proj(1,2).z0; theorem :: PDIFF_2:22 for z0 being Element of REAL 2 holds f is_partial_differentiable_in z0 ,2 implies SVF1(2,f,z0) is_continuous_in proj(2,2).z0;