environ
vocabularies HIDDEN, NUMBERS, INT_1, RAT_1, PARTFUN1, PREPOWER, FUNCT_1, REAL_1, SUBSET_1, ARYTM_3, RELAT_1, CARD_1, NEWTON, COMPLEX1, XXREAL_0, FDIFF_1, ARYTM_1, RCOMP_1, TARSKI, XBOOLE_0, VALUED_1, SIN_COS, SEQ_2, ORDINAL2, FCONT_1, FUNCT_2, POWER, SERIES_1, REALSET1, NAT_1, CARD_3, LIMFUNC1, SEQFUNC, SEQ_1, XXREAL_1, TAYLOR_1, IRRAT_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, IRRAT_1, LIMFUNC1, RCOMP_1, FCONT_1, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, RAT_1, ORDINAL1, NUMBERS, REAL_1, INT_1, NAT_1, NEWTON, VALUED_1, PARTFUN2, SEQ_1, SEQ_2, SERIES_1, FDIFF_1, SEQFUNC, PREPOWER, POWER, SIN_COS;
definitions ;
theorems XBOOLE_1, ABSVALUE, TARSKI, XBOOLE_0, PARTFUN1, PARTFUN2, XCMPLX_1, RELAT_1, CARD_4, RCOMP_1, SEQ_1, SEQ_2, SIN_COS, SERIES_1, FUNCT_1, NAT_1, INT_1, NEWTON, RAT_1, IRRAT_1, POWER, FCONT_1, FDIFF_1, FDIFF_2, ROLLE, SEQ_4, PREPOWER, FUNCT_2, XREAL_0, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, XXREAL_2;
schemes SEQ_1, RECDEF_1, NAT_1, INT_1, PARTFUN2, FUNCT_2;
registrations XBOOLE_0, RELSET_1, PARTFUN1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, RAT_1, MEMBERED, RCOMP_1, NEWTON, PREPOWER, SIN_COS, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, ORDINAL1, SEQ_4, FCONT_3, ABIAN;
constructors HIDDEN, PARTFUN1, ARYTM_0, REAL_1, NAT_1, SEQ_2, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, SEQFUNC, PREPOWER, COMSEQ_3, SIN_COS, XXREAL_2, SERIES_1, VALUED_1, POWER, RELSET_1, ABIAN, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SUBSET_1, LIMFUNC1;
expansions FUNCT_2;
Lm1:
for n being Nat
for x being Real holds (exp_R x) #R n = exp_R (n * x)
Lm2:
for i being Integer
for x being Real holds (exp_R x) #R i = exp_R (i * x)
Lm3:
for x being Real
for q being Rational holds (exp_R x) #R q = exp_R (q * x)
then Lm4:
number_e > 1
by XXREAL_0:2;
Lm5:
for b being Real ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds
( g . x = b - x & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) )
Lm6:
for n being Nat
for l, b being Real ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) )
Lm7:
for n being Nat
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b being Real ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
Lm8:
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f holds
for n being Nat st f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) holds
( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) )
Lm9:
for n being Nat
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) )
theorem Th25:
for
n being
Nat for
f being
PartFunc of
REAL,
REAL for
Z being
Subset of
REAL st
Z c= dom f &
f is_differentiable_on n,
Z holds
for
a,
b being
Real st
a < b &
[.a,b.] c= Z &
((diff (f,Z)) . n) | [.a,b.] is
continuous &
f is_differentiable_on n + 1,
].a,b.[ holds
for
l being
Real for
g being
PartFunc of
REAL,
REAL st
dom g = [#] REAL & ( for
x being
Real holds
g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) &
((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
(
g is_differentiable_on ].a,b.[ &
g . a = 0 &
g . b = 0 &
g | [.a,b.] is
continuous & ( for
x being
Real st
x in ].a,b.[ holds
diff (
g,
x)
= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) )
theorem Th27:
for
n being
Nat for
f being
PartFunc of
REAL,
REAL for
Z being
Subset of
REAL st
Z c= dom f &
f is_differentiable_on n,
Z holds
for
a,
b being
Real st
a < b &
[.a,b.] c= Z &
((diff (f,Z)) . n) | [.a,b.] is
continuous &
f is_differentiable_on n + 1,
].a,b.[ holds
ex
c being
Real st
(
c in ].a,b.[ &
f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) )
Lm10:
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f holds
for n being Nat st f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) )
Lm11:
for n being Nat
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) )
theorem Th28:
for
n being
Nat for
f being
PartFunc of
REAL,
REAL for
Z being
Subset of
REAL st
Z c= dom f &
f is_differentiable_on n,
Z holds
for
a,
b being
Real st
a < b &
[.a,b.] c= Z &
((diff (f,Z)) . n) | [.a,b.] is
continuous &
f is_differentiable_on n + 1,
].a,b.[ holds
for
l being
Real for
g being
PartFunc of
REAL,
REAL st
dom g = [#] REAL & ( for
x being
Real holds
g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) &
((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
(
g is_differentiable_on ].a,b.[ &
g . b = 0 &
g . a = 0 &
g | [.a,b.] is
continuous & ( for
x being
Real st
x in ].a,b.[ holds
diff (
g,
x)
= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
theorem Th29:
for
n being
Nat for
f being
PartFunc of
REAL,
REAL for
Z being
Subset of
REAL st
Z c= dom f &
f is_differentiable_on n,
Z holds
for
a,
b being
Real st
a < b &
[.a,b.] c= Z &
((diff (f,Z)) . n) | [.a,b.] is
continuous &
f is_differentiable_on n + 1,
].a,b.[ holds
ex
c being
Real st
(
c in ].a,b.[ &
f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
theorem
for
n being
Nat for
f being
PartFunc of
REAL,
REAL for
x0,
r being
Real st
].(x0 - r),(x0 + r).[ c= dom f &
0 < r &
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) !)) )