:: TAYLOR_2 semantic presentation

theorem Th1: :: TAYLOR_2:1

for x being Real
for n being Nat holds abs (x |^ n) = (abs x) |^ n

proof end;

definition

let f be PartFunc of REAL , REAL ;
let Z be Subset of REAL ;
let a be real number ;
func Maclaurin f,Z,a -> Real_Sequence equals :: TAYLOR_2:def 1
Taylor f,Z,0,a;
coherence ;

end;

:: deftheorem defines Maclaurin TAYLOR_2:def 1 :

theorem Th2: :: TAYLOR_2:2

for n being Nat
for f being PartFunc of REAL , REAL
for r being Real st 0 < r & 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) ! )) )

proof end;

theorem :: TAYLOR_2:3

for n being Nat
for f being PartFunc of REAL , REAL
for x0, r being Real st 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 & 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) ! )) )

proof end;

theorem Th4: :: TAYLOR_2:4

for n being Nat
for f being PartFunc of REAL , REAL
for r being Real st 0 < r & 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) ! )) )

proof end;

theorem Th5: :: TAYLOR_2:5

for r being Real holds
( exp `| ].(- r),r.[ = exp | ].(- r),r.[ & dom (exp | ].(- r),r.[) = ].(- r),r.[ )

proof end;

theorem Th6: :: TAYLOR_2:6

for n being Nat
for r being Real holds (diff exp ,].(- r),r.[) . n = exp | ].(- r),r.[

proof end;

theorem Th7: :: TAYLOR_2:7

for n being Nat
for r, x being Real st x in ].(- r),r.[ holds
((diff exp ,].(- r),r.[) . n) . x = exp . x

proof end;

theorem :: TAYLOR_2:8

for n being Nat
for r, x being Real st 0 < r holds
(Maclaurin exp ,].(- r),r.[,x) . n = (x |^ n) / (n ! )

proof end;

theorem :: TAYLOR_2:9

for n being Nat
for r, x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
abs (((((diff exp ,].(- r),r.[) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) ! )) <= ((abs (exp . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) ! )

proof end;

theorem Th10: :: TAYLOR_2:10

for r being Real
for n being Nat holds exp is_differentiable_on n,].(- r),r.[

proof end;

theorem Th11: :: TAYLOR_2:11

for r being Real st 0 < r holds
ex M, L being Real st
( 0 <= M & 0 <= L & ( for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
abs (((((diff exp ,].(- r),r.[) . n) . (s * x)) * (x |^ n)) / (n ! )) <= (M * (L |^ n)) / (n ! ) ) )

proof end;

theorem Th12: :: TAYLOR_2:12

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

proof end;

theorem Th13: :: TAYLOR_2:13

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
abs (((((diff exp ,].(- r),r.[) . m) . (s * x)) * (x |^ m)) / (m ! )) < e

proof end;

theorem :: TAYLOR_2:14

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
for x being real number st x in ].(- r),r.[ holds
abs ((exp . x) - ((Partial_Sums (Maclaurin exp ,].(- r),r.[,x)) . m)) < e

proof end;

theorem Th15: :: TAYLOR_2:15

for x being Real holds x ExpSeq is absolutely_summable

proof end;

theorem :: TAYLOR_2:16

for r, x being Real st 0 < r holds
( Maclaurin exp ,].(- r),r.[,x = x ExpSeq & Maclaurin exp ,].(- r),r.[,x is absolutely_summable & exp . x = Sum (Maclaurin exp ,].(- r),r.[,x) )

proof end;

theorem Th17: :: TAYLOR_2:17

proof end;

theorem :: TAYLOR_2:18

for f being PartFunc of REAL , REAL
for Z being Subset of REAL st f is_differentiable_on Z holds
(- f) `| Z = - (f `| Z)

proof end;

theorem Th19: :: TAYLOR_2:19

proof end;

theorem Th20: :: TAYLOR_2:20

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 )

proof end;

theorem Th21: :: TAYLOR_2:21

for r being Real
for n being Nat holds
( sin is_differentiable_on n,].(- r),r.[ & cos is_differentiable_on n,].(- r),r.[ )

proof end;

theorem Th22: :: TAYLOR_2:22

for r being Real st r > 0 holds
ex r1, r2 being Real st
( r1 >= 0 & r2 >= 0 & ( for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff sin ,].(- r),r.[) . n) . (s * x)) * (x |^ n)) / (n ! )) <= (r1 * (r2 |^ n)) / (n ! ) & abs (((((diff cos ,].(- r),r.[) . n) . (s * x)) * (x |^ n)) / (n ! )) <= (r1 * (r2 |^ n)) / (n ! ) ) ) )

proof end;

theorem Th23: :: TAYLOR_2:23

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff sin ,].(- r),r.[) . m) . (s * x)) * (x |^ m)) / (m ! )) < e & abs (((((diff cos ,].(- r),r.[) . m) . (s * x)) * (x |^ m)) / (m ! )) < e )

proof end;

theorem :: TAYLOR_2:24

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
for x being real number st x in ].(- r),r.[ holds
( abs ((sin . x) - ((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . m)) < e )

proof end;

theorem Th25: :: TAYLOR_2:25

for r, x being Real
for m being Nat st 0 < r holds
( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_sin )) . m & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_cos )) . m )

proof end;

theorem Th26: :: TAYLOR_2:26

for r, x being Real
for m being Nat st 0 < r & m > 0 holds
( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_sin )) . (m - 1) & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_cos )) . m )

proof end;

theorem Th27: :: TAYLOR_2:27

for r, x being Real
for m being Nat st 0 < r holds
(Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_cos )) . m

proof end;

theorem :: TAYLOR_2:28

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

proof end;