haftmann@28952: (* Title: HOL/Taylor.thy
berghofe@17634: Author: Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
berghofe@17634: *)
berghofe@17634:
berghofe@17634: header {* Taylor series *}
berghofe@17634:
berghofe@17634: theory Taylor
berghofe@17634: imports MacLaurin
berghofe@17634: begin
berghofe@17634:
berghofe@17634: text {*
berghofe@17634: We use MacLaurin and the translation of the expansion point @{text c} to @{text 0}
berghofe@17634: to prove Taylor's theorem.
berghofe@17634: *}
berghofe@17634:
berghofe@17634: lemma taylor_up:
nipkow@25162: assumes INIT: "n>0" "diff 0 = f"
berghofe@17634: and DERIV: "(\ m t. m < n & a \ t & t \ b \ DERIV (diff m) t :> (diff (Suc m) t))"
berghofe@17634: and INTERV: "a \ c" "c < b"
berghofe@17634: shows "\ t. c < t & t < b &
berghofe@17634: f b = setsum (%m. (diff m c / real (fact m)) * (b - c)^m) {0..0" "((\m x. diff m (x + c)) 0) = (\x. f (x + c))" by auto
berghofe@17634: moreover
nipkow@25162: 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: proof (intro strip)
berghofe@17634: fix m t
berghofe@17634: assume "m < n & 0 <= t & t <= b - c"
berghofe@17634: with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
berghofe@17634: moreover
huffman@23069: from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
berghofe@17634: ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
berghofe@17634: by (rule DERIV_chain2)
berghofe@17634: thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
berghofe@17634: qed
berghofe@17634: ultimately
berghofe@17634: have EX:"EX t>0. t < b - c &
berghofe@17634: f (b - c + c) = (SUM m = 0..m = 0.. f b = (\m = 0..0" "diff 0 = f"
berghofe@17634: and DERIV: "(\ m t. m < n & a \ t & t \ b \ DERIV (diff m) t :> (diff (Suc m) t))"
berghofe@17634: and INTERV: "a < c" "c \ b"
berghofe@17634: shows "\ t. a < t & t < c &
berghofe@17634: f a = setsum (% m. (diff m c / real (fact m)) * (a - c)^m) {0..0" "((\m x. diff m (x + c)) 0) = (\x. f (x + c))" by auto
berghofe@17634: moreover
berghofe@17634: 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: proof (rule allI impI)+
berghofe@17634: fix m t
berghofe@17634: assume "m < n & a-c <= t & t <= 0"
berghofe@17634: with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
berghofe@17634: moreover
huffman@23069: from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
berghofe@17634: ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
berghofe@17634: thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
berghofe@17634: qed
berghofe@17634: ultimately
berghofe@17634: have EX: "EX t>a - c. t < 0 &
berghofe@17634: f (a - c + c) = (SUM m = 0.. f a = (\m = 0..0" "diff 0 = f"
berghofe@17634: and DERIV: "(\ m t. m < n & a \ t & t \ b \ DERIV (diff m) t :> (diff (Suc m) t))"
berghofe@17634: and INTERV: "a \ c " "c \ b" "a \ x" "x \ b" "x \ c"
berghofe@17634: shows "\ t. (if xm t. m < n \ x \ t \ t \ b \ DERIV (diff m) t :> diff (Suc m) t"
nipkow@44890: by fastforce
berghofe@17634: moreover note True
berghofe@17634: moreover from INTERV have "c \ b" by simp
berghofe@17634: ultimately have EX: "\t>x. t < c \ f x =
berghofe@17634: (\m = 0..m t. m < n \ a \ t \ t \ x \ DERIV (diff m) t :> diff (Suc m) t"
nipkow@44890: by fastforce
berghofe@17634: moreover from INTERV have "a \ c" by arith
berghofe@17634: moreover from False and INTERV have "c < x" by arith
berghofe@17634: ultimately have EX: "\t>c. t < x \ f x =
berghofe@17634: (\m = 0..