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