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