:: TAYLOR_1 semantic presentation

definition

let q be Integer;
func #Z q -> Function of REAL , REAL means :Def1: :: TAYLOR_1:def 1
for x being real number holds it . x = x #Z q;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines #Z TAYLOR_1:def 1 :

theorem Th1: :: TAYLOR_1:1

for x being real number
for m, n being natural number holds x #Z (n + m) = (x #Z n) * (x #Z m)

proof end;

theorem Th2: :: TAYLOR_1:2

for n being natural number
for x being real number holds
( #Z n is_differentiable_in x & diff (#Z n),x = n * (x #Z (n - 1)) )

proof end;

theorem :: TAYLOR_1:3

for n being natural number
for x0 being real number
for f being PartFunc of REAL , REAL st f is_differentiable_in x0 holds
( (#Z n) * f is_differentiable_in x0 & diff ((#Z n) * f),x0 = (n * ((f . x0) #Z (n - 1))) * (diff f,x0) )

proof end;

Lm1: for n being natural number
for x being real number holds (exp x) #R n = exp (n * x)

proof end;

theorem Th4: :: TAYLOR_1:4

for x being real number holds exp (- x) = 1 / (exp x)

proof end;

Lm2: for i being Integer
for x being real number holds (exp x) #R i = exp (i * x)

proof end;

theorem Th5: :: TAYLOR_1:5

for i being Integer
for x being real number holds (exp x) #R (1 / i) = exp (x / i)

proof end;

theorem Th6: :: TAYLOR_1:6

for x being real number
for m, n being Integer holds (exp x) #R (m / n) = exp ((m / n) * x)

proof end;

Lm3: for x being real number
for q being Rational holds (exp x) #R q = exp (q * x)

proof end;

theorem Th7: :: TAYLOR_1:7

for x being real number
for q being Rational holds (exp x) #Q q = exp (q * x)

proof end;

theorem Th8: :: TAYLOR_1:8

for x, p being real number holds (exp x) #R p = exp (p * x)

proof end;

theorem Th9: :: TAYLOR_1:9

for x being real number holds
( (exp 1) #R x = exp x & (exp 1) to_power x = exp x & number_e to_power x = exp x & number_e #R x = exp x )

proof end;

theorem :: TAYLOR_1:10

for x being real number holds
( (exp . 1) #R x = exp . x & (exp . 1) to_power x = exp . x & number_e to_power x = exp . x & number_e #R x = exp . x )

proof end;

theorem :: TAYLOR_1:11

number_e >= 2

proof end;

then Lm4: ( number_e > 1 & number_e > 0 )
by XREAL_1:2;

theorem Th12: :: TAYLOR_1:12

for x being real number holds log number_e ,(exp x) = x

proof end;

theorem Th13: :: TAYLOR_1:13

for x being real number holds log number_e ,(exp . x) = x

proof end;

theorem Th14: :: TAYLOR_1:14

for y being real number st y > 0 holds
exp (log number_e ,y) = y

proof end;

theorem Th15: :: TAYLOR_1:15

for y being real number st y > 0 holds
exp . (log number_e ,y) = y

proof end;

theorem Th16: :: TAYLOR_1:16

( exp is one-to-one & exp is_differentiable_on REAL & exp is_differentiable_on [#] REAL & ( for x being Real holds diff exp ,x = exp . x ) & ( for x being Real holds 0 < diff exp ,x ) & dom exp = REAL & dom exp = [#] REAL & rng exp = right_open_halfline 0 )

proof end;

registration

cluster exp -> one-to-one ;
coherence by Th16;

end;

theorem Th17: :: TAYLOR_1:17

( exp " is_differentiable_on dom (exp " ) & ( for x being real number st x in dom (exp " ) holds
diff (exp " ),x = 1 / x ) )

proof end;

registration

cluster right_open_halfline 0 -> non empty ;
coherence

proof end;

end;

definition

let a be real number ;
func log_ a -> PartFunc of REAL , REAL means :Def2: :: TAYLOR_1:def 2
( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = log a,d ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines log_ TAYLOR_1:def 2 :

theorem Th18: :: TAYLOR_1:18

( log_ number_e = exp " & log_ number_e is one-to-one & dom (log_ number_e ) = right_open_halfline 0 & rng (log_ number_e ) = REAL & log_ number_e is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
log_ number_e is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (log_ number_e ),x = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (log_ number_e ),x ) )

proof end;

theorem :: TAYLOR_1:19

for x0 being real number
for f being PartFunc of REAL , REAL st f is_differentiable_in x0 holds
( exp * f is_differentiable_in x0 & diff (exp * f),x0 = (exp . (f . x0)) * (diff f,x0) )

proof end;

theorem :: TAYLOR_1:20

for x0 being real number
for f being PartFunc of REAL , REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( (log_ number_e ) * f is_differentiable_in x0 & diff ((log_ number_e ) * f),x0 = (diff f,x0) / (f . x0) )

proof end;

definition

let p be real number ;
func #R p -> PartFunc of REAL , REAL means :Def3: :: TAYLOR_1:def 3
( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = d #R p ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines #R TAYLOR_1:def 3 :

theorem Th21: :: TAYLOR_1:21

for x, p being real number st x > 0 holds
( #R p is_differentiable_in x & diff (#R p),x = p * (x #R (p - 1)) )

proof end;

theorem :: TAYLOR_1:22

for x0, p being real number
for f being PartFunc of REAL , REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( (#R p) * f is_differentiable_in x0 & diff ((#R p) * f),x0 = (p * ((f . x0) #R (p - 1))) * (diff f,x0) )

proof end;

definition

let f be PartFunc of REAL , REAL ;
let Z be Subset of REAL ;
func diff f,Z -> Functional_Sequence of REAL , REAL means :Def4: :: TAYLOR_1:def 4
( it . 0 = f | Z & ( for i being natural number holds it . (i + 1) = (it . i) `| Z ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines diff TAYLOR_1:def 4 :

definition

let f be PartFunc of REAL , REAL ;
let n be natural number ;
let Z be Subset of REAL ;
pred f is_differentiable_on n,Z means :Def5: :: TAYLOR_1:def 5
for i being Nat st i <= n - 1 holds
(diff f,Z) . i is_differentiable_on Z;

end;

:: deftheorem Def5 defines is_differentiable_on TAYLOR_1:def 5 :

theorem Th23: :: TAYLOR_1:23

for f being PartFunc of REAL , REAL
for Z being Subset of REAL
for n being natural number st f is_differentiable_on n,Z holds
for m being natural number st m <= n holds
f is_differentiable_on m,Z

proof end;

definition

let f be PartFunc of REAL , REAL ;
let Z be Subset of REAL ;
let a, b be real number ;
func Taylor f,Z,a,b -> Real_Sequence means :Def6: :: TAYLOR_1:def 6
for n being natural number holds it . n = ((((diff f,Z) . n) . a) * ((b - a) |^ n)) / (n ! );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Taylor TAYLOR_1:def 6 :

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

proof end;

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

proof end;

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

proof end;

theorem Th24: :: TAYLOR_1:24

for f being PartFunc of REAL , REAL
for Z being Subset of REAL
for n being Nat st f is_differentiable_on n,Z holds
for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff f,Z) . n) | ].a,b.[ = (diff f,].a,b.[) . n

proof end;

Lm8: for f being PartFunc of REAL , REAL
for Z being Subset of REAL
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 is_continuous_on [.a,b.] & 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 is_continuous_on [.a,b.] & 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 ! )) ) )

proof end;

Lm9: for n being Nat
for f being PartFunc of REAL , REAL
for Z being Subset of REAL st f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & (diff f,Z) . n is_continuous_on [.a,b.] & 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 is_continuous_on [.a,b.] & 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 ! )) ) )

proof end;

theorem Th25: :: TAYLOR_1:25

for n being Nat
for f being PartFunc of REAL , REAL
for Z being Subset of REAL st f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & (diff f,Z) . n is_continuous_on [.a,b.] & 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 is_continuous_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 ! ))) + ((l * ((b - x) |^ n)) / (n ! )) ) )

proof end;

theorem Th26: :: TAYLOR_1:26

for n being Nat
for f being PartFunc of REAL , REAL
for Z being Subset of REAL
for b, l being Real ex g being Function of REAL , REAL st
for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor f,Z,x,b)) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! ))

proof end;

theorem Th27: :: TAYLOR_1:27

for n being Nat
for f being PartFunc of REAL , REAL
for Z being Subset of REAL st f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & (diff f,Z) . n is_continuous_on [.a,b.] & 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) ! )) )

proof end;

Lm10: for f being PartFunc of REAL , REAL
for Z being Subset of REAL
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 is_continuous_on [.a,b.] & 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 is_continuous_on [.a,b.] & 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 ! )) ) )

proof end;

Lm11: for n being Nat
for f being PartFunc of REAL , REAL
for Z being Subset of REAL st f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & (diff f,Z) . n is_continuous_on [.a,b.] & 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 is_continuous_on [.a,b.] & 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 ! )) ) )

proof end;

theorem Th28: :: TAYLOR_1:28

for n being Nat
for f being PartFunc of REAL , REAL
for Z being Subset of REAL st f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & (diff f,Z) . n is_continuous_on [.a,b.] & 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 is_continuous_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 ! ))) + ((l * ((a - x) |^ n)) / (n ! )) ) )

proof end;

theorem Th29: :: TAYLOR_1:29

for n being Nat
for f being PartFunc of REAL , REAL
for Z being Subset of REAL st f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & (diff f,Z) . n is_continuous_on [.a,b.] & 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) ! )) )

proof end;

theorem Th30: :: TAYLOR_1:30

for f being PartFunc of REAL , REAL
for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n,Z holds
((diff f,Z) . n) | Z1 = (diff f,Z1) . n

proof end;

theorem Th31: :: TAYLOR_1:31

for f being PartFunc of REAL , REAL
for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being natural number st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1

proof end;

theorem Th32: :: TAYLOR_1:32

for f being PartFunc of REAL , REAL
for Z being Subset of REAL
for x being Real st x in Z holds
for n being Nat holds f . x = (Partial_Sums (Taylor f,Z,x,x)) . n

proof end;

theorem :: TAYLOR_1:33

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

proof end;