:: Several Higher Differentiation Formulas of Special Functions :: by Junjie Zhao , Xiquan Liang and Li Yan :: :: Received March 18, 2008 :: Copyright (c) 2008-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, PARTFUN1, NAT_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_1, VALUED_1, TARSKI, XXREAL_0, PREPOWER, ORDINAL4, CARD_1, NEWTON, ARYTM_3, FDIFF_1, SIN_COS, ABIAN, SQUARE_1, REALSET1, TAYLOR_1, TAYLOR_2, XXREAL_1, COMPLEX1, FUNCOP_1, FUNCT_7; notations SUBSET_1, FUNCT_1, PARTFUN1, RCOMP_1, XXREAL_0, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, FUNCT_2, XREAL_0, FUNCOP_1, REAL_1, NAT_1, NAT_D, VALUED_1, TAYLOR_2, FDIFF_1, SEQFUNC, NEWTON, SIN_COS, TAYLOR_1, ABIAN, XBOOLE_0, TARSKI, PREPOWER, RFUNCT_1, SQUARE_1, RELSET_1; constructors REAL_1, NAT_1, RCOMP_1, LIMFUNC1, TAYLOR_2, FDIFF_1, SIN_COS, ABIAN, TAYLOR_1, RFUNCT_1, SQUARE_1, PREPOWER, BINARITH, PARTFUN2, VALUED_1, BINOP_2, NAT_D, SEQFUNC, RELSET_1, NEWTON, NUMBERS; registrations RELSET_1, NUMBERS, NAT_1, MEMBERED, VALUED_0, RCOMP_1, FUNCT_1, INT_1, ORDINAL1, FUNCT_2, XREAL_0, NEWTON, PREPOWER, SQUARE_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin reserve x,r,a,x0,p for Real; reserve n,i,m for Element of NAT; reserve Z for open Subset of REAL; reserve f,f1,f2 for PartFunc of REAL,REAL; reserve k for Nat; theorem :: HFDIFF_1:1 for f being Function of REAL, REAL holds dom (f | Z) = Z; theorem :: HFDIFF_1:2 (-f1)(#)(-f2)=f1(#)f2; theorem :: HFDIFF_1:3 n>=1 implies dom(( #Z n)^) = REAL\{0} & ( #Z n)"{0}={0}; theorem :: HFDIFF_1:4 (r*p)(#)(( #Z n)^)=r(#)(p(#)(( #Z n)^)); theorem :: HFDIFF_1:5 for n,m be Real holds n(#)f1+m(#)f1=(n+m)(#)f1; theorem :: HFDIFF_1:6 f|Z is_differentiable_on Z implies f is_differentiable_on Z; theorem :: HFDIFF_1:7 n>=1 & f1 is_differentiable_on n,Z implies f1 is_differentiable_on Z; theorem :: HFDIFF_1:8 #Z n is_differentiable_on REAL; :: 1 f.x = sin.x theorem :: HFDIFF_1:9 x in Z implies (diff(sin,Z).2).x = -sin.x; theorem :: HFDIFF_1:10 x in Z implies (diff(sin,Z).3).x = (-cos).x; theorem :: HFDIFF_1:11 x in Z implies (diff(sin,Z).n).x = sin.(x + n*PI/2); :: 2 f.x = cos.x theorem :: HFDIFF_1:12 x in Z implies (diff(cos,Z).2).x = -cos.x; theorem :: HFDIFF_1:13 x in Z implies (diff(cos,Z).3).x = sin.x; theorem :: HFDIFF_1:14 x in Z implies (diff(cos,Z).n).x = cos.(x + n*PI/2); theorem :: HFDIFF_1:15 f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies diff(f1+f2,Z).n = diff(f1,Z).n + diff(f2,Z).n; theorem :: HFDIFF_1:16 f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies diff(f1-f2,Z).n = diff(f1,Z).n - diff(f2,Z).n; theorem :: HFDIFF_1:17 f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i<=n implies diff(f1+f2,Z).i = diff(f1,Z).i + diff(f2,Z).i; theorem :: HFDIFF_1:18 f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i<=n implies diff(f1-f2,Z).i = diff(f1,Z).i - diff(f2,Z).i; theorem :: HFDIFF_1:19 f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies f1+ f2 is_differentiable_on n,Z; theorem :: HFDIFF_1:20 f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies f1- f2 is_differentiable_on n,Z; theorem :: HFDIFF_1:21 f is_differentiable_on n,Z implies diff(r(#)f,Z).n = r(#)diff(f, Z).n; theorem :: HFDIFF_1:22 f is_differentiable_on n,Z implies r(#)f is_differentiable_on n, Z; theorem :: HFDIFF_1:23 f is_differentiable_on Z implies diff(f,Z).1 = f`|Z; theorem :: HFDIFF_1:24 n>=1 & f1 is_differentiable_on n,Z implies diff(f1,Z).1=f1`|Z; theorem :: HFDIFF_1:25 x in Z implies (diff(r(#)sin,Z).n).x = r*sin.(x + n*PI/2); theorem :: HFDIFF_1:26 x in Z implies (diff(r(#)cos,Z).n).x = r*cos.(x + n*PI/2); theorem :: HFDIFF_1:27 x in Z implies (diff(r(#)exp_R,Z).n).x = r*exp_R.x; theorem :: HFDIFF_1:28 #Z n `| Z = (n(#) #Z (n-1)) | Z; theorem :: HFDIFF_1:29 x <> 0 implies ( #Z n)^ is_differentiable_in x & diff(( #Z n)^,x ) = -(n * x #Z (n-1))/(x #Z n)^2; theorem :: HFDIFF_1:30 n>=1 implies diff( #Z n,Z).2 = (n*(n-1)(#) #Z (n-2))|Z; theorem :: HFDIFF_1:31 n>=2 implies diff( #Z n,Z).3 = (n*(n-1)*(n-2)(#) #Z (n-3))|Z; theorem :: HFDIFF_1:32 n>m implies diff( #Z n,Z).m = ((n choose m)*(m!)(#) #Z (n-m)) |Z; theorem :: HFDIFF_1:33 f is_differentiable_on n,Z implies diff(-f,Z).n = -diff(f,Z).n & -f is_differentiable_on n,Z; theorem :: HFDIFF_1:34 x0 in Z implies Taylor(sin,Z,x0,x).n = sin.(x0+n*PI/2)*(x-x0)|^ n / (n !) & Taylor(cos,Z,x0,x).n = cos.(x0+n*PI/2)*(x-x0)|^ n / (n!); theorem :: HFDIFF_1:35 r>0 implies Maclaurin(sin,].-r,r.[,x).n = sin.(n*PI/2)*x|^ n / (n!) & Maclaurin(cos,].-r,r.[,x).n = cos.(n*PI/2)*x|^ n / (n!); theorem :: HFDIFF_1:36 n>m & x in Z implies (diff( #Z n,Z).m).x = (n choose m)*(m!)*x #Z (n-m); theorem :: HFDIFF_1:37 x in Z implies (diff( #Z m,Z).m).x = m!; theorem :: HFDIFF_1:38 #Z n is_differentiable_on n,Z; theorem :: HFDIFF_1:39 x in Z & n>m implies (diff(a(#) #Z n,Z).m).x = a*(n choose m)*(m!)*x #Z (n-m) ; theorem :: HFDIFF_1:40 x in Z implies (diff(a(#) #Z n,Z).n).x = a*(n!); theorem :: HFDIFF_1:41 x0 in Z & n>m implies Taylor( #Z n,Z,x0,x).m = (n choose m)*x0 #Z (n-m) *(x-x0)|^ m & Taylor( #Z n,Z,x0,x).n = (x-x0)|^ n; theorem :: HFDIFF_1:42 for n,m be Element of NAT,r,x be Element of REAL st n>m & r>0 holds Maclaurin( #Z n,].-r,r.[,x).m = 0 & Maclaurin( #Z n,].-r,r.[,x).n = x|^ n; theorem :: HFDIFF_1:43 not 0 in Z implies ( #Z n)^ is_differentiable_on Z; theorem :: HFDIFF_1:44 not 0 in Z & x0 in Z implies ((( #Z n)^)`|Z).x0 =- n/( #Z (n+1)).x0; theorem :: HFDIFF_1:45 :: FDIFF_4:14 x <> 0 implies (id REAL)^ is_differentiable_in x & diff((id REAL )^,x) = -1/x^2; theorem :: HFDIFF_1:46 not 0 in Z implies ((id REAL)^)`|Z = ((-1)(#)(( #Z 2)^))|Z; theorem :: HFDIFF_1:47 x <> 0 implies ( #Z 2)^ is_differentiable_in x & diff(( #Z 2)^,x ) = -(2 * x)/(x #Z 2)^2; theorem :: HFDIFF_1:48 not 0 in Z implies (( #Z 2)^)`|Z = ((-2)(#)(( #Z 3)^))|Z; theorem :: HFDIFF_1:49 not 0 in Z & n>=1 implies (( #Z n)^)`|Z = ((-n)(#)(( #Z (n+1))^) )|Z; theorem :: HFDIFF_1:50 f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z implies diff(f1(#)f2,Z).2 = (diff(f1,Z).2)(#)f2 + 2(#)((f1`|Z)(#)(f2`|Z)) + f1 (#)(diff(f2,Z).2); theorem :: HFDIFF_1:51 Z c= dom ln & Z c= dom((id REAL)^) implies ln`| Z = ((id REAL)^)| Z; theorem :: HFDIFF_1:52 n>=1 & x0 in Z & not 0 in Z implies (diff((( #Z n)^),Z).2).x0 = n*(n+1 )*((( #Z (n+2))^).x0); theorem :: HFDIFF_1:53 diff(sin^2,Z).2 = 2(#)((cos^2)|Z) +(-2)(#)((sin^2)|Z); theorem :: HFDIFF_1:54 diff(cos^2,Z).2 = 2(#)((sin^2)|Z) +(-2)(#)((cos^2)|Z); theorem :: HFDIFF_1:55 diff(sin(#)cos,Z).2 = 4(#)((-sin)(#)cos)|Z; theorem :: HFDIFF_1:56 Z c= dom tan implies tan is_differentiable_on Z & tan`|Z = ((cos ^)^2)|Z; theorem :: HFDIFF_1:57 Z c= dom tan implies cos^ is_differentiable_on Z & (cos^)`|Z = ( (cos^)(#)tan)|Z; theorem :: HFDIFF_1:58 Z c= dom tan implies diff(tan,Z).2=2(#)((tan(#)(cos^)(#)(cos^))|Z); theorem :: HFDIFF_1:59 Z c= dom cot implies cot is_differentiable_on Z & cot`|Z = ((-1) (#)((sin^)^2))|Z; theorem :: HFDIFF_1:60 Z c= dom cot implies sin^ is_differentiable_on Z & (sin^)`|Z = ( -(sin^)(#)cot)|Z; theorem :: HFDIFF_1:61 Z c= dom cot implies diff(cot,Z).2=2(#)(cot(#)(sin^)(#)(sin^))|Z; theorem :: HFDIFF_1:62 diff(exp_R(#)sin,Z).2 = 2(#)((exp_R(#)cos)|Z); theorem :: HFDIFF_1:63 diff(exp_R(#)cos,Z).2 = 2(#)((exp_R(#)-sin)|Z); theorem :: HFDIFF_1:64 f1 is_differentiable_on 3,Z & f2 is_differentiable_on 3,Z implies diff(f1(#)f2,Z).3 =(diff(f1,Z).3)(#)f2 + (3(#)(diff(f1,Z).2(#)(f2`|Z)) +3(#)((f1`|Z)(#)diff(f2,Z).2))+ f1(#)(diff(f2,Z).3); theorem :: HFDIFF_1:65 diff(sin^2,Z).3=(-8)(#)((cos(#)sin)|Z); theorem :: HFDIFF_1:66 f is_differentiable_on 2,Z implies diff(f^2,Z).2=2(#)(f(#)(diff(f,Z).2 ))+2(#)((f`|Z)^2); theorem :: HFDIFF_1:67 f is_differentiable_on 2,Z & (for x0 st x0 in Z holds f.x0 <> 0) implies diff(f^,Z).2=((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f) /(f(#)(f(#)f))); theorem :: HFDIFF_1:68 diff(exp_R(#)sin,Z).3=(2(#)(exp_R(#)((-sin)+cos)))|Z;