author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44890  22f665a2e91c 
child 56193  c726ecfb22b6 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
25162
diff
changeset

1 
(* Title: HOL/Taylor.thy 
17634  2 
Author: Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen 
3 
*) 

4 

5 
header {* Taylor series *} 

6 

7 
theory Taylor 

8 
imports MacLaurin 

9 
begin 

10 

11 
text {* 

12 
We use MacLaurin and the translation of the expansion point @{text c} to @{text 0} 

13 
to prove Taylor's theorem. 

14 
*} 

15 

16 
lemma taylor_up: 

25162  17 
assumes INIT: "n>0" "diff 0 = f" 
17634  18 
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))" 
19 
and INTERV: "a \<le> c" "c < b" 

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

21 
f b = setsum (%m. (diff m c / real (fact m)) * (b  c)^m) {0..<n} + 

22 
(diff n t / real (fact n)) * (b  c)^n" 

23 
proof  

24 
from INTERV have "0 < bc" by arith 

25 
moreover 

25162  26 
from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto 
17634  27 
moreover 
25162  28 
have "ALL m t. m < n & 0 <= t & t <= b  c > DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" 
17634  29 
proof (intro strip) 
30 
fix m t 

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

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

33 
moreover 

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
17634
diff
changeset

34 
from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) 
17634  35 
ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" 
36 
by (rule DERIV_chain2) 

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

38 
qed 

39 
ultimately 

40 
have EX:"EX t>0. t < b  c & 

41 
f (b  c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (b  c) ^ m) + 

42 
diff n (t + c) / real (fact n) * (b  c) ^ n" 

43 
by (rule Maclaurin) 

44 
show ?thesis 

45 
proof  

46 
from EX obtain x where 

47 
X: "0 < x & x < b  c & 

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

49 
diff n (x + c) / real (fact n) * (b  c) ^ n" .. 

50 
let ?H = "x + c" 

51 
from X have "c<?H & ?H<b \<and> f b = (\<Sum>m = 0..<n. diff m c / real (fact m) * (b  c) ^ m) + 

52 
diff n ?H / real (fact n) * (b  c) ^ n" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
28952
diff
changeset

53 
by fastforce 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
28952
diff
changeset

54 
thus ?thesis by fastforce 
17634  55 
qed 
56 
qed 

57 

58 
lemma taylor_down: 

25162  59 
assumes INIT: "n>0" "diff 0 = f" 
17634  60 
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))" 
61 
and INTERV: "a < c" "c \<le> b" 

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

63 
f a = setsum (% m. (diff m c / real (fact m)) * (a  c)^m) {0..<n} + 

64 
(diff n t / real (fact n)) * (a  c)^n" 

65 
proof  

66 
from INTERV have "ac < 0" by arith 

67 
moreover 

25162  68 
from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto 
17634  69 
moreover 
70 
have "ALL m t. m < n & ac <= t & t <= 0 > DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" 

71 
proof (rule allI impI)+ 

72 
fix m t 

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

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

75 
moreover 

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
17634
diff
changeset

76 
from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) 
17634  77 
ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2) 
78 
thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp 

79 
qed 

80 
ultimately 

81 
have EX: "EX t>a  c. t < 0 & 

82 
f (a  c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a  c) ^ m) + 

83 
diff n (t + c) / real (fact n) * (a  c) ^ n" 

84 
by (rule Maclaurin_minus) 

85 
show ?thesis 

86 
proof  

87 
from EX obtain x where X: "a  c < x & x < 0 & 

88 
f (a  c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a  c) ^ m) + 

89 
diff n (x + c) / real (fact n) * (a  c) ^ n" .. 

90 
let ?H = "x + c" 

91 
from X have "a<?H & ?H<c \<and> f a = (\<Sum>m = 0..<n. diff m c / real (fact m) * (a  c) ^ m) + 

92 
diff n ?H / real (fact n) * (a  c) ^ n" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
28952
diff
changeset

93 
by fastforce 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
28952
diff
changeset

94 
thus ?thesis by fastforce 
17634  95 
qed 
96 
qed 

97 

98 
lemma taylor: 

25162  99 
assumes INIT: "n>0" "diff 0 = f" 
17634  100 
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))" 
101 
and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 

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

103 
f x = setsum (% m. (diff m c / real (fact m)) * (x  c)^m) {0..<n} + 

104 
(diff n t / real (fact n)) * (x  c)^n" 

105 
proof (cases "x<c") 

106 
case True 

107 
note INIT 

108 
moreover from DERIV and INTERV 

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

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
28952
diff
changeset

110 
by fastforce 
17634  111 
moreover note True 
112 
moreover from INTERV have "c \<le> b" by simp 

113 
ultimately have EX: "\<exists>t>x. t < c \<and> f x = 

114 
(\<Sum>m = 0..<n. diff m c / real (fact m) * (x  c) ^ m) + 

115 
diff n t / real (fact n) * (x  c) ^ n" 

116 
by (rule taylor_down) 

117 
with True show ?thesis by simp 

118 
next 

119 
case False 

120 
note INIT 

121 
moreover from DERIV and INTERV 

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

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
28952
diff
changeset

123 
by fastforce 
17634  124 
moreover from INTERV have "a \<le> c" by arith 
125 
moreover from False and INTERV have "c < x" by arith 

126 
ultimately have EX: "\<exists>t>c. t < x \<and> f x = 

127 
(\<Sum>m = 0..<n. diff m c / real (fact m) * (x  c) ^ m) + 

128 
diff n t / real (fact n) * (x  c) ^ n" 

129 
by (rule taylor_up) 

130 
with False show ?thesis by simp 

131 
qed 

132 

133 
end 