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 !)) ) )