TAYLOR_2: The {M}aclaurin Expansions

:: The {M}aclaurin Expansions
:: by Akira Nishino and Yasunari Shidama
::
:: Received July 6, 2005
:: Copyright (c) 2005-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TAYLOR_1;
theorems XBOOLE_1, ABSVALUE, PARTFUN1, XCMPLX_1, RELAT_1, RCOMP_1, SEQ_1, SEQ_2, SIN_COS, SERIES_1, FUNCT_1, RFUNCT_2, NAT_1, NEWTON, POWER, FDIFF_1, FDIFF_2, TAYLOR_1, SIN_COS2, XREAL_1, RFUNCT_1, ABIAN, COMPLEX1, XXREAL_0, VALUED_1, FUNCT_2, XREAL_0, ORDINAL1;
schemes NAT_1;
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;
constructors HIDDEN, 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;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities VALUED_1, SUBSET_1;
expansions TAYLOR_1;

theorem Th1: :: TAYLOR_2:1

for x being Real
for n being Nat holds |.(x |^ n).| = |.x.| |^ n

proof end;

definition

let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let a be Real;

func Maclaurin (f,Z,a) -> Real_Sequence equals :: TAYLOR_2:def 1
Taylor (f,Z,0,a);

coherence ;

end;

:: deftheorem defines Maclaurin TAYLOR_2:def 1 :

theorem Th2: :: TAYLOR_2:2

for n being Nat
for f being PartFunc of REAL,REAL
for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds
for x being Real st x in ].(- r),r.[ holds
ex s being 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) !)) )

proof end;

theorem :: TAYLOR_2:3

for n being Nat
for f being PartFunc of REAL,REAL
for x0, r being Real st 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds
for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being 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) !)).| )

proof end;

theorem Th4: :: TAYLOR_2:4

for n being Nat
for f being PartFunc of REAL,REAL
for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds
for x being Real st x in ].(- r),r.[ holds
ex s being 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) !)).| )

proof end;

Lm1: for Z being open Subset of REAL
for f being Function of REAL,REAL holds dom (f | Z) = Z

proof end;

theorem Th5: :: TAYLOR_2:5

for Z being open Subset of REAL holds
( exp_R `| Z = exp_R | Z & dom (exp_R | Z) = Z )

proof end;

theorem Th6: :: TAYLOR_2:6

for Z being open Subset of REAL
for n being Nat holds (diff (exp_R,Z)) . n = exp_R | Z

proof end;

theorem Th7: :: TAYLOR_2:7

for Z being open Subset of REAL
for n being Nat
for x being Real st x in Z holds
((diff (exp_R,Z)) . n) . x = exp_R . x

proof end;

theorem :: TAYLOR_2:8

for n being Element of NAT
for r, x being Real st 0 < r holds
(Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !)

proof end;

theorem :: TAYLOR_2:9

for n being Element of NAT
for r, x, s being 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) !)

proof end;

theorem Th10: :: TAYLOR_2:10

for Z being open Subset of REAL
for n being Element of NAT holds exp_R is_differentiable_on n,Z

proof end;

theorem Th11: :: TAYLOR_2:11

for r being Real st 0 < r holds
ex M, L being Real st
( 0 <= M & 0 <= L & ( for n being Nat
for x, s being 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 !) ) )

proof end;

theorem Th12: :: TAYLOR_2:12

for M, L being Real st M >= 0 & L >= 0 holds
for e being Real st e > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(M * (L |^ m)) / (m !) < e

proof end;

theorem Th13: :: TAYLOR_2:13

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
|.(((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e

proof end;

theorem :: TAYLOR_2:14

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being 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

proof end;

theorem Th15: :: TAYLOR_2:15

for x being Real holds x rExpSeq is absolutely_summable

proof end;

theorem :: TAYLOR_2:16

for r, x being 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)) )

proof end;

theorem Th17: :: TAYLOR_2:17

proof end;

theorem :: TAYLOR_2:18

for f being PartFunc of REAL,REAL
for Z being Subset of REAL st f is_differentiable_on Z holds
(- f) `| Z = - (f `| Z)

proof end;

theorem Th19: :: TAYLOR_2:19

proof end;

theorem Th20: :: TAYLOR_2:20

for n being Nat
for r, x being 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 )

proof end;

theorem Th21: :: TAYLOR_2:21

for Z being open Subset of REAL
for n being Element of NAT holds
( sin is_differentiable_on n,Z & cos is_differentiable_on n,Z )

proof end;

theorem Th22: :: TAYLOR_2:22

for r being Real st r > 0 holds
ex r1, r2 being Real st
( r1 >= 0 & r2 >= 0 & ( for n being Nat
for x, s being 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 !) ) ) )

proof end;

theorem Th23: :: TAYLOR_2:23

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
for x, s being 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 )

proof end;

theorem :: TAYLOR_2:24

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
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 )

proof end;

theorem Th25: :: TAYLOR_2:25

for r, x being Real
for m being 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 )

proof end;

theorem Th26: :: TAYLOR_2:26

for r, x being Real
for 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 )

proof end;

theorem Th27: :: TAYLOR_2:27

for r, x being Real
for m being Nat st 0 < r holds
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m

proof end;

theorem :: TAYLOR_2:28

for r, x being 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)) )

proof end;