author | wenzelm |

Sun Jul 31 18:05:20 2016 +0200 (2016-07-31) | |

changeset 63570 | 1826a90b9cbc |

parent 63569 | 7e0b0db5e9ac |

child 63571 | aee0d92995b6 |

simplified theory structure;

src/HOL/Complex_Main.thy | file | annotate | diff | revisions | |

src/HOL/Decision_Procs/Approximation.thy | file | annotate | diff | revisions | |

src/HOL/MacLaurin.thy | file | annotate | diff | revisions | |

src/HOL/Taylor.thy | file | annotate | diff | revisions |

1.1 --- a/src/HOL/Complex_Main.thy Sun Jul 31 17:25:38 2016 +0200 1.2 +++ b/src/HOL/Complex_Main.thy Sun Jul 31 18:05:20 2016 +0200 1.3 @@ -6,7 +6,7 @@ 1.4 Real 1.5 Complex 1.6 Transcendental 1.7 - Taylor 1.8 + MacLaurin 1.9 Deriv 1.10 begin 1.11

2.1 --- a/src/HOL/Decision_Procs/Approximation.thy Sun Jul 31 17:25:38 2016 +0200 2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Sun Jul 31 18:05:20 2016 +0200 2.3 @@ -4075,7 +4075,7 @@ 2.4 case False 2.5 have "lx \<le> real_of_float c" "real_of_float c \<le> ux" "lx \<le> xs!x" "xs!x \<le> ux" 2.6 using Suc bnd_c \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>] bnd_x by auto 2.7 - from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False] 2.8 + from taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False] 2.9 obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x" 2.10 and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) = 2.11 (\<Sum>m = 0..<Suc n'. F m c / (fact m) * (xs ! x - c) ^ m) +

3.1 --- a/src/HOL/MacLaurin.thy Sun Jul 31 17:25:38 2016 +0200 3.2 +++ b/src/HOL/MacLaurin.thy Sun Jul 31 18:05:20 2016 +0200 3.3 @@ -4,7 +4,7 @@ 3.4 Author: Lukas Bulwahn and Bernhard HÃ¤upler, 2005 3.5 *) 3.6 3.7 -section \<open>MacLaurin Series\<close> 3.8 +section \<open>MacLaurin and Taylor Series\<close> 3.9 3.10 theory MacLaurin 3.11 imports Transcendental 3.12 @@ -556,4 +556,118 @@ 3.13 done 3.14 qed 3.15 3.16 + 3.17 +section \<open>Taylor series\<close> 3.18 + 3.19 +text \<open> 3.20 + We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close> 3.21 + to prove Taylor's theorem. 3.22 +\<close> 3.23 + 3.24 +lemma taylor_up: 3.25 + assumes INIT: "n > 0" "diff 0 = f" 3.26 + and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)" 3.27 + and INTERV: "a \<le> c" "c < b" 3.28 + shows "\<exists>t::real. c < t \<and> t < b \<and> 3.29 + f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n" 3.30 +proof - 3.31 + from INTERV have "0 < b - c" by arith 3.32 + moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" 3.33 + by auto 3.34 + moreover 3.35 + have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> b - c \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" 3.36 + proof (intro strip) 3.37 + fix m t 3.38 + assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c" 3.39 + with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" 3.40 + by auto 3.41 + moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" 3.42 + by (rule DERIV_add) 3.43 + ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" 3.44 + by (rule DERIV_chain2) 3.45 + then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" 3.46 + by simp 3.47 + qed 3.48 + ultimately obtain x where 3.49 + "0 < x \<and> x < b - c \<and> 3.50 + f (b - c + c) = 3.51 + (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" 3.52 + by (rule Maclaurin [THEN exE]) 3.53 + then have "c < x + c \<and> x + c < b \<and> f b = 3.54 + (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" 3.55 + by fastforce 3.56 + then show ?thesis by fastforce 3.57 +qed 3.58 + 3.59 +lemma taylor_down: 3.60 + fixes a :: real and n :: nat 3.61 + assumes INIT: "n > 0" "diff 0 = f" 3.62 + and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)" 3.63 + and INTERV: "a < c" "c \<le> b" 3.64 + shows "\<exists>t. a < t \<and> t < c \<and> 3.65 + f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n" 3.66 +proof - 3.67 + from INTERV have "a-c < 0" by arith 3.68 + moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" 3.69 + by auto 3.70 + moreover 3.71 + have "\<forall>m t. m < n \<and> a - c \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" 3.72 + proof (rule allI impI)+ 3.73 + fix m t 3.74 + assume "m < n \<and> a - c \<le> t \<and> t \<le> 0" 3.75 + with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" 3.76 + by auto 3.77 + moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" 3.78 + by (rule DERIV_add) 3.79 + ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" 3.80 + by (rule DERIV_chain2) 3.81 + then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" 3.82 + by simp 3.83 + qed 3.84 + ultimately obtain x where 3.85 + "a - c < x \<and> x < 0 \<and> 3.86 + f (a - c + c) = 3.87 + (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" 3.88 + by (rule Maclaurin_minus [THEN exE]) 3.89 + then have "a < x + c \<and> x + c < c \<and> 3.90 + f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" 3.91 + by fastforce 3.92 + then show ?thesis by fastforce 3.93 +qed 3.94 + 3.95 +theorem taylor: 3.96 + fixes a :: real and n :: nat 3.97 + assumes INIT: "n > 0" "diff 0 = f" 3.98 + and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 3.99 + and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 3.100 + shows "\<exists>t. 3.101 + (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and> 3.102 + f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n" 3.103 +proof (cases "x < c") 3.104 + case True 3.105 + note INIT 3.106 + moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 3.107 + using DERIV and INTERV by fastforce 3.108 + moreover note True 3.109 + moreover from INTERV have "c \<le> b" 3.110 + by simp 3.111 + ultimately have "\<exists>t>x. t < c \<and> f x = 3.112 + (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" 3.113 + by (rule taylor_down) 3.114 + with True show ?thesis by simp 3.115 +next 3.116 + case False 3.117 + note INIT 3.118 + moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 3.119 + using DERIV and INTERV by fastforce 3.120 + moreover from INTERV have "a \<le> c" 3.121 + by arith 3.122 + moreover from False and INTERV have "c < x" 3.123 + by arith 3.124 + ultimately have "\<exists>t>c. t < x \<and> f x = 3.125 + (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" 3.126 + by (rule taylor_up) 3.127 + with False show ?thesis by simp 3.128 +qed 3.129 + 3.130 end

