src/HOL/MacLaurin.thy
 author wenzelm Fri Mar 07 22:30:58 2014 +0100 (2014-03-07) changeset 55990 41c6b99c5fb7 parent 51489 f738e6dbd844 child 56181 2aa0b19e74f3 permissions -rw-r--r--
more antiquotations;
```     1 (*  Author      : Jacques D. Fleuriot
```
```     2     Copyright   : 2001 University of Edinburgh
```
```     3     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
```
```     4     Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard HÃ¤upler, 2005
```
```     5 *)
```
```     6
```
```     7 header{*MacLaurin Series*}
```
```     8
```
```     9 theory MacLaurin
```
```    10 imports Transcendental
```
```    11 begin
```
```    12
```
```    13 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
```
```    14
```
```    15 text{*This is a very long, messy proof even now that it's been broken down
```
```    16 into lemmas.*}
```
```    17
```
```    18 lemma Maclaurin_lemma:
```
```    19     "0 < h ==>
```
```    20      \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
```
```    21                (B * ((h^n) / real(fact n)))"
```
```    22 by (rule exI[where x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
```
```    23                  real(fact n) / (h^n)"]) simp
```
```    24
```
```    25 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
```
```    26 by arith
```
```    27
```
```    28 lemma fact_diff_Suc [rule_format]:
```
```    29   "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
```
```    30   by (subst fact_reduce_nat, auto)
```
```    31
```
```    32 lemma Maclaurin_lemma2:
```
```    33   fixes B
```
```    34   assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
```
```    35     and INIT : "n = Suc k"
```
```    36   defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
```
```    37     B * (t ^ (n - m) / real (fact (n - m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
```
```    38   shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
```
```    39 proof (rule allI impI)+
```
```    40   fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h"
```
```    41   have "DERIV (difg m) t :> diff (Suc m) t -
```
```    42     ((\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
```
```    43      real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
```
```    44     by (auto intro!: DERIV_intros DERIV[rule_format, OF INIT2])
```
```    45       moreover
```
```    46   from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
```
```    47     unfolding atLeast0LessThan[symmetric] by auto
```
```    48   have "(\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
```
```    49       (\<Sum>x = 0..<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
```
```    50     unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
```
```    51   moreover
```
```    52   have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0"
```
```    53     by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff)
```
```    54   have "\<And>x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) =
```
```    55       diff (Suc m + x) 0 * t^x / real (fact x)"
```
```    56     by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2])
```
```    57   moreover
```
```    58   have "real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)) =
```
```    59       B * (t ^ (n - Suc m) / real (fact (n - Suc m)))"
```
```    60     using `0 < n - m` by (simp add: fact_reduce_nat)
```
```    61   ultimately show "DERIV (difg m) t :> difg (Suc m) t"
```
```    62     unfolding difg_def by simp
```
```    63 qed
```
```    64
```
```    65 lemma Maclaurin:
```
```    66   assumes h: "0 < h"
```
```    67   assumes n: "0 < n"
```
```    68   assumes diff_0: "diff 0 = f"
```
```    69   assumes diff_Suc:
```
```    70     "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
```
```    71   shows
```
```    72     "\<exists>t. 0 < t & t < h &
```
```    73               f h =
```
```    74               setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
```
```    75               (diff n t / real (fact n)) * h ^ n"
```
```    76 proof -
```
```    77   from n obtain m where m: "n = Suc m"
```
```    78     by (cases n) (simp add: n)
```
```    79
```
```    80   obtain B where f_h: "f h =
```
```    81         (\<Sum>m = 0..<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
```
```    82         B * (h ^ n / real (fact n))"
```
```    83     using Maclaurin_lemma [OF h] ..
```
```    84
```
```    85   def g \<equiv> "(\<lambda>t. f t -
```
```    86     (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {0..<n}
```
```    87       + (B * (t^n / real(fact n)))))"
```
```    88
```
```    89   have g2: "g 0 = 0 & g h = 0"
```
```    90     apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
```
```    91     apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
```
```    92     apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
```
```    93     done
```
```    94
```
```    95   def difg \<equiv> "(%m t. diff m t -
```
```    96     (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m}
```
```    97       + (B * ((t ^ (n - m)) / real (fact (n - m))))))"
```
```    98
```
```    99   have difg_0: "difg 0 = g"
```
```   100     unfolding difg_def g_def by (simp add: diff_0)
```
```   101
```
```   102   have difg_Suc: "\<forall>(m\<Colon>nat) t\<Colon>real.
```
```   103         m < n \<and> (0\<Colon>real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
```
```   104     using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2)
```
```   105
```
```   106   have difg_eq_0: "\<forall>m. m < n --> difg m 0 = 0"
```
```   107     apply clarify
```
```   108     apply (simp add: m difg_def)
```
```   109     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
```
```   110     apply (simp del: setsum_op_ivl_Suc)
```
```   111     apply (insert sumr_offset4 [of "Suc 0"])
```
```   112     apply (simp del: setsum_op_ivl_Suc fact_Suc)
```
```   113     done
```
```   114
```
```   115   have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
```
```   116     by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
```
```   117
```
```   118   have differentiable_difg:
```
```   119     "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x"
```
```   120     by (rule differentiableI [OF difg_Suc [rule_format]]) simp
```
```   121
```
```   122   have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk>
```
```   123         \<Longrightarrow> difg (Suc m) t = 0"
```
```   124     by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp
```
```   125
```
```   126   have "m < n" using m by simp
```
```   127
```
```   128   have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
```
```   129   using `m < n`
```
```   130   proof (induct m)
```
```   131     case 0
```
```   132     show ?case
```
```   133     proof (rule Rolle)
```
```   134       show "0 < h" by fact
```
```   135       show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
```
```   136       show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x"
```
```   137         by (simp add: isCont_difg n)
```
```   138       show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x"
```
```   139         by (simp add: differentiable_difg n)
```
```   140     qed
```
```   141   next
```
```   142     case (Suc m')
```
```   143     hence "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" by simp
```
```   144     then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast
```
```   145     have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
```
```   146     proof (rule Rolle)
```
```   147       show "0 < t" by fact
```
```   148       show "difg (Suc m') 0 = difg (Suc m') t"
```
```   149         using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0)
```
```   150       show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x"
```
```   151         using `t < h` `Suc m' < n` by (simp add: isCont_difg)
```
```   152       show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable x"
```
```   153         using `t < h` `Suc m' < n` by (simp add: differentiable_difg)
```
```   154     qed
```
```   155     thus ?case
```
```   156       using `t < h` by auto
```
```   157   qed
```
```   158
```
```   159   then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast
```
```   160
```
```   161   hence "difg (Suc m) t = 0"
```
```   162     using `m < n` by (simp add: difg_Suc_eq_0)
```
```   163
```
```   164   show ?thesis
```
```   165   proof (intro exI conjI)
```
```   166     show "0 < t" by fact
```
```   167     show "t < h" by fact
```
```   168     show "f h =
```
```   169       (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
```
```   170       diff n t / real (fact n) * h ^ n"
```
```   171       using `difg (Suc m) t = 0`
```
```   172       by (simp add: m f_h difg_def del: fact_Suc)
```
```   173   qed
```
```   174 qed
```
```   175
```
```   176 lemma Maclaurin_objl:
```
```   177   "0 < h & n>0 & diff 0 = f &
```
```   178   (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
```
```   179    --> (\<exists>t. 0 < t & t < h &
```
```   180             f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
```
```   181                   diff n t / real (fact n) * h ^ n)"
```
```   182 by (blast intro: Maclaurin)
```
```   183
```
```   184
```
```   185 lemma Maclaurin2:
```
```   186   assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
```
```   187   and DERIV: "\<forall>m t.
```
```   188   m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
```
```   189   shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
```
```   190   (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
```
```   191   diff n t / real (fact n) * h ^ n"
```
```   192 proof (cases "n")
```
```   193   case 0 with INIT1 INIT2 show ?thesis by fastforce
```
```   194 next
```
```   195   case Suc
```
```   196   hence "n > 0" by simp
```
```   197   from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
```
```   198     f h =
```
```   199     (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
```
```   200     by (rule Maclaurin)
```
```   201   thus ?thesis by fastforce
```
```   202 qed
```
```   203
```
```   204 lemma Maclaurin2_objl:
```
```   205      "0 < h & diff 0 = f &
```
```   206        (\<forall>m t.
```
```   207           m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
```
```   208     --> (\<exists>t. 0 < t &
```
```   209               t \<le> h &
```
```   210               f h =
```
```   211               (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
```
```   212               diff n t / real (fact n) * h ^ n)"
```
```   213 by (blast intro: Maclaurin2)
```
```   214
```
```   215 lemma Maclaurin_minus:
```
```   216   assumes "h < 0" "0 < n" "diff 0 = f"
```
```   217   and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
```
```   218   shows "\<exists>t. h < t & t < 0 &
```
```   219          f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
```
```   220          diff n t / real (fact n) * h ^ n"
```
```   221 proof -
```
```   222   txt "Transform @{text ABL'} into @{text DERIV_intros} format."
```
```   223   note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
```
```   224   from assms
```
```   225   have "\<exists>t>0. t < - h \<and>
```
```   226     f (- (- h)) =
```
```   227     (\<Sum>m = 0..<n.
```
```   228     (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
```
```   229     (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
```
```   230     by (intro Maclaurin) (auto intro!: DERIV_intros DERIV')
```
```   231   then guess t ..
```
```   232   moreover
```
```   233   have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
```
```   234     by (auto simp add: power_mult_distrib[symmetric])
```
```   235   moreover
```
```   236   have "(SUM m = 0..<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m = 0..<n. diff m 0 * h ^ m / real (fact m))"
```
```   237     by (auto intro: setsum_cong simp add: power_mult_distrib[symmetric])
```
```   238   ultimately have " h < - t \<and>
```
```   239     - t < 0 \<and>
```
```   240     f h =
```
```   241     (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
```
```   242     by auto
```
```   243   thus ?thesis ..
```
```   244 qed
```
```   245
```
```   246 lemma Maclaurin_minus_objl:
```
```   247      "(h < 0 & n > 0 & diff 0 = f &
```
```   248        (\<forall>m t.
```
```   249           m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
```
```   250     --> (\<exists>t. h < t &
```
```   251               t < 0 &
```
```   252               f h =
```
```   253               (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
```
```   254               diff n t / real (fact n) * h ^ n)"
```
```   255 by (blast intro: Maclaurin_minus)
```
```   256
```
```   257
```
```   258 subsection{*More Convenient "Bidirectional" Version.*}
```
```   259
```
```   260 (* not good for PVS sin_approx, cos_approx *)
```
```   261
```
```   262 lemma Maclaurin_bi_le_lemma [rule_format]:
```
```   263   "n>0 \<longrightarrow>
```
```   264    diff 0 0 =
```
```   265    (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
```
```   266    diff n 0 * 0 ^ n / real (fact n)"
```
```   267 by (induct "n") auto
```
```   268
```
```   269 lemma Maclaurin_bi_le:
```
```   270    assumes "diff 0 = f"
```
```   271    and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
```
```   272    shows "\<exists>t. abs t \<le> abs x &
```
```   273               f x =
```
```   274               (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
```
```   275      diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
```
```   276 proof cases
```
```   277   assume "n = 0" with `diff 0 = f` show ?thesis by force
```
```   278 next
```
```   279   assume "n \<noteq> 0"
```
```   280   show ?thesis
```
```   281   proof (cases rule: linorder_cases)
```
```   282     assume "x = 0" with `n \<noteq> 0` `diff 0 = f` DERIV
```
```   283     have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (force simp add: Maclaurin_bi_le_lemma)
```
```   284     thus ?thesis ..
```
```   285   next
```
```   286     assume "x < 0"
```
```   287     with `n \<noteq> 0` DERIV
```
```   288     have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t" by (intro Maclaurin_minus) auto
```
```   289     then guess t ..
```
```   290     with `x < 0` `diff 0 = f` have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
```
```   291     thus ?thesis ..
```
```   292   next
```
```   293     assume "x > 0"
```
```   294     with `n \<noteq> 0` `diff 0 = f` DERIV
```
```   295     have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t" by (intro Maclaurin) auto
```
```   296     then guess t ..
```
```   297     with `x > 0` `diff 0 = f` have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
```
```   298     thus ?thesis ..
```
```   299   qed
```
```   300 qed
```
```   301
```
```   302 lemma Maclaurin_all_lt:
```
```   303   assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
```
```   304   and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
```
```   305   shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
```
```   306     (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
```
```   307                 (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
```
```   308 proof (cases rule: linorder_cases)
```
```   309   assume "x = 0" with INIT3 show "?thesis"..
```
```   310 next
```
```   311   assume "x < 0"
```
```   312   with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t" by (intro Maclaurin_minus) auto
```
```   313   then guess t ..
```
```   314   with `x < 0` have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp
```
```   315   thus ?thesis ..
```
```   316 next
```
```   317   assume "x > 0"
```
```   318   with assms have "\<exists>t>0. t < x \<and> f x = ?f x t " by (intro Maclaurin) auto
```
```   319   then guess t ..
```
```   320   with `x > 0` have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp
```
```   321   thus ?thesis ..
```
```   322 qed
```
```   323
```
```   324
```
```   325 lemma Maclaurin_all_lt_objl:
```
```   326      "diff 0 = f &
```
```   327       (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
```
```   328       x ~= 0 & n > 0
```
```   329       --> (\<exists>t. 0 < abs t & abs t < abs x &
```
```   330                f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
```
```   331                      (diff n t / real (fact n)) * x ^ n)"
```
```   332 by (blast intro: Maclaurin_all_lt)
```
```   333
```
```   334 lemma Maclaurin_zero [rule_format]:
```
```   335      "x = (0::real)
```
```   336       ==> n \<noteq> 0 -->
```
```   337           (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
```
```   338           diff 0 0"
```
```   339 by (induct n, auto)
```
```   340
```
```   341
```
```   342 lemma Maclaurin_all_le:
```
```   343   assumes INIT: "diff 0 = f"
```
```   344   and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
```
```   345   shows "\<exists>t. abs t \<le> abs x & f x =
```
```   346     (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
```
```   347     (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
```
```   348 proof cases
```
```   349   assume "n = 0" with INIT show ?thesis by force
```
```   350   next
```
```   351   assume "n \<noteq> 0"
```
```   352   show ?thesis
```
```   353   proof cases
```
```   354     assume "x = 0"
```
```   355     with `n \<noteq> 0` have "(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
```
```   356       by (intro Maclaurin_zero) auto
```
```   357     with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force
```
```   358     thus ?thesis ..
```
```   359   next
```
```   360     assume "x \<noteq> 0"
```
```   361     with INIT `n \<noteq> 0` DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
```
```   362       by (intro Maclaurin_all_lt) auto
```
```   363     then guess t ..
```
```   364     hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
```
```   365     thus ?thesis ..
```
```   366   qed
```
```   367 qed
```
```   368
```
```   369 lemma Maclaurin_all_le_objl: "diff 0 = f &
```
```   370       (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
```
```   371       --> (\<exists>t. abs t \<le> abs x &
```
```   372               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
```
```   373                     (diff n t / real (fact n)) * x ^ n)"
```
```   374 by (blast intro: Maclaurin_all_le)
```
```   375
```
```   376
```
```   377 subsection{*Version for Exponential Function*}
```
```   378
```
```   379 lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
```
```   380       ==> (\<exists>t. 0 < abs t &
```
```   381                 abs t < abs x &
```
```   382                 exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
```
```   383                         (exp t / real (fact n)) * x ^ n)"
```
```   384 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
```
```   385
```
```   386
```
```   387 lemma Maclaurin_exp_le:
```
```   388      "\<exists>t. abs t \<le> abs x &
```
```   389             exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
```
```   390                        (exp t / real (fact n)) * x ^ n"
```
```   391 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
```
```   392
```
```   393
```
```   394 subsection{*Version for Sine Function*}
```
```   395
```
```   396 lemma mod_exhaust_less_4:
```
```   397   "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
```
```   398 by auto
```
```   399
```
```   400 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
```
```   401   "n\<noteq>0 --> Suc (Suc (2 * n - 2)) = 2*n"
```
```   402 by (induct "n", auto)
```
```   403
```
```   404 lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
```
```   405   "n\<noteq>0 --> Suc (Suc (4*n - 2)) = 4*n"
```
```   406 by (induct "n", auto)
```
```   407
```
```   408 lemma Suc_mult_two_diff_one [rule_format, simp]:
```
```   409   "n\<noteq>0 --> Suc (2 * n - 1) = 2*n"
```
```   410 by (induct "n", auto)
```
```   411
```
```   412
```
```   413 text{*It is unclear why so many variant results are needed.*}
```
```   414
```
```   415 lemma sin_expansion_lemma:
```
```   416      "sin (x + real (Suc m) * pi / 2) =
```
```   417       cos (x + real (m) * pi / 2)"
```
```   418 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib distrib_right, auto)
```
```   419
```
```   420 lemma Maclaurin_sin_expansion2:
```
```   421      "\<exists>t. abs t \<le> abs x &
```
```   422        sin x =
```
```   423        (\<Sum>m=0..<n. sin_coeff m * x ^ m)
```
```   424       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
```
```   425 apply (cut_tac f = sin and n = n and x = x
```
```   426         and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
```
```   427 apply safe
```
```   428 apply (simp (no_asm))
```
```   429 apply (simp (no_asm) add: sin_expansion_lemma)
```
```   430 apply (force intro!: DERIV_intros)
```
```   431 apply (subst (asm) setsum_0', clarify, case_tac "x", simp, simp)
```
```   432 apply (cases n, simp, simp)
```
```   433 apply (rule ccontr, simp)
```
```   434 apply (drule_tac x = x in spec, simp)
```
```   435 apply (erule ssubst)
```
```   436 apply (rule_tac x = t in exI, simp)
```
```   437 apply (rule setsum_cong[OF refl])
```
```   438 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
```
```   439 done
```
```   440
```
```   441 lemma Maclaurin_sin_expansion:
```
```   442      "\<exists>t. sin x =
```
```   443        (\<Sum>m=0..<n. sin_coeff m * x ^ m)
```
```   444       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
```
```   445 apply (insert Maclaurin_sin_expansion2 [of x n])
```
```   446 apply (blast intro: elim:)
```
```   447 done
```
```   448
```
```   449 lemma Maclaurin_sin_expansion3:
```
```   450      "[| n > 0; 0 < x |] ==>
```
```   451        \<exists>t. 0 < t & t < x &
```
```   452        sin x =
```
```   453        (\<Sum>m=0..<n. sin_coeff m * x ^ m)
```
```   454       + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
```
```   455 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)
```
```   456 apply safe
```
```   457 apply simp
```
```   458 apply (simp (no_asm) add: sin_expansion_lemma)
```
```   459 apply (force intro!: DERIV_intros)
```
```   460 apply (erule ssubst)
```
```   461 apply (rule_tac x = t in exI, simp)
```
```   462 apply (rule setsum_cong[OF refl])
```
```   463 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
```
```   464 done
```
```   465
```
```   466 lemma Maclaurin_sin_expansion4:
```
```   467      "0 < x ==>
```
```   468        \<exists>t. 0 < t & t \<le> x &
```
```   469        sin x =
```
```   470        (\<Sum>m=0..<n. sin_coeff m * x ^ m)
```
```   471       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
```
```   472 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)
```
```   473 apply safe
```
```   474 apply simp
```
```   475 apply (simp (no_asm) add: sin_expansion_lemma)
```
```   476 apply (force intro!: DERIV_intros)
```
```   477 apply (erule ssubst)
```
```   478 apply (rule_tac x = t in exI, simp)
```
```   479 apply (rule setsum_cong[OF refl])
```
```   480 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
```
```   481 done
```
```   482
```
```   483
```
```   484 subsection{*Maclaurin Expansion for Cosine Function*}
```
```   485
```
```   486 lemma sumr_cos_zero_one [simp]:
```
```   487   "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
```
```   488 by (induct "n", auto)
```
```   489
```
```   490 lemma cos_expansion_lemma:
```
```   491   "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
```
```   492 by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto)
```
```   493
```
```   494 lemma Maclaurin_cos_expansion:
```
```   495      "\<exists>t. abs t \<le> abs x &
```
```   496        cos x =
```
```   497        (\<Sum>m=0..<n. cos_coeff m * 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 x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
```
```   500 apply safe
```
```   501 apply (simp (no_asm))
```
```   502 apply (simp (no_asm) add: cos_expansion_lemma)
```
```   503 apply (case_tac "n", simp)
```
```   504 apply (simp del: setsum_op_ivl_Suc)
```
```   505 apply (rule ccontr, simp)
```
```   506 apply (drule_tac x = x in spec, simp)
```
```   507 apply (erule ssubst)
```
```   508 apply (rule_tac x = t in exI, simp)
```
```   509 apply (rule setsum_cong[OF refl])
```
```   510 apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
```
```   511 done
```
```   512
```
```   513 lemma Maclaurin_cos_expansion2:
```
```   514      "[| 0 < x; n > 0 |] ==>
```
```   515        \<exists>t. 0 < t & t < x &
```
```   516        cos x =
```
```   517        (\<Sum>m=0..<n. cos_coeff m * x ^ m)
```
```   518       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
```
```   519 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)
```
```   520 apply safe
```
```   521 apply simp
```
```   522 apply (simp (no_asm) add: cos_expansion_lemma)
```
```   523 apply (erule ssubst)
```
```   524 apply (rule_tac x = t in exI, simp)
```
```   525 apply (rule setsum_cong[OF refl])
```
```   526 apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
```
```   527 done
```
```   528
```
```   529 lemma Maclaurin_minus_cos_expansion:
```
```   530      "[| x < 0; n > 0 |] ==>
```
```   531        \<exists>t. x < t & t < 0 &
```
```   532        cos x =
```
```   533        (\<Sum>m=0..<n. cos_coeff m * x ^ m)
```
```   534       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
```
```   535 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)
```
```   536 apply safe
```
```   537 apply simp
```
```   538 apply (simp (no_asm) add: cos_expansion_lemma)
```
```   539 apply (erule ssubst)
```
```   540 apply (rule_tac x = t in exI, simp)
```
```   541 apply (rule setsum_cong[OF refl])
```
```   542 apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
```
```   543 done
```
```   544
```
```   545 (* ------------------------------------------------------------------------- *)
```
```   546 (* Version for ln(1 +/- x). Where is it??                                    *)
```
```   547 (* ------------------------------------------------------------------------- *)
```
```   548
```
```   549 lemma sin_bound_lemma:
```
```   550     "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
```
```   551 by auto
```
```   552
```
```   553 lemma Maclaurin_sin_bound:
```
```   554   "abs(sin x - (\<Sum>m=0..<n. sin_coeff m * x ^ m))
```
```   555   \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
```
```   556 proof -
```
```   557   have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
```
```   558     by (rule_tac mult_right_mono,simp_all)
```
```   559   note est = this[simplified]
```
```   560   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)"
```
```   561   have diff_0: "?diff 0 = sin" by simp
```
```   562   have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
```
```   563     apply (clarify)
```
```   564     apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
```
```   565     apply (cut_tac m=m in mod_exhaust_less_4)
```
```   566     apply (safe, auto intro!: DERIV_intros)
```
```   567     done
```
```   568   from Maclaurin_all_le [OF diff_0 DERIV_diff]
```
```   569   obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
```
```   570     t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) +
```
```   571       ?diff n t / real (fact n) * x ^ n" by fast
```
```   572   have diff_m_0:
```
```   573     "\<And>m. ?diff m 0 = (if even m then 0
```
```   574          else -1 ^ ((m - Suc 0) div 2))"
```
```   575     apply (subst even_even_mod_4_iff)
```
```   576     apply (cut_tac m=m in mod_exhaust_less_4)
```
```   577     apply (elim disjE, simp_all)
```
```   578     apply (safe dest!: mod_eqD, simp_all)
```
```   579     done
```
```   580   show ?thesis
```
```   581     unfolding sin_coeff_def
```
```   582     apply (subst t2)
```
```   583     apply (rule sin_bound_lemma)
```
```   584     apply (rule setsum_cong[OF refl])
```
```   585     apply (subst diff_m_0, simp)
```
```   586     apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
```
```   587                 simp add: est mult_nonneg_nonneg mult_ac divide_inverse
```
```   588                           power_abs [symmetric] abs_mult)
```
```   589     done
```
```   590 qed
```
```   591
```
```   592 end
```