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

begin

theorem Th1: :: TAYLOR_2:1

for x being Real
for n being Element of NAT holds abs (x |^ n) = (abs x) |^ n

proof end;

definition

let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let a be real number ;
func Maclaurin (f,Z,a) -> Real_Sequence equals :: TAYLOR_2:def 1
Taylor (f,Z,0,a);
coherence
Taylor (f,Z,0,a) is Real_Sequence ;

end;

:: deftheorem defines Maclaurin TAYLOR_2:def 1 :
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for a being real number holds Maclaurin (f,Z,a) = Taylor (f,Z,0,a);

theorem Th2: :: TAYLOR_2:2

for n being Element of 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 Element of 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 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((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 Element of 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 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((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 Element of 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 Element of 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
abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs 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 Element of NAT
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
abs (((((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 Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
abs (((((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 Element of NAT st
for m being Element of NAT st n <= m holds
for x being real number st x in ].(- r),r.[ holds
abs ((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

for Z being open Subset of REAL holds
( sin `| Z = cos | Z & cos `| Z = (- sin) | Z & dom (sin | Z) = Z & dom (cos | Z) = Z )

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

for Z being open Subset of REAL
for n being Element of 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) )

proof end;

theorem Th20: :: TAYLOR_2:20

for n being Element of 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 Element of NAT
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((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 Element of NAT st
for m being Element of NAT st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((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 Element of NAT st
for m being Element of NAT st n <= m holds
for x being real number st x in ].(- r),r.[ holds
( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((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 Element of 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 Element of 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 Element of 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;