:: 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 proofend; 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 proofend; 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) proofend; 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)) ) proofend; 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)) ) proofend; Lm1: for n being Nat for x being real number holds (exp_R x) #R n = exp_R (n * x) proofend; theorem Th4: :: TAYLOR_1:4 for x being real number holds exp_R (- x) = 1 / (exp_R x) proofend; Lm2: for i being Integer for x being real number holds (exp_R x) #R i = exp_R (i * x) proofend; 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) proofend; 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) proofend; Lm3: for x being real number for q being Rational holds (exp_R x) #R q = exp_R (q * x) proofend; theorem Th7: :: TAYLOR_1:7 for x being real number for q being Rational holds (exp_R x) #Q q = exp_R (q * x) proofend; theorem Th8: :: TAYLOR_1:8 for x, p being real number holds (exp_R x) #R p = exp_R (p * x) proofend; 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 ) proofend; 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 ) proofend; theorem :: TAYLOR_1:11 number_e > 2 proofend; 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 proofend; theorem Th13: :: TAYLOR_1:13 for x being real number holds log (number_e,(exp_R . x)) = x proofend; theorem Th14: :: TAYLOR_1:14 for y being real number st y > 0 holds exp_R (log (number_e,y)) = y proofend; theorem Th15: :: TAYLOR_1:15 for y being real number st y > 0 holds exp_R . (log (number_e,y)) = y proofend; 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 ) proofend; 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 ) ) proofend; registration cluster right_open_halfline 0 -> non empty ; coherence not right_open_halfline 0 is empty proofend; 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) ) ) proofend; 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 proofend; 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) ) ) proofend; 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)) ) proofend; 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) ) proofend; 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 ) ) proofend; 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 proofend; 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)) ) proofend; 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)) ) proofend; 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 ) ) proofend; 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 proofend; 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; predf 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 proofend; 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 !) proofend; 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 proofend; 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 ) ) ) ) ) proofend; 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 !)) ) ) ) ) ) proofend; 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) ) ) proofend; 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 proofend; 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 !)) ) ) proofend; 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 !)) ) ) proofend; 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 !)) ) ) proofend; 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) !)) proofend; 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) !)) ) proofend; 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 !)) ) ) proofend; 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 !)) ) ) proofend; 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 !)) ) ) proofend; 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) !)) ) proofend; 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 proofend; 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 proofend; 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 proofend; :: [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) !)) ) proofend;