src/HOL/MacLaurin.thy
 changeset 56193 c726ecfb22b6 parent 56181 2aa0b19e74f3 child 56238 5d147e1e18d1
```     1.1 --- a/src/HOL/MacLaurin.thy	Tue Mar 18 14:32:23 2014 +0100
1.2 +++ b/src/HOL/MacLaurin.thy	Tue Mar 18 15:53:48 2014 +0100
1.3 @@ -17,10 +17,9 @@
1.4
1.5  lemma Maclaurin_lemma:
1.6      "0 < h ==>
1.7 -     \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
1.8 +     \<exists>B. f h = (\<Sum>m<n. (j m / real (fact m)) * (h^m)) +
1.9                 (B * ((h^n) / real(fact n)))"
1.10 -by (rule exI[where x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
1.11 -                 real(fact n) / (h^n)"]) simp
1.12 +by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / real (fact m)) * h^m)) * real(fact n) / (h^n)"]) simp
1.13
1.14  lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
1.15  by arith
1.16 @@ -33,20 +32,20 @@
1.17    fixes B
1.18    assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1.19      and INIT : "n = Suc k"
1.20 -  defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
1.21 +  defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
1.22      B * (t ^ (n - m) / real (fact (n - m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
1.23    shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
1.24  proof (rule allI impI)+
1.25    fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h"
1.26    have "DERIV (difg m) t :> diff (Suc m) t -
1.27 -    ((\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
1.28 +    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
1.29       real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
1.30      by (auto intro!: DERIV_intros DERIV[rule_format, OF INIT2])
1.31 -      moreover
1.32 +  moreover
1.33    from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
1.34      unfolding atLeast0LessThan[symmetric] by auto
1.35 -  have "(\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
1.36 -      (\<Sum>x = 0..<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
1.37 +  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
1.38 +      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
1.39      unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
1.40    moreover
1.41    have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0"
1.42 @@ -71,29 +70,26 @@
1.43    shows
1.44      "\<exists>t. 0 < t & t < h &
1.45                f h =
1.46 -              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
1.47 +              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {..<n} +
1.48                (diff n t / real (fact n)) * h ^ n"
1.49  proof -
1.50    from n obtain m where m: "n = Suc m"
1.51      by (cases n) (simp add: n)
1.52
1.53    obtain B where f_h: "f h =
1.54 -        (\<Sum>m = 0..<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
1.55 +        (\<Sum>m<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
1.56          B * (h ^ n / real (fact n))"
1.57      using Maclaurin_lemma [OF h] ..
1.58
1.59    def g \<equiv> "(\<lambda>t. f t -
1.60 -    (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {0..<n}
1.61 +    (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {..<n}
1.62        + (B * (t^n / real(fact n)))))"
1.63
1.64    have g2: "g 0 = 0 & g h = 0"
1.65 -    apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
1.66 -    apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
1.67 -    apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
1.68 -    done
1.69 +    by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum_reindex)
1.70
1.71    def difg \<equiv> "(%m t. diff m t -
1.72 -    (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m}
1.73 +    (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..<n-m}
1.74        + (B * ((t ^ (n - m)) / real (fact (n - m))))))"
1.75
1.76    have difg_0: "difg 0 = g"
1.77 @@ -103,14 +99,8 @@
1.78          m < n \<and> (0\<Colon>real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
1.79      using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2)
1.80
1.81 -  have difg_eq_0: "\<forall>m. m < n --> difg m 0 = 0"
1.82 -    apply clarify
1.83 -    apply (simp add: m difg_def)
1.84 -    apply (frule less_iff_Suc_add [THEN iffD1], clarify)
1.85 -    apply (simp del: setsum_op_ivl_Suc)
1.86 -    apply (insert sumr_offset4 [of "Suc 0"])
1.87 -    apply (simp del: setsum_op_ivl_Suc fact_Suc)
1.88 -    done
1.89 +  have difg_eq_0: "\<forall>m<n. difg m 0 = 0"
1.90 +    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum_reindex)
1.91
1.92    have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
1.93      by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
1.94 @@ -166,7 +156,7 @@
1.95      show "0 < t" by fact
1.96      show "t < h" by fact
1.97      show "f h =
1.98 -      (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
1.99 +      (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.100        diff n t / real (fact n) * h ^ n"
1.101        using `difg (Suc m) t = 0`
1.102        by (simp add: m f_h difg_def del: fact_Suc)
1.103 @@ -177,7 +167,7 @@
1.104    "0 < h & n>0 & diff 0 = f &
1.105    (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
1.106     --> (\<exists>t. 0 < t & t < h &
1.107 -            f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.108 +            f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.109                    diff n t / real (fact n) * h ^ n)"
1.110  by (blast intro: Maclaurin)
1.111
1.112 @@ -187,7 +177,7 @@
1.113    and DERIV: "\<forall>m t.
1.114    m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
1.115    shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
1.116 -  (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.117 +  (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.118    diff n t / real (fact n) * h ^ n"
1.119  proof (cases "n")
1.120    case 0 with INIT1 INIT2 show ?thesis by fastforce
1.121 @@ -196,7 +186,7 @@
1.122    hence "n > 0" by simp
1.123    from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
1.124      f h =
1.125 -    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
1.126 +    (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
1.127      by (rule Maclaurin)
1.128    thus ?thesis by fastforce
1.129  qed
1.130 @@ -208,7 +198,7 @@
1.131      --> (\<exists>t. 0 < t &
1.132                t \<le> h &
1.133                f h =
1.134 -              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.135 +              (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.136                diff n t / real (fact n) * h ^ n)"
1.137  by (blast intro: Maclaurin2)
1.138
1.139 @@ -216,7 +206,7 @@
1.140    assumes "h < 0" "0 < n" "diff 0 = f"
1.141    and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
1.142    shows "\<exists>t. h < t & t < 0 &
1.143 -         f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.144 +         f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.145           diff n t / real (fact n) * h ^ n"
1.146  proof -
1.147    txt "Transform @{text ABL'} into @{text DERIV_intros} format."
1.148 @@ -224,7 +214,7 @@
1.149    from assms
1.150    have "\<exists>t>0. t < - h \<and>
1.151      f (- (- h)) =
1.152 -    (\<Sum>m = 0..<n.
1.153 +    (\<Sum>m<n.
1.154      (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
1.155      (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
1.156      by (intro Maclaurin) (auto intro!: DERIV_intros DERIV')
1.157 @@ -233,12 +223,12 @@
1.158    have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
1.159      by (auto simp add: power_mult_distrib[symmetric])
1.160    moreover
1.161 -  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))"
1.162 +  have "(SUM m<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
1.163      by (auto intro: setsum_cong simp add: power_mult_distrib[symmetric])
1.164    ultimately have " h < - t \<and>
1.165      - t < 0 \<and>
1.166      f h =
1.167 -    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
1.168 +    (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
1.169      by auto
1.170    thus ?thesis ..
1.171  qed
1.172 @@ -250,7 +240,7 @@
1.173      --> (\<exists>t. h < t &
1.174                t < 0 &
1.175                f h =
1.176 -              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.177 +              (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.178                diff n t / real (fact n) * h ^ n)"
1.179  by (blast intro: Maclaurin_minus)
1.180
1.181 @@ -262,7 +252,7 @@
1.182  lemma Maclaurin_bi_le_lemma [rule_format]:
1.183    "n>0 \<longrightarrow>
1.184     diff 0 0 =
1.185 -   (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
1.186 +   (\<Sum>m<n. diff m 0 * 0 ^ m / real (fact m)) +
1.187     diff n 0 * 0 ^ n / real (fact n)"
1.188  by (induct "n") auto
1.189
1.190 @@ -271,7 +261,7 @@
1.191     and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
1.192     shows "\<exists>t. abs t \<le> abs x &
1.193                f x =
1.194 -              (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
1.195 +              (\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) +
1.196       diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
1.197  proof cases
1.198    assume "n = 0" with `diff 0 = f` show ?thesis by force
1.199 @@ -303,7 +293,7 @@
1.200    assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
1.201    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
1.202    shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
1.203 -    (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.204 +    (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
1.205                  (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
1.206  proof (cases rule: linorder_cases)
1.207    assume "x = 0" with INIT3 show "?thesis"..
1.208 @@ -327,14 +317,14 @@
1.209        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
1.210        x ~= 0 & n > 0
1.211        --> (\<exists>t. 0 < abs t & abs t < abs x &
1.212 -               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.213 +               f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
1.214                       (diff n t / real (fact n)) * x ^ n)"
1.215  by (blast intro: Maclaurin_all_lt)
1.216
1.217  lemma Maclaurin_zero [rule_format]:
1.218       "x = (0::real)
1.219        ==> n \<noteq> 0 -->
1.220 -          (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
1.221 +          (\<Sum>m<n. (diff m (0::real) / real (fact m)) * x ^ m) =
1.222            diff 0 0"
1.223  by (induct n, auto)
1.224
1.225 @@ -343,7 +333,7 @@
1.226    assumes INIT: "diff 0 = f"
1.227    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
1.228    shows "\<exists>t. abs t \<le> abs x & f x =
1.229 -    (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.230 +    (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
1.231      (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
1.232  proof cases
1.233    assume "n = 0" with INIT show ?thesis by force
1.234 @@ -352,7 +342,7 @@
1.235    show ?thesis
1.236    proof cases
1.237      assume "x = 0"
1.238 -    with `n \<noteq> 0` have "(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
1.239 +    with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
1.240        by (intro Maclaurin_zero) auto
1.241      with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force
1.242      thus ?thesis ..
1.243 @@ -369,7 +359,7 @@
1.244  lemma Maclaurin_all_le_objl: "diff 0 = f &
1.245        (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
1.246        --> (\<exists>t. abs t \<le> abs x &
1.247 -              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.248 +              f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
1.249                      (diff n t / real (fact n)) * x ^ n)"
1.250  by (blast intro: Maclaurin_all_le)
1.251
1.252 @@ -379,14 +369,14 @@
1.253  lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
1.254        ==> (\<exists>t. 0 < abs t &
1.255                  abs t < abs x &
1.256 -                exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
1.257 +                exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
1.258                          (exp t / real (fact n)) * x ^ n)"
1.259  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
1.260
1.261
1.262  lemma Maclaurin_exp_le:
1.263       "\<exists>t. abs t \<le> abs x &
1.264 -            exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
1.265 +            exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
1.266                         (exp t / real (fact n)) * x ^ n"
1.267  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
1.268
1.269 @@ -420,7 +410,7 @@
1.270  lemma Maclaurin_sin_expansion2:
1.271       "\<exists>t. abs t \<le> abs x &
1.272         sin x =
1.273 -       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
1.274 +       (\<Sum>m<n. sin_coeff m * x ^ m)
1.275        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.276  apply (cut_tac f = sin and n = n and x = x
1.277          and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
1.278 @@ -440,7 +430,7 @@
1.279
1.280  lemma Maclaurin_sin_expansion:
1.281       "\<exists>t. sin x =
1.282 -       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
1.283 +       (\<Sum>m<n. sin_coeff m * x ^ m)
1.284        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.285  apply (insert Maclaurin_sin_expansion2 [of x n])
1.286  apply (blast intro: elim:)
1.287 @@ -450,7 +440,7 @@
1.288       "[| n > 0; 0 < x |] ==>
1.289         \<exists>t. 0 < t & t < x &
1.290         sin x =
1.291 -       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
1.292 +       (\<Sum>m<n. sin_coeff m * x ^ m)
1.293        + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
1.294  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)
1.295  apply safe
1.296 @@ -467,7 +457,7 @@
1.297       "0 < x ==>
1.298         \<exists>t. 0 < t & t \<le> x &
1.299         sin x =
1.300 -       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
1.301 +       (\<Sum>m<n. sin_coeff m * x ^ m)
1.302        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.303  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)
1.304  apply safe
1.305 @@ -484,7 +474,7 @@
1.306  subsection{*Maclaurin Expansion for Cosine Function*}
1.307
1.308  lemma sumr_cos_zero_one [simp]:
1.309 -  "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
1.310 +  "(\<Sum>m<(Suc n). cos_coeff m * 0 ^ m) = 1"
1.311  by (induct "n", auto)
1.312
1.313  lemma cos_expansion_lemma:
1.314 @@ -494,14 +484,14 @@
1.315  lemma Maclaurin_cos_expansion:
1.316       "\<exists>t. abs t \<le> abs x &
1.317         cos x =
1.318 -       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
1.319 +       (\<Sum>m<n. cos_coeff m * x ^ m)
1.320        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.321  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)
1.322  apply safe
1.323  apply (simp (no_asm))
1.324  apply (simp (no_asm) add: cos_expansion_lemma)
1.325  apply (case_tac "n", simp)
1.326 -apply (simp del: setsum_op_ivl_Suc)
1.327 +apply (simp del: setsum_lessThan_Suc)
1.328  apply (rule ccontr, simp)
1.329  apply (drule_tac x = x in spec, simp)
1.330  apply (erule ssubst)
1.331 @@ -514,7 +504,7 @@
1.332       "[| 0 < x; n > 0 |] ==>
1.333         \<exists>t. 0 < t & t < x &
1.334         cos x =
1.335 -       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
1.336 +       (\<Sum>m<n. cos_coeff m * x ^ m)
1.337        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.338  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)
1.339  apply safe
1.340 @@ -530,7 +520,7 @@
1.341       "[| x < 0; n > 0 |] ==>
1.342         \<exists>t. x < t & t < 0 &
1.343         cos x =
1.344 -       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
1.345 +       (\<Sum>m<n. cos_coeff m * x ^ m)
1.346        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.347  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)
1.348  apply safe
1.349 @@ -551,7 +541,7 @@
1.350  by auto
1.351
1.352  lemma Maclaurin_sin_bound:
1.353 -  "abs(sin x - (\<Sum>m=0..<n. sin_coeff m * x ^ m))
1.354 +  "abs(sin x - (\<Sum>m<n. sin_coeff m * x ^ m))
1.355    \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
1.356  proof -
1.357    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
1.358 @@ -567,7 +557,7 @@
1.359      done
1.360    from Maclaurin_all_le [OF diff_0 DERIV_diff]
1.361    obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
1.362 -    t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) +
1.363 +    t2: "sin x = (\<Sum>m<n. ?diff m 0 / real (fact m) * x ^ m) +
1.364        ?diff n t / real (fact n) * x ^ n" by fast
1.365    have diff_m_0:
1.366      "\<And>m. ?diff m 0 = (if even m then 0
```