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: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
berghofe@17634:   and INTERV: "a \<le> c" "c < b" 
berghofe@17634:   shows "\<exists> t. c < t & t < b & 
berghofe@17634:     f b = setsum (%m. (diff m c / real (fact m)) * (b - c)^m) {0..<n} +
berghofe@17634:       (diff n t / real (fact n)) * (b - c)^n"
berghofe@17634: proof -
berghofe@17634:   from INTERV have "0 < b-c" by arith
berghofe@17634:   moreover 
nipkow@25162:   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>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..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
berghofe@17634:       diff n (t + c) / real (fact n) * (b - c) ^ n" 
berghofe@17634:     by (rule Maclaurin)
berghofe@17634:   show ?thesis
berghofe@17634:   proof -
berghofe@17634:     from EX obtain x where 
berghofe@17634:       X: "0 < x & x < b - c & 
berghofe@17634:         f (b - c + c) = (\<Sum>m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
berghofe@17634:           diff n (x + c) / real (fact n) * (b - c) ^ n" ..
berghofe@17634:     let ?H = "x + c"
berghofe@17634:     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:       diff n ?H / real (fact n) * (b - c) ^ n"
nipkow@44890:       by fastforce
nipkow@44890:     thus ?thesis by fastforce
berghofe@17634:   qed
berghofe@17634: qed
berghofe@17634: 
berghofe@17634: lemma taylor_down:
nipkow@25162:   assumes INIT: "n>0" "diff 0 = f"
berghofe@17634:   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
berghofe@17634:   and INTERV: "a < c" "c \<le> b"
berghofe@17634:   shows "\<exists> t. a < t & t < c & 
berghofe@17634:     f a = setsum (% m. (diff m c / real (fact m)) * (a - c)^m) {0..<n} +
berghofe@17634:       (diff n t / real (fact n)) * (a - c)^n" 
berghofe@17634: proof -
berghofe@17634:   from INTERV have "a-c < 0" by arith
berghofe@17634:   moreover 
nipkow@25162:   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>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..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
berghofe@17634:       diff n (t + c) / real (fact n) * (a - c) ^ n" 
berghofe@17634:     by (rule Maclaurin_minus)
berghofe@17634:   show ?thesis
berghofe@17634:   proof -
berghofe@17634:     from EX obtain x where X: "a - c < x & x < 0 &
berghofe@17634:       f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
berghofe@17634:         diff n (x + c) / real (fact n) * (a - c) ^ n" ..
berghofe@17634:     let ?H = "x + c"
berghofe@17634:     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:       diff n ?H / real (fact n) * (a - c) ^ n"
nipkow@44890:       by fastforce
nipkow@44890:     thus ?thesis by fastforce
berghofe@17634:   qed
berghofe@17634: qed
berghofe@17634: 
berghofe@17634: lemma taylor:
nipkow@25162:   assumes INIT: "n>0" "diff 0 = f"
berghofe@17634:   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
berghofe@17634:   and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
berghofe@17634:   shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
berghofe@17634:     f x = setsum (% m. (diff m c / real (fact m)) * (x - c)^m) {0..<n} +
berghofe@17634:       (diff n t / real (fact n)) * (x - c)^n" 
berghofe@17634: proof (cases "x<c")
berghofe@17634:   case True
berghofe@17634:   note INIT
berghofe@17634:   moreover from DERIV and INTERV
berghofe@17634:   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:     by fastforce
berghofe@17634:   moreover note True
berghofe@17634:   moreover from INTERV have "c \<le> b" by simp
berghofe@17634:   ultimately have EX: "\<exists>t>x. t < c \<and> f x =
berghofe@17634:     (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
berghofe@17634:       diff n t / real (fact n) * (x - c) ^ n"
berghofe@17634:     by (rule taylor_down)
berghofe@17634:   with True show ?thesis by simp
berghofe@17634: next
berghofe@17634:   case False
berghofe@17634:   note INIT
berghofe@17634:   moreover from DERIV and INTERV
berghofe@17634:   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:     by fastforce
berghofe@17634:   moreover from INTERV have "a \<le> c" by arith
berghofe@17634:   moreover from False and INTERV have "c < x" by arith
berghofe@17634:   ultimately have EX: "\<exists>t>c. t < x \<and> f x =
berghofe@17634:     (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
berghofe@17634:       diff n t / real (fact n) * (x - c) ^ n" 
berghofe@17634:     by (rule taylor_up)
berghofe@17634:   with False show ?thesis by simp
berghofe@17634: qed
berghofe@17634: 
berghofe@17634: end