summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Taylor.thy

changeset 28952 | 15a4b2cf8c34 |

parent 25162 | ad4d5365d9d8 |

child 44890 | 22f665a2e91c |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/Taylor.thy Wed Dec 03 15:58:44 2008 +0100 1.3 @@ -0,0 +1,133 @@ 1.4 +(* Title: HOL/Taylor.thy 1.5 + Author: Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen 1.6 +*) 1.7 + 1.8 +header {* Taylor series *} 1.9 + 1.10 +theory Taylor 1.11 +imports MacLaurin 1.12 +begin 1.13 + 1.14 +text {* 1.15 +We use MacLaurin and the translation of the expansion point @{text c} to @{text 0} 1.16 +to prove Taylor's theorem. 1.17 +*} 1.18 + 1.19 +lemma taylor_up: 1.20 + assumes INIT: "n>0" "diff 0 = f" 1.21 + and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))" 1.22 + and INTERV: "a \<le> c" "c < b" 1.23 + shows "\<exists> t. c < t & t < b & 1.24 + f b = setsum (%m. (diff m c / real (fact m)) * (b - c)^m) {0..<n} + 1.25 + (diff n t / real (fact n)) * (b - c)^n" 1.26 +proof - 1.27 + from INTERV have "0 < b-c" by arith 1.28 + moreover 1.29 + from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto 1.30 + moreover 1.31 + have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" 1.32 + proof (intro strip) 1.33 + fix m t 1.34 + assume "m < n & 0 <= t & t <= b - c" 1.35 + with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto 1.36 + moreover 1.37 + from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) 1.38 + ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" 1.39 + by (rule DERIV_chain2) 1.40 + thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp 1.41 + qed 1.42 + ultimately 1.43 + have EX:"EX t>0. t < b - c & 1.44 + f (b - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) + 1.45 + diff n (t + c) / real (fact n) * (b - c) ^ n" 1.46 + by (rule Maclaurin) 1.47 + show ?thesis 1.48 + proof - 1.49 + from EX obtain x where 1.50 + X: "0 < x & x < b - c & 1.51 + f (b - c + c) = (\<Sum>m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) + 1.52 + diff n (x + c) / real (fact n) * (b - c) ^ n" .. 1.53 + let ?H = "x + c" 1.54 + from X have "c<?H & ?H<b \<and> f b = (\<Sum>m = 0..<n. diff m c / real (fact m) * (b - c) ^ m) + 1.55 + diff n ?H / real (fact n) * (b - c) ^ n" 1.56 + by fastsimp 1.57 + thus ?thesis by fastsimp 1.58 + qed 1.59 +qed 1.60 + 1.61 +lemma taylor_down: 1.62 + assumes INIT: "n>0" "diff 0 = f" 1.63 + and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))" 1.64 + and INTERV: "a < c" "c \<le> b" 1.65 + shows "\<exists> t. a < t & t < c & 1.66 + f a = setsum (% m. (diff m c / real (fact m)) * (a - c)^m) {0..<n} + 1.67 + (diff n t / real (fact n)) * (a - c)^n" 1.68 +proof - 1.69 + from INTERV have "a-c < 0" by arith 1.70 + moreover 1.71 + from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto 1.72 + moreover 1.73 + have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" 1.74 + proof (rule allI impI)+ 1.75 + fix m t 1.76 + assume "m < n & a-c <= t & t <= 0" 1.77 + with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto 1.78 + moreover 1.79 + from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) 1.80 + ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2) 1.81 + thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp 1.82 + qed 1.83 + ultimately 1.84 + have EX: "EX t>a - c. t < 0 & 1.85 + f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) + 1.86 + diff n (t + c) / real (fact n) * (a - c) ^ n" 1.87 + by (rule Maclaurin_minus) 1.88 + show ?thesis 1.89 + proof - 1.90 + from EX obtain x where X: "a - c < x & x < 0 & 1.91 + f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) + 1.92 + diff n (x + c) / real (fact n) * (a - c) ^ n" .. 1.93 + let ?H = "x + c" 1.94 + from X have "a<?H & ?H<c \<and> f a = (\<Sum>m = 0..<n. diff m c / real (fact m) * (a - c) ^ m) + 1.95 + diff n ?H / real (fact n) * (a - c) ^ n" 1.96 + by fastsimp 1.97 + thus ?thesis by fastsimp 1.98 + qed 1.99 +qed 1.100 + 1.101 +lemma taylor: 1.102 + assumes INIT: "n>0" "diff 0 = f" 1.103 + and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))" 1.104 + and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 1.105 + shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) & 1.106 + f x = setsum (% m. (diff m c / real (fact m)) * (x - c)^m) {0..<n} + 1.107 + (diff n t / real (fact n)) * (x - c)^n" 1.108 +proof (cases "x<c") 1.109 + case True 1.110 + note INIT 1.111 + moreover from DERIV and INTERV 1.112 + have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 1.113 + by fastsimp 1.114 + moreover note True 1.115 + moreover from INTERV have "c \<le> b" by simp 1.116 + ultimately have EX: "\<exists>t>x. t < c \<and> f x = 1.117 + (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) + 1.118 + diff n t / real (fact n) * (x - c) ^ n" 1.119 + by (rule taylor_down) 1.120 + with True show ?thesis by simp 1.121 +next 1.122 + case False 1.123 + note INIT 1.124 + moreover from DERIV and INTERV 1.125 + have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 1.126 + by fastsimp 1.127 + moreover from INTERV have "a \<le> c" by arith 1.128 + moreover from False and INTERV have "c < x" by arith 1.129 + ultimately have EX: "\<exists>t>c. t < x \<and> f x = 1.130 + (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) + 1.131 + diff n t / real (fact n) * (x - c) ^ n" 1.132 + by (rule taylor_up) 1.133 + with False show ?thesis by simp 1.134 +qed 1.135 + 1.136 +end