src/HOL/MacLaurin.thy
author bulwahn
Wed Dec 15 08:34:01 2010 +0100 (2010-12-15)
changeset 41120 74e41b2d48ea
parent 36974 b877866b5b00
child 41166 4b2a457b17e8
permissions -rw-r--r--
adding an Isar version of the MacLaurin theorem from some students' work in 2005
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
paulson@15944
     7
header{*MacLaurin Series*}
paulson@15944
     8
nipkow@15131
     9
theory MacLaurin
chaieb@29811
    10
imports Transcendental
nipkow@15131
    11
begin
paulson@15079
    12
paulson@15079
    13
subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
paulson@15079
    14
paulson@15079
    15
text{*This is a very long, messy proof even now that it's been broken down
paulson@15079
    16
into lemmas.*}
paulson@15079
    17
paulson@15079
    18
lemma Maclaurin_lemma:
paulson@15079
    19
    "0 < h ==>
nipkow@15539
    20
     \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
paulson@15079
    21
               (B * ((h^n) / real(fact n)))"
bulwahn@41120
    22
by (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
paulson@15079
    23
                 real(fact n) / (h^n)"
bulwahn@41120
    24
       in exI, simp)
paulson@15079
    25
paulson@15079
    26
lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
paulson@15079
    27
by arith
paulson@15079
    28
avigad@32038
    29
lemma fact_diff_Suc [rule_format]:
avigad@32038
    30
  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
avigad@32038
    31
  by (subst fact_reduce_nat, auto)
avigad@32038
    32
paulson@15079
    33
lemma Maclaurin_lemma2:
bulwahn@41120
    34
  assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
bulwahn@41120
    35
  and INIT : "n = Suc k"
bulwahn@41120
    36
  and DIFG_DEF: "difg = (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) + 
bulwahn@41120
    37
  B * (t ^ (n - m) / real (fact (n - m)))))"
bulwahn@41120
    38
  shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
bulwahn@41120
    39
proof (rule allI)+
bulwahn@41120
    40
  fix m
bulwahn@41120
    41
  fix t
bulwahn@41120
    42
  show "m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
bulwahn@41120
    43
  proof
bulwahn@41120
    44
    assume INIT2: "m < n & 0 \<le> t & t \<le> h"
bulwahn@41120
    45
    hence INTERV: "0 \<le> t & t \<le> h" ..
bulwahn@41120
    46
    from INIT2 and INIT have mtok: "m < Suc k" by arith
bulwahn@41120
    47
    have "DERIV (\<lambda>t. diff m t -
bulwahn@41120
    48
    ((\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * t ^ p) +
bulwahn@41120
    49
    B * (t ^ (Suc k - m) / real (fact (Suc k - m)))))
bulwahn@41120
    50
    t :> diff (Suc m) t -
bulwahn@41120
    51
    ((\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
bulwahn@41120
    52
    B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))))"
bulwahn@41120
    53
    proof -
bulwahn@41120
    54
      from DERIV and INIT2 have "DERIV (diff m) t :> diff (Suc m) t" by simp
bulwahn@41120
    55
      moreover
bulwahn@41120
    56
      have " DERIV (\<lambda>x. (\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) +
bulwahn@41120
    57
	B * (x ^ (Suc k - m) / real (fact (Suc k - m))))
bulwahn@41120
    58
	t :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
bulwahn@41120
    59
	B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
bulwahn@41120
    60
      proof -
bulwahn@41120
    61
	have "DERIV (\<lambda>x. \<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) t
bulwahn@41120
    62
	  :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p)"
bulwahn@41120
    63
	proof -
bulwahn@41120
    64
	  have "\<exists> d. k = m + d"
bulwahn@41120
    65
	  proof -
bulwahn@41120
    66
	    from INIT2 have "m < n" ..
bulwahn@41120
    67
	    hence "\<exists> d. n = m + d + Suc 0" by arith
bulwahn@41120
    68
	    with INIT show ?thesis by (simp del: setsum_op_ivl_Suc)
bulwahn@41120
    69
	  qed
bulwahn@41120
    70
	  from this obtain d where kmd: "k = m + d" ..
bulwahn@41120
    71
	  have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) +
bulwahn@41120
    72
            diff m 0)
bulwahn@41120
    73
	    t :> (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"
bulwahn@41120
    74
	    
bulwahn@41120
    75
	  proof - 
bulwahn@41120
    76
	    have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) + diff m 0) t :>  (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0"
bulwahn@41120
    77
	    proof -
bulwahn@41120
    78
	      from DERIV and INTERV have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma)))) t :>  (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r))"
bulwahn@41120
    79
	      proof -
bulwahn@41120
    80
		have "\<forall>r. 0 \<le> r \<and> r < 0 + d \<longrightarrow>
bulwahn@41120
    81
		  DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
bulwahn@41120
    82
		  :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
bulwahn@41120
    83
		proof (rule allI)
bulwahn@41120
    84
		  fix r
bulwahn@41120
    85
		  show " 0 \<le> r \<and> r < 0 + d \<longrightarrow>
bulwahn@41120
    86
		    DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
bulwahn@41120
    87
		    :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
bulwahn@41120
    88
		  proof 
bulwahn@41120
    89
		    assume "0 \<le> r & r < 0 + d"
bulwahn@41120
    90
		    have "DERIV (\<lambda>x. diff (Suc (m + r)) 0 *
bulwahn@41120
    91
                      (x ^ Suc r * inverse (real (fact (Suc r)))))
bulwahn@41120
    92
		      t :> diff (Suc (m + r)) 0 * (t ^ r * inverse (real (fact r)))"
bulwahn@41120
    93
		    proof -
bulwahn@41120
    94
                      have "(1 + real r) * real (fact r) \<noteq> 0" by auto
bulwahn@41120
    95
		      from this have "real (fact r) + real r * real (fact r) \<noteq> 0"
