:: Real Function Differentiability
::  by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-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, REAL_1, SUBSET_1, RCOMP_1, SEQ_1, PARTFUN1, VALUED_0,
      SEQ_2, ORDINAL2, CARD_1, ARYTM_3, FUNCT_1, RELAT_1, FUNCOP_1, VALUED_1,
      FUNCT_2, NAT_1, TARSKI, ARYTM_1, XXREAL_1, XBOOLE_0, XXREAL_0, COMPLEX1,
      FCONT_1, XXREAL_2, FDIFF_1, FUNCT_7, ASYMPT_1, XCMPLX_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1,
      SEQ_1, COMSEQ_2, SEQ_2, RELSET_1, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1,
      XXREAL_0;
 constructors PARTFUN1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, RCOMP_1,
      PARTFUN2, RFUNCT_2, FCONT_1, VALUED_1, REALSET1, FINSET_1, SETFAM_1,
      RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, NUMBERS;
 registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED,
      RCOMP_1, VALUED_0, VALUED_1, FUNCT_2, FUNCOP_1, SEQ_4, RELAT_1, SEQ_1,
      SEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve y for object, X for set;
reserve x,x0,x1,x2,g,g1,g2,r,r1,s,p,p1 for Real;
reserve n,m,k for Element of NAT;
reserve Y for Subset of REAL;
reserve Z for open Subset of REAL;
reserve s1,s3 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;

theorem :: FDIFF_1:1
  (for r holds r in Y iff r in REAL) iff Y = REAL;

definition let x be Real;
  let IT be Real_Sequence;
  attr IT is x-convergent means
:: FDIFF_1:def 1
    IT is convergent & lim IT = x;
end;

registration
  cluster 0-convergent non-zero for Real_Sequence;
end;

registration let f be 0-convergent Real_Sequence;
  cluster lim f -> zero;
end;

registration
  cluster 0-convergent -> convergent for Real_Sequence;
end;

reserve h for non-zero 0-convergent Real_Sequence;
reserve c for constant Real_Sequence;

definition
  let IT be PartFunc of REAL,REAL;
  attr IT is RestFunc-like means
