|
1 (* Title: HOL/Taylor.thy |
|
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: |
|
17 assumes INIT: "n>0" "diff 0 = f" |
|
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 < b-c" by arith |
|
25 moreover |
|
26 from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto |
|
27 moreover |
|
28 have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" |
|
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 |
|
34 from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) |
|
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" |
|
53 by fastsimp |
|
54 thus ?thesis by fastsimp |
|
55 qed |
|
56 qed |
|
57 |
|
58 lemma taylor_down: |
|
59 assumes INIT: "n>0" "diff 0 = f" |
|
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 "a-c < 0" by arith |
|
67 moreover |
|
68 from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto |
|
69 moreover |
|
70 have "ALL m t. m < n & a-c <= 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 & a-c <= t & t <= 0" |
|
74 with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto |
|
75 moreover |
|
76 from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) |
|
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" |
|
93 by fastsimp |
|
94 thus ?thesis by fastsimp |
|
95 qed |
|
96 qed |
|
97 |
|
98 lemma taylor: |
|
99 assumes INIT: "n>0" "diff 0 = f" |
|
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" |
|
110 by fastsimp |
|
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" |
|
123 by fastsimp |
|
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 |