:: Second-order Partial Differentiation of Real Binary Functions
::  by Bing Xie , Xiquan Liang and Xiuzhuan Shen
::
:: Received December 16, 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, FUNCT_1,
      PDIFF_1, FINSEQ_1, RCOMP_1, TARSKI, RELAT_1, PDIFF_2, ARYTM_1, ARYTM_3,
      CARD_1, XXREAL_1, VALUED_0, SEQ_2, ORDINAL2, XXREAL_0, NAT_1, VALUED_1,
      FUNCT_2, CARD_3, FCONT_1, PDIFF_3, FUNCT_7, XCMPLX_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1,
      XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, NUMBERS, REAL_1, VALUED_0,
      VALUED_1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, RCOMP_1, EUCLID, FDIFF_1,
      FCONT_1, PDIFF_1, PDIFF_2;
 constructors REAL_1, SEQ_2, RCOMP_1, FDIFF_1, FCONT_1, PDIFF_1, PDIFF_2,
      RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, COMPLEX1;
 registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
      XBOOLE_0, VALUED_0, VALUED_1, EUCLID, ORDINAL1;
 requirements SUBSET, REAL, NUMERALS, ARITHM;


begin :: Second-order Partial Derivatives

reserve x,x0,x1,y,y0,y1,r,r1,s,p,p1 for Real;
reserve z,z0 for Element of REAL 2;
reserve n for Element of NAT;
reserve s1 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL 2,REAL;
reserve R,R1 for RestFunc;
reserve L,L1 for LinearFunc;

registration
  cluster -> total for RestFunc;
end;

definition
  let i be Element of NAT;
  let n be non zero Element of NAT;
  let f be PartFunc of REAL n,REAL;
  func pdiff1(f,i) -> Function of REAL n, REAL means
:: PDIFF_3:def 1
  for z being Element of REAL n holds it.z = partdiff(f,z,i);
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let z be Element of REAL 2;
  pred f is_hpartial_differentiable`11_in z means
:: PDIFF_3:def 2

  ex x0,y0
st z = <*x0,y0*> & ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,1
),z) & ex L,R st for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(
  f,1),z).x0 = L.(x-x0) + R.(x-x0);
  pred f is_hpartial_differentiable`12_in z means
:: PDIFF_3:def 3

  ex x0,y0
st z = <*x0,y0*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,1
),z) & ex L,R st for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(
  f,1),z).y0 = L.(y-y0) + R.(y-y0);
  pred f is_hpartial_differentiable`21_in z means
:: PDIFF_3:def 4

  ex x0,y0
st z = <*x0,y0*> & ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,2
),z) & ex L,R st for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(
  f,2),z).x0 = L.(x-x0) + R.(x-x0);
  pred f is_hpartial_differentiable`22_in z means
:: PDIFF_3:def 5

  ex x0,y0
st z = <*x0,y0*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,2
),z) & ex L,R st for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(
  f,2),z).y0 = L.(y-y0) + R.(y-y0);
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let z be Element of REAL 2;
  assume
 f is_hpartial_differentiable`11_in z;
  func hpartdiff11(f,z) -> Real means
:: PDIFF_3:def 6

  ex x0,y0 st z = <*x0,
y0*> & ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,1),z) & ex L,
R st it = L.1 & for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f
  ,1),z).x0 = L.(x-x0) + R.(x-x0);
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let z be Element of REAL 2;
  assume
 f is_hpartial_differentiable`12_in z;
  func hpartdiff12(f,z) -> Real means
:: PDIFF_3:def 7

  ex x0,y0 st z = <*x0,
y0*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,1),z) & ex L,
R st it = L.1 & for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f
  ,1),z).y0 = L.(y-y0) + R.(y-y0);
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let z be Element of REAL 2;
  assume
 f is_hpartial_differentiable`21_in z;
  func hpartdiff21(f,z) -> Real means
:: PDIFF_3:def 8

  ex x0,y0 st z = <*x0,
y0*> & ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,2),z) & ex L,
R st it = L.1 & for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f
  ,2),z).x0 = L.(x-x0) + R.(x-x0);
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let z be Element of REAL 2;
  assume
 f is_hpartial_differentiable`22_in z;
  func hpartdiff22(f,z) -> Real means
:: PDIFF_3:def 9

  ex x0,y0 st z = <*x0,
y0*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,2),z) & ex L,
R st it = L.1 & for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f
  ,2),z).y0 = L.(y-y0) + R.(y-y0);
end;

theorem :: PDIFF_3:1
  z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies SVF1(1,
  pdiff1(f,1),z) is_differentiable_in x0;

