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


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
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 holds Maclaurin (f,Z,a) = Taylor (f,Z,0,a);

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