:: FDIFF_1:def 2
  IT is total & for h holds (h")(#)(IT/*h) is convergent &
  lim ((h")(#)(IT/*h)) = 0;
end;



registration
  cluster RestFunc-like for PartFunc of REAL,REAL;
end;

definition
  mode RestFunc is RestFunc-like PartFunc of REAL,REAL;
end;

definition
  let IT be PartFunc of REAL,REAL;
  attr IT is linear means
:: FDIFF_1:def 3
  IT is total & ex r st for p holds IT.p = r*p;
end;

registration
  cluster linear for PartFunc of REAL,REAL;
end;

definition
  mode LinearFunc is linear PartFunc of REAL,REAL;
end;

reserve R,R1,R2 for RestFunc;
reserve L,L1,L2 for LinearFunc;

theorem :: FDIFF_1:2
  L1+L2 is LinearFunc & L1-L2 is LinearFunc;

theorem :: FDIFF_1:3
  r(#)L is LinearFunc;

theorem :: FDIFF_1:4
  R1+R2 is RestFunc & R1-R2 is RestFunc & R1(#)R2 is RestFunc;

theorem :: FDIFF_1:5
  r(#)R is RestFunc;

theorem :: FDIFF_1:6
  L1(#)L2 is RestFunc-like;

theorem :: FDIFF_1:7
  R(#)L is RestFunc & L(#)R is RestFunc;

definition
  let f;
  let x0 be Real;
  pred f is_differentiable_in x0 means
:: FDIFF_1:def 4

  ex N being Neighbourhood of x0
st N c= dom f & ex L,R st for x st x in N holds f.x - f.x0 = L.(x-x0) + R.(x-x0
  );
end;

definition
  let f;
  let x0 be Real;
  assume
 f is_differentiable_in x0;
  func diff(f,x0) -> Real means
:: FDIFF_1:def 5

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

definition
  let f,X;
  pred f is_differentiable_on X means
:: FDIFF_1:def 6

  X c= dom f & for x st x in X holds f|X is_differentiable_in x;
end;

theorem :: FDIFF_1:8
  f is_differentiable_on X implies X is Subset of REAL;

theorem :: FDIFF_1:9
  f is_differentiable_on Z iff Z c= dom f & for x st x in Z holds
  f is_differentiable_in x;

theorem :: FDIFF_1:10
  f is_differentiable_on Y implies Y is open;

definition
  let f,X;
  assume
 f is_differentiable_on X;
  func f`|X -> PartFunc of REAL,REAL means
:: FDIFF_1:def 7

  dom it = X & for x st x in X holds it.x = diff(f,x);
end;

theorem :: FDIFF_1:11
  (Z c= dom f & ex r st rng f = {r}) implies f is_differentiable_on Z &
  for x st x in Z holds (f`|Z).x = 0;

registration
  let h be non-zero Real_Sequence; let n be Nat;
  cluster h^\n -> non-zero for Real_Sequence;
end;

registration
  let h; let n be Nat;
  cluster h^\n -> non-zero 0-convergent for Real_Sequence;
end;

theorem :: FDIFF_1:12
  for x0 being Real for N being Neighbourhood of x0 st f
is_differentiable_in x0 & N c= dom f holds for h,c st rng c = {x0} & rng (h+c)
c= N holds h"(#)(f/*(h+c) - f/*c) is convergent & diff(f,x0) = lim (h"(#)(f/*(h
  +c) - f/*c));

theorem :: FDIFF_1:13
  f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies
  f1+f2 is_differentiable_in x0 & diff(f1+f2,x0)=diff(f1,x0)+diff(f2,x0);

theorem :: FDIFF_1:14
  f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies
  f1-f2 is_differentiable_in x0 & diff(f1-f2,x0)=diff(f1,x0)-diff(f2,x0);

theorem :: FDIFF_1:15
  f is_differentiable_in x0 implies r(#)f is_differentiable_in x0
  & diff((r(#)f),x0) = r*diff(f,x0);

theorem :: FDIFF_1:16
  f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies
f1(#)f2 is_differentiable_in x0 & diff(f1(#)f2,x0)=(f2.x0)*diff(f1,x0)+(f1.x0)*
  diff(f2,x0);

theorem :: FDIFF_1:17
  Z c= dom f & f|Z = id Z implies f is_differentiable_on Z & for x
  st x in Z holds (f`|Z).x = 1;

theorem :: FDIFF_1:18
  Z c= dom (f1+f2) & f1 is_differentiable_on Z & f2 is_differentiable_on
Z implies f1+f2 is_differentiable_on Z & for x st x in Z holds ((f1+f2)`|Z).x =
  diff(f1,x) + diff(f2,x);

theorem :: FDIFF_1:19
  Z c= dom (f1-f2) & f1 is_differentiable_on Z & f2 is_differentiable_on
Z implies f1-f2 is_differentiable_on Z & for x st x in Z holds ((f1-f2)`|Z).x =
  diff(f1,x) - diff(f2,x);

theorem :: FDIFF_1:20
  Z c= dom (r(#)f) & f is_differentiable_on Z implies r(#)f
  is_differentiable_on Z & for x st x in Z holds ((r(#) f)`|Z).x =r*diff(f,x);

theorem :: FDIFF_1:21
  Z c= dom (f1(#)f2) & f1 is_differentiable_on Z & f2
is_differentiable_on Z implies f1(#)f2 is_differentiable_on Z & for x st x in Z
  holds ((f1(#)f2)`|Z).x = (f2.x)*diff(f1,x) + (f1.x)*diff(f2,x);

theorem :: FDIFF_1:22
  Z c= dom f & f|Z is constant implies f is_differentiable_on Z & for x
  st x in Z holds (f`|Z).x = 0;

theorem :: FDIFF_1:23
  Z c= dom f & (for x st x in Z holds f.x = r*x + p) implies f
  is_differentiable_on Z & for x st x in Z holds (f`|Z).x = r;

theorem :: FDIFF_1:24
  for x0 being Real holds f is_differentiable_in x0 implies
  f is_continuous_in x0;

theorem :: FDIFF_1:25
  f is_differentiable_on X implies f|X is continuous;

theorem :: FDIFF_1:26
  f is_differentiable_on X & Z c= X implies f is_differentiable_on Z;

theorem :: FDIFF_1:27 ::AN
::  f is_differentiable_in x0 implies
ex R st R.0=0 & R is_continuous_in 0;

definition
  let f be PartFunc of REAL, REAL;
  attr f is differentiable means
:: FDIFF_1:def 8
  f is_differentiable_on dom f;
end;

registration
  cluster differentiable for Function of REAL, REAL;
end;

theorem :: FDIFF_1:28
  for f being differentiable PartFunc of REAL, REAL st Z c= dom f holds
  f is_differentiable_on Z;