src/HOL/MacLaurin.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (21 months ago)
changeset 66983 df83b66f1d94
parent 65273 917ae0ba03a2
child 67091 1393c2340eec
permissions -rw-r--r--
proper merge (amending fb46c031c841);
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))"
nipkow@64267
    51
    unfolding intvl by (subst sum.insert) (auto simp add: sum.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>
nipkow@64267
    72
      f h = sum (\<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 =
nipkow@64267
    82
    f t - (sum (\<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"
nipkow@64267
    84
    by (simp_all add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 sum.reindex)
huffman@29187
    85
wenzelm@63040
    86
  define difg where [abs_def]: "difg m t =
nipkow@64267
    87
    diff m t - (sum (\<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"
nipkow@64267
    94
    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff sum.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)"
nipkow@64267
   201
    by (auto intro: sum.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
lp15@65273
   362
corollary 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
lp15@65273
   366
corollary ln_2_less_1: "ln 2 < (1::real)"
lp15@65273
   367
proof -
lp15@65273
   368
  have "2 < 5/(2::real)" by simp
lp15@65273
   369
  also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
lp15@65273
   370
  finally have "exp (ln 2) < exp (1::real)" by simp
lp15@65273
   371
  thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
lp15@65273
   372
qed
wenzelm@63569
   373
wenzelm@63569
   374
subsection \<open>Version for Sine Function\<close>
paulson@15079
   375
wenzelm@63569
   376
lemma mod_exhaust_less_4: "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = 3"
wenzelm@63569
   377
  for m :: nat
wenzelm@63569
   378
  by auto
wenzelm@63569
   379
wenzelm@63569
   380
lemma Suc_Suc_mult_two_diff_two [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (Suc (2 * n - 2)) = 2 * n"
wenzelm@63569
   381
  by (induct n) auto
wenzelm@63569
   382
wenzelm@63569
   383
lemma lemma_Suc_Suc_4n_diff_2 [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (Suc (4 * n - 2)) = 4 * n"
wenzelm@63569
   384
  by (induct n) auto
wenzelm@63569
   385
wenzelm@63569
   386
lemma Suc_mult_two_diff_one [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (2 * n - 1) = 2 * n"
wenzelm@63569
   387
  by (induct n) auto
lp15@60017
   388
paulson@15079
   389
wenzelm@63569
   390
text \<open>It is unclear why so many variant results are needed.\<close>
paulson@15079
   391
wenzelm@63569
   392
lemma sin_expansion_lemma: "sin (x + real (Suc m) * pi / 2) = cos (x + real m * pi / 2)"
wenzelm@63569
   393
  by (auto simp: cos_add sin_add add_divide_distrib distrib_right)
huffman@36974
   394
paulson@15079
   395
lemma Maclaurin_sin_expansion2:
wenzelm@63569
   396
  "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
wenzelm@63569
   397
    sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
wenzelm@63569
   398
  using Maclaurin_all_lt_objl
wenzelm@63569
   399
    [where f = sin and n = n and x = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
wenzelm@63569
   400
  apply safe
wenzelm@63569
   401
      apply simp
wenzelm@63569
   402
     apply (simp add: sin_expansion_lemma del: of_nat_Suc)
wenzelm@63569
   403
     apply (force intro!: derivative_eq_intros)
nipkow@64267
   404
    apply (subst (asm) sum.neutral; auto)
wenzelm@63569
   405
   apply (rule ccontr)
wenzelm@63569
   406
   apply simp
wenzelm@63569
   407
   apply (drule_tac x = x in spec)
wenzelm@63569
   408
   apply simp
wenzelm@63569
   409
  apply (erule ssubst)
wenzelm@63569
   410
  apply (rule_tac x = t in exI)
wenzelm@63569
   411
  apply simp
nipkow@64267
   412
  apply (rule sum.cong[OF refl])
wenzelm@63569
   413
  apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
wenzelm@63569
   414
  done
paulson@15079
   415
paulson@15234
   416
lemma Maclaurin_sin_expansion:
wenzelm@63569
   417
  "\<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
   418
  using Maclaurin_sin_expansion2 [of x n] by blast
paulson@15234
   419
paulson@15079
   420
lemma Maclaurin_sin_expansion3:
wenzelm@63569
   421
  "n > 0 \<Longrightarrow> 0 < x \<Longrightarrow>
wenzelm@63569
   422
    \<exists>t. 0 < t \<and> t < x \<and>
wenzelm@63569
   423
       sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
wenzelm@63569
   424
  using Maclaurin_objl
wenzelm@63569
   425
    [where f = sin and n = n and h = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
wenzelm@63569
   426
  apply safe
wenzelm@63569
   427
    apply simp
wenzelm@63569
   428
   apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
wenzelm@63569
   429
   apply (force intro!: derivative_eq_intros)
wenzelm@63569
   430
  apply (erule ssubst)
wenzelm@63569
   431
  apply (rule_tac x = t in exI)
wenzelm@63569
   432
  apply simp
nipkow@64267
   433
  apply (rule sum.cong[OF refl])
wenzelm@63569
   434
  apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
wenzelm@63569
   435
  done
wenzelm@63569
   436
wenzelm@63569
   437
lemma Maclaurin_sin_expansion4:
wenzelm@63569
   438
  "0 < x \<Longrightarrow>
wenzelm@63569
   439
    \<exists>t. 0 < t \<and> t \<le> x \<and>
wenzelm@63569
   440
      sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
wenzelm@63569
   441
  using Maclaurin2_objl
wenzelm@63569
   442
    [where f = sin and n = n and h = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
wenzelm@63569
   443
  apply safe
lp15@61284
   444
    apply simp
lp15@61609
   445
   apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
lp15@61284
   446
   apply (force intro!: derivative_eq_intros)
lp15@61284
   447
  apply (erule ssubst)
wenzelm@63569
   448
  apply (rule_tac x = t in exI)
wenzelm@63569
   449
  apply simp
nipkow@64267
   450
  apply (rule sum.cong[OF refl])
wenzelm@63569
   451
  apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
wenzelm@63569
   452
  done
paulson@15079
   453
paulson@15079
   454
wenzelm@63569
   455
subsection \<open>Maclaurin Expansion for Cosine Function\<close>
paulson@15079
   456
wenzelm@63569
   457
lemma sumr_cos_zero_one [simp]: "(\<Sum>m<Suc n. cos_coeff m * 0 ^ m) = 1"
wenzelm@63569
   458
  by (induct n) auto
paulson@15079
   459
wenzelm@63569
   460
lemma cos_expansion_lemma: "cos (x + real (Suc m) * pi / 2) = - sin (x + real m * pi / 2)"
wenzelm@63569
   461
  by (auto simp: cos_add sin_add distrib_right add_divide_distrib)
huffman@36974
   462
paulson@15079
   463
lemma Maclaurin_cos_expansion:
wenzelm@63569
   464
  "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
wenzelm@63569
   465
    cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos(t + 1/2 * real n * pi) / fact n) * x ^ n"
wenzelm@63569
   466
  using Maclaurin_all_lt_objl
wenzelm@63569
   467
    [where f = cos and n = n and x = x and diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"]
wenzelm@63569
   468
  apply safe
wenzelm@63569
   469
      apply simp
wenzelm@63569
   470
     apply (simp add: cos_expansion_lemma del: of_nat_Suc)
wenzelm@63569
   471
    apply (cases n)
wenzelm@63569
   472
     apply simp
nipkow@64267
   473
    apply (simp del: sum_lessThan_Suc)
wenzelm@63569
   474
   apply (rule ccontr)
wenzelm@63569
   475
   apply simp
wenzelm@63569
   476
   apply (drule_tac x = x in spec)
wenzelm@63569
   477
   apply simp
wenzelm@63569
   478
  apply (erule ssubst)
wenzelm@63569
   479
  apply (rule_tac x = t in exI)
wenzelm@63569
   480
  apply simp
nipkow@64267
   481
  apply (rule sum.cong[OF refl])
wenzelm@63569
   482
  apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
wenzelm@63569
   483
  done
paulson@15079
   484
paulson@15079
   485
lemma Maclaurin_cos_expansion2:
wenzelm@63569
   486
  "0 < x \<Longrightarrow> n > 0 \<Longrightarrow>
wenzelm@63569
   487
    \<exists>t. 0 < t \<and> t < x \<and>
wenzelm@63569
   488
      cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos (t + 1/2 * real n * pi) / fact n) * x ^ n"
wenzelm@63569
   489
  using Maclaurin_objl
wenzelm@63569
   490
    [where f = cos and n = n and h = x and diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"]
wenzelm@63569
   491
  apply safe
wenzelm@63569
   492
    apply simp
wenzelm@63569
   493
   apply (simp add: cos_expansion_lemma del: of_nat_Suc)
wenzelm@63569
   494
  apply (erule ssubst)
wenzelm@63569
   495
  apply (rule_tac x = t in exI)
lp15@61284
   496
  apply simp
nipkow@64267
   497
  apply (rule sum.cong[OF refl])
wenzelm@63569
   498
  apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
wenzelm@63569
   499
  done
paulson@15079
   500
paulson@15234
   501
lemma Maclaurin_minus_cos_expansion:
wenzelm@63569
   502
  "x < 0 \<Longrightarrow> n > 0 \<Longrightarrow>
wenzelm@63569
   503
    \<exists>t. x < t \<and> t < 0 \<and>
wenzelm@63569
   504
      cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + ((cos (t + 1/2 * real n * pi) / fact n) * x ^ n)"
wenzelm@63569
   505
  using Maclaurin_minus_objl
wenzelm@63569
   506
    [where f = cos and n = n and h = x and diff = "\<lambda>n x. cos (x + 1/2 * real n *pi)"]
wenzelm@63569
   507
  apply safe
wenzelm@63569
   508
    apply simp
wenzelm@63569
   509
   apply (simp add: cos_expansion_lemma del: of_nat_Suc)
wenzelm@63569
   510
  apply (erule ssubst)
wenzelm@63569
   511
  apply (rule_tac x = t in exI)
lp15@61284
   512
  apply simp
nipkow@64267
   513
  apply (rule sum.cong[OF refl])
wenzelm@63569
   514
  apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
wenzelm@63569
   515
  done
wenzelm@63569
   516
paulson@15079
   517
wenzelm@63569
   518
(* Version for ln(1 +/- x). Where is it?? *)
wenzelm@63569
   519
paulson@15079
   520
wenzelm@63569
   521
lemma sin_bound_lemma: "x = y \<Longrightarrow> \<bar>u\<bar> \<le> v \<Longrightarrow> \<bar>(x + u) - y\<bar> \<le> v"
wenzelm@63569
   522
  for x y u v :: real
wenzelm@63569
   523
  by auto
paulson@15079
   524
wenzelm@63569
   525
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
   526
proof -
wenzelm@63569
   527
  have est: "x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" for x y :: real
wenzelm@63569
   528
    by (rule mult_right_mono) simp_all
wenzelm@63569
   529
  let ?diff = "\<lambda>(n::nat) x.
wenzelm@63569
   530
    if n mod 4 = 0 then sin x
wenzelm@63569
   531
    else if n mod 4 = 1 then cos x
wenzelm@63569
   532
    else if n mod 4 = 2 then - sin x
wenzelm@63569
   533
    else - cos x"
huffman@22985
   534
  have diff_0: "?diff 0 = sin" by simp
huffman@22985
   535
  have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
wenzelm@63569
   536
    apply clarify
huffman@22985
   537
    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
huffman@22985
   538
    apply (cut_tac m=m in mod_exhaust_less_4)
wenzelm@63569
   539
    apply safe
wenzelm@63569
   540
       apply (auto intro!: derivative_eq_intros)
huffman@22985
   541
    done
huffman@22985
   542
  from Maclaurin_all_le [OF diff_0 DERIV_diff]
wenzelm@63569
   543
  obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>"
wenzelm@63569
   544
    and t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / (fact n) * x ^ n"
wenzelm@63569
   545
    by fast
wenzelm@63569
   546
  have diff_m_0: "\<And>m. ?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))"
huffman@22985
   547
    apply (subst even_even_mod_4_iff)
huffman@22985
   548
    apply (cut_tac m=m in mod_exhaust_less_4)
wenzelm@63569
   549
    apply (elim disjE)
wenzelm@63569
   550
       apply simp_all
wenzelm@63569
   551
     apply (safe dest!: mod_eqD)
wenzelm@63569
   552
     apply simp_all
huffman@22985
   553
    done
obua@14738
   554
  show ?thesis
huffman@44306
   555
    unfolding sin_coeff_def
huffman@22985
   556
    apply (subst t2)
paulson@15079
   557
    apply (rule sin_bound_lemma)
nipkow@64267
   558
     apply (rule sum.cong[OF refl])
wenzelm@63569
   559
     apply (subst diff_m_0, simp)
wenzelm@63569
   560
    using est
paulson@15079
   561
    apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
wenzelm@63569
   562
        simp: ac_simps divide_inverse power_abs [symmetric] abs_mult)
obua@14738
   563
    done
obua@14738
   564
qed
obua@14738
   565
wenzelm@63570
   566
wenzelm@63570
   567
section \<open>Taylor series\<close>
wenzelm@63570
   568
wenzelm@63570
   569
text \<open>
wenzelm@63570
   570
  We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
wenzelm@63570
   571
  to prove Taylor's theorem.
wenzelm@63570
   572
\<close>
wenzelm@63570
   573
wenzelm@63570
   574
lemma taylor_up:
wenzelm@63570
   575
  assumes INIT: "n > 0" "diff 0 = f"
wenzelm@63570
   576
    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
   577
    and INTERV: "a \<le> c" "c < b"
wenzelm@63570
   578
  shows "\<exists>t::real. c < t \<and> t < b \<and>
wenzelm@63570
   579
    f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n"
wenzelm@63570
   580
proof -
wenzelm@63570
   581
  from INTERV have "0 < b - c" by arith
wenzelm@63570
   582
  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
wenzelm@63570
   583
    by auto
wenzelm@63570
   584
  moreover
wenzelm@63570
   585
  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
   586
  proof (intro strip)
wenzelm@63570
   587
    fix m t
wenzelm@63570
   588
    assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c"
wenzelm@63570
   589
    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
wenzelm@63570
   590
      by auto
wenzelm@63570
   591
    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
wenzelm@63570
   592
      by (rule DERIV_add)
wenzelm@63570
   593
    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
wenzelm@63570
   594
      by (rule DERIV_chain2)
wenzelm@63570
   595
    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
wenzelm@63570
   596
      by simp
wenzelm@63570
   597
  qed
wenzelm@63570
   598
  ultimately obtain x where
wenzelm@63570
   599
    "0 < x \<and> x < b - c \<and>
wenzelm@63570
   600
      f (b - c + c) =
wenzelm@63570
   601
        (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
wenzelm@63570
   602
     by (rule Maclaurin [THEN exE])
wenzelm@63570
   603
   then have "c < x + c \<and> x + c < b \<and> f b =
wenzelm@63570
   604
     (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
wenzelm@63570
   605
    by fastforce
wenzelm@63570
   606
  then show ?thesis by fastforce
wenzelm@63570
   607
qed
wenzelm@63570
   608
wenzelm@63570
   609
lemma taylor_down:
wenzelm@63570
   610
  fixes a :: real and n :: nat
wenzelm@63570
   611
  assumes INIT: "n > 0" "diff 0 = f"
wenzelm@63570
   612
    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
   613
    and INTERV: "a < c" "c \<le> b"
wenzelm@63570
   614
  shows "\<exists>t. a < t \<and> t < c \<and>
wenzelm@63570
   615
    f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n"
wenzelm@63570
   616
proof -
wenzelm@63570
   617
  from INTERV have "a-c < 0" by arith
wenzelm@63570
   618
  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
wenzelm@63570
   619
    by auto
wenzelm@63570
   620
  moreover
wenzelm@63570
   621
  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
   622
  proof (rule allI impI)+
wenzelm@63570
   623
    fix m t
wenzelm@63570
   624
    assume "m < n \<and> a - c \<le> t \<and> t \<le> 0"
wenzelm@63570
   625
    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
wenzelm@63570
   626
      by auto
wenzelm@63570
   627
    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
wenzelm@63570
   628
      by (rule DERIV_add)
wenzelm@63570
   629
    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
wenzelm@63570
   630
      by (rule DERIV_chain2)
wenzelm@63570
   631
    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
wenzelm@63570
   632
      by simp
wenzelm@63570
   633
  qed
wenzelm@63570
   634
  ultimately obtain x where
wenzelm@63570
   635
    "a - c < x \<and> x < 0 \<and>
wenzelm@63570
   636
      f (a - c + c) =
wenzelm@63570
   637
        (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
wenzelm@63570
   638
    by (rule Maclaurin_minus [THEN exE])
wenzelm@63570
   639
  then have "a < x + c \<and> x + c < c \<and>
wenzelm@63570
   640
    f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
wenzelm@63570
   641
    by fastforce
wenzelm@63570
   642
  then show ?thesis by fastforce
wenzelm@63570
   643
qed
wenzelm@63570
   644
wenzelm@63570
   645
theorem taylor:
wenzelm@63570
   646
  fixes a :: real and n :: nat
wenzelm@63570
   647
  assumes INIT: "n > 0" "diff 0 = f"
wenzelm@63570
   648
    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
   649
    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
wenzelm@63570
   650
  shows "\<exists>t.
wenzelm@63570
   651
    (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and>
wenzelm@63570
   652
    f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n"
wenzelm@63570
   653
proof (cases "x < c")
wenzelm@63570
   654
  case True
wenzelm@63570
   655
  note INIT
wenzelm@63570
   656
  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
   657
    using DERIV and INTERV by fastforce
wenzelm@63570
   658
  moreover note True
wenzelm@63570
   659
  moreover from INTERV have "c \<le> b"
wenzelm@63570
   660
    by simp
wenzelm@63570
   661
  ultimately have "\<exists>t>x. t < c \<and> f x =
wenzelm@63570
   662
    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
wenzelm@63570
   663
    by (rule taylor_down)
wenzelm@63570
   664
  with True show ?thesis by simp
wenzelm@63570
   665
next
wenzelm@63570
   666
  case False
wenzelm@63570
   667
  note INIT
wenzelm@63570
   668
  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
   669
    using DERIV and INTERV by fastforce
wenzelm@63570
   670
  moreover from INTERV have "a \<le> c"
wenzelm@63570
   671
    by arith
wenzelm@63570
   672
  moreover from False and INTERV have "c < x"
wenzelm@63570
   673
    by arith
wenzelm@63570
   674
  ultimately have "\<exists>t>c. t < x \<and> f x =
wenzelm@63570
   675
    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
wenzelm@63570
   676
    by (rule taylor_up)
wenzelm@63570
   677
  with False show ?thesis by simp
wenzelm@63570
   678
qed
wenzelm@63570
   679
paulson@15079
   680
end