The Mizar abstract of FDIFF

Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users
The abstract of the Mizar article:: Real Function Differentiability --- Part II
by
Jaroslaw Kotowicz, and
Konrad Raczkowski
Received January 10, 1991
MML identifier: FDIFF_2
[ Mizar article, MML identifier index ]
environ

 vocabulary SEQ_1, FDIFF_1, SEQM_3, PRE_TOPC, PARTFUN1, ARYTM_1, SEQ_2,
      ORDINAL2, FUNCT_1, ARYTM, ABSVALUE, SQUARE_1, RELAT_1, RCOMP_1, ARYTM_3,
      FCONT_1, BOOLE, FINSEQ_1, PARTFUN2, LIMFUNC1, SUBSET_1, RFUNCT_2, PROB_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, FUNCT_1, FUNCT_2, SEQ_1, RELSET_1, SEQ_2, ABSVALUE,
      PARTFUN1, SQUARE_1, PARTFUN2, RFUNCT_1, RCOMP_1, RFUNCT_2, FCONT_1,
      FDIFF_1, LIMFUNC1, SEQM_3;
 constructors REAL_1, NAT_1, SEQ_2, SEQM_3, ABSVALUE, PROB_1, PARTFUN1,
      PARTFUN2, RFUNCT_1, RCOMP_1, RFUNCT_2, FCONT_1, FDIFF_1, LIMFUNC1,
      MEMBERED, XBOOLE_0;
 clusters RCOMP_1, FDIFF_1, FCONT_3, RELSET_1, RFUNCT_2, PARTFUN2, XREAL_0,
      SEQ_1, SEQM_3, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve x for set;
 reserve x0,r,r1,r2,g,g1,g2,p for Real;
 reserve n,m,k,l for Nat;
 reserve a,b,d for Real_Sequence;
 reserve h,h1,h2 for convergent_to_0 Real_Sequence;
 reserve c,c1 for constant Real_Sequence;
 reserve A for open Subset of REAL;
 reserve f,f1,f2 for PartFunc of REAL,REAL;
 reserve L for LINEAR;
 reserve R for REST;

definition let h;
 cluster -h -> convergent_to_0;
end;

theorem :: FDIFF_2:1
a is convergent & b is convergent & lim a = lim b &
(for n holds d.(2*n) = a.n & d.(2*n + 1) = b.n) implies
d is convergent & lim d = lim a;

theorem :: FDIFF_2:2
(for n holds a.n = 2*n) implies a is increasing natural-yielding;

theorem :: FDIFF_2:3
(for n holds a.n = 2*n + 1) implies a is increasing natural-yielding;

theorem :: FDIFF_2:4
rng c = {x0} implies c is convergent & lim c = x0 &
h + c is convergent & lim(h + c) = x0;

theorem :: FDIFF_2:5
rng a = {r} & rng b = {r} implies a = b;

theorem :: FDIFF_2:6
a is_subsequence_of h implies a is convergent_to_0 Real_Sequence;

