:: The {T}aylor Expansions
:: by Yasunari Shidama
::
:: Received February 24, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

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
ex b1 being Function of REAL,REAL st
for x being real number holds b1 . x = x #Z q
proof end;
uniqueness
for b1, b2 being Function of REAL,REAL st ( for x being real number holds b1 . x = x #Z q ) & ( for x being real number holds b2 . x = x #Z q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines #Z TAYLOR_1:def 1 :
for q being Integer
for b2 being Function of REAL,REAL holds
( b2 = #Z q iff for x being real number holds b2 . x = x #Z q );

theorem Th1: :: TAYLOR_1:1
for x being real number
for m, n being Nat holds x #Z (n + m) = (x #Z n) * (x #Z m)
proof end;

theorem Th2: :: TAYLOR_1:2
for n being Nat
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 Nat
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 Nat
for x being real number holds (exp_R x) #R n = exp_R (n * x)
proof end;

theorem Th4: :: TAYLOR_1:4
for x being real number holds exp_R (- x) = 1 / (exp_R x)
proof end;

Lm2: for i being Integer
for x being real number holds (exp_R x) #R i = exp_R (i * x)
proof end;

theorem Th5: :: TAYLOR_1:5
for i being Integer
for x being real number holds (exp_R x) #R (1 / i) = exp_R (x / i)
proof end;

theorem Th6: :: TAYLOR_1:6
for x being real number
for m, n being Integer holds (exp_R x) #R (m / n) = exp_R ((m / n) * x)
proof end;

Lm3: for x being real number
for q being Rational holds (exp_R x) #R q = exp_R (q * x)
proof end;

theorem Th7: :: TAYLOR_1:7
for x being real number
for q being Rational holds (exp_R x) #Q q = exp_R (q * x)
proof end;

theorem Th8: :: TAYLOR_1:8
for x, p being real number holds (exp_R x) #R p = exp_R (p * x)
proof end;

theorem Th9: :: TAYLOR_1:9
for x being real number holds
( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )
proof end;

theorem :: TAYLOR_1:10
for x being real number holds
( (exp_R . 1) #R x = exp_R . x & (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x )
proof end;

theorem :: TAYLOR_1:11
number_e > 2
proof end;

then Lm4: number_e > 1
by XXREAL_0:2;

theorem Th12: :: TAYLOR_1:12
for x being real number holds log (number_e,(exp_R x)) = x
proof end;

theorem Th13: :: TAYLOR_1:13
for x being real number holds log (number_e,(exp_R . x)) = x
proof end;

theorem Th14: :: TAYLOR_1:14
for y being real number st y > 0 holds
exp_R (log (number_e,y)) = y
proof end;

theorem Th15: :: TAYLOR_1:15
for y being real number st y > 0 holds
exp_R . (log (number_e,y)) = y
proof end;

theorem Th16: :: TAYLOR_1:16
( exp_R is one-to-one & exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL & ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )
proof end;

registration
cluster exp_R -> one-to-one ;
coherence
exp_R is one-to-one by Th16;
end;

theorem Th17: :: TAYLOR_1:17
( exp_R " is_differentiable_on dom (exp_R ") & ( for x being real number st x in dom (exp_R ") holds
diff ((exp_R "),x) = 1 / x ) )
proof end;

registration
cluster right_open_halfline 0 -> non empty ;
coherence
not right_open_halfline 0 is empty
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
ex b1 being PartFunc of REAL,REAL st
( dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = log (a,d) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of REAL,REAL st dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = log (a,d) ) & dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = log (a,d) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines log_ TAYLOR_1:def 2 :
for a being real number
for b2 being PartFunc of REAL,REAL holds
( b2 = log_ a iff ( dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = log (a,d) ) ) );

definition
func ln -> PartFunc of REAL,REAL equals :: TAYLOR_1:def 3
 log_ number_e;
correctness
coherence
log_ number_e is PartFunc of REAL,REAL;
;
end;

:: deftheorem defines ln TAYLOR_1:def 3 :
ln = log_ number_e;

theorem Th18: :: TAYLOR_1:18
( ln = exp_R " & ln is one-to-one & dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,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_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (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
( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )
proof end;

definition
let p be real number ;
func #R p -> PartFunc of REAL,REAL means :Def4: :: TAYLOR_1:def 4
( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = d #R p ) );
existence
ex b1 being PartFunc of REAL,REAL st
( dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = d #R p ) )
proof end;
uniqueness
for b1, b2 being PartFunc of REAL,REAL st dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = d #R p ) & dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = d #R p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines #R TAYLOR_1:def 4 :
for p being real number
for b2 being PartFunc of REAL,REAL holds
( b2 = #R p iff ( dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = d #R p ) ) );

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;

begin

definition
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
func diff (f,Z) -> Functional_Sequence of REAL,REAL means :Def5: :: TAYLOR_1:def 5
( it . 0 = f | Z & ( for i being Nat holds it . (i + 1) = (it . i) `| Z ) );
existence
ex b1 being Functional_Sequence of REAL,REAL st
( b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (b1 . i) `| Z ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of REAL,REAL st b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (b1 . i) `| Z ) & b2 . 0 = f | Z & ( for i being Nat holds b2 . (i + 1) = (b2 . i) `| Z ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines diff TAYLOR_1:def 5 :
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b3 being Functional_Sequence of REAL,REAL holds
( b3 = diff (f,Z) iff ( b3 . 0 = f | Z & ( for i being Nat holds b3 . (i + 1) = (b3 . i) `| Z ) ) );

definition
let f be PartFunc of REAL,REAL;
let n be Nat;
let Z be Subset of REAL;
pred f is_differentiable_on n,Z means :Def6: :: TAYLOR_1:def 6
 for i being Element of NAT st i <= n - 1 holds
(diff (f,Z)) . i is_differentiable_on Z;
end;

:: deftheorem Def6 defines is_differentiable_on TAYLOR_1:def 6 :
for f being PartFunc of REAL,REAL
for n being Nat
for Z being Subset of REAL holds
( f is_differentiable_on n,Z iff for i being Element of NAT st i <= n - 1 holds
(diff (f,Z)) . i is_differentiable_on Z );

theorem Th23: :: TAYLOR_1:23
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 m being Nat 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 :Def7: :: TAYLOR_1:def 7
 for n being Nat holds it . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !);
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) & ( for n being Nat holds b2 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Taylor TAYLOR_1:def 7 :
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for a, b being real number
for b5 being Real_Sequence holds
( b5 = Taylor (f,Z,a,b) iff for n being Nat holds b5 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) );

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 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 !)) ) ) ) ) )
proof end;

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) ) )
proof end;

theorem Th24: :: TAYLOR_1:24
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
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 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 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 !)) ) )
proof end;

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 !)) ) )
proof end;

theorem Th25: :: TAYLOR_1:25
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 !)) ) )
proof end;

theorem Th26: :: TAYLOR_1:26
for n being Element of 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 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) !)) )
proof end;

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 !)) ) )
proof end;

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 !)) ) )
proof end;

theorem Th28: :: TAYLOR_1:28
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 !)) ) )
proof end;

theorem Th29: :: TAYLOR_1:29
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) !)) )
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 Element of 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 Nat 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 Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n
proof end;

:: WP: Taylor's Theorem
theorem :: TAYLOR_1:33
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) !)) )
proof end;