:: Partial Differentiation of Real Ternary Functions
::  by Takao Inou\'e , Bing Xie and Xiquan Liang
::
:: Received November 7, 2009
:: Copyright (c) 2009-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 SUBSET_1, NUMBERS, FINSEQ_1, FINSEQ_2, PARTFUN1, REAL_1, EUCLID,
      FUNCT_1, RELAT_1, ARYTM_3, ARYTM_1, RVSUM_1, CARD_3, CARD_1, SQUARE_1,
      COMPLEX1, XXREAL_0, FDIFF_1, VALUED_1, XXREAL_1, TARSKI, EUCLID_8,
      FUNCT_2, XBOOLE_0, NAT_1, VALUED_0, ORDINAL2, SEQ_1, SEQ_2, RCOMP_1,
      PDIFF_1, PDIFF_2, FCONT_1, PDIFF_4, 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, SQUARE_1,
      RVSUM_1, VALUED_1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, RCOMP_1, EUCLID,
      FDIFF_1, XXREAL_0, FCONT_1, PDIFF_1, PDIFF_2, EUCLID_8;
 constructors REAL_1, SEQ_2, COMPLEX1, RCOMP_1, FDIFF_1, FCONT_1, PDIFF_1,
      RELSET_1, PDIFF_2, EUCLID_8, SQUARE_1, BINOP_2, FINSEQOP, FINSEQ_4,
      MONOID_0, COMSEQ_2;
 registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
      FINSEQ_1, VALUED_0, VALUED_1, ORDINAL1, EUCLID, RVSUM_1, RCOMP_1,
      FUNCOP_1, FCONT_3, SQUARE_1, SEQ_2;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Preliminaries

reserve D for set;
reserve x,x0,x1,x2,y,y0,y1,y2,z,z0,z1,z2,r,s,t for Real;
reserve p,a,u,u0 for Element of REAL 3;
reserve n,m,k for Element of NAT;
reserve f,f1,f2,f3,g for PartFunc of REAL 3,REAL;
reserve R,R1,R2 for RestFunc;
reserve L,L1,L2 for LinearFunc;

theorem :: PDIFF_4:1
  dom proj(1,3) = REAL 3 & rng proj(1,3) = REAL &
  for x,y,z be Real holds proj(1,3).<*x,y,z*> = x;

theorem :: PDIFF_4:2
  dom proj(2,3) = REAL 3 & rng proj(2,3) = REAL &
  for x,y,z be Real holds proj(2,3).<*x,y,z*> = y;

theorem :: PDIFF_4:3
  dom proj(3,3) = REAL 3 & rng proj(3,3) = REAL &
  for x,y,z be Real holds proj(3,3).<*x,y,z*> = z;

begin :: Partial Differentiation of Real Ternary Functions

theorem :: PDIFF_4:4
  u = <*x,y,z*> & f is_partial_differentiable_in u,1 implies
  SVF1(1,f,u) is_differentiable_in x;

theorem :: PDIFF_4:5
  u = <*x,y,z*> & f is_partial_differentiable_in u,2 implies
  SVF1(2,f,u) is_differentiable_in y;

theorem :: PDIFF_4:6
  u = <*x,y,z*> & f is_partial_differentiable_in u,3 implies
  SVF1(3,f,u) is_differentiable_in z;

theorem :: PDIFF_4:7
  for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
  (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  SVF1(1,f,u) is_differentiable_in x0) iff
  f is_partial_differentiable_in u,1;

theorem :: PDIFF_4:8
  for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
  (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  SVF1(2,f,u) is_differentiable_in y0) iff
  f is_partial_differentiable_in u,2;

theorem :: PDIFF_4:9
  for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
  (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  SVF1(3,f,u) is_differentiable_in z0) iff
  f is_partial_differentiable_in u,3;

theorem :: PDIFF_4:10
  u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 implies
  ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
  ex L,R st for x st x in N holds
  SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0);

theorem :: PDIFF_4:11
  u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 implies
  ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
  ex L,R st for y st y in N holds
  SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0);

theorem :: PDIFF_4:12
  u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 implies
  ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
  ex L,R st for z st z in N holds
  SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0);

theorem :: PDIFF_4:13
  for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
  f is_partial_differentiable_in u,1 iff
  ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
  ex L,R st for x st x in N holds
  SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0);

theorem :: PDIFF_4:14
  for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
  f is_partial_differentiable_in u,2 iff
  ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
  ex L,R st for y st y in N holds
  SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0);

theorem :: PDIFF_4:15
  for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
  f is_partial_differentiable_in u,3 iff
  ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
  ex L,R st for z st z in N holds
  SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0);

theorem :: PDIFF_4:16
  u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 implies
  (r = partdiff(f,u,1) iff
  ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
  ex L,R st r = L.1 & for x st x in N holds
  SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0));