theorem :: FDIFF_2:7
(for h,c st rng c = {g} & rng (h + c) c= dom f & {g} c= dom f holds
h"(#)(f*(h + c) - f*c) is convergent) implies
(for h1,h2,c st rng c = {g} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f &
 {g} c= dom f holds
 lim (h1"(#)(f*(h1 + c) - f*c)) = lim(h2"(#)(f*(h2 + c) - f*c)));

theorem :: FDIFF_2:8
(ex N be Neighbourhood of r st N c= dom f) implies
ex h,c st rng c = {r} & rng (h+c) c= dom f & {r} c= dom f;

theorem :: FDIFF_2:9
rng a c= dom (f2*f1) implies rng a c= dom f1 & rng (f1*a) c= dom f2;

scheme ExInc_Seq_of_Nat{ s()->Real_Sequence,P[set] }:
ex q being increasing Seq_of_Nat st
(for n holds P[(s()*q).n]) &
for n st (for r st r = s().n holds P[r]) ex m st n = q.m
provided
 for n ex m st n <= m & P[s().m];

theorem :: FDIFF_2:10
  f.x0 <> r & f is_differentiable_in x0 implies
ex N be Neighbourhood of x0 st N c= dom f & for g st g in N holds f.g <> r;

theorem :: FDIFF_2:11
f is_differentiable_in x0 iff
(ex N be Neighbourhood of x0 st N c= dom f) &
for h,c st rng c = {x0} & rng (h + c) c= dom f holds
h"(#)(f*(h + c) - f*c) is convergent;

theorem :: FDIFF_2:12
f is_differentiable_in x0 & diff(f,x0) = g iff
(ex N be Neighbourhood of x0 st N c= dom f) &
for h,c st rng c = {x0} & rng (h + c) c= dom f holds
h"(#)(f*(h + c) - f*c) is convergent & lim (h"(#)(f*(h + c) - f*c)) = g;

theorem :: FDIFF_2:13
f1 is_differentiable_in x0 & f2 is_differentiable_in f1.x0 implies
f2*f1 is_differentiable_in x0 &
diff(f2*f1,x0) = diff(f2,f1.x0)*diff(f1,x0);

theorem :: FDIFF_2:14
f2.x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies
f1/f2 is_differentiable_in x0 &
diff(f1/f2,x0) = (diff(f1,x0) * f2.x0 - diff(f2,x0) * f1.x0)/(f2.x0)^2;

theorem :: FDIFF_2:15
f.x0 <> 0 & f is_differentiable_in x0 implies
f^ is_differentiable_in x0 & diff(f^,x0) = - diff(f,x0)/(f.x0)^2;

theorem :: FDIFF_2:16
  f is_differentiable_on A implies f|A is_differentiable_on A & f`|A = (f|A)`|A
;

theorem :: FDIFF_2:17
  f1 is_differentiable_on A & f2 is_differentiable_on A implies
f1 + f2 is_differentiable_on A & (f1 + f2)`|A = f1`|A + f2`|A;

theorem :: FDIFF_2:18
  f1 is_differentiable_on A & f2 is_differentiable_on A implies
f1 - f2 is_differentiable_on A & (f1 - f2)`|A = f1`|A - f2`|A;

theorem :: FDIFF_2:19
  f is_differentiable_on A implies
r(#)f is_differentiable_on A & (r(#)f)`|A = r(#)(f`|A);

theorem :: FDIFF_2:20
  f1 is_differentiable_on A & f2 is_differentiable_on A implies
f1 (#) f2 is_differentiable_on A & (f1(#)f2)`|A = (f1`|A)(#)f2 + f1(#)(f2`|A);

theorem :: FDIFF_2:21
  f1 is_differentiable_on A & f2 is_differentiable_on A &
(for x0 st x0 in A holds f2.x0 <> 0) implies
f1/f2 is_differentiable_on A &
(f1/f2)`|A = (f1`|A (#) f2 - f2`|A (#) f1)/(f2 (#) f2);

theorem :: FDIFF_2:22
  f is_differentiable_on A & (for x0 st x0 in A holds f.x0 <> 0) implies
f^ is_differentiable_on A & (f^)`|A = - (f`|A)/ (f (#) f);

theorem :: FDIFF_2:23
  f1 is_differentiable_on A & (f1.:A) is open Subset of REAL &
f2 is_differentiable_on (f1.:A) implies
f2*f1 is_differentiable_on A & (f2*f1)`|A = ((f2`|(f1.:A))*f1) (#) (f1`|A);

theorem :: FDIFF_2:24
A c= dom f &
(for r,p st r in A & p in A holds abs(f.r - f.p) <= (r - p)^2) implies
f is_differentiable_on A & for x0 st x0 in A holds diff(f,x0) = 0;

theorem :: FDIFF_2:25
(for r1,r2 st r1 in ].p,g.[ & r2 in ].p,g.[ holds abs(f.r1 - f.r2) <=
 (r1 - r2)^2) &
p < g & ].p,g.[ c= dom f implies
f is_differentiable_on ].p,g.[ & f is_constant_on ].p,g.[;

theorem :: FDIFF_2:26
  left_open_halfline(r) c= dom f &
(for r1,r2 st r1 in left_open_halfline(r) & r2 in left_open_halfline(r) holds
abs(f.r1 - f.r2) <= (r1 - r2)^2) implies
f is_differentiable_on left_open_halfline(r) &
f is_constant_on left_open_halfline(r);

theorem :: FDIFF_2:27
  right_open_halfline(r) c= dom f &
(for r1,r2 st r1 in right_open_halfline(r) & r2 in right_open_halfline(r) holds
abs(f.r1 - f.r2) <= (r1 - r2)^2) implies
f is_differentiable_on right_open_halfline(r) &
f is_constant_on right_open_halfline(r);

theorem :: FDIFF_2:28
  f is total & (for r1,r2 holds abs(f.r1 - f.r2) <= (r1 - r2)^2) implies
f is_differentiable_on [#](REAL) & f is_constant_on [#](REAL);

theorem :: FDIFF_2:29
f is_differentiable_on left_open_halfline(r) &
(for x0 st x0 in left_open_halfline(r) holds 0 < diff(f,x0)) implies
f is_increasing_on left_open_halfline(r) &
f|left_open_halfline(r) is one-to-one;

theorem :: FDIFF_2:30
f is_differentiable_on left_open_halfline(r) &
(for x0 st x0 in left_open_halfline(r) holds diff(f,x0) < 0) implies
f is_decreasing_on left_open_halfline(r) &
f|left_open_halfline(r) is one-to-one;

theorem :: FDIFF_2:31
  f is_differentiable_on left_open_halfline(r) &
(for x0 st x0 in left_open_halfline(r) holds 0 <= diff(f,x0)) implies
f is_non_decreasing_on left_open_halfline(r);

theorem :: FDIFF_2:32
  f is_differentiable_on left_open_halfline(r) &
(for x0 st x0 in left_open_halfline(r) holds diff(f,x0) <= 0) implies
f is_non_increasing_on left_open_halfline(r);

theorem :: FDIFF_2:33
f is_differentiable_on right_open_halfline(r) &
(for x0 st x0 in right_open_halfline(r) holds 0 < diff(f,x0)) implies
f is_increasing_on right_open_halfline(r) &
f|right_open_halfline(r) is one-to-one;

theorem :: FDIFF_2:34
f is_differentiable_on right_open_halfline(r) &
(for x0 st x0 in right_open_halfline(r) holds diff(f,x0) < 0) implies
f is_decreasing_on right_open_halfline(r) &
f|right_open_halfline(r) is one-to-one;

theorem :: FDIFF_2:35
  f is_differentiable_on right_open_halfline(r) &
(for x0 st x0 in right_open_halfline(r) holds 0 <= diff(f,x0)) implies
f is_non_decreasing_on right_open_halfline(r);

theorem :: FDIFF_2:36
  f is_differentiable_on right_open_halfline(r) &
(for x0 st x0 in right_open_halfline(r) holds diff(f,x0) <= 0) implies
f is_non_increasing_on right_open_halfline(r);

theorem :: FDIFF_2:37
f is_differentiable_on [#](REAL) & (for x0 holds 0 < diff(f,x0)) implies
f is_increasing_on [#](REAL) & f is one-to-one;

theorem :: FDIFF_2:38
f is_differentiable_on [#](REAL) & (for x0 holds diff(f,x0) < 0) implies
f is_decreasing_on [#](REAL) & f is one-to-one;

theorem :: FDIFF_2:39
  f is_differentiable_on [#](REAL) & (for x0 holds 0 <= diff(f,x0)) implies
f is_non_decreasing_on [#](REAL);

theorem :: FDIFF_2:40
  f is_differentiable_on [#](REAL) & (for x0 holds diff(f,x0) <= 0) implies
f is_non_increasing_on [#](REAL);

theorem :: FDIFF_2:41
f is_differentiable_on ].p,g.[ &
((for x0 st x0 in ].p,g.[ holds 0 < diff(f,x0)) or
for x0 st x0 in ].p,g.[ holds diff(f,x0) < 0) implies
rng (f|].p,g.[) is open;

theorem :: FDIFF_2:42
f is_differentiable_on left_open_halfline(p) &
((for x0 st x0 in left_open_halfline(p) holds 0 < diff(f,x0)) or
for x0 st x0 in left_open_halfline(p) holds diff(f,x0) < 0) implies
rng (f|left_open_halfline(p)) is open;

theorem :: FDIFF_2:43
f is_differentiable_on right_open_halfline(p) &
((for x0 st x0 in right_open_halfline(p) holds 0 < diff(f,x0)) or
for x0 st x0 in right_open_halfline(p) holds diff(f,x0) < 0) implies
rng (f|right_open_halfline(p)) is open;

theorem :: FDIFF_2:44
f is_differentiable_on [#](REAL) &
((for x0 holds 0 < diff(f,x0)) or for x0 holds diff(f,x0) < 0) implies
rng f is open;

theorem :: FDIFF_2:45
  for f be one-to-one PartFunc of REAL,REAL st f is_differentiable_on [#](REAL)
&
((for x0 holds 0 < diff(f,x0)) or for x0 holds diff(f,x0) < 0) holds
f is one-to-one & f" is_differentiable_on dom (f") &
for x0 st x0 in dom (f") holds diff(f",x0) = 1/diff(f,(f").x0);


theorem :: FDIFF_2:46
  for f be one-to-one PartFunc of REAL,REAL st
f is_differentiable_on left_open_halfline(p) &
((for x0 st x0 in left_open_halfline(p) holds 0 < diff(f,x0)) or
for x0 st x0 in left_open_halfline(p) holds diff(f,x0) < 0) holds
f|left_open_halfline(p) is one-to-one &
(f|left_open_halfline(p))" is_differentiable_on
dom ((f|left_open_halfline(p))") &
for x0 st x0 in dom ((f|left_open_halfline(p))") holds
diff((f|left_open_halfline(p))",x0) = 1/diff(f,((f|left_open_halfline(p))").x0)
;

theorem :: FDIFF_2:47
  for f be one-to-one PartFunc of REAL,REAL st
f is_differentiable_on right_open_halfline(p) &
((for x0 st x0 in right_open_halfline(p) holds 0 < diff(f,x0)) or
for x0 st x0 in right_open_halfline(p) holds diff(f,x0) < 0) holds
f|right_open_halfline(p) is one-to-one &
(f|right_open_halfline(p))" is_differentiable_on
dom ((f|right_open_halfline(p))") &
for x0 st x0 in dom ((f|right_open_halfline(p))") holds
diff((f|right_open_halfline(p))",x0) =
1/diff(f,((f|right_open_halfline(p))").x0);

theorem :: FDIFF_2:48
  for f be one-to-one PartFunc of REAL,REAL st
f is_differentiable_on ].p,g.[ &
((for x0 st x0 in ].p,g.[ holds 0 < diff(f,x0)) or
for x0 st x0 in ].p,g.[ holds diff(f,x0) < 0) holds
f|].p,g.[ is one-to-one &
(f|].p,g.[)" is_differentiable_on dom ((f|].p,g.[)") &
for x0 st x0 in dom ((f|].p,g.[)") holds
diff((f|].p,g.[)",x0) = 1/diff(f,((f|].p,g.[)").x0);

theorem :: FDIFF_2:49
  f is_differentiable_in x0 implies
for h,c st rng c = {x0} & rng (h + c) c= dom f & rng (-h + c) c= dom f holds
(2(#)h)"(#)(f*(c + h) - f*(c - h)) is convergent &
lim((2(#)h)"(#)(f*(c + h) - f*(c - h))) = diff(f,x0);
The abstract of the Mizar article:

Real Function Differentiability --- Part II
