begin
theorem Th1:
:: 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:
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
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:
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) ! )) )
Lm1:
for Z being open Subset of REAL
for f being Function of REAL ,REAL holds dom (f | Z) = Z
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
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:
theorem
theorem Th19:
theorem Th20:
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:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
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) )