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