src/HOL/MacLaurin.thy
 author wenzelm Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) changeset 35115 446c5063e4fd parent 32047 c141f139ce26 child 36974 b877866b5b00 permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
 haftmann@28952 ` 1` ```(* Author : Jacques D. Fleuriot ``` paulson@12224 ` 2` ``` Copyright : 2001 University of Edinburgh ``` paulson@15079 ` 3` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2004 ``` paulson@12224 ` 4` ```*) ``` paulson@12224 ` 5` paulson@15944 ` 6` ```header{*MacLaurin Series*} ``` paulson@15944 ` 7` nipkow@15131 ` 8` ```theory MacLaurin ``` chaieb@29811 ` 9` ```imports Transcendental ``` nipkow@15131 ` 10` ```begin ``` paulson@15079 ` 11` paulson@15079 ` 12` ```subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*} ``` paulson@15079 ` 13` paulson@15079 ` 14` ```text{*This is a very long, messy proof even now that it's been broken down ``` paulson@15079 ` 15` ```into lemmas.*} ``` paulson@15079 ` 16` paulson@15079 ` 17` ```lemma Maclaurin_lemma: ``` paulson@15079 ` 18` ``` "0 < h ==> ``` nipkow@15539 ` 19` ``` \B. f h = (\m=0.. fact (Suc m - n) = (Suc m - n) * fact (m - n)" ``` avigad@32038 ` 32` ``` by (subst fact_reduce_nat, auto) ``` avigad@32038 ` 33` paulson@15079 ` 34` ```lemma Maclaurin_lemma2: ``` huffman@29187 ` 35` ``` assumes diff: "\m t. m < n \ 0\t \ t\h \ DERIV (diff m) t :> diff (Suc m) t" ``` huffman@29187 ` 36` ``` assumes n: "n = Suc k" ``` huffman@29187 ` 37` ``` assumes difg: "difg = ``` paulson@15079 ` 38` ``` (\m t. diff m t - ``` paulson@15079 ` 39` ``` ((\p = 0..m t. m < n & 0 \ t & t \ h --> DERIV (difg m) t :> difg (Suc m) t" ``` huffman@29187 ` 43` ```unfolding difg ``` huffman@29187 ` 44` ``` apply clarify ``` huffman@29187 ` 45` ``` apply (rule DERIV_diff) ``` huffman@29187 ` 46` ``` apply (simp add: diff) ``` huffman@29187 ` 47` ``` apply (simp only: n) ``` huffman@29187 ` 48` ``` apply (rule DERIV_add) ``` huffman@29187 ` 49` ``` apply (rule_tac [2] DERIV_cmult) ``` huffman@29187 ` 50` ``` apply (rule_tac [2] lemma_DERIV_subst) ``` huffman@29187 ` 51` ``` apply (rule_tac [2] DERIV_quotient) ``` huffman@29187 ` 52` ``` apply (rule_tac [3] DERIV_const) ``` huffman@29187 ` 53` ``` apply (rule_tac [2] DERIV_pow) ``` avigad@32038 ` 54` ``` prefer 3 ``` avigad@32038 ` 55` avigad@32038 ` 56` ```apply (simp add: fact_diff_Suc) ``` huffman@29187 ` 57` ``` prefer 2 apply simp ``` huffman@29187 ` 58` ``` apply (frule less_iff_Suc_add [THEN iffD1], clarify) ``` huffman@29187 ` 59` ``` apply (simp del: setsum_op_ivl_Suc) ``` huffman@30082 ` 60` ``` apply (insert sumr_offset4 [of "Suc 0"]) ``` avigad@32047 ` 61` ``` apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc) ``` huffman@29187 ` 62` ``` apply (rule lemma_DERIV_subst) ``` huffman@29187 ` 63` ``` apply (rule DERIV_add) ``` huffman@29187 ` 64` ``` apply (rule_tac [2] DERIV_const) ``` huffman@29187 ` 65` ``` apply (rule DERIV_sumr, clarify) ``` huffman@29187 ` 66` ``` prefer 2 apply simp ``` avigad@32047 ` 67` ``` apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc) ``` huffman@29187 ` 68` ``` apply (rule DERIV_cmult) ``` huffman@29187 ` 69` ``` apply (rule lemma_DERIV_subst) ``` hoelzl@31881 ` 70` ``` apply (best intro!: DERIV_intros) ``` avigad@32047 ` 71` ``` apply (subst fact_Suc) ``` huffman@29187 ` 72` ``` apply (subst real_of_nat_mult) ``` huffman@29187 ` 73` ``` apply (simp add: mult_ac) ``` paulson@15079 ` 74` ```done ``` paulson@15079 ` 75` paulson@15079 ` 76` ```lemma Maclaurin: ``` huffman@29187 ` 77` ``` assumes h: "0 < h" ``` huffman@29187 ` 78` ``` assumes n: "0 < n" ``` huffman@29187 ` 79` ``` assumes diff_0: "diff 0 = f" ``` huffman@29187 ` 80` ``` assumes diff_Suc: ``` huffman@29187 ` 81` ``` "\m t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t" ``` huffman@29187 ` 82` ``` shows ``` huffman@29187 ` 83` ``` "\t. 0 < t & t < h & ``` paulson@15079 ` 84` ``` f h = ``` nipkow@15539 ` 85` ``` setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..m = 0..real) / real (fact m) * h ^ m) + ``` huffman@29187 ` 93` ``` B * (h ^ n / real (fact n))" ``` huffman@29187 ` 94` ``` using Maclaurin_lemma [OF h] .. ``` huffman@29187 ` 95` huffman@29187 ` 96` ``` obtain g where g_def: "g = (%t. f t - ``` huffman@29187 ` 97` ``` (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..(m\nat) t\real. ``` huffman@29187 ` 114` ``` m < n \ (0\real) \ t \ t \ h \ DERIV (difg m) t :> difg (Suc m) t" ``` huffman@29187 ` 115` ``` using diff_Suc m difg_def by (rule Maclaurin_lemma2) ``` huffman@29187 ` 116` huffman@29187 ` 117` ``` have difg_eq_0: "\m. m < n --> difg m 0 = 0" ``` huffman@29187 ` 118` ``` apply clarify ``` huffman@29187 ` 119` ``` apply (simp add: m difg_def) ``` huffman@29187 ` 120` ``` apply (frule less_iff_Suc_add [THEN iffD1], clarify) ``` huffman@29187 ` 121` ``` apply (simp del: setsum_op_ivl_Suc) ``` huffman@30082 ` 122` ``` apply (insert sumr_offset4 [of "Suc 0"]) ``` avigad@32047 ` 123` ``` apply (simp del: setsum_op_ivl_Suc fact_Suc) ``` huffman@29187 ` 124` ``` done ``` huffman@29187 ` 125` huffman@29187 ` 126` ``` have isCont_difg: "\m x. \m < n; 0 \ x; x \ h\ \ isCont (difg m) x" ``` huffman@29187 ` 127` ``` by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 128` huffman@29187 ` 129` ``` have differentiable_difg: ``` huffman@29187 ` 130` ``` "\m x. \m < n; 0 \ x; x \ h\ \ difg m differentiable x" ``` huffman@29187 ` 131` ``` by (rule differentiableI [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 132` huffman@29187 ` 133` ``` have difg_Suc_eq_0: "\m t. \m < n; 0 \ t; t \ h; DERIV (difg m) t :> 0\ ``` huffman@29187 ` 134` ``` \ difg (Suc m) t = 0" ``` huffman@29187 ` 135` ``` by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 136` huffman@29187 ` 137` ``` have "m < n" using m by simp ``` huffman@29187 ` 138` huffman@29187 ` 139` ``` have "\t. 0 < t \ t < h \ DERIV (difg m) t :> 0" ``` huffman@29187 ` 140` ``` using `m < n` ``` huffman@29187 ` 141` ``` proof (induct m) ``` huffman@29187 ` 142` ``` case 0 ``` huffman@29187 ` 143` ``` show ?case ``` huffman@29187 ` 144` ``` proof (rule Rolle) ``` huffman@29187 ` 145` ``` show "0 < h" by fact ``` huffman@29187 ` 146` ``` show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2) ``` huffman@29187 ` 147` ``` show "\x. 0 \ x \ x \ h \ isCont (difg (0\nat)) x" ``` huffman@29187 ` 148` ``` by (simp add: isCont_difg n) ``` huffman@29187 ` 149` ``` show "\x. 0 < x \ x < h \ difg (0\nat) differentiable x" ``` huffman@29187 ` 150` ``` by (simp add: differentiable_difg n) ``` huffman@29187 ` 151` ``` qed ``` huffman@29187 ` 152` ``` next ``` huffman@29187 ` 153` ``` case (Suc m') ``` huffman@29187 ` 154` ``` hence "\t. 0 < t \ t < h \ DERIV (difg m') t :> 0" by simp ``` huffman@29187 ` 155` ``` then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast ``` huffman@29187 ` 156` ``` have "\t'. 0 < t' \ t' < t \ DERIV (difg (Suc m')) t' :> 0" ``` huffman@29187 ` 157` ``` proof (rule Rolle) ``` huffman@29187 ` 158` ``` show "0 < t" by fact ``` huffman@29187 ` 159` ``` show "difg (Suc m') 0 = difg (Suc m') t" ``` huffman@29187 ` 160` ``` using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0) ``` huffman@29187 ` 161` ``` show "\x. 0 \ x \ x \ t \ isCont (difg (Suc m')) x" ``` huffman@29187 ` 162` ``` using `t < h` `Suc m' < n` by (simp add: isCont_difg) ``` huffman@29187 ` 163` ``` show "\x. 0 < x \ x < t \ difg (Suc m') differentiable x" ``` huffman@29187 ` 164` ``` using `t < h` `Suc m' < n` by (simp add: differentiable_difg) ``` huffman@29187 ` 165` ``` qed ``` huffman@29187 ` 166` ``` thus ?case ``` huffman@29187 ` 167` ``` using `t < h` by auto ``` huffman@29187 ` 168` ``` qed ``` huffman@29187 ` 169` huffman@29187 ` 170` ``` then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast ``` huffman@29187 ` 171` huffman@29187 ` 172` ``` hence "difg (Suc m) t = 0" ``` huffman@29187 ` 173` ``` using `m < n` by (simp add: difg_Suc_eq_0) ``` huffman@29187 ` 174` huffman@29187 ` 175` ``` show ?thesis ``` huffman@29187 ` 176` ``` proof (intro exI conjI) ``` huffman@29187 ` 177` ``` show "0 < t" by fact ``` huffman@29187 ` 178` ``` show "t < h" by fact ``` huffman@29187 ` 179` ``` show "f h = ``` huffman@29187 ` 180` ``` (\m = 0..0 & diff 0 = f & ``` nipkow@25134 ` 190` ``` (\m t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t) ``` nipkow@25134 ` 191` ``` --> (\t. 0 < t & t < h & ``` nipkow@25134 ` 192` ``` f h = (\m=0..m t. ``` paulson@15079 ` 200` ``` m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t |] ``` paulson@15079 ` 201` ``` ==> \t. 0 < t & ``` paulson@15079 ` 202` ``` t \ h & ``` paulson@15079 ` 203` ``` f h = ``` nipkow@15539 ` 204` ``` (\m=0..m t. ``` paulson@15079 ` 213` ``` m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t) ``` paulson@15079 ` 214` ``` --> (\t. 0 < t & ``` paulson@15079 ` 215` ``` t \ h & ``` paulson@15079 ` 216` ``` f h = ``` nipkow@15539 ` 217` ``` (\m=0.. 0; diff 0 = f; ``` paulson@15079 ` 223` ``` \m t. m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t |] ``` paulson@15079 ` 224` ``` ==> \t. h < t & ``` paulson@15079 ` 225` ``` t < 0 & ``` paulson@15079 ` 226` ``` f h = ``` nipkow@15539 ` 227` ``` (\m=0..m = 0..m = 0.. 0 & diff 0 = f & ``` paulson@15079 ` 250` ``` (\m t. ``` paulson@15079 ` 251` ``` m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t)) ``` paulson@15079 ` 252` ``` --> (\t. h < t & ``` paulson@15079 ` 253` ``` t < 0 & ``` paulson@15079 ` 254` ``` f h = ``` nipkow@15539 ` 255` ``` (\m=0..0 \ ``` nipkow@25134 ` 266` ``` diff 0 0 = ``` nipkow@25134 ` 267` ``` (\m = 0..m t. m < n & abs t \ abs x --> DERIV (diff m) t :> diff (Suc m) t |] ``` paulson@15079 ` 274` ``` ==> \t. abs t \ abs x & ``` paulson@15079 ` 275` ``` f x = ``` nipkow@15539 ` 276` ``` (\m=0..m x. DERIV (diff m) x :> diff(Suc m) x; ``` nipkow@25162 ` 298` ``` x ~= 0; n > 0 ``` paulson@15079 ` 299` ``` |] ==> \t. 0 < abs t & abs t < abs x & ``` nipkow@15539 ` 300` ``` f x = (\m=0..m x. DERIV (diff m) x :> diff(Suc m) x) & ``` nipkow@25162 ` 312` ``` x ~= 0 & n > 0 ``` paulson@15079 ` 313` ``` --> (\t. 0 < abs t & abs t < abs x & ``` nipkow@15539 ` 314` ``` f x = (\m=0.. n \ 0 --> ``` nipkow@15539 ` 321` ``` (\m=0..m x. DERIV (diff m) x :> diff (Suc m) x ``` paulson@15079 ` 327` ``` |] ==> \t. abs t \ abs x & ``` nipkow@15539 ` 328` ``` f x = (\m=0..m x. DERIV (diff m) x :> diff (Suc m) x) ``` paulson@15079 ` 342` ``` --> (\t. abs t \ abs x & ``` nipkow@15539 ` 343` ``` f x = (\m=0.. 0 |] ``` paulson@15079 ` 351` ``` ==> (\t. 0 < abs t & ``` paulson@15079 ` 352` ``` abs t < abs x & ``` nipkow@15539 ` 353` ``` exp x = (\m=0..t. abs t \ abs x & ``` nipkow@15539 ` 360` ``` exp x = (\m=0..0 --> Suc (Suc (2 * n - 2)) = 2*n" ``` paulson@15251 ` 373` ```by (induct "n", auto) ``` paulson@15079 ` 374` paulson@15079 ` 375` ```lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: ``` nipkow@25134 ` 376` ``` "n\0 --> Suc (Suc (4*n - 2)) = 4*n" ``` paulson@15251 ` 377` ```by (induct "n", auto) ``` paulson@15079 ` 378` paulson@15079 ` 379` ```lemma Suc_mult_two_diff_one [rule_format, simp]: ``` nipkow@25134 ` 380` ``` "n\0 --> Suc (2 * n - 1) = 2*n" ``` paulson@15251 ` 381` ```by (induct "n", auto) ``` paulson@15079 ` 382` paulson@15234 ` 383` paulson@15234 ` 384` ```text{*It is unclear why so many variant results are needed.*} ``` paulson@15079 ` 385` paulson@15079 ` 386` ```lemma Maclaurin_sin_expansion2: ``` paulson@15079 ` 387` ``` "\t. abs t \ abs x & ``` paulson@15079 ` 388` ``` sin x = ``` nipkow@15539 ` 389` ``` (\m=0..t. sin x = ``` nipkow@15539 ` 409` ``` (\m=0.. 0; 0 < x |] ==> ``` paulson@15079 ` 420` ``` \t. 0 < t & t < x & ``` paulson@15079 ` 421` ``` sin x = ``` nipkow@15539 ` 422` ``` (\m=0.. ``` paulson@15079 ` 438` ``` \t. 0 < t & t \ x & ``` paulson@15079 ` 439` ``` sin x = ``` nipkow@15539 ` 440` ``` (\m=0..m=0..<(Suc n). ``` huffman@23177 ` 459` ``` (if even m then -1 ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1" ``` paulson@15251 ` 460` ```by (induct "n", auto) ``` paulson@15079 ` 461` paulson@15079 ` 462` ```lemma Maclaurin_cos_expansion: ``` paulson@15079 ` 463` ``` "\t. abs t \ abs x & ``` paulson@15079 ` 464` ``` cos x = ``` nipkow@15539 ` 465` ``` (\m=0.. 0 |] ==> ``` paulson@15079 ` 486` ``` \t. 0 < t & t < x & ``` paulson@15079 ` 487` ``` cos x = ``` nipkow@15539 ` 488` ``` (\m=0.. 0 |] ==> ``` paulson@15079 ` 505` ``` \t. x < t & t < 0 & ``` paulson@15079 ` 506` ``` cos x = ``` nipkow@15539 ` 507` ``` (\m=0.. (v::real) |] ==> \(x + u) - y\ \ v" ``` paulson@15079 ` 528` ```by auto ``` paulson@15079 ` 529` paulson@15079 ` 530` ```lemma Maclaurin_sin_bound: ``` huffman@23177 ` 531` ``` "abs(sin x - (\m=0.. inverse(real (fact n)) * \x\ ^ n" ``` obua@14738 ` 533` ```proof - ``` paulson@15079 ` 534` ``` have "!! x (y::real). x \ 1 \ 0 \ y \ x * y \ 1 * y" ``` obua@14738 ` 535` ``` by (rule_tac mult_right_mono,simp_all) ``` obua@14738 ` 536` ``` note est = this[simplified] ``` huffman@22985 ` 537` ``` let ?diff = "\(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)" ``` huffman@22985 ` 538` ``` have diff_0: "?diff 0 = sin" by simp ``` huffman@22985 ` 539` ``` have DERIV_diff: "\m x. DERIV (?diff m) x :> ?diff (Suc m) x" ``` huffman@22985 ` 540` ``` apply (clarify) ``` huffman@22985 ` 541` ``` apply (subst (1 2 3) mod_Suc_eq_Suc_mod) ``` huffman@22985 ` 542` ``` apply (cut_tac m=m in mod_exhaust_less_4) ``` hoelzl@31881 ` 543` ``` apply (safe, auto intro!: DERIV_intros) ``` huffman@22985 ` 544` ``` done ``` huffman@22985 ` 545` ``` from Maclaurin_all_le [OF diff_0 DERIV_diff] ``` huffman@22985 ` 546` ``` obtain t where t1: "\t\ \ \x\" and ``` huffman@22985 ` 547` ``` t2: "sin x = (\m = 0..m. ?diff m 0 = (if even m then 0 ``` huffman@23177 ` 551` ``` else -1 ^ ((m - Suc 0) div 2))" ``` huffman@22985 ` 552` ``` apply (subst even_even_mod_4_iff) ``` huffman@22985 ` 553` ``` apply (cut_tac m=m in mod_exhaust_less_4) ``` huffman@22985 ` 554` ``` apply (elim disjE, simp_all) ``` huffman@22985 ` 555` ``` apply (safe dest!: mod_eqD, simp_all) ``` huffman@22985 ` 556` ``` done ``` obua@14738 ` 557` ``` show ?thesis ``` huffman@22985 ` 558` ``` apply (subst t2) ``` paulson@15079 ` 559` ``` apply (rule sin_bound_lemma) ``` nipkow@15536 ` 560` ``` apply (rule setsum_cong[OF refl]) ``` huffman@22985 ` 561` ``` apply (subst diff_m_0, simp) ``` paulson@15079 ` 562` ``` apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono ``` avigad@16775 ` 563` ``` simp add: est mult_nonneg_nonneg mult_ac divide_inverse ``` paulson@16924 ` 564` ``` power_abs [symmetric] abs_mult) ``` obua@14738 ` 565` ``` done ``` obua@14738 ` 566` ```qed ``` obua@14738 ` 567` paulson@15079 ` 568` ```end ```