:: The {M}aclaurin Expansions
:: by Akira Nishino and Yasunari Shidama
::
:: Received July 6, 2005
:: Copyright (c) 2005-2012 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
proofend;

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 &amp; ].(- r),r.[ c= dom f &amp; 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 &amp; s < 1 &amp; f . x = ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n) + (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) )
proofend;

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 &amp; ].(x0 - r),(x0 + r).[ c= dom f &amp; 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 &amp; s < 1 &amp; 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) !)) )
proofend;

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 &amp; ].(- r),r.[ c= dom f &amp; 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 &amp; s < 1 &amp; 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) !)) )
proofend;

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

theorem Th5: :: TAYLOR_2:5
for Z being open Subset of REAL holds
( exp_R `| Z = exp_R | Z &amp; dom (exp_R | Z) = Z )
proofend;

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
proofend;

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
proofend;

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 !)
proofend;

theorem :: TAYLOR_2:9
for n being Element of NAT
for r, x, s being Real st x in ].(- r),r.[ &amp; 0 < s &amp; 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) !)
proofend;

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
proofend;

theorem Th11: :: TAYLOR_2:11
for r being Real st 0 < r holds
ex M, L being Real st
( 0 <= M &amp; 0 <= L &amp; ( for n being Element of NAT
for x, s being Real st x in ].(- r),r.[ &amp; 0 < s &amp; s < 1 holds
abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ) )
proofend;

theorem Th12: :: TAYLOR_2:12
for M, L being Real st M >= 0 &amp; 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
proofend;

theorem Th13: :: TAYLOR_2:13
for r, e being Real st 0 < r &amp; 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.[ &amp; 0 < s &amp; s < 1 holds
abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e
proofend;

theorem :: TAYLOR_2:14
for r, e being Real st 0 < r &amp; 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
proofend;

theorem Th15: :: TAYLOR_2:15
for x being Real holds x rExpSeq is absolutely_summable
proofend;

theorem :: TAYLOR_2:16
for r, x being Real st 0 < r holds
( Maclaurin (exp_R,].(- r),r.[,x) = x rExpSeq &amp; Maclaurin (exp_R,].(- r),r.[,x) is absolutely_summable &amp; exp_R . x = Sum (Maclaurin (exp_R,].(- r),r.[,x)) )
proofend;

theorem Th17: :: TAYLOR_2:17
for Z being open Subset of REAL holds
( sin `| Z = cos | Z &amp; cos `| Z = (- sin) | Z &amp; dom (sin | Z) = Z &amp; dom (cos | Z) = Z )
proofend;

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)
proofend;

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) &amp; (diff (sin,Z)) . ((2 * n) + 1) = ((- 1) |^ n) (#) (cos | Z) &amp; (diff (cos,Z)) . (2 * n) = ((- 1) |^ n) (#) (cos | Z) &amp; (diff (cos,Z)) . ((2 * n) + 1) = ((- 1) |^ (n + 1)) (#) (sin | Z) )
proofend;

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 &amp; (Maclaurin (sin,].(- r),r.[,x)) . ((2 * n) + 1) = (((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) &amp; (Maclaurin (cos,].(- r),r.[,x)) . (2 * n) = (((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) !) &amp; (Maclaurin (cos,].(- r),r.[,x)) . ((2 * n) + 1) = 0 )
proofend;

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 &amp; cos is_differentiable_on n,Z )
proofend;

theorem Th22: :: TAYLOR_2:22
for r being Real st r > 0 holds
ex r1, r2 being Real st
( r1 >= 0 &amp; r2 >= 0 &amp; ( for n being Element of NAT
for x, s being Real st x in ].(- r),r.[ &amp; 0 < s &amp; s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) &amp; abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) )
proofend;

theorem Th23: :: TAYLOR_2:23
for r, e being Real st 0 < r &amp; 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.[ &amp; 0 < s &amp; s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e &amp; abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e )
proofend;

theorem :: TAYLOR_2:24
for r, e being Real st 0 < r &amp; 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 &amp; abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e )
proofend;

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 &amp; (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) + 1) = (Partial_Sums (x P_cos)) . m )
proofend;

theorem Th26: :: TAYLOR_2:26
for r, x being Real
for m being Element of NAT st 0 < r &amp; m > 0 holds
( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_sin)) . (m - 1) &amp; (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m )
proofend;

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
proofend;

theorem :: TAYLOR_2:28
for r, x being Real st r > 0 holds
( Partial_Sums (Maclaurin (sin,].(- r),r.[,x)) is convergent &amp; sin . x = Sum (Maclaurin (sin,].(- r),r.[,x)) &amp; Partial_Sums (Maclaurin (cos,].(- r),r.[,x)) is convergent &amp; cos . x = Sum (Maclaurin (cos,].(- r),r.[,x)) )
proofend;