src/HOL/Taylor.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61954 1d43f86f48be
child 63569 7e0b0db5e9ac
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Taylor.thy
     2     Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
     3 *)
     4 
     5 section \<open>Taylor series\<close>
     6 
     7 theory Taylor
     8 imports MacLaurin
     9 begin
    10 
    11 text \<open>
    12 We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
    13 to prove Taylor's theorem.
    14 \<close>
    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::real. c < t & t < b & 
    21     f b = (\<Sum>m<n. (diff m c / (fact m)) * (b - c)^m) + (diff n t / (fact n)) * (b - c)^n"
    22 proof -
    23   from INTERV have "0 < b-c" by arith
    24   moreover 
    25   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
    26   moreover
    27   have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    28   proof (intro strip)
    29     fix m t
    30     assume "m < n & 0 <= t & t <= b - c"
    31     with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
    32     moreover
    33     from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
    34     ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
    35       by (rule DERIV_chain2)
    36     thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
    37   qed
    38   ultimately obtain x where 
    39         "0 < x & x < b - c & 
    40         f (b - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (b - c) ^ m) +
    41           diff n (x + c) / (fact n) * (b - c) ^ n"
    42      by (rule Maclaurin [THEN exE])
    43   then have "c<x+c & x+c<b \<and> f b = (\<Sum>m<n. diff m c / (fact m) * (b - c) ^ m) +
    44     diff n (x+c) / (fact n) * (b - c) ^ n"
    45     by fastforce
    46   thus ?thesis by fastforce
    47 qed
    48 
    49 lemma taylor_down:
    50   fixes a::real
    51   assumes INIT: "n>0" "diff 0 = f"
    52   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
    53   and INTERV: "a < c" "c \<le> b"
    54   shows "\<exists> t. a < t & t < c & 
    55     f a = (\<Sum>m<n. (diff m c / (fact m)) * (a - c)^m) + (diff n t / (fact n)) * (a - c)^n" 
    56 proof -
    57   from INTERV have "a-c < 0" by arith
    58   moreover 
    59   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
    60   moreover
    61   have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    62   proof (rule allI impI)+
    63     fix m t
    64     assume "m < n & a-c <= t & t <= 0"
    65     with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto 
    66     moreover
    67     from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
    68     ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
    69     thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
    70   qed
    71   ultimately obtain x where 
    72          "a - c < x & x < 0 &
    73       f (a - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
    74         diff n (x + c) / (fact n) * (a - c) ^ n"
    75      by (rule Maclaurin_minus [THEN exE])
    76   then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a - c) ^ m) +
    77       diff n (x+c) / (fact n) * (a - c) ^ n"
    78     by fastforce
    79   thus ?thesis by fastforce
    80 qed
    81 
    82 lemma taylor:
    83   fixes a::real
    84   assumes INIT: "n>0" "diff 0 = f"
    85   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
    86   and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
    87   shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
    88     f x = (\<Sum>m<n. (diff m c / (fact m)) * (x - c)^m) + (diff n t / (fact n)) * (x - c)^n" 
    89 proof (cases "x<c")
    90   case True
    91   note INIT
    92   moreover from DERIV and INTERV
    93   have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
    94     by fastforce
    95   moreover note True
    96   moreover from INTERV have "c \<le> b" by simp
    97   ultimately have "\<exists>t>x. t < c \<and> f x =
    98     (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
    99     by (rule taylor_down)
   100   with True show ?thesis by simp
   101 next
   102   case False
   103   note INIT
   104   moreover from DERIV and INTERV
   105   have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   106     by fastforce
   107   moreover from INTERV have "a \<le> c" by arith
   108   moreover from False and INTERV have "c < x" by arith
   109   ultimately have "\<exists>t>c. t < x \<and> f x =
   110     (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" 
   111     by (rule taylor_up)
   112   with False show ?thesis by simp
   113 qed
   114 
   115 end