:: Real Function One-Side Differantiability
::  by Ewa Burakowska and Beata Madras
::
:: Received December 12, 1991
:: Copyright (c) 1991-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, FDIFF_1, SEQ_1, FUNCT_1, PARTFUN1, REAL_1, SUBSET_1,
      XXREAL_0, CARD_1, XXREAL_1, ARYTM_1, TARSKI, RELAT_1, ARYTM_3, VALUED_0,
      SEQ_2, ORDINAL2, VALUED_1, FUNCT_2, NAT_1, LIMFUNC1, XBOOLE_0, COMPLEX1,
      SQUARE_1, ORDINAL4, RCOMP_1, FDIFF_3, ASYMPT_1;
 notations TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0,
      COMPLEX1, REAL_1, SQUARE_1, NAT_1, RELSET_1, PARTFUN1, FUNCT_1, FUNCT_2,
      FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, RFUNCT_1, RCOMP_1,
      FDIFF_1, LIMFUNC1, RECDEF_1;
 constructors FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3,
      PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, PARTFUN1, FDIFF_1,
      VALUED_1, RECDEF_1, XXREAL_2, SETFAM_1, RELSET_1, BINOP_2, RVSUM_1,
      COMSEQ_2, SEQ_1;
 registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, FDIFF_1,
      VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, SEQ_4, SQUARE_1, NAT_1, SEQ_1,
      SEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve h,h1,h2 for 0-convergent non-zero Real_Sequence,
  c,c1 for constant Real_Sequence,
  f,f1,f2 for PartFunc of REAL,REAL,
  x0,r,r0,r1,r2,g,g1,g2 for Real,
  n0,k,n,m for Element of NAT,
  a,b,d for Real_Sequence,
  x for set;

theorem :: FDIFF_3:1
  (ex r st r>0 & [.x0-r,x0.] c= dom f) implies ex h,c st rng c ={x0
  } & rng (h+c) c= dom f & for n being Nat holds h.n < 0;

theorem :: FDIFF_3:2
  (ex r st r>0 & [.x0,x0+r.] c= dom f) implies ex h,c st rng c ={x0
  } & rng (h+c) c= dom f & for n being Nat holds h.n > 0;

theorem :: FDIFF_3:3
  (for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n being Nat holds h.n <
0) holds h"(#)(f/*(h+c) - f/*c) is convergent) & {x0} c= dom f implies for h1,
h2,c st rng c ={x0} & rng (h1+c) c= dom f &
 (for n being Nat holds h1.n < 0) & rng (h2+c)
 c= dom f & (for n being Nat holds h2.n < 0)
