src/HOL/Taylor.thy
changeset 28952 15a4b2cf8c34
parent 25162 ad4d5365d9d8
child 44890 22f665a2e91c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Taylor.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,133 @@
     1.4 +(*  Title:      HOL/Taylor.thy
     1.5 +    Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Taylor series *}
     1.9 +
    1.10 +theory Taylor
    1.11 +imports MacLaurin
    1.12 +begin
    1.13 +
    1.14 +text {*
    1.15 +We use MacLaurin and the translation of the expansion point @{text c} to @{text 0}
    1.16 +to prove Taylor's theorem.
    1.17 +*}
    1.18 +
    1.19 +lemma taylor_up: 
    1.20 +  assumes INIT: "n>0" "diff 0 = f"
    1.21 +  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
    1.22 +  and INTERV: "a \<le> c" "c < b" 
    1.23 +  shows "\<exists> t. c < t & t < b & 
    1.24 +    f b = setsum (%m. (diff m c / real (fact m)) * (b - c)^m) {0..<n} +
    1.25 +      (diff n t / real (fact n)) * (b - c)^n"
    1.26 +proof -
    1.27 +  from INTERV have "0 < b-c" by arith
    1.28 +  moreover 
    1.29 +  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
    1.30 +  moreover
    1.31 +  have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    1.32 +  proof (intro strip)
    1.33 +    fix m t
    1.34 +    assume "m < n & 0 <= t & t <= b - c"
    1.35 +    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
    1.36 +    moreover
    1.37 +    from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
    1.38 +    ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
    1.39 +      by (rule DERIV_chain2)
    1.40 +    thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
    1.41 +  qed
    1.42 +  ultimately 
    1.43 +  have EX:"EX t>0. t < b - c & 
    1.44 +    f (b - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
    1.45 +      diff n (t + c) / real (fact n) * (b - c) ^ n" 
    1.46 +    by (rule Maclaurin)
    1.47 +  show ?thesis
    1.48 +  proof -
    1.49 +    from EX obtain x where 
    1.50 +      X: "0 < x & x < b - c & 
    1.51 +        f (b - c + c) = (\<Sum>m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
    1.52 +          diff n (x + c) / real (fact n) * (b - c) ^ n" ..
    1.53 +    let ?H = "x + c"
    1.54 +    from X have "c<?H & ?H<b \<and> f b = (\<Sum>m = 0..<n. diff m c / real (fact m) * (b - c) ^ m) +
    1.55 +      diff n ?H / real (fact n) * (b - c) ^ n"
    1.56 +      by fastsimp
    1.57 +    thus ?thesis by fastsimp
    1.58 +  qed
    1.59 +qed
    1.60 +
    1.61 +lemma taylor_down:
    1.62 +  assumes INIT: "n>0" "diff 0 = f"
    1.63 +  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
    1.64 +  and INTERV: "a < c" "c \<le> b"
    1.65 +  shows "\<exists> t. a < t & t < c & 
    1.66 +    f a = setsum (% m. (diff m c / real (fact m)) * (a - c)^m) {0..<n} +
    1.67 +      (diff n t / real (fact n)) * (a - c)^n" 
    1.68 +proof -
    1.69 +  from INTERV have "a-c < 0" by arith
    1.70 +  moreover 
    1.71 +  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
    1.72 +  moreover
    1.73 +  have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    1.74 +  proof (rule allI impI)+
    1.75 +    fix m t
    1.76 +    assume "m < n & a-c <= t & t <= 0"
    1.77 +    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto 
    1.78 +    moreover
    1.79 +    from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
    1.80 +    ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
    1.81 +    thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
    1.82 +  qed
    1.83 +  ultimately 
    1.84 +  have EX: "EX t>a - c. t < 0 &
    1.85 +    f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
    1.86 +      diff n (t + c) / real (fact n) * (a - c) ^ n" 
    1.87 +    by (rule Maclaurin_minus)
    1.88 +  show ?thesis
    1.89 +  proof -
    1.90 +    from EX obtain x where X: "a - c < x & x < 0 &
    1.91 +      f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
    1.92 +        diff n (x + c) / real (fact n) * (a - c) ^ n" ..
    1.93 +    let ?H = "x + c"
    1.94 +    from X have "a<?H & ?H<c \<and> f a = (\<Sum>m = 0..<n. diff m c / real (fact m) * (a - c) ^ m) +
    1.95 +      diff n ?H / real (fact n) * (a - c) ^ n"
    1.96 +      by fastsimp
    1.97 +    thus ?thesis by fastsimp
    1.98 +  qed
    1.99 +qed
   1.100 +
   1.101 +lemma taylor:
   1.102 +  assumes INIT: "n>0" "diff 0 = f"
   1.103 +  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   1.104 +  and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
   1.105 +  shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
   1.106 +    f x = setsum (% m. (diff m c / real (fact m)) * (x - c)^m) {0..<n} +
   1.107 +      (diff n t / real (fact n)) * (x - c)^n" 
   1.108 +proof (cases "x<c")
   1.109 +  case True
   1.110 +  note INIT
   1.111 +  moreover from DERIV and INTERV
   1.112 +  have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   1.113 +    by fastsimp
   1.114 +  moreover note True
   1.115 +  moreover from INTERV have "c \<le> b" by simp
   1.116 +  ultimately have EX: "\<exists>t>x. t < c \<and> f x =
   1.117 +    (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
   1.118 +      diff n t / real (fact n) * (x - c) ^ n"
   1.119 +    by (rule taylor_down)
   1.120 +  with True show ?thesis by simp
   1.121 +next
   1.122 +  case False
   1.123 +  note INIT
   1.124 +  moreover from DERIV and INTERV
   1.125 +  have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   1.126 +    by fastsimp
   1.127 +  moreover from INTERV have "a \<le> c" by arith
   1.128 +  moreover from False and INTERV have "c < x" by arith
   1.129 +  ultimately have EX: "\<exists>t>c. t < x \<and> f x =
   1.130 +    (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
   1.131 +      diff n t / real (fact n) * (x - c) ^ n" 
   1.132 +    by (rule taylor_up)
   1.133 +  with False show ?thesis by simp
   1.134 +qed
   1.135 +
   1.136 +end