begin
Lm1:
for n being Nat
for x being real number holds (exp_R x) #R n = exp_R (n * x)
Lm2:
for i being Integer
for x being real number holds (exp_R x) #R i = exp_R (i * x)
Lm3:
for x being real number
for q being Rational holds (exp_R x) #R q = exp_R (q * x)
then Lm4:
number_e > 1
by XXREAL_0:2;
begin
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 Element of 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 Element of 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 Element of 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 Element of 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
Element of
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
Element of
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 Element of 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 Element of 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
Element of
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
Element of
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
Element of
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) !)) )