theorem :: PDIFF_3:2
  z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies SVF1(2,
  pdiff1(f,1),z) is_differentiable_in y0;

theorem :: PDIFF_3:3
  z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies SVF1(1,
  pdiff1(f,2),z) is_differentiable_in x0;

theorem :: PDIFF_3:4
  z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies SVF1(2,
  pdiff1(f,2),z) is_differentiable_in y0;

theorem :: PDIFF_3:5
  z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies
  hpartdiff11(f,z) = diff(SVF1(1,pdiff1(f,1),z),x0);

theorem :: PDIFF_3:6
  z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies
  hpartdiff12(f,z) = diff(SVF1(2,pdiff1(f,1),z),y0);

theorem :: PDIFF_3:7
  z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies
  hpartdiff21(f,z) = diff(SVF1(1,pdiff1(f,2),z),x0);

theorem :: PDIFF_3:8
  z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies
  hpartdiff22(f,z) = diff(SVF1(2,pdiff1(f,2),z),y0);

definition
  let f be PartFunc of REAL 2,REAL;
  let Z be set;
  pred f is_hpartial_differentiable`11_on Z means
:: PDIFF_3:def 10

  Z c= dom f & for z
  be Element of REAL 2 st z in Z holds f|Z is_hpartial_differentiable`11_in z;
  pred f is_hpartial_differentiable`12_on Z means
:: PDIFF_3:def 11

  Z c= dom f & for z
  be Element of REAL 2 st z in Z holds f|Z is_hpartial_differentiable`12_in z;
  pred f is_hpartial_differentiable`21_on Z means
:: PDIFF_3:def 12

  Z c= dom f & for z
  be Element of REAL 2 st z in Z holds f|Z is_hpartial_differentiable`21_in z;
  pred f is_hpartial_differentiable`22_on Z means
:: PDIFF_3:def 13

  Z c= dom f & for z
  be Element of REAL 2 st z in Z holds f|Z is_hpartial_differentiable`22_in z;
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let Z be set;
  assume
 f is_hpartial_differentiable`11_on Z;
  func f`hpartial11|Z -> PartFunc of REAL 2,REAL means
:: PDIFF_3:def 14
  dom it = Z & for z be
  Element of REAL 2 st z in Z holds it.z = hpartdiff11(f,z);
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let Z be set;
  assume
 f is_hpartial_differentiable`12_on Z;
  func f`hpartial12|Z -> PartFunc of REAL 2,REAL means
:: PDIFF_3:def 15
  dom it = Z & for z be
  Element of REAL 2 st z in Z holds it.z = hpartdiff12(f,z);
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let Z be set;
  assume
 f is_hpartial_differentiable`21_on Z;
  func f`hpartial21|Z -> PartFunc of REAL 2,REAL means
:: PDIFF_3:def 16
  dom it = Z & for z be
  Element of REAL 2 st z in Z holds it.z = hpartdiff21(f,z);
end;

definition
  let f be PartFunc of REAL 2,REAL;
  let Z be set;
  assume
 f is_hpartial_differentiable`22_on Z;
  func f`hpartial22|Z -> PartFunc of REAL 2,REAL means
:: PDIFF_3:def 17
  dom it = Z & for z be
  Element of REAL 2 st z in Z holds it.z = hpartdiff22(f,z);
end;

begin :: Main Properties of Second-order Partial Derivatives

theorem :: PDIFF_3:9
  f is_hpartial_differentiable`11_in z iff pdiff1(f,1)
  is_partial_differentiable_in z,1;

theorem :: PDIFF_3:10
  f is_hpartial_differentiable`12_in z iff pdiff1(f,1)
  is_partial_differentiable_in z,2;

theorem :: PDIFF_3:11
  f is_hpartial_differentiable`21_in z iff pdiff1(f,2)
  is_partial_differentiable_in z,1;

theorem :: PDIFF_3:12
  f is_hpartial_differentiable`22_in z iff pdiff1(f,2)
  is_partial_differentiable_in z,2;

theorem :: PDIFF_3:13
  f is_hpartial_differentiable`11_in z implies hpartdiff11(f,z) =
  partdiff(pdiff1(f,1),z,1);

theorem :: PDIFF_3:14
  f is_hpartial_differentiable`12_in z implies hpartdiff12(f,z) =
  partdiff(pdiff1(f,1),z,2);