theorem :: PDIFF_4:17
  u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 implies
  (r = partdiff(f,u,2) iff
  ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
  ex L,R st r = L.1 & for y st y in N holds
  SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0));

theorem :: PDIFF_4:18
  u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 implies
  (r = partdiff(f,u,3) iff
  ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
  ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
  ex L,R st r = L.1 & for z st z in N holds
  SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0));

theorem :: PDIFF_4:19
  u = <*x0,y0,z0*> implies partdiff(f,u,1) = diff(SVF1(1,f,u),x0);

theorem :: PDIFF_4:20
  u = <*x0,y0,z0*> implies partdiff(f,u,2) = diff(SVF1(2,f,u),y0);

theorem :: PDIFF_4:21
  u = <*x0,y0,z0*> implies partdiff(f,u,3) = diff(SVF1(3,f,u),z0);

definition
  let f be PartFunc of REAL 3,REAL;
  let D be set;
  pred f is_partial_differentiable`1_on D means
:: PDIFF_4:def 1
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_partial_differentiable_in u,1;
  pred f is_partial_differentiable`2_on D means
:: PDIFF_4:def 2
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_partial_differentiable_in u,2;
  pred f is_partial_differentiable`3_on D means
:: PDIFF_4:def 3
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_partial_differentiable_in u,3;
end;

theorem :: PDIFF_4:22
  f is_partial_differentiable`1_on D implies
  D c= dom f & for u st u in D holds f is_partial_differentiable_in u,1;

theorem :: PDIFF_4:23
  f is_partial_differentiable`2_on D implies
  D c= dom f & for u st u in D holds f is_partial_differentiable_in u,2;

theorem :: PDIFF_4:24
  f is_partial_differentiable`3_on D implies
  D c= dom f & for u st u in D holds f is_partial_differentiable_in u,3;

definition
  let f be PartFunc of REAL 3,REAL;
  let D be set;
  assume  f is_partial_differentiable`1_on D;
  func f`partial1|D -> PartFunc of REAL 3,REAL means
:: PDIFF_4:def 4
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = partdiff(f,u,1);
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let D be set;
  assume  f is_partial_differentiable`2_on D;
  func f`partial2|D -> PartFunc of REAL 3,REAL means
:: PDIFF_4:def 5
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = partdiff(f,u,2);
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let D be set;
  assume  f is_partial_differentiable`3_on D;
  func f`partial3|D -> PartFunc of REAL 3,REAL means
:: PDIFF_4:def 6
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = partdiff(f,u,3);
end;

begin :: Main Properties of Partial Differentiation of Real Ternary Functions

