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