environ
vocabularies HIDDEN, NUMBERS, RCOMP_1, SUBSET_1, REAL_1, COMPLEX1, NEWTON, ARYTM_3, RELAT_1, CARD_1, PARTFUN1, SEQ_1, TAYLOR_1, XXREAL_1, ARYTM_1, TARSKI, FDIFF_1, FUNCT_1, SERIES_1, REALSET1, XBOOLE_0, SIN_COS, XXREAL_0, VALUED_0, VALUED_1, SEQ_2, ORDINAL2, CARD_3, ABIAN, TAYLOR_2, NAT_1;
notations HIDDEN, TARSKI, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RFUNCT_2, RCOMP_1, XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, NUMBERS, COMPLEX1, REAL_1, NAT_1, FUNCT_2, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SERIES_1, FDIFF_1, SEQFUNC, NEWTON, SIN_COS, TAYLOR_1, ABIAN;
definitions TAYLOR_1;
theorems XBOOLE_1, ABSVALUE, PARTFUN1, XCMPLX_1, RELAT_1, RCOMP_1, SEQ_1, SEQ_2, SIN_COS, SERIES_1, FUNCT_1, RFUNCT_2, NAT_1, NEWTON, POWER, FDIFF_1, FDIFF_2, TAYLOR_1, SIN_COS2, XREAL_1, RFUNCT_1, ABIAN, COMPLEX1, XXREAL_0, VALUED_1, FUNCT_2, XREAL_0, ORDINAL1;
schemes NAT_1;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, NEWTON, SIN_COS, INT_1, ORDINAL1;
constructors HIDDEN, ARYTM_0, REAL_1, NAT_1, SEQ_2, RCOMP_1, RFUNCT_2, LIMFUNC1, FDIFF_1, COMSEQ_3, SIN_COS, ABIAN, TAYLOR_1, SEQFUNC, SERIES_1, VALUED_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities VALUED_1, SUBSET_1;
expansions TAYLOR_1;
theorem Th2:
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) !)) )
theorem
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) !)).| )
theorem Th4:
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) !)).| )
Lm1:
for Z being open Subset of REAL
for f being Function of REAL,REAL holds dom (f | Z) = Z
theorem Th12:
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
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 Th20:
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 )
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)) )