:: The {M}aclaurin Expansions
:: by Akira Nishino and Yasunari Shidama
::
:: Received July 6, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: TAYLOR_2:1
:: deftheorem defines Maclaurin TAYLOR_2:def 1 :
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) ! )) )
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) ! )) )
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) ! )) )
LemX:
for Z being open Subset of REAL
for f being Function of REAL , REAL holds dom (f | Z) = Z
theorem Th5: :: TAYLOR_2:5
theorem Th6: :: TAYLOR_2:6
theorem Th7: :: TAYLOR_2:7
theorem :: TAYLOR_2:8
theorem :: TAYLOR_2:9
theorem Th10: :: TAYLOR_2:10
theorem Th11: :: TAYLOR_2:11
theorem Th12: :: TAYLOR_2:12
theorem Th13: :: TAYLOR_2:13
theorem :: TAYLOR_2:14
theorem Th15: :: TAYLOR_2:15
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) )
theorem Th17: :: TAYLOR_2:17
theorem :: TAYLOR_2:18
theorem Th19: :: TAYLOR_2:19
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 )
theorem Th21: :: TAYLOR_2:21
theorem Th22: :: TAYLOR_2:22
theorem Th23: :: TAYLOR_2:23
theorem :: TAYLOR_2:24
theorem Th25: :: TAYLOR_2:25
theorem Th26: :: TAYLOR_2:26
theorem Th27: :: TAYLOR_2:27
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) )