src/HOL/Taylor.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 61954 1d43f86f48be child 63569 7e0b0db5e9ac permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
 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 \Taylor series\ berghofe@17634 6 berghofe@17634 7 theory Taylor berghofe@17634 8 imports MacLaurin berghofe@17634 9 begin berghofe@17634 10 wenzelm@60758 11 text \ wenzelm@61799 12 We use MacLaurin and the translation of the expansion point \c\ to \0\ berghofe@17634 13 to prove Taylor's theorem. wenzelm@60758 14 \ berghofe@17634 15 berghofe@17634 16 lemma taylor_up: nipkow@25162 17 assumes INIT: "n>0" "diff 0 = f" berghofe@17634 18 and DERIV: "(\ m t. m < n & a \ t & t \ b \ DERIV (diff m) t :> (diff (Suc m) t))" berghofe@17634 19 and INTERV: "a \ c" "c < b" lp15@59730 20 shows "\t::real. c < t & t < b & lp15@59730 21 f b = (\m0" "((\m x. diff m (x + c)) 0) = (\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) = (\m f b = (\m0" "diff 0 = f" berghofe@17634 52 and DERIV: "(\ m t. m < n & a \ t & t \ b \ DERIV (diff m) t :> (diff (Suc m) t))" berghofe@17634 53 and INTERV: "a < c" "c \ b" berghofe@17634 54 shows "\ t. a < t & t < c & lp15@59730 55 f a = (\m0" "((\m x. diff m (x + c)) 0) = (\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) = (\m f a = (\m0" "diff 0 = f" berghofe@17634 85 and DERIV: "(\ m t. m < n & a \ t & t \ b \ DERIV (diff m) t :> (diff (Suc m) t))" berghofe@17634 86 and INTERV: "a \ c " "c \ b" "a \ x" "x \ b" "x \ c" berghofe@17634 87 shows "\ t. (if xmm t. m < n \ x \ t \ t \ b \ 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 \ b" by simp lp15@59730 97 ultimately have "\t>x. t < c \ f x = lp15@59730 98 (\mm t. m < n \ a \ t \ t \ x \ DERIV (diff m) t :> diff (Suc m) t" nipkow@44890 106 by fastforce berghofe@17634 107 moreover from INTERV have "a \ c" by arith berghofe@17634 108 moreover from False and INTERV have "c < x" by arith lp15@59730 109 ultimately have "\t>c. t < x \ f x = lp15@59730 110 (\m