:: The {M}aclaurin Expansions :: by Akira Nishino and Yasunari Shidama :: :: Received July 6, 2005 :: Copyright (c) 2005-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, RCOMP_1, SUBSET_1, REAL_1, COMPLEX1, NEWTON, ARYTM_3, RELAT_1, CARD_1, PARTFUN1, SEQ_1, TAYLOR_1, XXREAL_1, ARYTM_1, TARSKI, FDIFF_1, FUNCT_1, SERIES_1, REALSET1, XBOOLE_0, SIN_COS, XXREAL_0, VALUED_0, VALUED_1, SEQ_2, ORDINAL2, CARD_3, ABIAN, TAYLOR_2, NAT_1; notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RFUNCT_2, RCOMP_1, XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, NUMBERS, COMPLEX1, REAL_1, NAT_1, FUNCT_2, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SERIES_1, FDIFF_1, SEQFUNC, NEWTON, SIN_COS, TAYLOR_1, ABIAN; constructors ARYTM_0, REAL_1, NAT_1, SEQ_2, RCOMP_1, RFUNCT_2, LIMFUNC1, FDIFF_1, COMSEQ_3, SIN_COS, ABIAN, TAYLOR_1, SEQFUNC, SERIES_1, VALUED_1, RELSET_1, COMSEQ_2; registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, NEWTON, SIN_COS, INT_1, ORDINAL1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin reserve Z for open Subset of REAL; theorem :: TAYLOR_2:1 for x be Real, n be Nat holds |.x |^ n.| = |.x.| |^ n; definition let f be PartFunc of REAL,REAL, Z be Subset of REAL, a be Real; func Maclaurin(f,Z,a) -> Real_Sequence equals :: TAYLOR_2:def 1 Taylor(f,Z,0,a); end; theorem :: TAYLOR_2:2 for n be Nat, f be PartFunc of REAL,REAL, r be Real st 0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1,].-r,r.[ for x be Real st x in ].-r, r.[ ex s be Real st 0 < s & s < 1 & f.x = Partial_Sums( Maclaurin(f,].-r,r.[,x)).n + (diff(f,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n+ 1)!); theorem :: TAYLOR_2:3 for n be Nat, f be PartFunc of REAL,REAL, x0, r be Real st 0 < r & ].x0-r,x0+r.[ c= dom f & f is_differentiable_on n+1, ].x0-r,x0+r.[ for x be Real st x in ].x0-r, x0+r.[ ex s be Real st 0 < s & s < 1 & |.f.x- Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n.| = |. (diff(f,].x0-r,x0+r.[).(n +1)).(x0+s*(x-x0)) * (x-x0) |^ (n+1) / ((n+1)!).|; theorem :: TAYLOR_2:4 for n be Nat, f be PartFunc of REAL,REAL, r be Real st 0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1, ].-r,r.[ for x be Real st x in ].-r, r.[ ex s be Real st 0 < s & s < 1 & |.f.x-Partial_Sums( Maclaurin(f,].-r,r.[,x)).n.| = |. (diff(f,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n+1)!).|; theorem :: TAYLOR_2:5 exp_R `| Z = exp_R | Z & dom(exp_R | Z) = Z; theorem :: TAYLOR_2:6 for n be Nat holds diff(exp_R,Z).n=exp_R | Z; theorem :: TAYLOR_2:7 for n be Nat, x be Real st x in Z holds (diff(exp_R,Z) .n).x = exp_R.x; theorem :: TAYLOR_2:8 for n be Element of NAT, r,x be Real st 0 < r holds Maclaurin(exp_R, ].-r,r.[,x).n = x |^ n / (n!); theorem :: TAYLOR_2:9 for n be Element of NAT, r,x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(exp_R,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n+1)!) .| <= |.exp_R.(s*x).| * |.x.| |^ (n+1) / ((n+1)!); theorem :: TAYLOR_2:10 for n be Element of NAT holds exp_R is_differentiable_on n, Z; theorem :: TAYLOR_2:11 for r be Real st 0 < r ex M,L be Real st 0 <= M & 0 <= L & for n be Nat for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n /(n!).| <= M * L |^ n / (n!); theorem :: TAYLOR_2:12 for M,L be Real st M >= 0 & L >= 0 for e be Real st e > 0 ex n be Nat st for m be Nat st n <= m holds (M*L |^ m / (m!)) < e; theorem :: TAYLOR_2:13 for r, e be Real st 0 < r & 0 < e ex n be Nat st for m be Nat st n <= m for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(exp_R,].-r,r.[).m).(s*x) * x |^ m / (m!).|< e; theorem :: TAYLOR_2:14 for r, e be Real st 0 < r & 0 < e ex n be Nat st for m be Nat st n <= m holds for x being Real st x in ].-r,r.[ holds |.exp_R.x-Partial_Sums(Maclaurin(exp_R,].-r,r.[,x)).m.| < e; theorem :: TAYLOR_2:15 for x be Real holds x rExpSeq is absolutely_summable; theorem :: TAYLOR_2:16 for r, x be Real st 0 < r holds Maclaurin(exp_R,].-r,r.[,x) = (x rExpSeq) & Maclaurin(exp_R,].-r,r.[,x) is absolutely_summable & exp_R.x=Sum( Maclaurin(exp_R,].-r,r.[,x)); theorem :: TAYLOR_2:17 sin `| Z = cos | Z & cos `| Z = (-sin) | Z & dom(sin | Z) = Z & dom(cos | Z) = Z; theorem :: TAYLOR_2:18 for f be PartFunc of REAL,REAL, Z be Subset of REAL st f is_differentiable_on Z holds (-f) `| Z = -f `| Z; theorem :: TAYLOR_2:19 for n be Nat holds diff(sin,Z).(2*n) = (-1) |^ n (#) sin | Z & diff(sin,Z).(2*n+1) = (-1) |^ n (#) cos | Z & diff(cos,Z).(2*n) = (-1 ) |^ n (#)cos | Z & diff(cos,Z).(2*n+1) = (-1) |^ (n+1) (#)sin | Z; theorem :: TAYLOR_2:20 for n be Nat, r,x be Real st r > 0 holds Maclaurin( sin, ].-r,r.[,x).(2*n) = 0 & Maclaurin(sin, ].-r,r.[,x).(2*n+1) = (-1) |^ n * x |^ (2*n+1) / ((2*n+1)!) & Maclaurin(cos, ].-r,r.[,x).(2*n) = (-1) |^ n * x |^ ( 2*n) / ((2*n)!) & Maclaurin(cos, ].-r,r.[,x).(2*n+1) = 0; theorem :: TAYLOR_2:21 for n be Element of NAT holds sin is_differentiable_on n, Z & cos is_differentiable_on n, Z; theorem :: TAYLOR_2:22 for r be Real st r > 0 ex r1,r2 be Real st r1 >= 0 & r2 >= 0 & for n be Nat for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1 * r2 |^ n / (n!) & |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1 * r2 |^ n / (n!); theorem :: TAYLOR_2:23 for r, e be Real st 0 < r & 0 < e ex n be Nat st for m be Nat st n <= m for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(sin,].-r,r.[).m).(s*x) * x |^ m / (m!).| < e & |.( diff(cos,].-r,r.[).m).(s*x) * x |^ m / (m!).| < e; theorem :: TAYLOR_2:24 for r, e be Real st 0 < r & 0 < e ex n be Nat st for m be Nat st n <= m for x being Real st x in ].-r,r.[ holds |.sin.x-Partial_Sums(Maclaurin(sin,].-r,r.[,x)).m.| < e & |.cos.x- Partial_Sums(Maclaurin(cos,].-r,r.[,x)).m.| < e; theorem :: TAYLOR_2:25 for r, x be Real, m be Nat st 0 < r holds Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m+1) = Partial_Sums(x P_sin).m & Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m+1) = Partial_Sums(x P_cos).m; theorem :: TAYLOR_2:26 for r, x be Real, m being Nat st 0 < r & m > 0 holds Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m) = Partial_Sums(x P_sin).(m-1) & Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m) = Partial_Sums(x P_cos).m; theorem :: TAYLOR_2:27 for r, x be Real, m be Nat st 0 < r holds Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m) = Partial_Sums(x P_cos).m; theorem :: TAYLOR_2:28 for r, x be Real st r > 0 holds Partial_Sums(Maclaurin(sin,].-r,r.[,x) ) is convergent & sin.x = Sum(Maclaurin(sin,].-r,r.[,x)) & Partial_Sums( Maclaurin(cos,].-r,r.[,x)) is convergent & cos.x = Sum(Maclaurin(cos,].-r,r.[,x ));