holds lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (
  h2"(#)(f/*(h2+c) - f/*c));

theorem :: FDIFF_3:4
  (for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n being Nat holds h.n>0
) holds h"(#)(f/*(h+c) - f/*c) is convergent) & {x0} c= dom f implies for h1,h2
,c st rng c ={x0} & rng (h1 + c)c= dom f & rng (h2 + c) c= dom f &
 (for n being Nat holds
h1.n >0) & (for n being Nat holds h2.n >0)
 holds lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (h2
  "(#)(f/*(h2+c) - f/*c));

definition
  let f,x0;
  pred f is_Lcontinuous_in x0 means
:: FDIFF_3:def 1

  x0 in dom f & for a st rng a c=
  left_open_halfline(x0) /\ dom f & a is convergent & lim a = x0 holds f/*a is
  convergent & f.x0 = lim(f/*a);
  pred f is_Rcontinuous_in x0 means
:: FDIFF_3:def 2

  x0 in dom f & for a st rng a c=
  right_open_halfline(x0) /\ dom f & a is convergent & lim a = x0 holds f/*a is
  convergent & f.x0 = lim(f/*a);
  pred f is_right_differentiable_in x0 means
:: FDIFF_3:def 3

  (ex r st r>0 & [.x0, x0+r
.] c= dom f) & for h,c st rng c ={x0} & rng (h+c) c= dom f &
  (for n being Nat holds h.n >
  0) holds h"(#)(f/*(h+c) - f/*c) is convergent;
  pred f is_left_differentiable_in x0 means
:: FDIFF_3:def 4

  (ex r st r>0 & [.x0-r,x0.]
  c= dom f) & for h,c st rng c ={x0} & rng (h+c) c= dom f &
   (for n being Nat holds h.n<0)
  holds h"(#)(f/*(h+c) - f/*c) is convergent;
end;

theorem :: FDIFF_3:5
  f is_left_differentiable_in x0 implies f is_Lcontinuous_in x0;

theorem :: FDIFF_3:6
  f is_Lcontinuous_in x0 & f.x0<>g2 & (ex r st r>0 & [.x0-r,x0.] c=
dom f) implies ex r1 st r1 > 0 & [.x0-r1,x0.] c= dom f & for g st g in [.x0-r1,
  x0.] holds f.g <> g2;

theorem :: FDIFF_3:7
  f is_right_differentiable_in x0 implies f is_Rcontinuous_in x0;

theorem :: FDIFF_3:8
  f is_Rcontinuous_in x0 & f.x0 <> g2 & (ex r st r>0 & [.x0, x0+r.]
c= dom f) implies ex r1 st r1>0 & [.x0, x0+r1.] c= dom f & for g st g in [.x0,
  x0+r1.] holds f.g <> g2;

definition
  let x0,f;
  assume
 f is_left_differentiable_in x0;
  func Ldiff (f,x0) -> Real means
:: FDIFF_3:def 5

  for h,c st rng c = {x0} & rng (h + c) c= dom f &
  (for n being Nat holds h.n <0) holds it =lim (h"(#)(f/*(h+c) - f/*c));
end;

definition
  let x0,f;
  assume
 f is_right_differentiable_in x0;
  func Rdiff(f,x0) -> Real means
:: FDIFF_3:def 6

  for h,c st rng c = {x0} & rng (h+c) c=
  dom f & (for n being Nat holds h.n > 0)
  holds it=lim (h"(#)(f/*(h+c) - f/*c));
end;

theorem :: FDIFF_3:9
 for g being Real holds
  f is_left_differentiable_in x0 & Ldiff(f,x0) = g iff (ex r st 0 <
  r & [.x0 -r,x0.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f &
  (for n being Nat holds h.n < 0)
 holds h"(#)(f/*(h+c) - f/*c) is convergent & lim(h"(#)(f/*(h+c) - f/*c)) = g;

theorem :: FDIFF_3:10
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0
implies f1 + f2 is_left_differentiable_in x0 & Ldiff(f1+f2,x0) = Ldiff(f1,x0) +
  Ldiff(f2,x0);

theorem :: FDIFF_3:11
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0
implies f1 - f2 is_left_differentiable_in x0 & Ldiff(f1-f2,x0) = Ldiff(f1,x0) -
  Ldiff(f2,x0);

theorem :: FDIFF_3:12
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0
implies f1(#)f2 is_left_differentiable_in x0 & Ldiff(f1(#)f2,x0) = Ldiff(f1,x0)
  *f2.x0 + Ldiff(f2,x0)*f1.x0;

theorem :: FDIFF_3:13
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2
.x0 <> 0 implies f1/f2 is_left_differentiable_in x0 & Ldiff(f1/f2,x0) = (Ldiff(
  f1,x0)*f2.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2;

theorem :: FDIFF_3:14
  f is_left_differentiable_in x0 & f.x0 <> 0 implies f^
  is_left_differentiable_in x0 & Ldiff(f^,x0) = - Ldiff(f,x0)/(f.x0)^2;

theorem :: FDIFF_3:15
 for g1 being Real holds
  f is_right_differentiable_in x0 & Rdiff(f,x0) = g1 iff (ex r st
r>0 & [.x0,x0+r.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f & (
for n being Nat holds h.n > 0)
holds h"(#)(f/*(h+c) - f/*c) is convergent & lim (h"(#)(f
  /*(h+c) - f/*c)) = g1;

theorem :: FDIFF_3:16
  f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
  implies f1+f2 is_right_differentiable_in x0 & Rdiff(f1+f2,x0) = Rdiff(f1,x0)+
  Rdiff(f2,x0);

theorem :: FDIFF_3:17
  f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
implies f1 - f2 is_right_differentiable_in x0 & Rdiff(f1-f2,x0) = Rdiff(f1,x0)
  - Rdiff(f2,x0);

theorem :: FDIFF_3:18
  f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
implies f1(#)f2 is_right_differentiable_in x0 & Rdiff(f1(#)f2,x0) = Rdiff(f1,x0
  )*f2.x0 + Rdiff(f2,x0)*f1.x0;

theorem :: FDIFF_3:19
  f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 &
  f2.x0 <> 0 implies f1/f2 is_right_differentiable_in x0 & Rdiff(f1/f2,x0) = (
  Rdiff(f1,x0)*f2.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2;

theorem :: FDIFF_3:20
  f is_right_differentiable_in x0 & f.x0 <> 0 implies f^
  is_right_differentiable_in x0 & Rdiff(f^,x0) = - Rdiff(f,x0)/(f.x0)^2;

theorem :: FDIFF_3:21
  f is_right_differentiable_in x0 & f is_left_differentiable_in x0 &
Rdiff(f,x0) = Ldiff(f,x0) implies f is_differentiable_in x0 & diff(f,x0)=Rdiff(
  f,x0) & diff(f,x0)=Ldiff(f,x0);

theorem :: FDIFF_3:22
  f is_differentiable_in x0 implies f is_right_differentiable_in x0 & f
is_left_differentiable_in x0 & diff(f,x0) = Rdiff(f,x0) & diff(f,x0) = Ldiff(f,
  x0);