author | wenzelm |
Sun, 31 Jul 2016 17:25:38 +0200 | |
changeset 63569 | 7e0b0db5e9ac |
parent 61954 | 1d43f86f48be |
permissions | -rw-r--r-- |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
25162
diff
changeset
|
1 |
(* Title: HOL/Taylor.thy |
17634 | 2 |
Author: Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen |
3 |
*) |
|
4 |
||
60758 | 5 |
section \<open>Taylor series\<close> |
17634 | 6 |
|
7 |
theory Taylor |
|
8 |
imports MacLaurin |
|
9 |
begin |
|
10 |
||
60758 | 11 |
text \<open> |
63569 | 12 |
We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close> |
13 |
to prove Taylor's theorem. |
|
60758 | 14 |
\<close> |
17634 | 15 |
|
63569 | 16 |
lemma taylor_up: |
17 |
assumes INIT: "n > 0" "diff 0 = f" |
|
18 |
and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)" |
|
19 |
and INTERV: "a \<le> c" "c < b" |
|
20 |
shows "\<exists>t::real. c < t \<and> t < b \<and> |
|
21 |
f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n" |
|
17634 | 22 |
proof - |
63569 | 23 |
from INTERV have "0 < b - c" by arith |
24 |
moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" |
|
25 |
by auto |
|
17634 | 26 |
moreover |
63569 | 27 |
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)" |
17634 | 28 |
proof (intro strip) |
29 |
fix m t |
|
63569 | 30 |
assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c" |
31 |
with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" |
|
32 |
by auto |
|
33 |
moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" |
|
34 |
by (rule DERIV_add) |
|
35 |
ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" |
|
17634 | 36 |
by (rule DERIV_chain2) |
63569 | 37 |
then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" |
38 |
by simp |
|
17634 | 39 |
qed |
63569 | 40 |
ultimately obtain x where |
41 |
"0 < x \<and> x < b - c \<and> |
|
42 |
f (b - c + c) = |
|
43 |
(\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
44 |
by (rule Maclaurin [THEN exE]) |
63569 | 45 |
then have "c < x + c \<and> x + c < b \<and> f b = |
46 |
(\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
47 |
by fastforce |
63569 | 48 |
then show ?thesis by fastforce |
17634 | 49 |
qed |
50 |
||
51 |
lemma taylor_down: |
|
63569 | 52 |
fixes a :: real and n :: nat |
53 |
assumes INIT: "n > 0" "diff 0 = f" |
|
54 |
and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)" |
|
55 |
and INTERV: "a < c" "c \<le> b" |
|
56 |
shows "\<exists>t. a < t \<and> t < c \<and> |
|
57 |
f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n" |
|
17634 | 58 |
proof - |
59 |
from INTERV have "a-c < 0" by arith |
|
63569 | 60 |
moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" |
61 |
by auto |
|
17634 | 62 |
moreover |
63569 | 63 |
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)" |
17634 | 64 |
proof (rule allI impI)+ |
65 |
fix m t |
|
63569 | 66 |
assume "m < n \<and> a - c \<le> t \<and> t \<le> 0" |
67 |
with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" |
|
68 |
by auto |
|
69 |
moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" |
|
70 |
by (rule DERIV_add) |
|
71 |
ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" |
|
72 |
by (rule DERIV_chain2) |
|
73 |
then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" |
|
74 |
by simp |
|
17634 | 75 |
qed |
63569 | 76 |
ultimately obtain x where |
77 |
"a - c < x \<and> x < 0 \<and> |
|
78 |
f (a - c + c) = |
|
79 |
(\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" |
|
80 |
by (rule Maclaurin_minus [THEN exE]) |
|
81 |
then have "a < x + c \<and> x + c < c \<and> |
|
82 |
f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
83 |
by fastforce |
63569 | 84 |
then show ?thesis by fastforce |
17634 | 85 |
qed |
86 |
||
63569 | 87 |
theorem taylor: |
88 |
fixes a :: real and n :: nat |
|
89 |
assumes INIT: "n > 0" "diff 0 = f" |
|
90 |
and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
91 |
and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" |
|
92 |
shows "\<exists>t. |
|
93 |
(if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and> |
|
94 |
f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n" |
|
95 |
proof (cases "x < c") |
|
17634 | 96 |
case True |
97 |
note INIT |
|
63569 | 98 |
moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
99 |
using DERIV and INTERV by fastforce |
|
17634 | 100 |
moreover note True |
63569 | 101 |
moreover from INTERV have "c \<le> b" |
102 |
by simp |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
103 |
ultimately have "\<exists>t>x. t < c \<and> f x = |
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
104 |
(\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" |
17634 | 105 |
by (rule taylor_down) |
106 |
with True show ?thesis by simp |
|
107 |
next |
|
108 |
case False |
|
109 |
note INIT |
|
63569 | 110 |
moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
111 |
using DERIV and INTERV by fastforce |
|
112 |
moreover from INTERV have "a \<le> c" |
|
113 |
by arith |
|
114 |
moreover from False and INTERV have "c < x" |
|
115 |
by arith |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
116 |
ultimately have "\<exists>t>c. t < x \<and> f x = |
63569 | 117 |
(\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" |
17634 | 118 |
by (rule taylor_up) |
119 |
with False show ?thesis by simp |
|
120 |
qed |
|
121 |
||
122 |
end |