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

definition

let q be Integer;

func #Z q -> Function of REAL,REAL means :Def1: :: TAYLOR_1:def 1
for x being Real holds it . x = x #Z q;

existence
ex b₁ being Function of REAL,REAL st
for x being Real holds b₁ . x = x #Z q

proof end;

uniqueness
for b₁, b₂ being Function of REAL,REAL st ( for x being Real holds b₁ . x = x #Z q ) & ( for x being Real holds b₂ . x = x #Z q ) holds
b₁ = b₂

proof end;

end;

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

theorem Th1: :: TAYLOR_1:1

for x being Real
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 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
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 holds (exp_R x) #R n = exp_R (n * x)

proof end;

theorem Th4: :: TAYLOR_1:4

for x being Real holds exp_R (- x) = 1 / (exp_R x)

proof end;

Lm2: for i being Integer
for x being Real 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 holds (exp_R x) #R (1 / i) = exp_R (x / i)

proof end;

theorem Th6: :: TAYLOR_1:6

for x being Real
for m, n being Integer holds (exp_R x) #R (m / n) = exp_R ((m / n) * x)

proof end;

Lm3: for x being Real
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
for q being Rational holds (exp_R x) #Q q = exp_R (q * x)

proof end;

theorem Th8: :: TAYLOR_1:8

for p, x being Real holds (exp_R x) #R p = exp_R (p * x)

proof end;

theorem Th9: :: TAYLOR_1:9

for x being Real 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 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;

registration

cluster number_e -> positive ;

coherence
number_e is positive by Lm4;

end;

theorem Th12: :: TAYLOR_1:12

for x being Real holds log (number_e,(exp_R x)) = x

proof end;

theorem Th13: :: TAYLOR_1:13

for x being Real holds log (number_e,(exp_R . x)) = x

proof end;

theorem Th14: :: TAYLOR_1:14

for y being Real st y > 0 holds
exp_R (log (number_e,y)) = y

proof end;

theorem Th15: :: TAYLOR_1:15

for y being Real 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 & 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 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;

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 b₁ being PartFunc of REAL,REAL st
( dom b₁ = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b₁ . d = log (a,d) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of REAL,REAL st dom b₁ = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b₁ . d = log (a,d) ) & dom b₂ = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b₂ . d = log (a,d) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines log_ TAYLOR_1:def 2 :
for a being Real
for b₂ being PartFunc of REAL,REAL holds
( b₂ = log_ a iff ( dom b₂ = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b₂ . 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
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
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;

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 b₁ being PartFunc of REAL,REAL st
( dom b₁ = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b₁ . d = d #R p ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of REAL,REAL st dom b₁ = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b₁ . d = d #R p ) & dom b₂ = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b₂ . d = d #R p ) holds
b₁ = b₂

proof end;

end;

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

theorem Th21: :: TAYLOR_1:21

for p, x being Real 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 p, x0 being Real
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 :Def5: :: TAYLOR_1:def 5
( it . 0 = f | Z & ( for i being Nat holds it . (i + 1) = (it . i) `| Z ) );

existence
ex b₁ being Functional_Sequence of REAL,REAL st
( b₁ . 0 = f | Z & ( for i being Nat holds b₁ . (i + 1) = (b₁ . i) `| Z ) )

proof end;

uniqueness
for b₁, b₂ being Functional_Sequence of REAL,REAL st b₁ . 0 = f | Z & ( for i being Nat holds b₁ . (i + 1) = (b₁ . i) `| Z ) & b<sub>2</sub> . 0 = f | Z & ( for i being Nat holds b<sub>2</sub> . (i + 1) = (b<sub>2</sub> . i) `| Z ) holds
b₁ = b₂

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 b₃ being Functional_Sequence of REAL,REAL holds
( b₃ = diff (f,Z) iff ( b₃ . 0 = f | Z & ( for i being Nat holds b₃ . (i + 1) = (b₃ . 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 :: TAYLOR_1:def 6
for i being Nat st i <= n - 1 holds
(diff (f,Z)) . i is_differentiable_on Z;

end;

:: deftheorem 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 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;

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 b₁ being Real_Sequence st
for n being Nat holds b₁ . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) & ( for n being Nat holds b₂ . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) holds
b₁ = b₂

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
for b₅ being Real_Sequence holds
( b₅ = Taylor (f,Z,a,b) iff for n being Nat holds b₅ . 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 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 st Z c= dom f holds
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) | [.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 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 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 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 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 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 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 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 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 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 Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

proof end;

:: Taylor's Theorem

theorem :: TAYLOR_1:33

for n being 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;