src/HOL/MacLaurin.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 61954 1d43f86f48be child 63040 eb4ddd18d635 permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
 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 ``` bulwahn@41120 ` 4` ``` Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard HÃ¤upler, 2005 ``` paulson@12224 ` 5` ```*) ``` paulson@12224 ` 6` wenzelm@60758 ` 7` ```section\MacLaurin Series\ ``` paulson@15944 ` 8` nipkow@15131 ` 9` ```theory MacLaurin ``` chaieb@29811 ` 10` ```imports Transcendental ``` nipkow@15131 ` 11` ```begin ``` paulson@15079 ` 12` wenzelm@60758 ` 13` ```subsection\Maclaurin's Theorem with Lagrange Form of Remainder\ ``` paulson@15079 ` 14` wenzelm@60758 ` 15` ```text\This is a very long, messy proof even now that it's been broken down ``` wenzelm@60758 ` 16` ```into lemmas.\ ``` paulson@15079 ` 17` paulson@15079 ` 18` ```lemma Maclaurin_lemma: ``` paulson@15079 ` 19` ``` "0 < h ==> ``` lp15@59730 ` 20` ``` \B::real. f h = (\m fact (Suc m - n) = (Suc m - n) * fact (m - n)" ``` lp15@59730 ` 29` ``` by (subst fact_reduce, auto) ``` avigad@32038 ` 30` paulson@15079 ` 31` ```lemma Maclaurin_lemma2: ``` hoelzl@41166 ` 32` ``` fixes B ``` bulwahn@41120 ` 33` ``` assumes DERIV : "\m t. m < n \ 0\t \ t\h \ DERIV (diff m) t :> diff (Suc m) t" ``` lp15@59730 ` 34` ``` and INIT : "n = Suc k" ``` lp15@61609 ` 35` ``` defines "difg \ ``` lp15@61609 ` 36` ``` (\m t::real. diff m t - ``` lp15@61609 ` 37` ``` ((\p (\m t. diff m t - ?difg m t)") ``` bulwahn@41120 ` 39` ``` shows "\m t. m < n & 0 \ t & t \ h --> DERIV (difg m) t :> difg (Suc m) t" ``` hoelzl@41166 ` 40` ```proof (rule allI impI)+ ``` lp15@59730 ` 41` ``` fix m and t::real ``` lp15@59730 ` 42` ``` assume INIT2: "m < n & 0 \ t & t \ h" ``` hoelzl@41166 ` 43` ``` have "DERIV (difg m) t :> diff (Suc m) t - ``` lp15@59730 ` 44` ``` ((\xxxx. (fact x) + real x * (fact x) \ 0" ``` lp15@61609 ` 56` ``` by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2 less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff) ``` lp15@59730 ` 57` ``` have "\x. (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)) = ``` lp15@59730 ` 58` ``` diff (Suc m + x) 0 * t^x / (fact x)" ``` lp15@59730 ` 59` ``` by (rule nonzero_divide_eq_eq[THEN iffD2]) auto ``` hoelzl@41166 ` 60` ``` moreover ``` lp15@59730 ` 61` ``` have "(n - m) * t ^ (n - Suc m) * B / (fact (n - m)) = ``` lp15@59730 ` 62` ``` B * (t ^ (n - Suc m) / (fact (n - Suc m)))" ``` wenzelm@60758 ` 63` ``` using \0 < n - m\ ``` lp15@59730 ` 64` ``` by (simp add: divide_simps fact_reduce) ``` hoelzl@41166 ` 65` ``` ultimately show "DERIV (difg m) t :> difg (Suc m) t" ``` lp15@61609 ` 66` ``` unfolding difg_def by (simp add: mult.commute) ``` bulwahn@41120 ` 67` ```qed ``` avigad@32038 ` 68` paulson@15079 ` 69` ```lemma Maclaurin: ``` huffman@29187 ` 70` ``` assumes h: "0 < h" ``` huffman@29187 ` 71` ``` assumes n: "0 < n" ``` huffman@29187 ` 72` ``` assumes diff_0: "diff 0 = f" ``` huffman@29187 ` 73` ``` assumes diff_Suc: ``` huffman@29187 ` 74` ``` "\m t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t" ``` huffman@29187 ` 75` ``` shows ``` lp15@59730 ` 76` ``` "\t::real. 0 < t & t < h & ``` paulson@15079 ` 77` ``` f h = ``` lp15@59730 ` 78` ``` setsum (%m. (diff m 0 / (fact m)) * h ^ m) {..m "(\t. f t - ``` lp15@59730 ` 89` ``` (setsum (\m. (diff m 0 / (fact m)) * t^m) {.. "(%m t. diff m t - ``` lp15@59730 ` 95` ``` (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..(m::nat) t::real. ``` wenzelm@61076 ` 102` ``` m < n \ (0::real) \ t \ t \ h \ DERIV (difg m) t :> difg (Suc m) t" ``` hoelzl@41166 ` 103` ``` using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2) ``` huffman@29187 ` 104` hoelzl@56193 ` 105` ``` have difg_eq_0: "\mm x. \m < n; 0 \ x; x \ h\ \ isCont (difg m) x" ``` huffman@29187 ` 109` ``` by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 110` huffman@29187 ` 111` ``` have differentiable_difg: ``` hoelzl@56181 ` 112` ``` "\m x. \m < n; 0 \ x; x \ h\ \ difg m differentiable (at x)" ``` huffman@29187 ` 113` ``` by (rule differentiableI [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 114` huffman@29187 ` 115` ``` have difg_Suc_eq_0: "\m t. \m < n; 0 \ t; t \ h; DERIV (difg m) t :> 0\ ``` huffman@29187 ` 116` ``` \ difg (Suc m) t = 0" ``` huffman@29187 ` 117` ``` by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 118` huffman@29187 ` 119` ``` have "m < n" using m by simp ``` huffman@29187 ` 120` huffman@29187 ` 121` ``` have "\t. 0 < t \ t < h \ DERIV (difg m) t :> 0" ``` wenzelm@60758 ` 122` ``` using \m < n\ ``` huffman@29187 ` 123` ``` proof (induct m) ``` hoelzl@41166 ` 124` ``` case 0 ``` huffman@29187 ` 125` ``` show ?case ``` huffman@29187 ` 126` ``` proof (rule Rolle) ``` huffman@29187 ` 127` ``` show "0 < h" by fact ``` huffman@29187 ` 128` ``` show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2) ``` wenzelm@61076 ` 129` ``` show "\x. 0 \ x \ x \ h \ isCont (difg (0::nat)) x" ``` huffman@29187 ` 130` ``` by (simp add: isCont_difg n) ``` wenzelm@61076 ` 131` ``` show "\x. 0 < x \ x < h \ difg (0::nat) differentiable (at x)" ``` huffman@29187 ` 132` ``` by (simp add: differentiable_difg n) ``` huffman@29187 ` 133` ``` qed ``` huffman@29187 ` 134` ``` next ``` hoelzl@41166 ` 135` ``` case (Suc m') ``` huffman@29187 ` 136` ``` hence "\t. 0 < t \ t < h \ DERIV (difg m') t :> 0" by simp ``` huffman@29187 ` 137` ``` then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast ``` huffman@29187 ` 138` ``` have "\t'. 0 < t' \ t' < t \ DERIV (difg (Suc m')) t' :> 0" ``` huffman@29187 ` 139` ``` proof (rule Rolle) ``` huffman@29187 ` 140` ``` show "0 < t" by fact ``` huffman@29187 ` 141` ``` show "difg (Suc m') 0 = difg (Suc m') t" ``` wenzelm@60758 ` 142` ``` using t \Suc m' < n\ by (simp add: difg_Suc_eq_0 difg_eq_0) ``` huffman@29187 ` 143` ``` show "\x. 0 \ x \ x \ t \ isCont (difg (Suc m')) x" ``` wenzelm@60758 ` 144` ``` using \t < h\ \Suc m' < n\ by (simp add: isCont_difg) ``` hoelzl@56181 ` 145` ``` show "\x. 0 < x \ x < t \ difg (Suc m') differentiable (at x)" ``` wenzelm@60758 ` 146` ``` using \t < h\ \Suc m' < n\ by (simp add: differentiable_difg) ``` huffman@29187 ` 147` ``` qed ``` huffman@29187 ` 148` ``` thus ?case ``` wenzelm@60758 ` 149` ``` using \t < h\ by auto ``` huffman@29187 ` 150` ``` qed ``` huffman@29187 ` 151` ``` then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast ``` huffman@29187 ` 152` huffman@29187 ` 153` ``` hence "difg (Suc m) t = 0" ``` wenzelm@60758 ` 154` ``` using \m < n\ by (simp add: difg_Suc_eq_0) ``` huffman@29187 ` 155` huffman@29187 ` 156` ``` show ?thesis ``` huffman@29187 ` 157` ``` proof (intro exI conjI) ``` huffman@29187 ` 158` ``` show "0 < t" by fact ``` huffman@29187 ` 159` ``` show "t < h" by fact ``` lp15@59730 ` 160` ``` show "f h = (\mdifg (Suc m) t = 0\ ``` lp15@59730 ` 162` ``` by (simp add: m f_h difg_def) ``` huffman@29187 ` 163` ``` qed ``` huffman@29187 ` 164` ```qed ``` paulson@15079 ` 165` paulson@15079 ` 166` ```lemma Maclaurin_objl: ``` nipkow@25162 ` 167` ``` "0 < h & n>0 & diff 0 = f & ``` nipkow@25134 ` 168` ``` (\m t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t) ``` lp15@59730 ` 169` ``` --> (\t::real. 0 < t & t < h & ``` lp15@59730 ` 170` ``` f h = (\mm t::real. ``` bulwahn@41120 ` 178` ``` m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t" ``` bulwahn@41120 ` 179` ``` shows "\t. 0 < t \ t \ h \ f h = ``` lp15@59730 ` 180` ``` (\m 0" by simp ``` bulwahn@41120 ` 187` ``` from INIT1 this INIT2 DERIV have "\t>0. t < h \ ``` bulwahn@41120 ` 188` ``` f h = ``` lp15@59730 ` 189` ``` (\mm t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t) ``` lp15@59730 ` 197` ``` --> (\t::real. 0 < t & ``` paulson@15079 ` 198` ``` t \ h & ``` paulson@15079 ` 199` ``` f h = ``` lp15@59730 ` 200` ``` (\mm t. m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t" ``` bulwahn@41120 ` 208` ``` shows "\t. h < t & t < 0 & ``` lp15@59730 ` 209` ``` f h = (\mABL'\ into \derivative_intros\ format." ``` hoelzl@41166 ` 213` ``` note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong] ``` hoelzl@41166 ` 214` ``` from assms ``` hoelzl@41166 ` 215` ``` have "\t>0. t < - h \ ``` bulwahn@41120 ` 216` ``` f (- (- h)) = ``` hoelzl@56193 ` 217` ``` (\mmm ``` bulwahn@41120 ` 229` ``` - t < 0 \ ``` bulwahn@41120 ` 230` ``` f h = ``` lp15@59730 ` 231` ``` (\m 0 & diff 0 = f & ``` paulson@15079 ` 240` ``` (\m t. ``` paulson@15079 ` 241` ``` m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t)) ``` paulson@15079 ` 242` ``` --> (\t. h < t & ``` paulson@15079 ` 243` ``` t < 0 & ``` paulson@15079 ` 244` ``` f h = ``` lp15@59730 ` 245` ``` (\mMore Convenient "Bidirectional" Version.\ ``` paulson@15079 ` 251` paulson@15079 ` 252` ```(* not good for PVS sin_approx, cos_approx *) ``` paulson@15079 ` 253` lp15@59730 ` 254` ```lemma Maclaurin_bi_le_lemma: ``` lp15@59730 ` 255` ``` "n>0 \ ``` nipkow@25134 ` 256` ``` diff 0 0 = ``` lp15@59730 ` 257` ``` (\mm t::real. m < n & \t\ \ \x\ --> DERIV (diff m) t :> diff (Suc m) t" ``` wenzelm@61944 ` 263` ``` shows "\t. \t\ \ \x\ & ``` paulson@15079 ` 264` ``` f x = ``` lp15@59730 ` 265` ``` (\mt. _ \ f x = ?f x t") ``` hoelzl@41166 ` 267` ```proof cases ``` wenzelm@60758 ` 268` ``` assume "n = 0" with \diff 0 = f\ show ?thesis by force ``` bulwahn@41120 ` 269` ```next ``` hoelzl@41166 ` 270` ``` assume "n \ 0" ``` hoelzl@41166 ` 271` ``` show ?thesis ``` hoelzl@41166 ` 272` ``` proof (cases rule: linorder_cases) ``` wenzelm@60758 ` 273` ``` assume "x = 0" with \n \ 0\ \diff 0 = f\ DERIV ``` lp15@56238 ` 274` ``` have "\0\ \ \x\ \ f x = ?f x 0" by (auto simp add: Maclaurin_bi_le_lemma) ``` hoelzl@41166 ` 275` ``` thus ?thesis .. ``` bulwahn@41120 ` 276` ``` next ``` hoelzl@41166 ` 277` ``` assume "x < 0" ``` wenzelm@60758 ` 278` ``` with \n \ 0\ DERIV ``` hoelzl@41166 ` 279` ``` have "\t>x. t < 0 \ diff 0 x = ?f x t" by (intro Maclaurin_minus) auto ``` hoelzl@41166 ` 280` ``` then guess t .. ``` wenzelm@60758 ` 281` ``` with \x < 0\ \diff 0 = f\ have "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 282` ``` thus ?thesis .. ``` hoelzl@41166 ` 283` ``` next ``` hoelzl@41166 ` 284` ``` assume "x > 0" ``` wenzelm@60758 ` 285` ``` with \n \ 0\ \diff 0 = f\ DERIV ``` hoelzl@41166 ` 286` ``` have "\t>0. t < x \ diff 0 x = ?f x t" by (intro Maclaurin) auto ``` hoelzl@41166 ` 287` ``` then guess t .. ``` wenzelm@60758 ` 288` ``` with \x > 0\ \diff 0 = f\ have "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 289` ``` thus ?thesis .. ``` bulwahn@41120 ` 290` ``` qed ``` bulwahn@41120 ` 291` ```qed ``` bulwahn@41120 ` 292` paulson@15079 ` 293` ```lemma Maclaurin_all_lt: ``` lp15@59730 ` 294` ``` fixes x::real ``` bulwahn@41120 ` 295` ``` assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \ 0" ``` bulwahn@41120 ` 296` ``` and DERIV: "\m x. DERIV (diff m) x :> diff(Suc m) x" ``` wenzelm@61944 ` 297` ``` shows "\t. 0 < \t\ & \t\ < \x\ & f x = ``` lp15@59730 ` 298` ``` (\mt. _ \ _ \ f x = ?f x t") ``` hoelzl@41166 ` 300` ```proof (cases rule: linorder_cases) ``` hoelzl@41166 ` 301` ``` assume "x = 0" with INIT3 show "?thesis".. ``` hoelzl@41166 ` 302` ```next ``` hoelzl@41166 ` 303` ``` assume "x < 0" ``` hoelzl@41166 ` 304` ``` with assms have "\t>x. t < 0 \ f x = ?f x t" by (intro Maclaurin_minus) auto ``` hoelzl@41166 ` 305` ``` then guess t .. ``` wenzelm@60758 ` 306` ``` with \x < 0\ have "0 < \t\ \ \t\ < \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 307` ``` thus ?thesis .. ``` hoelzl@41166 ` 308` ```next ``` hoelzl@41166 ` 309` ``` assume "x > 0" ``` hoelzl@41166 ` 310` ``` with assms have "\t>0. t < x \ f x = ?f x t " by (intro Maclaurin) auto ``` hoelzl@41166 ` 311` ``` then guess t .. ``` wenzelm@60758 ` 312` ``` with \x > 0\ have "0 < \t\ \ \t\ < \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 313` ``` thus ?thesis .. ``` bulwahn@41120 ` 314` ```qed ``` bulwahn@41120 ` 315` paulson@15079 ` 316` paulson@15079 ` 317` ```lemma Maclaurin_all_lt_objl: ``` lp15@59730 ` 318` ``` fixes x::real ``` lp15@59730 ` 319` ``` shows ``` paulson@15079 ` 320` ``` "diff 0 = f & ``` paulson@15079 ` 321` ``` (\m x. DERIV (diff m) x :> diff(Suc m) x) & ``` nipkow@25162 ` 322` ``` x ~= 0 & n > 0 ``` wenzelm@61944 ` 323` ``` --> (\t. 0 < \t\ & \t\ < \x\ & ``` lp15@59730 ` 324` ``` f x = (\m n \ 0 --> ``` lp15@59730 ` 331` ``` (\mm x::real. DERIV (diff m) x :> diff (Suc m) x" ``` wenzelm@61944 ` 339` ``` shows "\t. \t\ \ \x\ & f x = ``` lp15@59730 ` 340` ``` (\mt. _ \ f x = ?f x t") ``` hoelzl@41166 ` 342` ```proof cases ``` hoelzl@41166 ` 343` ``` assume "n = 0" with INIT show ?thesis by force ``` bulwahn@41120 ` 344` ``` next ``` hoelzl@41166 ` 345` ``` assume "n \ 0" ``` hoelzl@41166 ` 346` ``` show ?thesis ``` hoelzl@41166 ` 347` ``` proof cases ``` hoelzl@41166 ` 348` ``` assume "x = 0" ``` wenzelm@60758 ` 349` ``` with \n \ 0\ have "(\mx = 0\ \n \ 0\ have " \0\ \ \x\ \ f x = ?f x 0" by force ``` hoelzl@41166 ` 352` ``` thus ?thesis .. ``` hoelzl@41166 ` 353` ``` next ``` hoelzl@41166 ` 354` ``` assume "x \ 0" ``` wenzelm@60758 ` 355` ``` with INIT \n \ 0\ DERIV have "\t. 0 < \t\ \ \t\ < \x\ \ f x = ?f x t" ``` hoelzl@41166 ` 356` ``` by (intro Maclaurin_all_lt) auto ``` hoelzl@41166 ` 357` ``` then guess t .. ``` hoelzl@41166 ` 358` ``` hence "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 359` ``` thus ?thesis .. ``` bulwahn@41120 ` 360` ``` qed ``` bulwahn@41120 ` 361` ```qed ``` bulwahn@41120 ` 362` lp15@59730 ` 363` ```lemma Maclaurin_all_le_objl: ``` lp15@59730 ` 364` ``` "diff 0 = f & ``` paulson@15079 ` 365` ``` (\m x. DERIV (diff m) x :> diff (Suc m) x) ``` wenzelm@61944 ` 366` ``` --> (\t::real. \t\ \ \x\ & ``` lp15@59730 ` 367` ``` f x = (\mVersion for Exponential Function\ ``` paulson@15079 ` 373` lp15@59730 ` 374` ```lemma Maclaurin_exp_lt: ``` lp15@59730 ` 375` ``` fixes x::real ``` lp15@59730 ` 376` ``` shows ``` lp15@59730 ` 377` ``` "[| x ~= 0; n > 0 |] ``` wenzelm@61944 ` 378` ``` ==> (\t. 0 < \t\ & ``` wenzelm@61944 ` 379` ``` \t\ < \x\ & ``` lp15@59730 ` 380` ``` exp x = (\mt::real. \t\ \ \x\ & ``` lp15@59730 ` 387` ``` exp x = (\m x \ 1 + x + x\<^sup>2 / 2 \ exp x" ``` lp15@60017 ` 394` ``` using Maclaurin_exp_le [of x 3] ``` lp15@60017 ` 395` ``` by (auto simp: numeral_3_eq_3 power2_eq_square power_Suc) ``` lp15@60017 ` 396` paulson@15079 ` 397` wenzelm@60758 ` 398` ```subsection\Version for Sine Function\ ``` paulson@15079 ` 399` paulson@15079 ` 400` ```lemma mod_exhaust_less_4: ``` nipkow@25134 ` 401` ``` "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)" ``` webertj@20217 ` 402` ```by auto ``` paulson@15079 ` 403` paulson@15079 ` 404` ```lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: ``` nipkow@25134 ` 405` ``` "n\0 --> Suc (Suc (2 * n - 2)) = 2*n" ``` paulson@15251 ` 406` ```by (induct "n", auto) ``` paulson@15079 ` 407` paulson@15079 ` 408` ```lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: ``` nipkow@25134 ` 409` ``` "n\0 --> Suc (Suc (4*n - 2)) = 4*n" ``` paulson@15251 ` 410` ```by (induct "n", auto) ``` paulson@15079 ` 411` paulson@15079 ` 412` ```lemma Suc_mult_two_diff_one [rule_format, simp]: ``` nipkow@25134 ` 413` ``` "n\0 --> Suc (2 * n - 1) = 2*n" ``` paulson@15251 ` 414` ```by (induct "n", auto) ``` paulson@15079 ` 415` paulson@15234 ` 416` wenzelm@60758 ` 417` ```text\It is unclear why so many variant results are needed.\ ``` paulson@15079 ` 418` huffman@36974 ` 419` ```lemma sin_expansion_lemma: ``` hoelzl@41166 ` 420` ``` "sin (x + real (Suc m) * pi / 2) = ``` huffman@36974 ` 421` ``` cos (x + real (m) * pi / 2)" ``` lp15@61609 ` 422` ```by (simp only: cos_add sin_add of_nat_Suc add_divide_distrib distrib_right, auto) ``` huffman@36974 ` 423` paulson@15079 ` 424` ```lemma Maclaurin_sin_expansion2: ``` wenzelm@61944 ` 425` ``` "\t. \t\ \ \x\ & ``` paulson@15079 ` 426` ``` sin x = ``` hoelzl@56193 ` 427` ``` (\mt. sin x = ``` hoelzl@56193 ` 446` ``` (\m 0; 0 < x |] ==> ``` paulson@15079 ` 454` ``` \t. 0 < t & t < x & ``` paulson@15079 ` 455` ``` sin x = ``` hoelzl@56193 ` 456` ``` (\m ``` paulson@15079 ` 471` ``` \t. 0 < t & t \ x & ``` paulson@15079 ` 472` ``` sin x = ``` hoelzl@56193 ` 473` ``` (\mMaclaurin Expansion for Cosine Function\ ``` paulson@15079 ` 488` paulson@15079 ` 489` ```lemma sumr_cos_zero_one [simp]: ``` hoelzl@56193 ` 490` ``` "(\m<(Suc n). cos_coeff m * 0 ^ m) = 1" ``` paulson@15251 ` 491` ```by (induct "n", auto) ``` paulson@15079 ` 492` huffman@36974 ` 493` ```lemma cos_expansion_lemma: ``` huffman@36974 ` 494` ``` "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)" ``` lp15@61609 ` 495` ```by (simp only: cos_add sin_add of_nat_Suc distrib_right add_divide_distrib, auto) ``` huffman@36974 ` 496` paulson@15079 ` 497` ```lemma Maclaurin_cos_expansion: ``` wenzelm@61944 ` 498` ``` "\t::real. \t\ \ \x\ & ``` paulson@15079 ` 499` ``` cos x = ``` hoelzl@56193 ` 500` ``` (\m 0 |] ==> ``` paulson@15079 ` 518` ``` \t. 0 < t & t < x & ``` paulson@15079 ` 519` ``` cos x = ``` hoelzl@56193 ` 520` ``` (\m 0 |] ==> ``` paulson@15079 ` 534` ``` \t. x < t & t < 0 & ``` paulson@15079 ` 535` ``` cos x = ``` hoelzl@56193 ` 536` ``` (\mu\ \ (v::real) |] ==> \(x + u) - y\ \ v" ``` paulson@15079 ` 554` ```by auto ``` paulson@15079 ` 555` paulson@15079 ` 556` ```lemma Maclaurin_sin_bound: ``` wenzelm@61944 ` 557` ``` "\sin x - (\m \ inverse((fact n)) * \x\ ^ n" ``` obua@14738 ` 558` ```proof - ``` paulson@15079 ` 559` ``` have "!! x (y::real). x \ 1 \ 0 \ y \ x * y \ 1 * y" ``` obua@14738 ` 560` ``` by (rule_tac mult_right_mono,simp_all) ``` obua@14738 ` 561` ``` note est = this[simplified] ``` huffman@22985 ` 562` ``` 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 ` 563` ``` have diff_0: "?diff 0 = sin" by simp ``` huffman@22985 ` 564` ``` have DERIV_diff: "\m x. DERIV (?diff m) x :> ?diff (Suc m) x" ``` huffman@22985 ` 565` ``` apply (clarify) ``` huffman@22985 ` 566` ``` apply (subst (1 2 3) mod_Suc_eq_Suc_mod) ``` huffman@22985 ` 567` ``` apply (cut_tac m=m in mod_exhaust_less_4) ``` hoelzl@56381 ` 568` ``` apply (safe, auto intro!: derivative_eq_intros) ``` huffman@22985 ` 569` ``` done ``` huffman@22985 ` 570` ``` from Maclaurin_all_le [OF diff_0 DERIV_diff] ``` huffman@22985 ` 571` ``` obtain t where t1: "\t\ \ \x\" and ``` lp15@59730 ` 572` ``` t2: "sin x = (\mm. ?diff m 0 = (if even m then 0 ``` haftmann@58410 ` 576` ``` else (- 1) ^ ((m - Suc 0) div 2))" ``` huffman@22985 ` 577` ``` apply (subst even_even_mod_4_iff) ``` huffman@22985 ` 578` ``` apply (cut_tac m=m in mod_exhaust_less_4) ``` huffman@22985 ` 579` ``` apply (elim disjE, simp_all) ``` huffman@22985 ` 580` ``` apply (safe dest!: mod_eqD, simp_all) ``` huffman@22985 ` 581` ``` done ``` obua@14738 ` 582` ``` show ?thesis ``` huffman@44306 ` 583` ``` unfolding sin_coeff_def ``` huffman@22985 ` 584` ``` apply (subst t2) ``` paulson@15079 ` 585` ``` apply (rule sin_bound_lemma) ``` haftmann@57418 ` 586` ``` apply (rule setsum.cong[OF refl]) ``` huffman@22985 ` 587` ``` apply (subst diff_m_0, simp) ``` paulson@15079 ` 588` ``` apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono ``` haftmann@57514 ` 589` ``` simp add: est ac_simps divide_inverse power_abs [symmetric] abs_mult) ``` obua@14738 ` 590` ``` done ``` obua@14738 ` 591` ```qed ``` obua@14738 ` 592` paulson@15079 ` 593` ```end ```