bulwahn@41120
    96
                        by (metis add_nonneg_eq_0_iff mult_nonneg_nonneg real_of_nat_fact_not_zero real_of_nat_ge_zero)
bulwahn@41120
    97
                      from this have "DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t :> real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
bulwahn@41120
    98
			0 * t ^ Suc r"
bulwahn@41120
    99
                        apply - by ( rule DERIV_intros | rule refl)+ auto
bulwahn@41120
   100
		      moreover
bulwahn@41120
   101
		      have "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
bulwahn@41120
   102
			0 * t ^ Suc r =
bulwahn@41120
   103
			t ^ r * inverse (real (fact r))"
bulwahn@41120
   104
		      proof -
bulwahn@41120
   105
			
bulwahn@41120
   106
			have " real (Suc r) * t ^ (Suc r - Suc 0) *
bulwahn@41120
   107
			  inverse (real (Suc r) * real (fact r)) +
bulwahn@41120
   108
			  0 * t ^ Suc r =
bulwahn@41120
   109
			  t ^ r * inverse (real (fact r))" by (simp add: mult_ac)
bulwahn@41120
   110
			hence "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (Suc r * fact r)) +
bulwahn@41120
   111
			  0 * t ^ Suc r =
bulwahn@41120
   112
			  t ^ r * inverse (real (fact r))" by (subst real_of_nat_mult)
bulwahn@41120
   113
			thus ?thesis by (subst fact_Suc)
bulwahn@41120
   114
		      qed
bulwahn@41120
   115
		      ultimately have " DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t
bulwahn@41120
   116
			:> t ^ r * inverse (real (fact r))" by (rule lemma_DERIV_subst)
bulwahn@41120
   117
		      thus ?thesis by (rule DERIV_cmult)
bulwahn@41120
   118
		    qed
bulwahn@41120
   119
		    thus "DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r /
bulwahn@41120
   120
                      real (fact (Suc r)))
bulwahn@41120
   121
		      t :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)" by (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
bulwahn@41120
   122
		  qed
bulwahn@41120
   123
		qed
bulwahn@41120
   124
		thus ?thesis by (rule DERIV_sumr)
bulwahn@41120
   125
	      qed
bulwahn@41120
   126
	      moreover
bulwahn@41120
   127
	      from DERIV_const have "DERIV (\<lambda>x. diff m 0) t :> 0" .
bulwahn@41120
   128
	      ultimately show ?thesis by (rule DERIV_add)
bulwahn@41120
   129
	    qed
bulwahn@41120
   130
	    moreover
bulwahn@41120
   131
	    have " (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0 =  (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"  by simp
bulwahn@41120
   132
	    ultimately show ?thesis by (rule lemma_DERIV_subst)
bulwahn@41120
   133
	  qed
bulwahn@41120
   134
	  with kmd and sumr_offset4 [of 1] show ?thesis by (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
bulwahn@41120
   135
	qed
bulwahn@41120
   136
	moreover
bulwahn@41120
   137
	have " DERIV (\<lambda>x. B * (x ^ (Suc k - m) / real (fact (Suc k - m)))) t
bulwahn@41120
   138
	  :> B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
bulwahn@41120
   139
	proof -
bulwahn@41120
   140
	  have " DERIV (\<lambda>x. x ^ (Suc k - m) / real (fact (Suc k - m))) t
bulwahn@41120
   141
	    :> t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))"
bulwahn@41120
   142
	  proof -
bulwahn@41120
   143
	    have "DERIV (\<lambda>x. x ^ (Suc k - m)) t :> real (Suc k - m) * t ^ (Suc k - m - Suc 0)" by (rule DERIV_pow)
bulwahn@41120
   144
	    moreover
bulwahn@41120
   145
	    have "DERIV (\<lambda>x. real (fact (Suc k - m))) t :> 0" by (rule DERIV_const)
bulwahn@41120
   146
	    moreover
bulwahn@41120
   147
	    have "(\<lambda>x. real (fact (Suc k - m))) t \<noteq> 0" by simp
bulwahn@41120
   148
	    ultimately have " DERIV (\<lambda>y. y ^ (Suc k - m) / real (fact (Suc k - m))) t
bulwahn@41120
   149
	      :>  ( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
bulwahn@41120
   150
	      real (fact (Suc k - m)) ^ Suc (Suc 0)"
bulwahn@41120
   151
              apply -
bulwahn@41120
   152
              apply (rule DERIV_cong) by (rule DERIV_intros | rule refl)+ auto
bulwahn@41120
   153
	    moreover
bulwahn@41120
   154
	    from mtok and INIT have "( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
bulwahn@41120
   155
	      real (fact (Suc k - m)) ^ Suc (Suc 0) =  t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))" by (simp add: fact_diff_Suc)
bulwahn@41120
   156
	    ultimately show ?thesis by (rule lemma_DERIV_subst)
bulwahn@41120
   157
	  qed
bulwahn@41120
   158
	  moreover
bulwahn@41120
   159
	  thus ?thesis by (rule DERIV_cmult)
bulwahn@41120
   160
	qed
bulwahn@41120
   161
	ultimately show ?thesis by (rule DERIV_add)
bulwahn@41120
   162
      qed
bulwahn@41120
   163
      ultimately show ?thesis by (rule DERIV_diff) 
bulwahn@41120
   164
    qed
bulwahn@41120
   165
    from INIT and this and DIFG_DEF show "DERIV (difg m) t :> difg (Suc m) t" by clarify
bulwahn@41120
   166
  qed
bulwahn@41120
   167
qed
avigad@32038
   168
paulson@15079
   169
paulson@15079
   170
lemma Maclaurin:
huffman@29187
   171
  assumes h: "0 < h"
huffman@29187
   172
  assumes n: "0 < n"
huffman@29187
   173
  assumes diff_0: "diff 0 = f"
huffman@29187
   174
  assumes diff_Suc:
huffman@29187
   175
    "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
huffman@29187
   176
  shows
