1 (* Title : MacLaurin.thy |
1 (* Title : MacLaurin.thy |
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 2001 University of Edinburgh |
3 Copyright : 2001 University of Edinburgh |
4 Description : MacLaurin series |
4 Description : MacLaurin series |
|
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 *) |
6 *) |
6 |
7 |
7 theory MacLaurin = Log |
8 theory MacLaurin = Log: |
8 files ("MacLaurin_lemmas.ML"): |
9 |
9 |
10 lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" |
10 use "MacLaurin_lemmas.ML" |
11 by (induct_tac "n", auto) |
11 |
12 |
12 lemma Maclaurin_sin_bound: |
13 lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" |
13 "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
14 by (induct_tac "n", auto) |
14 x ^ m)) <= inverse(real (fact n)) * abs(x) ^ n" |
15 |
|
16 lemma sumr_offset3: "sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f" |
|
17 by (simp add: sumr_offset) |
|
18 |
|
19 lemma sumr_offset4: "\<forall>n f. sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f" |
|
20 by (simp add: sumr_offset) |
|
21 |
|
22 lemma sumr_from_1_from_0: "0 < n ==> |
|
23 sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else |
|
24 ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = |
|
25 sumr 0 (Suc n) (%n. (if even(n) then 0 else |
|
26 ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)" |
|
27 by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto) |
|
28 |
|
29 |
|
30 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*} |
|
31 |
|
32 text{*This is a very long, messy proof even now that it's been broken down |
|
33 into lemmas.*} |
|
34 |
|
35 lemma Maclaurin_lemma: |
|
36 "0 < h ==> |
|
37 \<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) + |
|
38 (B * ((h^n) / real(fact n)))" |
|
39 by (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) * |
|
40 real(fact n) / (h^n)" |
|
41 in exI, auto) |
|
42 |
|
43 |
|
44 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))" |
|
45 by arith |
|
46 |
|
47 text{*A crude tactic to differentiate by proof.*} |
|
48 ML |
|
49 {* |
|
50 exception DERIV_name; |
|
51 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f |
|
52 | get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f |
|
53 | get_fun_name _ = raise DERIV_name; |
|
54 |
|
55 val deriv_rulesI = [DERIV_Id,DERIV_const,DERIV_cos,DERIV_cmult, |
|
56 DERIV_sin, DERIV_exp, DERIV_inverse,DERIV_pow, |
|
57 DERIV_add, DERIV_diff, DERIV_mult, DERIV_minus, |
|
58 DERIV_inverse_fun,DERIV_quotient,DERIV_fun_pow, |
|
59 DERIV_fun_exp,DERIV_fun_sin,DERIV_fun_cos, |
|
60 DERIV_Id,DERIV_const,DERIV_cos]; |
|
61 |
|
62 val deriv_tac = |
|
63 SUBGOAL (fn (prem,i) => |
|
64 (resolve_tac deriv_rulesI i) ORELSE |
|
65 ((rtac (read_instantiate [("f",get_fun_name prem)] |
|
66 DERIV_chain2) i) handle DERIV_name => no_tac));; |
|
67 |
|
68 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i)); |
|
69 *} |
|
70 |
|
71 lemma Maclaurin_lemma2: |
|
72 "[| \<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t; |
|
73 n = Suc k; |
|
74 difg = |
|
75 (\<lambda>m t. diff m t - |
|
76 ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) + |
|
77 B * (t ^ (n - m) / real (fact (n - m)))))|] ==> |
|
78 \<forall>m t. m < n & 0 \<le> t & t \<le> h --> |
|
79 DERIV (difg m) t :> difg (Suc m) t" |
|
80 apply clarify |
|
81 apply (rule DERIV_diff) |
|
82 apply (simp (no_asm_simp)) |
|
83 apply (tactic DERIV_tac) |
|
84 apply (tactic DERIV_tac) |
|
85 apply (rule_tac [2] lemma_DERIV_subst) |
|
86 apply (rule_tac [2] DERIV_quotient) |
|
87 apply (rule_tac [3] DERIV_const) |
|
88 apply (rule_tac [2] DERIV_pow) |
|
89 prefer 3 apply (simp add: fact_diff_Suc) |
|
90 prefer 2 apply simp |
|
91 apply (frule_tac m = m in less_add_one, clarify) |
|
92 apply (simp del: sumr_Suc) |
|
93 apply (insert sumr_offset4 [of 1]) |
|
94 apply (simp del: sumr_Suc fact_Suc realpow_Suc) |
|
95 apply (rule lemma_DERIV_subst) |
|
96 apply (rule DERIV_add) |
|
97 apply (rule_tac [2] DERIV_const) |
|
98 apply (rule DERIV_sumr, clarify) |
|
99 prefer 2 apply simp |
|
100 apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc) |
|
101 apply (rule DERIV_cmult) |
|
102 apply (rule lemma_DERIV_subst) |
|
103 apply (best intro: DERIV_chain2 intro!: DERIV_intros) |
|
104 apply (subst fact_Suc) |
|
105 apply (subst real_of_nat_mult) |
|
106 apply (simp add: inverse_mult_distrib mult_ac) |
|
107 done |
|
108 |
|
109 |
|
110 lemma Maclaurin_lemma3: |
|
111 "[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t; |
|
112 \<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0; n < m; 0 < t; |
|
113 t < h|] |
|
114 ==> \<exists>ta. 0 < ta & ta < t & DERIV (difg (Suc n)) ta :> 0" |
|
115 apply (rule Rolle, assumption, simp) |
|
116 apply (drule_tac x = n and P="%k. k<Suc m --> difg k 0 = 0" in spec) |
|
117 apply (rule DERIV_unique) |
|
118 prefer 2 apply assumption |
|
119 apply force |
|
120 apply (subgoal_tac "\<forall>ta. 0 \<le> ta & ta \<le> t --> (difg (Suc n)) differentiable ta") |
|
121 apply (simp add: differentiable_def) |
|
122 apply (blast dest!: DERIV_isCont) |
|
123 apply (simp add: differentiable_def, clarify) |
|
124 apply (rule_tac x = "difg (Suc (Suc n)) ta" in exI) |
|
125 apply force |
|
126 apply (simp add: differentiable_def, clarify) |
|
127 apply (rule_tac x = "difg (Suc (Suc n)) x" in exI) |
|
128 apply force |
|
129 done |
|
130 |
|
131 lemma Maclaurin: |
|
132 "[| 0 < h; 0 < n; diff 0 = f; |
|
133 \<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |] |
|
134 ==> \<exists>t. 0 < t & |
|
135 t < h & |
|
136 f h = |
|
137 sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + |
|
138 (diff n t / real (fact n)) * h ^ n" |
|
139 apply (case_tac "n = 0", force) |
|
140 apply (drule not0_implies_Suc) |
|
141 apply (erule exE) |
|
142 apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma) |
|
143 apply (erule exE) |
|
144 apply (subgoal_tac "\<exists>g. |
|
145 g = (%t. f t - (sumr 0 n (%m. (diff m 0 / real(fact m)) * t^m) + (B * (t^n / real(fact n)))))") |
|
146 prefer 2 apply blast |
|
147 apply (erule exE) |
|
148 apply (subgoal_tac "g 0 = 0 & g h =0") |
|
149 prefer 2 |
|
150 apply (simp del: sumr_Suc) |
|
151 apply (cut_tac n = m and k = 1 in sumr_offset2) |
|
152 apply (simp add: eq_diff_eq' del: sumr_Suc) |
|
153 apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) + (B * ((t ^ (n - m)) / real (fact (n - m))))))") |
|
154 prefer 2 apply blast |
|
155 apply (erule exE) |
|
156 apply (subgoal_tac "difg 0 = g") |
|
157 prefer 2 apply simp |
|
158 apply (frule Maclaurin_lemma2, assumption+) |
|
159 apply (subgoal_tac "\<forall>ma. ma < n --> (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ") |
|
160 apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec) |
|
161 apply (erule impE) |
|
162 apply (simp (no_asm_simp)) |
|
163 apply (erule exE) |
|
164 apply (rule_tac x = t in exI) |
|
165 apply (simp del: realpow_Suc fact_Suc) |
|
166 apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0") |
|
167 prefer 2 |
|
168 apply clarify |
|
169 apply simp |
|
170 apply (frule_tac m = ma in less_add_one, clarify) |
|
171 apply (simp del: sumr_Suc) |
|
172 apply (insert sumr_offset4 [of 1]) |
|
173 apply (simp del: sumr_Suc fact_Suc realpow_Suc) |
|
174 apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ") |
|
175 apply (rule allI, rule impI) |
|
176 apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec) |
|
177 apply (erule impE, assumption) |
|
178 apply (erule exE) |
|
179 apply (rule_tac x = t in exI) |
|
180 (* do some tidying up *) |
|
181 apply (erule_tac [!] V= "difg = (%m t. diff m t - (sumr 0 (n - m) (%p. diff (m + p) 0 / real (fact p) * t ^ p) + B * (t ^ (n - m) / real (fact (n - m)))))" |
|
182 in thin_rl) |
|
183 apply (erule_tac [!] V="g = (%t. f t - (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + B * (t ^ n / real (fact n))))" |
|
184 in thin_rl) |
|
185 apply (erule_tac [!] V="f h = sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + B * (h ^ n / real (fact n))" |
|
186 in thin_rl) |
|
187 (* back to business *) |
|
188 apply (simp (no_asm_simp)) |
|
189 apply (rule DERIV_unique) |
|
190 prefer 2 apply blast |
|
191 apply force |
|
192 apply (rule allI, induct_tac "ma") |
|
193 apply (rule impI, rule Rolle, assumption, simp, simp) |
|
194 apply (subgoal_tac "\<forall>t. 0 \<le> t & t \<le> h --> g differentiable t") |
|
195 apply (simp add: differentiable_def) |
|
196 apply (blast dest: DERIV_isCont) |
|
197 apply (simp add: differentiable_def, clarify) |
|
198 apply (rule_tac x = "difg (Suc 0) t" in exI) |
|
199 apply force |
|
200 apply (simp add: differentiable_def, clarify) |
|
201 apply (rule_tac x = "difg (Suc 0) x" in exI) |
|
202 apply force |
|
203 apply safe |
|
204 apply force |
|
205 apply (frule Maclaurin_lemma3, assumption+, safe) |
|
206 apply (rule_tac x = ta in exI, force) |
|
207 done |
|
208 |
|
209 lemma Maclaurin_objl: |
|
210 "0 < h & 0 < n & diff 0 = f & |
|
211 (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t) |
|
212 --> (\<exists>t. 0 < t & |
|
213 t < h & |
|
214 f h = |
|
215 sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + |
|
216 diff n t / real (fact n) * h ^ n)" |
|
217 by (blast intro: Maclaurin) |
|
218 |
|
219 |
|
220 lemma Maclaurin2: |
|
221 "[| 0 < h; diff 0 = f; |
|
222 \<forall>m t. |
|
223 m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |] |
|
224 ==> \<exists>t. 0 < t & |
|
225 t \<le> h & |
|
226 f h = |
|
227 sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + |
|
228 diff n t / real (fact n) * h ^ n" |
|
229 apply (case_tac "n", auto) |
|
230 apply (drule Maclaurin, auto) |
|
231 done |
|
232 |
|
233 lemma Maclaurin2_objl: |
|
234 "0 < h & diff 0 = f & |
|
235 (\<forall>m t. |
|
236 m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t) |
|
237 --> (\<exists>t. 0 < t & |
|
238 t \<le> h & |
|
239 f h = |
|
240 sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + |
|
241 diff n t / real (fact n) * h ^ n)" |
|
242 by (blast intro: Maclaurin2) |
|
243 |
|
244 lemma Maclaurin_minus: |
|
245 "[| h < 0; 0 < n; diff 0 = f; |
|
246 \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |] |
|
247 ==> \<exists>t. h < t & |
|
248 t < 0 & |
|
249 f h = |
|
250 sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + |
|
251 diff n t / real (fact n) * h ^ n" |
|
252 apply (cut_tac f = "%x. f (-x)" |
|
253 and diff = "%n x. ((- 1) ^ n) * diff n (-x)" |
|
254 and h = "-h" and n = n in Maclaurin_objl) |
|
255 apply simp |
|
256 apply safe |
|
257 apply (subst minus_mult_right) |
|
258 apply (rule DERIV_cmult) |
|
259 apply (rule lemma_DERIV_subst) |
|
260 apply (rule DERIV_chain2 [where g=uminus]) |
|
261 apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_Id) |
|
262 prefer 2 apply force |
|
263 apply force |
|
264 apply (rule_tac x = "-t" in exI, auto) |
|
265 apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) = |
|
266 (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))") |
|
267 apply (rule_tac [2] sumr_fun_eq) |
|
268 apply (auto simp add: divide_inverse power_mult_distrib [symmetric]) |
|
269 done |
|
270 |
|
271 lemma Maclaurin_minus_objl: |
|
272 "(h < 0 & 0 < n & diff 0 = f & |
|
273 (\<forall>m t. |
|
274 m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t)) |
|
275 --> (\<exists>t. h < t & |
|
276 t < 0 & |
|
277 f h = |
|
278 sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + |
|
279 diff n t / real (fact n) * h ^ n)" |
|
280 by (blast intro: Maclaurin_minus) |
|
281 |
|
282 |
|
283 subsection{*More Convenient "Bidirectional" Version.*} |
|
284 |
|
285 (* not good for PVS sin_approx, cos_approx *) |
|
286 |
|
287 lemma Maclaurin_bi_le_lemma [rule_format]: |
|
288 "0 < n \<longrightarrow> |
|
289 diff 0 0 = |
|
290 (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) + |
|
291 diff n 0 * 0 ^ n / real (fact n)" |
|
292 by (induct_tac "n", auto) |
|
293 |
|
294 lemma Maclaurin_bi_le: |
|
295 "[| diff 0 = f; |
|
296 \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |] |
|
297 ==> \<exists>t. abs t \<le> abs x & |
|
298 f x = |
|
299 sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + |
|
300 diff n t / real (fact n) * x ^ n" |
|
301 apply (case_tac "n = 0", force) |
|
302 apply (case_tac "x = 0") |
|
303 apply (rule_tac x = 0 in exI) |
|
304 apply (force simp add: Maclaurin_bi_le_lemma) |
|
305 apply (cut_tac x = x and y = 0 in linorder_less_linear, auto) |
|
306 txt{*Case 1, where @{term "x < 0"}*} |
|
307 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe) |
|
308 apply (simp add: abs_if) |
|
309 apply (rule_tac x = t in exI) |
|
310 apply (simp add: abs_if) |
|
311 txt{*Case 2, where @{term "0 < x"}*} |
|
312 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe) |
|
313 apply (simp add: abs_if) |
|
314 apply (rule_tac x = t in exI) |
|
315 apply (simp add: abs_if) |
|
316 done |
|
317 |
|
318 lemma Maclaurin_all_lt: |
|
319 "[| diff 0 = f; |
|
320 \<forall>m x. DERIV (diff m) x :> diff(Suc m) x; |
|
321 x ~= 0; 0 < n |
|
322 |] ==> \<exists>t. 0 < abs t & abs t < abs x & |
|
323 f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + |
|
324 (diff n t / real (fact n)) * x ^ n" |
|
325 apply (rule_tac x = x and y = 0 in linorder_cases) |
|
326 prefer 2 apply blast |
|
327 apply (drule_tac [2] diff=diff in Maclaurin) |
|
328 apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe) |
|
329 apply (rule_tac [!] x = t in exI, auto, arith+) |
|
330 done |
|
331 |
|
332 lemma Maclaurin_all_lt_objl: |
|
333 "diff 0 = f & |
|
334 (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) & |
|
335 x ~= 0 & 0 < n |
|
336 --> (\<exists>t. 0 < abs t & abs t < abs x & |
|
337 f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + |
|
338 (diff n t / real (fact n)) * x ^ n)" |
|
339 by (blast intro: Maclaurin_all_lt) |
|
340 |
|
341 lemma Maclaurin_zero [rule_format]: |
|
342 "x = (0::real) |
|
343 ==> 0 < n --> |
|
344 sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = |
|
345 diff 0 0" |
|
346 by (induct n, auto) |
|
347 |
|
348 lemma Maclaurin_all_le: "[| diff 0 = f; |
|
349 \<forall>m x. DERIV (diff m) x :> diff (Suc m) x |
|
350 |] ==> \<exists>t. abs t \<le> abs x & |
|
351 f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + |
|
352 (diff n t / real (fact n)) * x ^ n" |
|
353 apply (insert linorder_le_less_linear [of n 0]) |
|
354 apply (erule disjE, force) |
|
355 apply (case_tac "x = 0") |
|
356 apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption) |
|
357 apply (drule gr_implies_not0 [THEN not0_implies_Suc]) |
|
358 apply (rule_tac x = 0 in exI, force) |
|
359 apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto) |
|
360 apply (rule_tac x = t in exI, auto) |
|
361 done |
|
362 |
|
363 lemma Maclaurin_all_le_objl: "diff 0 = f & |
|
364 (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) |
|
365 --> (\<exists>t. abs t \<le> abs x & |
|
366 f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + |
|
367 (diff n t / real (fact n)) * x ^ n)" |
|
368 by (blast intro: Maclaurin_all_le) |
|
369 |
|
370 |
|
371 subsection{*Version for Exponential Function*} |
|
372 |
|
373 lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |] |
|
374 ==> (\<exists>t. 0 < abs t & |
|
375 abs t < abs x & |
|
376 exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + |
|
377 (exp t / real (fact n)) * x ^ n)" |
|
378 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto) |
|
379 |
|
380 |
|
381 lemma Maclaurin_exp_le: |
|
382 "\<exists>t. abs t \<le> abs x & |
|
383 exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + |
|
384 (exp t / real (fact n)) * x ^ n" |
|
385 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto) |
|
386 |
|
387 |
|
388 subsection{*Version for Sine Function*} |
|
389 |
|
390 lemma MVT2: |
|
391 "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |] |
|
392 ==> \<exists>z. a < z & z < b & (f b - f a = (b - a) * f'(z))" |
|
393 apply (drule MVT) |
|
394 apply (blast intro: DERIV_isCont) |
|
395 apply (force dest: order_less_imp_le simp add: differentiable_def) |
|
396 apply (blast dest: DERIV_unique order_less_imp_le) |
|
397 done |
|
398 |
|
399 lemma mod_exhaust_less_4: |
|
400 "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)" |
|
401 by (case_tac "m mod 4", auto, arith) |
|
402 |
|
403 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: |
|
404 "0 < n --> Suc (Suc (2 * n - 2)) = 2*n" |
|
405 by (induct_tac "n", auto) |
|
406 |
|
407 lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: |
|
408 "0 < n --> Suc (Suc (4*n - 2)) = 4*n" |
|
409 by (induct_tac "n", auto) |
|
410 |
|
411 lemma Suc_mult_two_diff_one [rule_format, simp]: |
|
412 "0 < n --> Suc (2 * n - 1) = 2*n" |
|
413 by (induct_tac "n", auto) |
|
414 |
|
415 lemma Maclaurin_sin_expansion: |
|
416 "\<exists>t. sin x = |
|
417 (sumr 0 n (%m. (if even m then 0 |
|
418 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
|
419 x ^ m)) |
|
420 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
|
421 apply (cut_tac f = sin and n = n and x = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl) |
|
422 apply safe |
|
423 apply (simp (no_asm)) |
|
424 apply (simp (no_asm)) |
|
425 apply (case_tac "n", clarify, simp) |
|
426 apply (drule_tac x = 0 in spec, simp, simp) |
|
427 apply (rule ccontr, simp) |
|
428 apply (drule_tac x = x in spec, simp) |
|
429 apply (erule ssubst) |
|
430 apply (rule_tac x = t in exI, simp) |
|
431 apply (rule sumr_fun_eq) |
|
432 apply (auto simp add: odd_Suc_mult_two_ex) |
|
433 apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc) |
|
434 (*Could sin_zero_iff help?*) |
|
435 done |
|
436 |
|
437 lemma Maclaurin_sin_expansion2: |
|
438 "\<exists>t. abs t \<le> abs x & |
|
439 sin x = |
|
440 (sumr 0 n (%m. (if even m then 0 |
|
441 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
|
442 x ^ m)) |
|
443 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
|
444 apply (cut_tac f = sin and n = n and x = x |
|
445 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl) |
|
446 apply safe |
|
447 apply (simp (no_asm)) |
|
448 apply (simp (no_asm)) |
|
449 apply (case_tac "n", clarify, simp, simp) |
|
450 apply (rule ccontr, simp) |
|
451 apply (drule_tac x = x in spec, simp) |
|
452 apply (erule ssubst) |
|
453 apply (rule_tac x = t in exI, simp) |
|
454 apply (rule sumr_fun_eq) |
|
455 apply (auto simp add: odd_Suc_mult_two_ex) |
|
456 apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc) |
|
457 done |
|
458 |
|
459 lemma Maclaurin_sin_expansion3: |
|
460 "[| 0 < n; 0 < x |] ==> |
|
461 \<exists>t. 0 < t & t < x & |
|
462 sin x = |
|
463 (sumr 0 n (%m. (if even m then 0 |
|
464 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
|
465 x ^ m)) |
|
466 + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)" |
|
467 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl) |
|
468 apply safe |
|
469 apply simp |
|
470 apply (simp (no_asm)) |
|
471 apply (erule ssubst) |
|
472 apply (rule_tac x = t in exI, simp) |
|
473 apply (rule sumr_fun_eq) |
|
474 apply (auto simp add: odd_Suc_mult_two_ex) |
|
475 apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc) |
|
476 done |
|
477 |
|
478 lemma Maclaurin_sin_expansion4: |
|
479 "0 < x ==> |
|
480 \<exists>t. 0 < t & t \<le> x & |
|
481 sin x = |
|
482 (sumr 0 n (%m. (if even m then 0 |
|
483 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
|
484 x ^ m)) |
|
485 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
|
486 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl) |
|
487 apply safe |
|
488 apply simp |
|
489 apply (simp (no_asm)) |
|
490 apply (erule ssubst) |
|
491 apply (rule_tac x = t in exI, simp) |
|
492 apply (rule sumr_fun_eq) |
|
493 apply (auto simp add: odd_Suc_mult_two_ex) |
|
494 apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc) |
|
495 done |
|
496 |
|
497 |
|
498 subsection{*Maclaurin Expansion for Cosine Function*} |
|
499 |
|
500 lemma sumr_cos_zero_one [simp]: |
|
501 "sumr 0 (Suc n) |
|
502 (%m. (if even m |
|
503 then (- 1) ^ (m div 2)/(real (fact m)) |
|
504 else 0) * |
|
505 0 ^ m) = 1" |
|
506 by (induct_tac "n", auto) |
|
507 |
|
508 lemma Maclaurin_cos_expansion: |
|
509 "\<exists>t. abs t \<le> abs x & |
|
510 cos x = |
|
511 (sumr 0 n (%m. (if even m |
|
512 then (- 1) ^ (m div 2)/(real (fact m)) |
|
513 else 0) * |
|
514 x ^ m)) |
|
515 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
|
516 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl) |
|
517 apply safe |
|
518 apply (simp (no_asm)) |
|
519 apply (simp (no_asm)) |
|
520 apply (case_tac "n", simp) |
|
521 apply (simp del: sumr_Suc) |
|
522 apply (rule ccontr, simp) |
|
523 apply (drule_tac x = x in spec, simp) |
|
524 apply (erule ssubst) |
|
525 apply (rule_tac x = t in exI, simp) |
|
526 apply (rule sumr_fun_eq) |
|
527 apply (auto simp add: odd_Suc_mult_two_ex) |
|
528 apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc) |
|
529 apply (simp add: mult_commute [of _ pi]) |
|
530 done |
|
531 |
|
532 lemma Maclaurin_cos_expansion2: |
|
533 "[| 0 < x; 0 < n |] ==> |
|
534 \<exists>t. 0 < t & t < x & |
|
535 cos x = |
|
536 (sumr 0 n (%m. (if even m |
|
537 then (- 1) ^ (m div 2)/(real (fact m)) |
|
538 else 0) * |
|
539 x ^ m)) |
|
540 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
|
541 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl) |
|
542 apply safe |
|
543 apply simp |
|
544 apply (simp (no_asm)) |
|
545 apply (erule ssubst) |
|
546 apply (rule_tac x = t in exI, simp) |
|
547 apply (rule sumr_fun_eq) |
|
548 apply (auto simp add: odd_Suc_mult_two_ex) |
|
549 apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc) |
|
550 apply (simp add: mult_commute [of _ pi]) |
|
551 done |
|
552 |
|
553 lemma Maclaurin_minus_cos_expansion: "[| x < 0; 0 < n |] ==> |
|
554 \<exists>t. x < t & t < 0 & |
|
555 cos x = |
|
556 (sumr 0 n (%m. (if even m |
|
557 then (- 1) ^ (m div 2)/(real (fact m)) |
|
558 else 0) * |
|
559 x ^ m)) |
|
560 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
|
561 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl) |
|
562 apply safe |
|
563 apply simp |
|
564 apply (simp (no_asm)) |
|
565 apply (erule ssubst) |
|
566 apply (rule_tac x = t in exI, simp) |
|
567 apply (rule sumr_fun_eq) |
|
568 apply (auto simp add: odd_Suc_mult_two_ex) |
|
569 apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc) |
|
570 apply (simp add: mult_commute [of _ pi]) |
|
571 done |
|
572 |
|
573 (* ------------------------------------------------------------------------- *) |
|
574 (* Version for ln(1 +/- x). Where is it?? *) |
|
575 (* ------------------------------------------------------------------------- *) |
|
576 |
|
577 lemma sin_bound_lemma: |
|
578 "[|x = y; abs u \<le> (v::real) |] ==> abs ((x + u) - y) \<le> v" |
|
579 by auto |
|
580 |
|
581 lemma Maclaurin_sin_bound: |
|
582 "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
|
583 x ^ m)) \<le> inverse(real (fact n)) * abs(x) ^ n" |
15 proof - |
584 proof - |
16 have "!! x (y::real). x <= 1 \<Longrightarrow> 0 <= y \<Longrightarrow> x * y \<le> 1 * y" |
585 have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" |
17 by (rule_tac mult_right_mono,simp_all) |
586 by (rule_tac mult_right_mono,simp_all) |
18 note est = this[simplified] |
587 note est = this[simplified] |
19 show ?thesis |
588 show ?thesis |
20 apply (cut_tac f=sin and n=n and x=x and |
589 apply (cut_tac f=sin and n=n and x=x and |
21 diff = "%n x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then -sin(x) else -cos(x)" |
590 diff = "%n x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then -sin(x) else -cos(x)" |
22 in Maclaurin_all_le_objl) |
591 in Maclaurin_all_le_objl) |
23 apply (tactic{* (Step_tac 1) *}) |
592 apply safe |
24 apply (simp) |
593 apply simp |
25 apply (subst mod_Suc_eq_Suc_mod) |
594 apply (subst mod_Suc_eq_Suc_mod) |
26 apply (tactic{* cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1*}) |
595 apply (cut_tac m=m in mod_exhaust_less_4, safe, simp+) |
27 apply (tactic{* Step_tac 1 *}) |
|
28 apply (simp)+ |
|
29 apply (rule DERIV_minus, simp+) |
596 apply (rule DERIV_minus, simp+) |
30 apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp) |
597 apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp) |
31 apply (tactic{* dtac ssubst 1 THEN assume_tac 2 *}) |
598 apply (erule ssubst) |
32 apply (tactic {* rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1 *}) |
599 apply (rule sin_bound_lemma) |
33 apply (rule sumr_fun_eq) |
600 apply (rule sumr_fun_eq, safe) |
34 apply (tactic{* Step_tac 1 *}) |
601 apply (rule_tac f = "%u. u * (x^r)" in arg_cong) |
35 apply (tactic{*rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1*}) |
|
36 apply (subst even_even_mod_4_iff) |
602 apply (subst even_even_mod_4_iff) |
37 apply (tactic{* cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1 *}) |
603 apply (cut_tac m=r in mod_exhaust_less_4, simp, safe) |
38 apply (tactic{* Step_tac 1 *}) |
|
39 apply (simp) |
|
40 apply (simp_all add:even_num_iff) |
604 apply (simp_all add:even_num_iff) |
41 apply (drule lemma_even_mod_4_div_2[simplified]) |
605 apply (drule lemma_even_mod_4_div_2[simplified]) |
42 apply(simp add: numeral_2_eq_2 real_divide_def) |
606 apply(simp add: numeral_2_eq_2 divide_inverse) |
43 apply (drule lemma_odd_mod_4_div_2 ); |
607 apply (drule lemma_odd_mod_4_div_2) |
44 apply (simp add: numeral_2_eq_2 real_divide_def) |
608 apply (simp add: numeral_2_eq_2 divide_inverse) |
45 apply (auto intro: real_mult_le_lemma mult_right_mono simp add: est mult_pos_le mult_ac real_divide_def abs_mult abs_inverse power_abs[symmetric]) |
609 apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono |
|
610 simp add: est mult_pos_le mult_ac divide_inverse |
|
611 power_abs [symmetric]) |
46 done |
612 done |
47 qed |
613 qed |
48 |
614 |
49 end |
615 end |