haftmann@28952

1 
(* Title: HOL/Taylor.thy

berghofe@17634

2 
Author: Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen

berghofe@17634

3 
*)

berghofe@17634

4 

wenzelm@60758

5 
section \<open>Taylor series\<close>

berghofe@17634

6 

berghofe@17634

7 
theory Taylor

berghofe@17634

8 
imports MacLaurin

berghofe@17634

9 
begin

berghofe@17634

10 

wenzelm@60758

11 
text \<open>

wenzelm@61799

12 
We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>

berghofe@17634

13 
to prove Taylor's theorem.

wenzelm@60758

14 
\<close>

berghofe@17634

15 

berghofe@17634

16 
lemma taylor_up:

nipkow@25162

17 
assumes INIT: "n>0" "diff 0 = f"

berghofe@17634

18 
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"

berghofe@17634

19 
and INTERV: "a \<le> c" "c < b"

lp15@59730

20 
shows "\<exists>t::real. c < t & t < b &

lp15@59730

21 
f b = (\<Sum>m<n. (diff m c / (fact m)) * (b  c)^m) + (diff n t / (fact n)) * (b  c)^n"

berghofe@17634

22 
proof 

berghofe@17634

23 
from INTERV have "0 < bc" by arith

berghofe@17634

24 
moreover

nipkow@25162

25 
from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto

berghofe@17634

26 
moreover

nipkow@25162

27 
have "ALL m t. m < n & 0 <= t & t <= b  c > DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"

berghofe@17634

28 
proof (intro strip)

berghofe@17634

29 
fix m t

berghofe@17634

30 
assume "m < n & 0 <= t & t <= b  c"

berghofe@17634

31 
with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto

berghofe@17634

32 
moreover

huffman@23069

33 
from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)

berghofe@17634

34 
ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"

berghofe@17634

35 
by (rule DERIV_chain2)

berghofe@17634

36 
thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp

berghofe@17634

37 
qed

lp15@59730

38 
ultimately obtain x where

lp15@59730

39 
"0 < x & x < b  c &

lp15@59730

40 
f (b  c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (b  c) ^ m) +

lp15@59730

41 
diff n (x + c) / (fact n) * (b  c) ^ n"

lp15@59730

42 
by (rule Maclaurin [THEN exE])

lp15@59730

43 
then have "c<x+c & x+c<b \<and> f b = (\<Sum>m<n. diff m c / (fact m) * (b  c) ^ m) +

lp15@59730

44 
diff n (x+c) / (fact n) * (b  c) ^ n"

lp15@59730

45 
by fastforce

lp15@59730

46 
thus ?thesis by fastforce

berghofe@17634

47 
qed

berghofe@17634

48 

berghofe@17634

49 
lemma taylor_down:

lp15@59730

50 
fixes a::real

nipkow@25162

51 
assumes INIT: "n>0" "diff 0 = f"

berghofe@17634

52 
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"

berghofe@17634

53 
and INTERV: "a < c" "c \<le> b"

berghofe@17634

54 
shows "\<exists> t. a < t & t < c &

lp15@59730

55 
f a = (\<Sum>m<n. (diff m c / (fact m)) * (a  c)^m) + (diff n t / (fact n)) * (a  c)^n"

berghofe@17634

56 
proof 

berghofe@17634

57 
from INTERV have "ac < 0" by arith

berghofe@17634

58 
moreover

nipkow@25162

59 
from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto

berghofe@17634

60 
moreover

berghofe@17634

61 
have "ALL m t. m < n & ac <= t & t <= 0 > DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"

berghofe@17634

62 
proof (rule allI impI)+

berghofe@17634

63 
fix m t

berghofe@17634

64 
assume "m < n & ac <= t & t <= 0"

berghofe@17634

65 
with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto

berghofe@17634

66 
moreover

huffman@23069

67 
from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)

berghofe@17634

68 
ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)

berghofe@17634

69 
thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp

berghofe@17634

70 
qed

lp15@59730

71 
ultimately obtain x where

lp15@59730

72 
"a  c < x & x < 0 &

wenzelm@61954

73 
f (a  c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (a  c) ^ m) +

lp15@59730

74 
diff n (x + c) / (fact n) * (a  c) ^ n"

lp15@59730

75 
by (rule Maclaurin_minus [THEN exE])

lp15@59730

76 
then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a  c) ^ m) +

lp15@59730

77 
diff n (x+c) / (fact n) * (a  c) ^ n"

lp15@59730

78 
by fastforce

lp15@59730

79 
thus ?thesis by fastforce

berghofe@17634

80 
qed

berghofe@17634

81 

berghofe@17634

82 
lemma taylor:

lp15@59730

83 
fixes a::real

nipkow@25162

84 
assumes INIT: "n>0" "diff 0 = f"

berghofe@17634

85 
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"

berghofe@17634

86 
and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"

berghofe@17634

87 
shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &

lp15@59730

88 
f x = (\<Sum>m<n. (diff m c / (fact m)) * (x  c)^m) + (diff n t / (fact n)) * (x  c)^n"

berghofe@17634

89 
proof (cases "x<c")

berghofe@17634

90 
case True

berghofe@17634

91 
note INIT

berghofe@17634

92 
moreover from DERIV and INTERV

berghofe@17634

93 
have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"

nipkow@44890

94 
by fastforce

berghofe@17634

95 
moreover note True

berghofe@17634

96 
moreover from INTERV have "c \<le> b" by simp

lp15@59730

97 
ultimately have "\<exists>t>x. t < c \<and> f x =

lp15@59730

98 
(\<Sum>m<n. diff m c / (fact m) * (x  c) ^ m) + diff n t / (fact n) * (x  c) ^ n"

berghofe@17634

99 
by (rule taylor_down)

berghofe@17634

100 
with True show ?thesis by simp

berghofe@17634

101 
next

berghofe@17634

102 
case False

berghofe@17634

103 
note INIT

berghofe@17634

104 
moreover from DERIV and INTERV

berghofe@17634

105 
have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"

nipkow@44890

106 
by fastforce

berghofe@17634

107 
moreover from INTERV have "a \<le> c" by arith

berghofe@17634

108 
moreover from False and INTERV have "c < x" by arith

lp15@59730

109 
ultimately have "\<exists>t>c. t < x \<and> f x =

lp15@59730

110 
(\<Sum>m<n. diff m c / (fact m) * (x  c) ^ m) + diff n t / (fact n) * (x  c) ^ n"

berghofe@17634

111 
by (rule taylor_up)

berghofe@17634

112 
with False show ?thesis by simp

berghofe@17634

113 
qed

berghofe@17634

114 

berghofe@17634

115 
end