huffman@29187
   177
    "\<exists>t. 0 < t & t < h &
paulson@15079
   178
              f h =
nipkow@15539
   179
              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
bulwahn@41120
   180
              (diff n t / real (fact n)) * h ^ n"  
huffman@29187
   181
proof -
huffman@29187
   182
  from n obtain m where m: "n = Suc m"
huffman@29187
   183
    by (cases n, simp add: n)
huffman@29187
   184
huffman@29187
   185
  obtain B where f_h: "f h =
huffman@29187
   186
        (\<Sum>m = 0..<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
huffman@29187
   187
        B * (h ^ n / real (fact n))"
huffman@29187
   188
    using Maclaurin_lemma [OF h] ..
huffman@29187
   189
huffman@29187
   190
  obtain g where g_def: "g = (%t. f t -
huffman@29187
   191
    (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n}
huffman@29187
   192
      + (B * (t^n / real(fact n)))))" by blast
huffman@29187
   193
huffman@29187
   194
  have g2: "g 0 = 0 & g h = 0"
huffman@29187
   195
    apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
huffman@30082
   196
    apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
huffman@29187
   197
    apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
huffman@29187
   198
    done
huffman@29187
   199
huffman@29187
   200
  obtain difg where difg_def: "difg = (%m t. diff m t -
huffman@29187
   201
    (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m}
huffman@29187
   202
      + (B * ((t ^ (n - m)) / real (fact (n - m))))))" by blast
huffman@29187
   203
huffman@29187
   204
  have difg_0: "difg 0 = g"
huffman@29187
   205
    unfolding difg_def g_def by (simp add: diff_0)
huffman@29187
   206
huffman@29187
   207
  have difg_Suc: "\<forall>(m\<Colon>nat) t\<Colon>real.
