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