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