:: Real Function Differentiability - Part II :: by Jaros{\l}aw Kotowicz and Konrad Raczkowski :: :: Received January 10, 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, REAL_1, SUBSET_1, SEQ_1, FDIFF_1, FUNCT_1, RCOMP_1, PARTFUN1, ARYTM_1, VALUED_0, SEQ_2, ORDINAL2, CARD_1, RELAT_1, ARYTM_3, XXREAL_0, COMPLEX1, NAT_1, TARSKI, VALUED_1, FUNCT_2, FUNCOP_1, XXREAL_1, FCONT_1, SQUARE_1, XBOOLE_0, ORDINAL4, LIMFUNC1, FUNCT_7, ASYMPT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, NAT_1, FUNCT_1, FUNCT_2, VALUED_0, VALUED_1, SEQ_1, RELSET_1, COMSEQ_2, SEQ_2, PARTFUN1, PARTFUN2, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, LIMFUNC1, RECDEF_1; constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, PARTFUN2, RFUNCT_1, RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, VALUED_1, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, NUMBERS; registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, SEQM_3, RCOMP_1, RFUNCT_2, FDIFF_1, FCONT_3, VALUED_0, VALUED_1, FUNCT_2, SEQ_4, SQUARE_1, SEQ_1, SEQ_2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve x for object; reserve x0,r,r1,r2,g,g1,g2,p,y0 for Real; reserve n,m,k,l for Element of NAT; reserve a,b,d for Real_Sequence; reserve h,h1,h2 for non-zero 0-convergent 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 LinearFunc; reserve R for RestFunc; registration let h; cluster -h -> non-zero convergent; 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 sequence of NAT; theorem :: FDIFF_2:3 (for n holds a.n = 2*n + 1) implies a is increasing sequence of NAT; 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 0-convergent non-zero 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 :: FDIFF_2:sch 1 ExIncSeqofNat{ s()->Real_Sequence,P[object] }: ex q being increasing sequence of NAT st (for n being Nat 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 |.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 |.f.r1 - f.r2.| <= (r1 - r2)^2) & ].p,g.[ c= dom f implies f is_differentiable_on ].p,g.[ & f|].p,g.[ is constant; 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 |.f.r1 - f.r2.| <= ( r1 - r2)^2) implies f is_differentiable_on left_open_halfline(r) & f| left_open_halfline r is constant; 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 |.f.r1 - f.r2.| <= (r1 - r2)^2) implies f is_differentiable_on right_open_halfline(r) & f| right_open_halfline r is constant; theorem :: FDIFF_2:28 f is total & (for r1,r2 holds |.f.r1 - f.r2.| <= (r1 - r2)^2) implies f is_differentiable_on [#](REAL) & f|[#]REAL is constant; theorem :: FDIFF_2:29 left_open_halfline(r) c= dom f & f is_differentiable_on left_open_halfline(r) & (for x0 st x0 in left_open_halfline(r) holds 0 < diff(f ,x0)) implies f|left_open_halfline r is increasing & f|left_open_halfline(r) is one-to-one; theorem :: FDIFF_2:30 left_open_halfline(r) c= dom f & f is_differentiable_on left_open_halfline(r) & (for x0 st x0 in left_open_halfline(r) holds diff(f,x0) < 0) implies f|left_open_halfline r is decreasing & f|left_open_halfline(r) is one-to-one; theorem :: FDIFF_2:31 left_open_halfline(r) c= dom f & f is_differentiable_on left_open_halfline(r) & (for x0 st x0 in left_open_halfline(r) holds 0 <= diff( f,x0)) implies f|left_open_halfline r is non-decreasing; theorem :: FDIFF_2:32 left_open_halfline(r) c= dom f & f is_differentiable_on left_open_halfline(r) & (for x0 st x0 in left_open_halfline(r) holds diff(f,x0) <= 0) implies f|left_open_halfline r is non-increasing; theorem :: FDIFF_2:33 right_open_halfline(r) c= dom f & f is_differentiable_on right_open_halfline(r) & (for x0 st x0 in right_open_halfline(r) holds 0 < diff (f,x0)) implies f|right_open_halfline r is increasing & f|right_open_halfline(r ) is one-to-one; theorem :: FDIFF_2:34 right_open_halfline(r) c= dom f & f is_differentiable_on right_open_halfline(r) & (for x0 st x0 in right_open_halfline(r) holds diff(f, x0) < 0) implies f|right_open_halfline r is decreasing & f|right_open_halfline( r) is one-to-one; theorem :: FDIFF_2:35 right_open_halfline(r) c= dom f & f is_differentiable_on right_open_halfline(r) & (for x0 st x0 in right_open_halfline(r) holds 0 <= diff(f,x0)) implies f|right_open_halfline r is non-decreasing; theorem :: FDIFF_2:36 right_open_halfline(r) c= dom f & f is_differentiable_on right_open_halfline(r) & (for x0 st x0 in right_open_halfline(r) holds diff(f, x0) <= 0) implies f|right_open_halfline r is non-increasing; theorem :: FDIFF_2:37 [#](REAL) c= dom f & f is_differentiable_on [#](REAL) & (for x0 holds 0 < diff(f,x0)) implies f|[#]REAL is increasing & f is one-to-one; theorem :: FDIFF_2:38 [#](REAL) c= dom f & f is_differentiable_on [#](REAL) & (for x0 holds diff(f,x0) < 0) implies f|[#]REAL is decreasing & f is one-to-one; theorem :: FDIFF_2:39 [#](REAL) c= dom f & f is_differentiable_on [#](REAL) & (for x0 holds 0 <= diff(f,x0)) implies f|[#]REAL is non-decreasing; theorem :: FDIFF_2:40 [#](REAL) c= dom f & f is_differentiable_on [#](REAL) & (for x0 holds diff(f,x0) <= 0) implies f|[#]REAL is non-increasing; theorem :: FDIFF_2:41 ].p,g.[ c= dom f & 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 left_open_halfline(p) c= dom f & 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 right_open_halfline(p) c= dom f& 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 [#](REAL) c= dom f & 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 [#]REAL c= dom f & 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 left_open_halfline(p) c= dom f & 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 right_open_halfline(p) c= dom f & 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 ].p,g.[ c= dom f & 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);