summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 31 Jul 2016 18:05:20 +0200 | |

changeset 63570 | 1826a90b9cbc |

parent 63569 | 7e0b0db5e9ac |

child 63571 | aee0d92995b6 |

simplified theory structure;

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

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

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

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

--- a/src/HOL/Complex_Main.thy Sun Jul 31 17:25:38 2016 +0200 +++ b/src/HOL/Complex_Main.thy Sun Jul 31 18:05:20 2016 +0200 @@ -6,7 +6,7 @@ Real Complex Transcendental - Taylor + MacLaurin Deriv begin

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

--- a/src/HOL/MacLaurin.thy Sun Jul 31 17:25:38 2016 +0200 +++ b/src/HOL/MacLaurin.thy Sun Jul 31 18:05:20 2016 +0200 @@ -4,7 +4,7 @@ Author: Lukas Bulwahn and Bernhard HÃ¤upler, 2005 *) -section \<open>MacLaurin Series\<close> +section \<open>MacLaurin and Taylor Series\<close> theory MacLaurin imports Transcendental @@ -556,4 +556,118 @@ done qed + +section \<open>Taylor series\<close> + +text \<open> + We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close> + to prove Taylor's theorem. +\<close> + +lemma taylor_up: + assumes INIT: "n > 0" "diff 0 = f" + and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)" + and INTERV: "a \<le> c" "c < b" + shows "\<exists>t::real. c < t \<and> t < b \<and> + f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n" +proof - + from INTERV have "0 < b - c" by arith + moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" + by auto + moreover + 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)" + proof (intro strip) + fix m t + assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c" + with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" + by auto + moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" + by (rule DERIV_add) + ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" + by (rule DERIV_chain2) + then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" + by simp + qed + ultimately obtain x where + "0 < x \<and> x < b - c \<and> + f (b - c + c) = + (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" + by (rule Maclaurin [THEN exE]) + then have "c < x + c \<and> x + c < b \<and> f b = + (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" + by fastforce + then show ?thesis by fastforce +qed + +lemma taylor_down: + fixes a :: real and n :: nat + assumes INIT: "n > 0" "diff 0 = f" + and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)" + and INTERV: "a < c" "c \<le> b" + shows "\<exists>t. a < t \<and> t < c \<and> + f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n" +proof - + from INTERV have "a-c < 0" by arith + moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" + by auto + moreover + 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)" + proof (rule allI impI)+ + fix m t + assume "m < n \<and> a - c \<le> t \<and> t \<le> 0" + with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" + by auto + moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" + by (rule DERIV_add) + ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" + by (rule DERIV_chain2) + then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" + by simp + qed + ultimately obtain x where + "a - c < x \<and> x < 0 \<and> + f (a - c + c) = + (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" + by (rule Maclaurin_minus [THEN exE]) + then have "a < x + c \<and> x + c < c \<and> + f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" + by fastforce + then show ?thesis by fastforce +qed + +theorem taylor: + fixes a :: real and n :: nat + assumes INIT: "n > 0" "diff 0 = f" + and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" + and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" + shows "\<exists>t. + (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and> + f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n" +proof (cases "x < c") + case True + note INIT + moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" + using DERIV and INTERV by fastforce + moreover note True + moreover from INTERV have "c \<le> b" + by simp + ultimately have "\<exists>t>x. t < c \<and> f x = + (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" + by (rule taylor_down) + with True show ?thesis by simp +next + case False + note INIT + moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" + using DERIV and INTERV by fastforce + moreover from INTERV have "a \<le> c" + by arith + moreover from False and INTERV have "c < x" + by arith + ultimately have "\<exists>t>c. t < x \<and> f x = + (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" + by (rule taylor_up) + with False show ?thesis by simp +qed + end

--- a/src/HOL/Taylor.thy Sun Jul 31 17:25:38 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,122 +0,0 @@ -(* Title: HOL/Taylor.thy - Author: Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen -*) - -section \<open>Taylor series\<close> - -theory Taylor -imports MacLaurin -begin - -text \<open> - We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close> - to prove Taylor's theorem. -\<close> - -lemma taylor_up: - assumes INIT: "n > 0" "diff 0 = f" - and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)" - and INTERV: "a \<le> c" "c < b" - shows "\<exists>t::real. c < t \<and> t < b \<and> - f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n" -proof - - from INTERV have "0 < b - c" by arith - moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" - by auto - moreover - 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)" - proof (intro strip) - fix m t - assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c" - with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" - by auto - moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" - by (rule DERIV_add) - ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" - by (rule DERIV_chain2) - then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" - by simp - qed - ultimately obtain x where - "0 < x \<and> x < b - c \<and> - f (b - c + c) = - (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" - by (rule Maclaurin [THEN exE]) - then have "c < x + c \<and> x + c < b \<and> f b = - (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" - by fastforce - then show ?thesis by fastforce -qed - -lemma taylor_down: - fixes a :: real and n :: nat - assumes INIT: "n > 0" "diff 0 = f" - and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)" - and INTERV: "a < c" "c \<le> b" - shows "\<exists>t. a < t \<and> t < c \<and> - f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n" -proof - - from INTERV have "a-c < 0" by arith - moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" - by auto - moreover - 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)" - proof (rule allI impI)+ - fix m t - assume "m < n \<and> a - c \<le> t \<and> t \<le> 0" - with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" - by auto - moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" - by (rule DERIV_add) - ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" - by (rule DERIV_chain2) - then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" - by simp - qed - ultimately obtain x where - "a - c < x \<and> x < 0 \<and> - f (a - c + c) = - (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" - by (rule Maclaurin_minus [THEN exE]) - then have "a < x + c \<and> x + c < c \<and> - f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" - by fastforce - then show ?thesis by fastforce -qed - -theorem taylor: - fixes a :: real and n :: nat - assumes INIT: "n > 0" "diff 0 = f" - and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" - and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" - shows "\<exists>t. - (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and> - f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n" -proof (cases "x < c") - case True - note INIT - moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" - using DERIV and INTERV by fastforce - moreover note True - moreover from INTERV have "c \<le> b" - by simp - ultimately have "\<exists>t>x. t < c \<and> f x = - (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" - by (rule taylor_down) - with True show ?thesis by simp -next - case False - note INIT - moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" - using DERIV and INTERV by fastforce - moreover from INTERV have "a \<le> c" - by arith - moreover from False and INTERV have "c < x" - by arith - ultimately have "\<exists>t>c. t < x \<and> f x = - (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" - by (rule taylor_up) - with False show ?thesis by simp -qed - -end