theorem :: PDIFF_4:25
  for u0 being Element of REAL 3 for N being Neighbourhood of proj(1,3).u0 st
  f is_partial_differentiable_in u0,1 & N c= dom SVF1(1,f,u0) holds
  for h be 0-convergent non-zero Real_Sequence,
  c be constant Real_Sequence st rng c = {proj(1,3).u0} & rng (h+c) c= N
  holds h"(#)(SVF1(1,f,u0)/*(h+c) - SVF1(1,f,u0)/*c) is convergent &
  partdiff(f,u0,1) = lim (h"(#)(SVF1(1,f,u0)/*(h+c) - SVF1(1,f,u0)/*c));

theorem :: PDIFF_4:26
  for u0 being Element of REAL 3 for N being Neighbourhood of proj(2,3).u0 st
  f is_partial_differentiable_in u0,2 & N c= dom SVF1(2,f,u0) holds
  for h be 0-convergent non-zero Real_Sequence,
  c be constant Real_Sequence st rng c = {proj(2,3).u0} & rng (h+c) c= N
  holds h"(#)(SVF1(2,f,u0)/*(h+c) - SVF1(2,f,u0)/*c) is convergent &
  partdiff(f,u0,2) = lim (h"(#)(SVF1(2,f,u0)/*(h+c) - SVF1(2,f,u0)/*c));

theorem :: PDIFF_4:27
  for u0 being Element of REAL 3 for N being Neighbourhood of proj(3,3).u0 st
  f is_partial_differentiable_in u0,3 & N c= dom SVF1(3,f,u0) holds
  for h be 0-convergent non-zero Real_Sequence,
  c be constant Real_Sequence st rng c = {proj(3,3).u0} & rng (h+c) c= N
  holds h"(#)(SVF1(3,f,u0)/*(h+c) - SVF1(3,f,u0)/*c) is convergent &
  partdiff(f,u0,3) = lim (h"(#)(SVF1(3,f,u0)/*(h+c) - SVF1(3,f,u0)/*c));

theorem :: PDIFF_4:28
  f1 is_partial_differentiable_in u0,1 &
  f2 is_partial_differentiable_in u0,1 implies
  f1(#)f2 is_partial_differentiable_in u0,1;

theorem :: PDIFF_4:29
  f1 is_partial_differentiable_in u0,2 &
  f2 is_partial_differentiable_in u0,2 implies
  f1(#)f2 is_partial_differentiable_in u0,2;

theorem :: PDIFF_4:30
  f1 is_partial_differentiable_in u0,3 &
  f2 is_partial_differentiable_in u0,3 implies
  f1(#)f2 is_partial_differentiable_in u0,3;

theorem :: PDIFF_4:31
  for u0 being Element of REAL 3 holds f is_partial_differentiable_in u0,1
  implies SVF1(1,f,u0) is_continuous_in proj(1,3).u0;

theorem :: PDIFF_4:32
  for u0 being Element of REAL 3 holds f is_partial_differentiable_in u0,2
  implies SVF1(2,f,u0) is_continuous_in proj(2,3).u0;

theorem :: PDIFF_4:33
  for u0 being Element of REAL 3 holds f is_partial_differentiable_in u0,3
  implies SVF1(3,f,u0) is_continuous_in proj(3,3).u0;

begin

definition
  let f be PartFunc of REAL 3,REAL;
  let p be Element of REAL 3;
  func grad(f,p) -> Element of REAL 3 equals
:: PDIFF_4:def 7
  partdiff(f,p,1)*<e1>+partdiff(f,p,2)*<e2>+partdiff(f,p,3)*<e3>;
end;

theorem :: PDIFF_4:34
  grad(f,p) = |[ partdiff(f,p,1),partdiff(f,p,2),partdiff(f,p,3) ]|;

theorem :: PDIFF_4:35
  (f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
  f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 &
  g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3)
  implies grad(f+g,p) = grad(f,p)+grad(g,p);

theorem :: PDIFF_4:36
  (f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
  f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 &
  g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3)
  implies grad(f-g,p) = grad(f,p)-grad(g,p);

theorem :: PDIFF_4:37
  (f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
  f is_partial_differentiable_in p,3) implies grad(r(#)f,p) = r*grad(f,p);

theorem :: PDIFF_4:38
  (f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
  f is_partial_differentiable_in p,3) & (g is_partial_differentiable_in p,1 &
  g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3)
  implies grad(s(#)f+t(#)g,p) = s*grad(f,p)+t*grad(g,p);

theorem :: PDIFF_4:39
  (f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
  f is_partial_differentiable_in p,3) & (g is_partial_differentiable_in p,1 &
  g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3)
  implies grad(s(#)f-t(#)g,p) = s*grad(f,p)-t*grad(g,p);

theorem :: PDIFF_4:40
  f is total & f is constant implies grad(f,p) = 0.REAL 3;

definition
  let a be Element of REAL 3;
  func unitvector(a) -> Element of REAL 3 equals
:: PDIFF_4:def 8
  |[ a.1/sqrt((a.1)^2+(a.2)^2+(a.3)^2),a.2/sqrt((a.1)^2+(a.2)^2+(a.3)^2),
  a.3/sqrt((a.1)^2+(a.2)^2+(a.3)^2) ]|;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let p, a be Element of REAL 3;
  func Directiondiff(f,p,a) -> Real equals
:: PDIFF_4:def 9
  partdiff(f,p,1)*(unitvector(a)).1+
  partdiff(f,p,2)*(unitvector(a)).2+
  partdiff(f,p,3)*(unitvector(a)).3;
end;

theorem :: PDIFF_4:41
  a = <*x0,y0,z0*> implies Directiondiff(f,p,a) =
    partdiff(f,p,1)*x0/sqrt(x0^2+y0^2+z0^2)+
    partdiff(f,p,2)*y0/sqrt(x0^2+y0^2+z0^2)+
    partdiff(f,p,3)*z0/sqrt(x0^2+y0^2+z0^2);

theorem :: PDIFF_4:42
  Directiondiff(f,p,a) = |( grad(f,p),unitvector(a) )|;

definition
  let f1,f2,f3 be PartFunc of REAL 3,REAL;
  let p be Element of REAL 3;
  func curl(f1,f2,f3,p) -> Element of REAL 3 equals
:: PDIFF_4:def 10
  (partdiff(f3,p,2)-partdiff(f2,p,3))*<e1>+
  (partdiff(f1,p,3)-partdiff(f3,p,1))*<e2>+
  (partdiff(f2,p,1)-partdiff(f1,p,2))*<e3>;
end;

theorem :: PDIFF_4:43
  curl(f1,f2,f3,p) = |[ partdiff(f3,p,2)-partdiff(f2,p,3),
  partdiff(f1,p,3)-partdiff(f3,p,1),partdiff(f2,p,1)-partdiff(f1,p,2) ]|;