src/HOL/Taylor.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 44890 22f665a2e91c
child 56193 c726ecfb22b6
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 (*  Title:      HOL/Taylor.thy
     2     Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
     3 *)
     4 
     5 header {* Taylor series *}
     6 
     7 theory Taylor
     8 imports MacLaurin
     9 begin
    10 
    11 text {*
    12 We use MacLaurin and the translation of the expansion point @{text c} to @{text 0}
    13 to prove Taylor's theorem.
    14 *}
    15 
    16 lemma taylor_up: 
    17   assumes INIT: "n>0" "diff 0 = f"
    18   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
    19   and INTERV: "a \<le> c" "c < b" 
    20   shows "\<exists> t. c < t & t < b & 
    21     f b = setsum (%m. (diff m c / real (fact m)) * (b - c)^m) {0..<n} +
    22       (diff n t / real (fact n)) * (b - c)^n"
    23 proof -
    24   from INTERV have "0 < b-c" by arith
    25   moreover 
    26   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
    27   moreover
    28   have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    29   proof (intro strip)
    30     fix m t
    31     assume "m < n & 0 <= t & t <= b - c"
    32     with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
    33     moreover
    34     from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
    35     ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
    36       by (rule DERIV_chain2)
    37     thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
    38   qed
    39   ultimately 
    40   have EX:"EX t>0. t < b - c & 
    41     f (b - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
    42       diff n (t + c) / real (fact n) * (b - c) ^ n" 
    43     by (rule Maclaurin)
    44   show ?thesis
    45   proof -
    46     from EX obtain x where 
    47       X: "0 < x & x < b - c & 
    48         f (b - c + c) = (\<Sum>m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
    49           diff n (x + c) / real (fact n) * (b - c) ^ n" ..
    50     let ?H = "x + c"
    51     from X have "c<?H & ?H<b \<and> f b = (\<Sum>m = 0..<n. diff m c / real (fact m) * (b - c) ^ m) +
    52       diff n ?H / real (fact n) * (b - c) ^ n"
    53       by fastforce
    54     thus ?thesis by fastforce
    55   qed
    56 qed
    57 
    58 lemma taylor_down:
    59   assumes INIT: "n>0" "diff 0 = f"
    60   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
    61   and INTERV: "a < c" "c \<le> b"
    62   shows "\<exists> t. a < t & t < c & 
    63     f a = setsum (% m. (diff m c / real (fact m)) * (a - c)^m) {0..<n} +
    64       (diff n t / real (fact n)) * (a - c)^n" 
    65 proof -
    66   from INTERV have "a-c < 0" by arith
    67   moreover 
    68   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
    69   moreover
    70   have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    71   proof (rule allI impI)+
    72     fix m t
    73     assume "m < n & a-c <= t & t <= 0"
    74     with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto 
    75     moreover
    76     from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
    77     ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
    78     thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
    79   qed
    80   ultimately 
    81   have EX: "EX t>a - c. t < 0 &
    82     f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
    83       diff n (t + c) / real (fact n) * (a - c) ^ n" 
    84     by (rule Maclaurin_minus)
    85   show ?thesis
    86   proof -
    87     from EX obtain x where X: "a - c < x & x < 0 &
    88       f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
    89         diff n (x + c) / real (fact n) * (a - c) ^ n" ..
    90     let ?H = "x + c"
    91     from X have "a<?H & ?H<c \<and> f a = (\<Sum>m = 0..<n. diff m c / real (fact m) * (a - c) ^ m) +
    92       diff n ?H / real (fact n) * (a - c) ^ n"
    93       by fastforce
    94     thus ?thesis by fastforce
    95   qed
    96 qed
    97 
    98 lemma taylor:
    99   assumes INIT: "n>0" "diff 0 = f"
   100   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   101   and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
   102   shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
   103     f x = setsum (% m. (diff m c / real (fact m)) * (x - c)^m) {0..<n} +
   104       (diff n t / real (fact n)) * (x - c)^n" 
   105 proof (cases "x<c")
   106   case True
   107   note INIT
   108   moreover from DERIV and INTERV
   109   have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   110     by fastforce
   111   moreover note True
   112   moreover from INTERV have "c \<le> b" by simp
   113   ultimately have EX: "\<exists>t>x. t < c \<and> f x =
   114     (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
   115       diff n t / real (fact n) * (x - c) ^ n"
   116     by (rule taylor_down)
   117   with True show ?thesis by simp
   118 next
   119   case False
   120   note INIT
   121   moreover from DERIV and INTERV
   122   have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   123     by fastforce
   124   moreover from INTERV have "a \<le> c" by arith
   125   moreover from False and INTERV have "c < x" by arith
   126   ultimately have EX: "\<exists>t>c. t < x \<and> f x =
   127     (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
   128       diff n t / real (fact n) * (x - c) ^ n" 
   129     by (rule taylor_up)
   130   with False show ?thesis by simp
   131 qed
   132 
   133 end