4.1 --- a/src/HOL/Taylor.thy Sun Jul 31 17:25:38 2016 +0200 4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 4.3 @@ -1,122 +0,0 @@ 4.4 -(* Title: HOL/Taylor.thy 4.5 - Author: Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen 4.6 -*) 4.7 - 4.8 -section \<open>Taylor series\<close> 4.9 - 4.10 -theory Taylor 4.11 -imports MacLaurin 4.12 -begin 4.13 - 4.14 -text \<open> 4.15 - We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close> 4.16 - to prove Taylor's theorem. 4.17 -\<close> 4.18 - 4.19 -lemma taylor_up: 4.20 - assumes INIT: "n > 0" "diff 0 = f" 4.21 - and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)" 4.22 - and INTERV: "a \<le> c" "c < b" 4.23 - shows "\<exists>t::real. c < t \<and> t < b \<and> 4.24 - f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n" 4.25 -proof - 4.26 - from INTERV have "0 < b - c" by arith 4.27 - moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" 4.28 - by auto 4.29 - moreover 4.30 - have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> b - c \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" 4.31 - proof (intro strip) 4.32 - fix m t 4.33 - assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c" 4.34 - with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" 4.35 - by auto 4.36 - moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" 4.37 - by (rule DERIV_add) 4.38 - ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" 4.39 - by (rule DERIV_chain2) 4.40 - then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" 4.41 - by simp 4.42 - qed 4.43 - ultimately obtain x where 4.44 - "0 < x \<and> x < b - c \<and> 4.45 - f (b - c + c) = 4.46 - (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" 4.47 - by (rule Maclaurin [THEN exE]) 4.48 - then have "c < x + c \<and> x + c < b \<and> f b = 4.49 - (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" 4.50 - by fastforce 4.51 - then show ?thesis by fastforce 4.52 -qed 4.53 - 4.54 -lemma taylor_down: 4.55 - fixes a :: real and n :: nat 4.56 - assumes INIT: "n > 0" "diff 0 = f" 4.57 - and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)" 4.58 - and INTERV: "a < c" "c \<le> b" 4.59 - shows "\<exists>t. a < t \<and> t < c \<and> 4.60 - f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n" 4.61 -proof - 4.62 - from INTERV have "a-c < 0" by arith 4.63 - moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" 4.64 - by auto 4.65 - moreover 4.66 - have "\<forall>m t. m < n \<and> a - c \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" 4.67 - proof (rule allI impI)+ 4.68 - fix m t 4.69 - assume "m < n \<and> a - c \<le> t \<and> t \<le> 0" 4.70 - with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" 4.71 - by auto 4.72 - moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" 4.73 - by (rule DERIV_add) 4.74 - ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" 4.75 - by (rule DERIV_chain2) 4.76 - then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" 4.77 - by simp 4.78 - qed 4.79 - ultimately obtain x where 4.80 - "a - c < x \<and> x < 0 \<and> 4.81 - f (a - c + c) = 4.82 - (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" 4.83 - by (rule Maclaurin_minus [THEN exE]) 4.84 - then have "a < x + c \<and> x + c < c \<and> 4.85 - f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" 4.86 - by fastforce 4.87 - then show ?thesis by fastforce 4.88 -qed 4.89 - 4.90 -theorem taylor: 4.91 - fixes a :: real and n :: nat 4.92 - assumes INIT: "n > 0" "diff 0 = f" 4.93 - and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 4.94 - and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 4.95 - shows "\<exists>t. 4.96 - (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and> 4.97 - f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n" 4.98 -proof (cases "x < c") 4.99 - case True 4.100 - note INIT 4.101 - moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 4.102 - using DERIV and INTERV by fastforce 4.103 - moreover note True 4.104 - moreover from INTERV have "c \<le> b" 4.105 - by simp 4.106 - ultimately have "\<exists>t>x. t < c \<and> f x = 4.107 - (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" 4.108 - by (rule taylor_down) 4.109 - with True show ?thesis by simp 4.110 -next 4.111 - case False 4.112 - note INIT 4.113 - moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 4.114 - using DERIV and INTERV by fastforce 4.115 - moreover from INTERV have "a \<le> c" 4.116 - by arith 4.117 - moreover from False and INTERV have "c < x" 4.118 - by arith 4.119 - ultimately have "\<exists>t>c. t < x \<and> f x = 4.120 - (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" 4.121 - by (rule taylor_up) 4.122 - with False show ?thesis by simp 4.123 -qed 4.124 - 4.125 -end