huffman@29187
   208
        m < n \<and> (0\<Colon>real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
huffman@29187
   209
    using diff_Suc m difg_def by (rule Maclaurin_lemma2)
huffman@29187
   210
huffman@29187
   211
  have difg_eq_0: "\<forall>m. m < n --> difg m 0 = 0"
huffman@29187
   212
    apply clarify
huffman@29187
   213
    apply (simp add: m difg_def)
huffman@29187
   214
    apply (frule less_iff_Suc_add [THEN iffD1], clarify)
huffman@29187
   215
    apply (simp del: setsum_op_ivl_Suc)
huffman@30082
   216
    apply (insert sumr_offset4 [of "Suc 0"])
avigad@32047
   217
    apply (simp del: setsum_op_ivl_Suc fact_Suc)
huffman@29187
   218
    done
huffman@29187
   219
huffman@29187
   220
  have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
huffman@29187
   221
    by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
huffman@29187
   222
huffman@29187
   223
  have differentiable_difg:
huffman@29187
   224
    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x"
huffman@29187
   225
    by (rule differentiableI [OF difg_Suc [rule_format]]) simp
huffman@29187
   226
huffman@29187
   227
  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
   228
        \<Longrightarrow> difg (Suc m) t = 0"
huffman@29187
   229
    by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp
huffman@29187
   230
huffman@29187
   231
  have "m < n" using m by simp
huffman@29187
   232
huffman@29187
   233
  have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
huffman@29187
   234
  using `m < n`
huffman@29187
   235
  proof (induct m)
huffman@29187
   236
  case 0
huffman@29187
   237
    show ?case
huffman@29187
   238
    proof (rule Rolle)
huffman@29187
   239
      show "0 < h" by fact
huffman@29187
   240
      show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
huffman@29187
   241
      show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x"
huffman@29187
   242
        by (simp add: isCont_difg n)
huffman@29187
   243
      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x"
huffman@29187
   244
        by (simp add: differentiable_difg n)
huffman@29187
   245
    qed
huffman@29187
   246
  next
huffman@29187
   247
  case (Suc m')
huffman@29187
   248
    hence "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" by simp
huffman@29187
   249
    then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast
huffman@29187
   250
    have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
huffman@29187
   251
    proof (rule Rolle)
huffman@29187
   252
      show "0 < t" by fact
huffman@29187
   253
      show "difg (Suc m') 0 = difg (Suc m') t"
huffman@29187
   254
        using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0)
huffman@29187
   255
      show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x"
huffman@29187
   256
        using `t < h` `Suc m' < n` by (simp add: isCont_difg)
huffman@29187
   257
      show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable x"
huffman@29187
   258
        using `t < h` `Suc m' < n` by (simp add: differentiable_difg)
huffman@29187
   259
    qed
huffman@29187
   260
    thus ?case
huffman@29187
   261
      using `t < h` by auto
huffman@29187
   262
  qed
huffman@29187
   263
huffman@29187
   264
  then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast
huffman@29187
   265
huffman@29187
   266
  hence "difg (Suc m) t = 0"
huffman@29187
   267
    using `m < n` by (simp add: difg_Suc_eq_0)
huffman@29187
   268
huffman@29187
   269
  show ?thesis
huffman@29187
   270
  proof (intro exI conjI)
huffman@29187
   271
    show "0 < t" by fact
huffman@29187
   272
    show "t < h" by fact
huffman@29187
   273
    show "f h =
huffman@29187
   274
      (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
huffman@29187
   275
      diff n t / real (fact n) * h ^ n"
huffman@29187
   276
      using `difg (Suc m) t = 0`
avigad@32047
   277
      by (simp add: m f_h difg_def del: fact_Suc)
huffman@29187
   278
  qed
huffman@29187
   279
huffman@29187
   280
qed
paulson@15079
   281
paulson@15079
   282
lemma Maclaurin_objl:
nipkow@25162
   283
  "0 < h & n>0 & diff 0 = f &
nipkow@25134
   284
  (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
nipkow@25134
   285
   --> (\<exists>t. 0 < t & t < h &
nipkow@25134
   286
            f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
nipkow@25134
   287
                  diff n t / real (fact n) * h ^ n)"
paulson@15079
   288
by (blast intro: Maclaurin)
paulson@15079
   289
paulson@15079
   290
paulson@15079
   291
lemma Maclaurin2:
bulwahn@41120
   292
  assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
bulwahn@41120
   293
  and DERIV: "\<forall>m t.
bulwahn@41120
   294
  m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
bulwahn@41120
   295
  shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
bulwahn@41120
   296
  (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
bulwahn@41120
   297
  diff n t / real (fact n) * h ^ n"
bulwahn@41120
   298
proof (cases "n")
bulwahn@41120
   299
  case 0 with INIT1 INIT2 show ?thesis by fastsimp
bulwahn@41120
   300
next
bulwahn@41120
   301
  case Suc 
bulwahn@41120
   302
  hence "n > 0" by simp
bulwahn@41120
   303
  from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
bulwahn@41120
   304
    f h =
bulwahn@41120
   305
    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n" 
bulwahn@41120
   306
    by (rule Maclaurin)
bulwahn@41120
   307
  thus ?thesis by fastsimp
bulwahn@41120
   308
qed
paulson@15079
   309
paulson@15079
   310
lemma Maclaurin2_objl:
paulson@15079
   311
     "0 < h & diff 0 = f &
paulson@15079
   312
       (\<forall>m t.
paulson@15079
   313
          m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
paulson@15079
   314
    --> (\<exists>t. 0 < t &
paulson@15079
   315
              t \<le> h &
paulson@15079
   316
              f h =
nipkow@15539
   317
              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
paulson@15079
   318
              diff n t / real (fact n) * h ^ n)"
paulson@15079
   319
by (blast intro: Maclaurin2)
paulson@15079
   320
paulson@15079
   321
lemma Maclaurin_minus:
bulwahn@41120
   322
  assumes INTERV : "h < 0" and
bulwahn@41120
   323
  INIT : "0 < n" "diff 0 = f" and
bulwahn@41120
   324
             ABL : "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
bulwahn@41120
   325
  shows "\<exists>t. h < t & t < 0 &
bulwahn@41120
   326
         f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
bulwahn@41120
   327
         diff n t / real (fact n) * h ^ n"
bulwahn@41120
   328
proof -
bulwahn@41120
   329
  from INTERV have "0 < -h" by simp
bulwahn@41120
   330
  moreover
bulwahn@41120
   331
  from INIT have "0 < n" by simp
bulwahn@41120
   332
  moreover
bulwahn@41120
   333
  from INIT have "(% x. ( - 1) ^ 0 * diff 0 (- x)) = (% x. f (- x))" by simp
bulwahn@41120
   334
  moreover
bulwahn@41120
   335
  have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> - h \<longrightarrow>
bulwahn@41120
   336
    DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
bulwahn@41120
   337
  proof (rule allI impI)+
bulwahn@41120
   338
    fix m t
bulwahn@41120
   339
    assume tINTERV:" m < n \<and> 0 \<le> t \<and> t \<le> - h"
bulwahn@41120
   340
    with ABL show "DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
bulwahn@41120
   341
    proof -
bulwahn@41120
   342
      
bulwahn@41120
   343
      from ABL and tINTERV have "DERIV (\<lambda>x. diff m (- x)) t :> - diff (Suc m) (- t)" (is ?tABL)
bulwahn@41120
   344
      proof -
bulwahn@41120
   345
	from ABL and tINTERV have "DERIV (diff m) (- t) :> diff (Suc m) (- t)" by force
bulwahn@41120
   346
	moreover
bulwahn@41120
   347
	from DERIV_ident[of t] have "DERIV uminus t :> (- 1)" by (rule DERIV_minus) 
bulwahn@41120
   348
	ultimately have "DERIV (\<lambda>x. diff m (- x)) t :> diff (Suc m) (- t) * - 1" by (rule DERIV_chain2)
bulwahn@41120
   349
	thus ?thesis by simp
bulwahn@41120
   350
      qed
bulwahn@41120
   351
      thus ?thesis
bulwahn@41120
   352
      proof -
bulwahn@41120
   353
	assume ?tABL hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> -1 ^ m * - diff (Suc m) (- t)" by (rule DERIV_cmult)
bulwahn@41120
   354
	hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> - (-1 ^ m * diff (Suc m) (- t))" by (subst minus_mult_right)
bulwahn@41120
   355
	thus ?thesis by simp 
bulwahn@41120
   356
      qed
bulwahn@41120
   357
    qed
bulwahn@41120
   358
  qed
bulwahn@41120
   359
  ultimately have t_exists: "\<exists>t>0. t < - h \<and>
bulwahn@41120
   360
    f (- (- h)) =
bulwahn@41120
   361
    (\<Sum>m = 0..<n.
bulwahn@41120
   362
    (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
bulwahn@41120
   363
    (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
bulwahn@41120
   364
  from this obtain t where t_def: "?P t" ..
bulwahn@41120
   365
  moreover
bulwahn@41120
   366
  have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
bulwahn@41120
   367
    by (auto simp add: power_mult_distrib[symmetric])
bulwahn@41120
   368
  moreover
bulwahn@41120
   369
  have "(SUM m = 0..<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m = 0..<n. diff m 0 * h ^ m / real (fact m))"
bulwahn@41120
   370
    by (auto intro: setsum_cong simp add: power_mult_distrib[symmetric])
bulwahn@41120
   371
  ultimately have " h < - t \<and>
bulwahn@41120
   372
    - t < 0 \<and>
bulwahn@41120
   373
    f h =
bulwahn@41120
   374
    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
bulwahn@41120
   375
    by auto
bulwahn@41120
   376
  thus ?thesis ..
bulwahn@41120
   377
qed
paulson@15079
   378
paulson@15079
   379
lemma Maclaurin_minus_objl:
nipkow@25162
   380
     "(h < 0 & n > 0 & diff 0 = f &
paulson@15079
   381
       (\<forall>m t.
paulson@15079
   382
          m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
paulson@15079
   383
    --> (\<exists>t. h < t &
paulson@15079
   384
              t < 0 &
paulson@15079
   385
              f h =
nipkow@15539
   386
              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
paulson@15079
   387
              diff n t / real (fact n) * h ^ n)"
paulson@15079
   388
by (blast intro: Maclaurin_minus)
paulson@15079
   389
paulson@15079
   390
paulson@15079
   391
subsection{*More Convenient "Bidirectional" Version.*}
paulson@15079
   392
paulson@15079
   393
(* not good for PVS sin_approx, cos_approx *)
paulson@15079
   394
paulson@15079
   395
lemma Maclaurin_bi_le_lemma [rule_format]:
nipkow@25162
   396
  "n>0 \<longrightarrow>
nipkow@25134
   397
   diff 0 0 =
nipkow@25134
   398
   (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
nipkow@25134
   399
   diff n 0 * 0 ^ n / real (fact n)"
paulson@15251
   400
by (induct "n", auto)
obua@14738
   401
paulson@15079
   402
lemma Maclaurin_bi_le:
bulwahn@41120
   403
   assumes INIT : "diff 0 = f"
bulwahn@41120
   404
   and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
bulwahn@41120
   405
   shows "\<exists>t. abs t \<le> abs x &
paulson@15079
   406
              f x =
nipkow@15539
   407
              (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
paulson@15079
   408
              diff n t / real (fact n) * x ^ n"
bulwahn@41120
   409
proof (cases "n = 0")
bulwahn@41120
   410
  case True from INIT True show ?thesis by force
bulwahn@41120
   411
next
bulwahn@41120
   412
  case False
bulwahn@41120
   413
  from this have n_not_zero:"n \<noteq> 0" .
bulwahn@41120
   414
  from False INIT DERIV show ?thesis
bulwahn@41120
   415
  proof (cases "x = 0")
bulwahn@41120
   416
    case True show ?thesis
bulwahn@41120
   417
    proof -
bulwahn@41120
   418
      from n_not_zero True INIT DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
bulwahn@41120
   419
	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n" by(force simp add: Maclaurin_bi_le_lemma) 
bulwahn@41120
   420
      thus ?thesis ..
bulwahn@41120
   421
    qed
bulwahn@41120
   422
  next
bulwahn@41120
   423
    case False 
bulwahn@41120
   424
    note linorder_less_linear [of "x" "0"] 
bulwahn@41120
   425
    thus ?thesis
bulwahn@41120
   426
    proof (elim disjE)
bulwahn@41120
   427
      assume "x = 0" with False show ?thesis ..
bulwahn@41120
   428
      next
bulwahn@41120
   429
      assume x_less_zero: "x < 0" moreover
bulwahn@41120
   430
      from n_not_zero have "0 < n" by simp moreover
bulwahn@41120
   431
      have "diff 0 = diff 0" by simp moreover
bulwahn@41120
   432
      have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
bulwahn@41120
   433
      proof (rule allI, rule allI, rule impI)
bulwahn@41120
   434
	fix m t
bulwahn@41120
   435
	assume "m < n & x \<le> t & t \<le> 0"
bulwahn@41120
   436
	with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by (fastsimp simp add: abs_if)
bulwahn@41120
   437
      qed
bulwahn@41120
   438
      ultimately have t_exists:"\<exists>t>x. t < 0 \<and>
bulwahn@41120
   439
        diff 0 x =
bulwahn@41120
   440
        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)
bulwahn@41120
   441
      from this obtain t where t_def: "?P t" ..
bulwahn@41120
   442
      from t_def x_less_zero INIT  have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
bulwahn@41120
   443
	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"
bulwahn@41120
   444
	by (simp add: abs_if order_less_le)
bulwahn@41120
   445
      thus ?thesis by (rule exI)
bulwahn@41120
   446
    next
bulwahn@41120
   447
    assume x_greater_zero: "x > 0" moreover
bulwahn@41120
   448
    from n_not_zero have "0 < n" by simp moreover
bulwahn@41120
   449
    have "diff 0 = diff 0" by simp moreover
bulwahn@41120
   450
    have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
bulwahn@41120
   451
      proof (rule allI, rule allI, rule impI)
bulwahn@41120
   452
	fix m t
bulwahn@41120
   453
	assume "m < n & 0 \<le> t & t \<le> x"
bulwahn@41120
   454
	with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by fastsimp
bulwahn@41120
   455
      qed
bulwahn@41120
   456
      ultimately have t_exists:"\<exists>t>0. t < x \<and>
bulwahn@41120
   457
        diff 0 x =
bulwahn@41120
   458
        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
bulwahn@41120
   459
      from this obtain t where t_def: "?P t" ..
bulwahn@41120
   460
      from t_def x_greater_zero INIT  have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
bulwahn@41120
   461
	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"
bulwahn@41120
   462
	by fastsimp
bulwahn@41120
   463
      thus ?thesis ..
bulwahn@41120
   464
    qed
bulwahn@41120
   465
  qed
bulwahn@41120
   466
qed
bulwahn@41120
   467
paulson@15079
   468
paulson@15079
   469
lemma Maclaurin_all_lt:
bulwahn@41120
   470
  assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
bulwahn@41120
   471
  and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
bulwahn@41120
   472
  shows "\<exists>t. 0 < abs t & abs t < abs x &
nipkow@15539
   473
               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
bulwahn@41120
   474
                     (diff n t / real (fact n)) * x ^ n" 
bulwahn@41120
   475
proof -
bulwahn@41120
   476
  have "(x = 0) \<Longrightarrow> ?thesis"
bulwahn@41120
   477
  proof -
bulwahn@41120
   478
    assume "x = 0"
bulwahn@41120
   479
    with INIT3 show "(x = 0) \<Longrightarrow> ?thesis"..
bulwahn@41120
   480
  qed
bulwahn@41120
   481
  moreover have "(x < 0) \<Longrightarrow> ?thesis"
bulwahn@41120
   482
  proof -
bulwahn@41120
   483
    assume x_less_zero: "x < 0"
bulwahn@41120
   484
    from DERIV have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp 
bulwahn@41120
   485
    with x_less_zero INIT2 INIT1 have "\<exists>t>x. t < 0 \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)
bulwahn@41120
   486
    from this obtain t where "?P t" ..
bulwahn@41120
   487
    with x_less_zero have "0 < \<bar>t\<bar> \<and>
bulwahn@41120
   488
      \<bar>t\<bar> < \<bar>x\<bar> \<and>
bulwahn@41120
   489
      f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by simp
bulwahn@41120
   490
    thus ?thesis ..
bulwahn@41120
   491
  qed
bulwahn@41120
   492
  moreover have "(x > 0) \<Longrightarrow> ?thesis"
bulwahn@41120
   493
  proof -
bulwahn@41120
   494
    assume x_greater_zero: "x > 0"
bulwahn@41120
   495
    from DERIV have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp
bulwahn@41120
   496
    with x_greater_zero INIT2 INIT1 have "\<exists>t>0. t < x \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
bulwahn@41120
   497
    from this obtain t where "?P t" ..
bulwahn@41120
   498
    with x_greater_zero have "0 < \<bar>t\<bar> \<and>
bulwahn@41120
   499
      \<bar>t\<bar> < \<bar>x\<bar> \<and>
bulwahn@41120
   500
      f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by fastsimp
bulwahn@41120
   501
    thus ?thesis ..
bulwahn@41120
   502
  qed
bulwahn@41120
   503
  ultimately show ?thesis by (fastsimp) 
bulwahn@41120
   504
qed
bulwahn@41120
   505
paulson@15079
   506
paulson@15079
   507
lemma Maclaurin_all_lt_objl:
paulson@15079
   508
     "diff 0 = f &
paulson@15079
   509
      (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
nipkow@25162
   510
      x ~= 0 & n > 0
paulson@15079
   511
      --> (\<exists>t. 0 < abs t & abs t < abs x &
nipkow@15539
   512
               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
paulson@15079
   513
                     (diff n t / real (fact n)) * x ^ n)"
paulson@15079
   514
by (blast intro: Maclaurin_all_lt)
paulson@15079
   515
paulson@15079
   516
lemma Maclaurin_zero [rule_format]:
paulson@15079
   517
     "x = (0::real)
nipkow@25134
   518
      ==> n \<noteq> 0 -->
nipkow@15539
   519
          (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
paulson@15079
   520
          diff 0 0"
paulson@15079
   521
by (induct n, auto)
paulson@15079
   522
bulwahn@41120
   523
bulwahn@41120
   524
lemma Maclaurin_all_le:
bulwahn@41120
   525
  assumes INIT: "diff 0 = f"
bulwahn@41120
   526
  and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
bulwahn@41120
   527
  shows "\<exists>t. abs t \<le> abs x &
nipkow@15539
   528
              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
paulson@15079
   529
                    (diff n t / real (fact n)) * x ^ n"
bulwahn@41120
   530
proof -
bulwahn@41120
   531
  note linorder_le_less_linear [of n 0]
bulwahn@41120
   532
  thus ?thesis
bulwahn@41120
   533
  proof
bulwahn@41120
   534
    assume "n\<le> 0" with INIT show ?thesis by force
bulwahn@41120
   535
  next
bulwahn@41120
   536
    assume n_greater_zero: "n > 0" show ?thesis
bulwahn@41120
   537
    proof (cases "x = 0")
bulwahn@41120
   538
      case True
bulwahn@41120
   539
      from n_greater_zero have "n \<noteq> 0" by auto
bulwahn@41120
   540
      from True this  have f_0:"(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0" by (rule Maclaurin_zero)
bulwahn@41120
   541
      from n_greater_zero have "n \<noteq> 0" by (rule gr_implies_not0)
bulwahn@41120
   542
      hence "\<exists> m. n = Suc m" by (rule not0_implies_Suc)
bulwahn@41120
   543
      with f_0 True INIT have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
bulwahn@41120
   544
       f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n"
bulwahn@41120
   545
	by force
bulwahn@41120
   546
      thus ?thesis ..
bulwahn@41120
   547
    next
bulwahn@41120
   548
      case False
bulwahn@41120
   549
      from INIT n_greater_zero this DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and>
bulwahn@41120
   550
	\<bar>t\<bar> < \<bar>x\<bar> \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_all_lt)
bulwahn@41120
   551
      from this obtain t where "?P t" ..
bulwahn@41120
   552
      hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
bulwahn@41120
   553
       f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by (simp add: order_less_le)
bulwahn@41120
   554
      thus ?thesis ..
bulwahn@41120
   555
    qed
bulwahn@41120
   556
  qed
bulwahn@41120
   557
qed
bulwahn@41120
   558
paulson@15079
   559
paulson@15079
   560
lemma Maclaurin_all_le_objl: "diff 0 = f &
paulson@15079
   561
      (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
paulson@15079
   562
      --> (\<exists>t. abs t \<le> abs x &
nipkow@15539
   563
              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
paulson@15079
   564
                    (diff n t / real (fact n)) * x ^ n)"
paulson@15079
   565
by (blast intro: Maclaurin_all_le)
paulson@15079
   566
paulson@15079
   567
paulson@15079
   568
subsection{*Version for Exponential Function*}
paulson@15079
   569
nipkow@25162
   570
lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
paulson@15079
   571
      ==> (\<exists>t. 0 < abs t &
paulson@15079
   572
                abs t < abs x &
nipkow@15539
   573
                exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
paulson@15079
   574
                        (exp t / real (fact n)) * x ^ n)"
paulson@15079
   575
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
paulson@15079
   576
paulson@15079
   577
paulson@15079
   578
lemma Maclaurin_exp_le:
paulson@15079
   579
     "\<exists>t. abs t \<le> abs x &
nipkow@15539
   580
            exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
paulson@15079
   581
                       (exp t / real (fact n)) * x ^ n"
paulson@15079
   582
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
paulson@15079
   583
paulson@15079
   584
paulson@15079
   585
subsection{*Version for Sine Function*}
paulson@15079
   586
paulson@15079
   587
lemma mod_exhaust_less_4:
nipkow@25134
   588
  "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
webertj@20217
   589
by auto
paulson@15079
   590
paulson@15079
   591
lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
nipkow@25134
   592
  "n\<noteq>0 --> Suc (Suc (2 * n - 2)) = 2*n"
paulson@15251
   593
by (induct "n", auto)
paulson@15079
   594
paulson@15079
   595
lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
nipkow@25134
   596
  "n\<noteq>0 --> Suc (Suc (4*n - 2)) = 4*n"
paulson@15251
   597
by (induct "n", auto)
paulson@15079
   598
paulson@15079
   599
lemma Suc_mult_two_diff_one [rule_format, simp]:
nipkow@25134
   600
  "n\<noteq>0 --> Suc (2 * n - 1) = 2*n"
paulson@15251
   601
by (induct "n", auto)
paulson@15079
   602
paulson@15234
   603
paulson@15234
   604
text{*It is unclear why so many variant results are needed.*}
paulson@15079
   605
huffman@36974
   606
lemma sin_expansion_lemma:
huffman@36974
   607
     "sin (x + real (Suc m) * pi / 2) =  
huffman@36974
   608
      cos (x + real (m) * pi / 2)"
huffman@36974
   609
by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
huffman@36974
   610
paulson@15079
   611
lemma Maclaurin_sin_expansion2:
paulson@15079
   612
     "\<exists>t. abs t \<le> abs x &
paulson@15079
   613
       sin x =
nipkow@15539
   614
       (\<Sum>m=0..<n. (if even m then 0
huffman@23177
   615
                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
nipkow@15539
   616
                       x ^ m)
paulson@15079
   617
      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
paulson@15079
   618
apply (cut_tac f = sin and n = n and x = x
paulson@15079
   619
        and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
paulson@15079
   620
apply safe
paulson@15079
   621
apply (simp (no_asm))
huffman@36974
   622
apply (simp (no_asm) add: sin_expansion_lemma)
huffman@23242
   623
apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
paulson@15079
   624
apply (rule ccontr, simp)
paulson@15079
   625
apply (drule_tac x = x in spec, simp)
paulson@15079
   626
apply (erule ssubst)
paulson@15079
   627
apply (rule_tac x = t in exI, simp)
nipkow@15536
   628
apply (rule setsum_cong[OF refl])
nipkow@15539
   629
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
paulson@15079
   630
done
paulson@15079
   631
paulson@15234
   632
lemma Maclaurin_sin_expansion:
paulson@15234
   633
     "\<exists>t. sin x =
nipkow@15539
   634
       (\<Sum>m=0..<n. (if even m then 0
huffman@23177
   635
                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
nipkow@15539
   636
                       x ^ m)
paulson@15234
   637
      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
paulson@15234
   638
apply (insert Maclaurin_sin_expansion2 [of x n]) 
paulson@15234
   639
apply (blast intro: elim:); 
paulson@15234
   640
done
paulson@15234
   641
paulson@15079
   642
lemma Maclaurin_sin_expansion3:
nipkow@25162
   643
     "[| n > 0; 0 < x |] ==>
paulson@15079
   644
       \<exists>t. 0 < t & t < x &
paulson@15079
   645
       sin x =
nipkow@15539
   646
       (\<Sum>m=0..<n. (if even m then 0
huffman@23177
   647
                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
nipkow@15539
   648
                       x ^ m)
paulson@15079
   649
      + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
paulson@15079
   650
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
   651
apply safe
paulson@15079
   652
apply simp
huffman@36974
   653
apply (simp (no_asm) add: sin_expansion_lemma)
paulson@15079
   654
apply (erule ssubst)
paulson@15079
   655
apply (rule_tac x = t in exI, simp)
nipkow@15536
   656
apply (rule setsum_cong[OF refl])
nipkow@15539
   657
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
paulson@15079
   658
done
paulson@15079
   659
paulson@15079
   660
lemma Maclaurin_sin_expansion4:
paulson@15079
   661
     "0 < x ==>
paulson@15079
   662
       \<exists>t. 0 < t & t \<le> x &
paulson@15079
   663
       sin x =
nipkow@15539
   664
       (\<Sum>m=0..<n. (if even m then 0
huffman@23177
   665
                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
nipkow@15539
   666
                       x ^ m)
paulson@15079
   667
      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
paulson@15079
   668
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
   669
apply safe
paulson@15079
   670
apply simp
huffman@36974
   671
apply (simp (no_asm) add: sin_expansion_lemma)
paulson@15079
   672
apply (erule ssubst)
paulson@15079
   673
apply (rule_tac x = t in exI, simp)
nipkow@15536
   674
apply (rule setsum_cong[OF refl])
nipkow@15539
   675
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
paulson@15079
   676
done
paulson@15079
   677
paulson@15079
   678
paulson@15079
   679
subsection{*Maclaurin Expansion for Cosine Function*}
paulson@15079
   680
paulson@15079
   681
lemma sumr_cos_zero_one [simp]:
nipkow@15539
   682
 "(\<Sum>m=0..<(Suc n).
huffman@23177
   683
     (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
paulson@15251
   684
by (induct "n", auto)
paulson@15079
   685
huffman@36974
   686
lemma cos_expansion_lemma:
huffman@36974
   687
  "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
huffman@36974
   688
by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
huffman@36974
   689
paulson@15079
   690
lemma Maclaurin_cos_expansion:
paulson@15079
   691
     "\<exists>t. abs t \<le> abs x &
paulson@15079
   692
       cos x =
nipkow@15539
   693
       (\<Sum>m=0..<n. (if even m
huffman@23177
   694
                       then -1 ^ (m div 2)/(real (fact m))
paulson@15079
   695
                       else 0) *
nipkow@15539
   696
                       x ^ m)
paulson@15079
   697
      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
paulson@15079
   698
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
   699
apply safe
paulson@15079
   700
apply (simp (no_asm))
huffman@36974
   701
apply (simp (no_asm) add: cos_expansion_lemma)
paulson@15079
   702
apply (case_tac "n", simp)
nipkow@15561
   703
apply (simp del: setsum_op_ivl_Suc)
paulson@15079
   704
apply (rule ccontr, simp)
paulson@15079
   705
apply (drule_tac x = x in spec, simp)
paulson@15079
   706
apply (erule ssubst)
paulson@15079
   707
apply (rule_tac x = t in exI, simp)
nipkow@15536
   708
apply (rule setsum_cong[OF refl])
paulson@15234
   709
apply (auto simp add: cos_zero_iff even_mult_two_ex)
paulson@15079
   710
done
paulson@15079
   711
paulson@15079
   712
lemma Maclaurin_cos_expansion2:
nipkow@25162
   713
     "[| 0 < x; n > 0 |] ==>
paulson@15079
   714
       \<exists>t. 0 < t & t < x &
paulson@15079
   715
       cos x =
nipkow@15539
   716
       (\<Sum>m=0..<n. (if even m
huffman@23177
   717
                       then -1 ^ (m div 2)/(real (fact m))
paulson@15079
   718
                       else 0) *
nipkow@15539
   719
                       x ^ m)
paulson@15079
   720
      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
paulson@15079
   721
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
   722
apply safe
paulson@15079
   723
apply simp
huffman@36974
   724
apply (simp (no_asm) add: cos_expansion_lemma)
paulson@15079
   725
apply (erule ssubst)
paulson@15079
   726
apply (rule_tac x = t in exI, simp)
nipkow@15536
   727
apply (rule setsum_cong[OF refl])
paulson@15234
   728
apply (auto simp add: cos_zero_iff even_mult_two_ex)
paulson@15079
   729
done
paulson@15079
   730
paulson@15234
   731
lemma Maclaurin_minus_cos_expansion:
nipkow@25162
   732
     "[| x < 0; n > 0 |] ==>
paulson@15079
   733
       \<exists>t. x < t & t < 0 &
paulson@15079
   734
       cos x =
nipkow@15539
   735
       (\<Sum>m=0..<n. (if even m
huffman@23177
   736
                       then -1 ^ (m div 2)/(real (fact m))
paulson@15079
   737
                       else 0) *
nipkow@15539
   738
                       x ^ m)
paulson@15079
   739
      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
paulson@15079
   740
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
   741
apply safe
paulson@15079
   742
apply simp
huffman@36974
   743
apply (simp (no_asm) add: cos_expansion_lemma)
paulson@15079
   744
apply (erule ssubst)
paulson@15079
   745
apply (rule_tac x = t in exI, simp)
nipkow@15536
   746
apply (rule setsum_cong[OF refl])
paulson@15234
   747
apply (auto simp add: cos_zero_iff even_mult_two_ex)
paulson@15079
   748
done
paulson@15079
   749
paulson@15079
   750
(* ------------------------------------------------------------------------- *)
paulson@15079
   751
(* Version for ln(1 +/- x). Where is it??                                    *)
paulson@15079
   752
(* ------------------------------------------------------------------------- *)
paulson@15079
   753
paulson@15079
   754
lemma sin_bound_lemma:
paulson@15081
   755
    "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
paulson@15079
   756
by auto
paulson@15079
   757
paulson@15079
   758
lemma Maclaurin_sin_bound:
huffman@23177
   759
  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
paulson@15081
   760
  x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
obua@14738
   761
proof -
paulson@15079
   762
  have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
obua@14738
   763
    by (rule_tac mult_right_mono,simp_all)
obua@14738
   764
  note est = this[simplified]
huffman@22985
   765
  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
   766
  have diff_0: "?diff 0 = sin" by simp
huffman@22985
   767
  have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
huffman@22985
   768
    apply (clarify)
huffman@22985
   769
    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
huffman@22985
   770
    apply (cut_tac m=m in mod_exhaust_less_4)
hoelzl@31881
   771
    apply (safe, auto intro!: DERIV_intros)
huffman@22985
   772
    done
huffman@22985
   773
  from Maclaurin_all_le [OF diff_0 DERIV_diff]
huffman@22985
   774
  obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
huffman@22985
   775
    t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) +
huffman@22985
   776
      ?diff n t / real (fact n) * x ^ n" by fast
huffman@22985
   777
  have diff_m_0:
huffman@22985
   778
    "\<And>m. ?diff m 0 = (if even m then 0
huffman@23177
   779
         else -1 ^ ((m - Suc 0) div 2))"
huffman@22985
   780
    apply (subst even_even_mod_4_iff)
huffman@22985
   781
    apply (cut_tac m=m in mod_exhaust_less_4)
huffman@22985
   782
    apply (elim disjE, simp_all)
huffman@22985
   783
    apply (safe dest!: mod_eqD, simp_all)
huffman@22985
   784
    done
obua@14738
   785
  show ?thesis
huffman@22985
   786
    apply (subst t2)
paulson@15079
   787
    apply (rule sin_bound_lemma)
nipkow@15536
   788
    apply (rule setsum_cong[OF refl])
huffman@22985
   789
    apply (subst diff_m_0, simp)
paulson@15079
   790
    apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
avigad@16775
   791
                   simp add: est mult_nonneg_nonneg mult_ac divide_inverse
paulson@16924
   792
                          power_abs [symmetric] abs_mult)
obua@14738
   793
    done
obua@14738
   794
qed
obua@14738
   795
paulson@15079
   796
end