theorem :: PDIFF_3:15
  f is_hpartial_differentiable`21_in z implies hpartdiff21(f,z) =
  partdiff(pdiff1(f,2),z,1);

theorem :: PDIFF_3:16
  f is_hpartial_differentiable`22_in z implies hpartdiff22(f,z) =
  partdiff(pdiff1(f,2),z,2);

theorem :: PDIFF_3:17
  for z0 being Element of REAL 2 for N being Neighbourhood of proj(1,2).
  z0 st f is_hpartial_differentiable`11_in z0 & N c= dom SVF1(1,pdiff1(f,1),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,pdiff1(f,1),z0)/*(h+
c) - SVF1(1,pdiff1(f,1),z0)/*c) is convergent & hpartdiff11(f,z0) = lim (h"(#)(
  SVF1(1,pdiff1(f,1),z0)/*(h+c) - SVF1(1,pdiff1(f,1),z0)/*c));

theorem :: PDIFF_3:18
  for z0 being Element of REAL 2 for N being Neighbourhood of proj(2,2).
  z0 st f is_hpartial_differentiable`12_in z0 & N c= dom SVF1(2,pdiff1(f,1),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,pdiff1(f,1),z0)/*(h+
c) - SVF1(2,pdiff1(f,1),z0)/*c) is convergent & hpartdiff12(f,z0) = lim (h"(#)(
  SVF1(2,pdiff1(f,1),z0)/*(h+c) - SVF1(2,pdiff1(f,1),z0)/*c));

theorem :: PDIFF_3:19
  for z0 being Element of REAL 2 for N being Neighbourhood of proj(1,2).
  z0 st f is_hpartial_differentiable`21_in z0 & N c= dom SVF1(1,pdiff1(f,2),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,pdiff1(f,2),z0)/*(h+
c) - SVF1(1,pdiff1(f,2),z0)/*c) is convergent & hpartdiff21(f,z0) = lim (h"(#)(
  SVF1(1,pdiff1(f,2),z0)/*(h+c) - SVF1(1,pdiff1(f,2),z0)/*c));

theorem :: PDIFF_3:20
  for z0 being Element of REAL 2 for N being Neighbourhood of proj(2,2).
  z0 st f is_hpartial_differentiable`22_in z0 & N c= dom SVF1(2,pdiff1(f,2),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,pdiff1(f,2),z0)/*(h+
c) - SVF1(2,pdiff1(f,2),z0)/*c) is convergent & hpartdiff22(f,z0) = lim (h"(#)(
  SVF1(2,pdiff1(f,2),z0)/*(h+c) - SVF1(2,pdiff1(f,2),z0)/*c));

theorem :: PDIFF_3:21
  f1 is_hpartial_differentiable`11_in z0 & f2
  is_hpartial_differentiable`11_in z0 implies pdiff1(f1,1)+pdiff1(f2,1)
is_partial_differentiable_in z0,1 & partdiff(pdiff1(f1,1)+pdiff1(f2,1),z0,1) =
  hpartdiff11(f1,z0) + hpartdiff11(f2,z0);

theorem :: PDIFF_3:22
  f1 is_hpartial_differentiable`12_in z0 & f2
  is_hpartial_differentiable`12_in z0 implies pdiff1(f1,1)+pdiff1(f2,1)
is_partial_differentiable_in z0,2 & partdiff(pdiff1(f1,1)+pdiff1(f2,1),z0,2) =
  hpartdiff12(f1,z0) + hpartdiff12(f2,z0);

theorem :: PDIFF_3:23
  f1 is_hpartial_differentiable`21_in z0 & f2
  is_hpartial_differentiable`21_in z0 implies pdiff1(f1,2)+pdiff1(f2,2)
is_partial_differentiable_in z0,1 & partdiff(pdiff1(f1,2)+pdiff1(f2,2),z0,1) =
  hpartdiff21(f1,z0) + hpartdiff21(f2,z0);

theorem :: PDIFF_3:24
  f1 is_hpartial_differentiable`22_in z0 & f2
  is_hpartial_differentiable`22_in z0 implies pdiff1(f1,2)+pdiff1(f2,2)
is_partial_differentiable_in z0,2 & partdiff(pdiff1(f1,2)+pdiff1(f2,2),z0,2) =
  hpartdiff22(f1,z0) + hpartdiff22(f2,z0);

theorem :: PDIFF_3:25
  f1 is_hpartial_differentiable`11_in z0 & f2
  is_hpartial_differentiable`11_in z0 implies pdiff1(f1,1)-pdiff1(f2,1)
is_partial_differentiable_in z0,1 & partdiff(pdiff1(f1,1)-pdiff1(f2,1),z0,1) =
  hpartdiff11(f1,z0) - hpartdiff11(f2,z0);

theorem :: PDIFF_3:26
  f1 is_hpartial_differentiable`12_in z0 & f2
  is_hpartial_differentiable`12_in z0 implies pdiff1(f1,1)-pdiff1(f2,1)
is_partial_differentiable_in z0,2 & partdiff(pdiff1(f1,1)-pdiff1(f2,1),z0,2) =
  hpartdiff12(f1,z0) - hpartdiff12(f2,z0);

theorem :: PDIFF_3:27
  f1 is_hpartial_differentiable`21_in z0 & f2
  is_hpartial_differentiable`21_in z0 implies pdiff1(f1,2)-pdiff1(f2,2)
is_partial_differentiable_in z0,1 & partdiff(pdiff1(f1,2)-pdiff1(f2,2),z0,1) =
  hpartdiff21(f1,z0) - hpartdiff21(f2,z0);

theorem :: PDIFF_3:28
  f1 is_hpartial_differentiable`22_in z0 & f2
  is_hpartial_differentiable`22_in z0 implies pdiff1(f1,2)-pdiff1(f2,2)
is_partial_differentiable_in z0,2 & partdiff(pdiff1(f1,2)-pdiff1(f2,2),z0,2) =
  hpartdiff22(f1,z0) - hpartdiff22(f2,z0);

theorem :: PDIFF_3:29
  f is_hpartial_differentiable`11_in z0 implies r(#)pdiff1(f,1)
  is_partial_differentiable_in z0,1 & partdiff((r(#)pdiff1(f,1)),z0,1) = r*
  hpartdiff11(f,z0);

theorem :: PDIFF_3:30
  f is_hpartial_differentiable`12_in z0 implies r(#)pdiff1(f,1)
  is_partial_differentiable_in z0,2 & partdiff((r(#)pdiff1(f,1)),z0,2) = r*
  hpartdiff12(f,z0);

theorem :: PDIFF_3:31
  f is_hpartial_differentiable`21_in z0 implies r(#)pdiff1(f,2)
  is_partial_differentiable_in z0,1 & partdiff((r(#)pdiff1(f,2)),z0,1) = r*
  hpartdiff21(f,z0);

theorem :: PDIFF_3:32
  f is_hpartial_differentiable`22_in z0 implies r(#)pdiff1(f,2)
  is_partial_differentiable_in z0,2 & partdiff((r(#)pdiff1(f,2)),z0,2) = r*
  hpartdiff22(f,z0);

theorem :: PDIFF_3:33
  f1 is_hpartial_differentiable`11_in z0 & f2
  is_hpartial_differentiable`11_in z0 implies pdiff1(f1,1)(#)pdiff1(f2,1)
  is_partial_differentiable_in z0,1;

theorem :: PDIFF_3:34
  f1 is_hpartial_differentiable`12_in z0 & f2
  is_hpartial_differentiable`12_in z0 implies pdiff1(f1,1)(#)pdiff1(f2,1)
  is_partial_differentiable_in z0,2;

theorem :: PDIFF_3:35
  f1 is_hpartial_differentiable`21_in z0 & f2
  is_hpartial_differentiable`21_in z0 implies pdiff1(f1,2)(#)pdiff1(f2,2)
  is_partial_differentiable_in z0,1;

theorem :: PDIFF_3:36
  f1 is_hpartial_differentiable`22_in z0 & f2
  is_hpartial_differentiable`22_in z0 implies pdiff1(f1,2)(#)pdiff1(f2,2)
  is_partial_differentiable_in z0,2;

theorem :: PDIFF_3:37
  for z0 being Element of REAL 2 holds f
  is_hpartial_differentiable`11_in z0 implies SVF1(1,pdiff1(f,1),z0)
  is_continuous_in proj(1,2).z0;

theorem :: PDIFF_3:38
  for z0 being Element of REAL 2 holds f
  is_hpartial_differentiable`12_in z0 implies SVF1(2,pdiff1(f,1),z0)
  is_continuous_in proj(2,2).z0;

theorem :: PDIFF_3:39
  for z0 being Element of REAL 2 holds f
  is_hpartial_differentiable`21_in z0 implies SVF1(1,pdiff1(f,2),z0)
  is_continuous_in proj(1,2).z0;

theorem :: PDIFF_3:40
  for z0 being Element of REAL 2 holds f
  is_hpartial_differentiable`22_in z0 implies SVF1(2,pdiff1(f,2),z0)
  is_continuous_in proj(2,2).z0;