author | paulson <lp15@cam.ac.uk> |
Sat, 21 Jul 2018 23:25:22 +0200 | |
changeset 68671 | 205749fba102 |
parent 68669 | 7ddf297cfcde |
child 69020 | 4f94e262976d |
permissions | -rw-r--r-- |
63569 | 1 |
(* Title: HOL/MacLaurin.thy |
2 |
Author: Jacques D. Fleuriot, 2001 University of Edinburgh |
|
3 |
Author: Lawrence C Paulson, 2004 |
|
4 |
Author: Lukas Bulwahn and Bernhard Häupler, 2005 |
|
12224 | 5 |
*) |
6 |
||
63570 | 7 |
section \<open>MacLaurin and Taylor Series\<close> |
15944 | 8 |
|
15131 | 9 |
theory MacLaurin |
29811
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieb-laptop
parents:
29803
diff
changeset
|
10 |
imports Transcendental |
15131 | 11 |
begin |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
12 |
|
63569 | 13 |
subsection \<open>Maclaurin's Theorem with Lagrange Form of Remainder\<close> |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
14 |
|
63569 | 15 |
text \<open>This is a very long, messy proof even now that it's been broken down |
16 |
into lemmas.\<close> |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
17 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
18 |
lemma Maclaurin_lemma: |
63569 | 19 |
"0 < h \<Longrightarrow> |
20 |
\<exists>B::real. f h = (\<Sum>m<n. (j m / (fact m)) * (h^m)) + (B * ((h^n) /(fact n)))" |
|
21 |
by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / (fact m)) * h^m)) * (fact n) / (h^n)"]) simp |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
22 |
|
63569 | 23 |
lemma eq_diff_eq': "x = y - z \<longleftrightarrow> y = x + z" |
24 |
for x y z :: real |
|
25 |
by arith |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
26 |
|
63569 | 27 |
lemma fact_diff_Suc: "n < Suc m \<Longrightarrow> fact (Suc m - n) = (Suc m - n) * fact (m - n)" |
28 |
by (subst fact_reduce) auto |
|
32038 | 29 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
30 |
lemma Maclaurin_lemma2: |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
31 |
fixes B |
63569 | 32 |
assumes DERIV: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
33 |
and INIT: "n = Suc k" |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
34 |
defines "difg \<equiv> |
63569 | 35 |
(\<lambda>m t::real. diff m t - |
36 |
((\<Sum>p<n - m. diff (m + p) 0 / fact p * t ^ p) + B * (t ^ (n - m) / fact (n - m))))" |
|
37 |
(is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)") |
|
38 |
shows "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t" |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
39 |
proof (rule allI impI)+ |
63569 | 40 |
fix m t |
41 |
assume INIT2: "m < n \<and> 0 \<le> t \<and> t \<le> h" |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
42 |
have "DERIV (difg m) t :> diff (Suc m) t - |
63569 | 43 |
((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) + |
44 |
real (n - m) * t ^ (n - Suc m) * B / fact (n - m))" |
|
45 |
by (auto simp: difg_def intro!: derivative_eq_intros DERIV[rule_format, OF INIT2]) |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset
|
46 |
moreover |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
47 |
from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m" |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
48 |
unfolding atLeast0LessThan[symmetric] by auto |
63569 | 49 |
have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) = |
50 |
(\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x))" |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
51 |
unfolding intvl by (subst sum.insert) (auto simp: sum.reindex) |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
52 |
moreover |
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
53 |
have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0" |
63569 | 54 |
by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2 |
55 |
less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff) |
|
56 |
have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x) = diff (Suc m + x) 0 * t^x / fact x" |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
57 |
by (rule nonzero_divide_eq_eq[THEN iffD2]) auto |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
58 |
moreover |
63569 | 59 |
have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))" |
60 |
using \<open>0 < n - m\<close> by (simp add: divide_simps fact_reduce) |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
61 |
ultimately show "DERIV (difg m) t :> difg (Suc m) t" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
62 |
unfolding difg_def by (simp add: mult.commute) |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
63 |
qed |
32038 | 64 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
65 |
lemma Maclaurin: |
29187 | 66 |
assumes h: "0 < h" |
63569 | 67 |
and n: "0 < n" |
68 |
and diff_0: "diff 0 = f" |
|
69 |
and diff_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
29187 | 70 |
shows |
63569 | 71 |
"\<exists>t::real. 0 < t \<and> t < h \<and> |
64267 | 72 |
f h = sum (\<lambda>m. (diff m 0 / fact m) * h ^ m) {..<n} + (diff n t / fact n) * h ^ n" |
29187 | 73 |
proof - |
74 |
from n obtain m where m: "n = Suc m" |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
75 |
by (cases n) (simp add: n) |
63569 | 76 |
from m have "m < n" by simp |
29187 | 77 |
|
63569 | 78 |
obtain B where f_h: "f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + B * (h ^ n / fact n)" |
29187 | 79 |
using Maclaurin_lemma [OF h] .. |
80 |
||
63040 | 81 |
define g where [abs_def]: "g t = |
64267 | 82 |
f t - (sum (\<lambda>m. (diff m 0 / fact m) * t^m) {..<n} + B * (t^n / fact n))" for t |
63569 | 83 |
have g2: "g 0 = 0" "g h = 0" |
64267 | 84 |
by (simp_all add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 sum.reindex) |
29187 | 85 |
|
63040 | 86 |
define difg where [abs_def]: "difg m t = |
64267 | 87 |
diff m t - (sum (\<lambda>p. (diff (m + p) 0 / fact p) * (t ^ p)) {..<n-m} + |
63569 | 88 |
B * ((t ^ (n - m)) / fact (n - m)))" for m t |
29187 | 89 |
have difg_0: "difg 0 = g" |
63569 | 90 |
by (simp add: difg_def g_def diff_0) |
91 |
have difg_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t" |
|
63040 | 92 |
using diff_Suc m unfolding difg_def [abs_def] by (rule Maclaurin_lemma2) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset
|
93 |
have difg_eq_0: "\<forall>m<n. difg m 0 = 0" |
64267 | 94 |
by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff sum.reindex) |
63569 | 95 |
have isCont_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> isCont (difg m) x" |
29187 | 96 |
by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp |
63569 | 97 |
have differentiable_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> difg m differentiable (at x)" |
29187 | 98 |
by (rule differentiableI [OF difg_Suc [rule_format]]) simp |
63569 | 99 |
have difg_Suc_eq_0: |
100 |
"\<And>m t. m < n \<Longrightarrow> 0 \<le> t \<Longrightarrow> t \<le> h \<Longrightarrow> DERIV (difg m) t :> 0 \<Longrightarrow> difg (Suc m) t = 0" |
|
29187 | 101 |
by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp |
102 |
||
103 |
have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0" |
|
60758 | 104 |
using \<open>m < n\<close> |
29187 | 105 |
proof (induct m) |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
106 |
case 0 |
29187 | 107 |
show ?case |
108 |
proof (rule Rolle) |
|
109 |
show "0 < h" by fact |
|
63569 | 110 |
show "difg 0 0 = difg 0 h" |
111 |
by (simp add: difg_0 g2) |
|
61076 | 112 |
show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0::nat)) x" |
29187 | 113 |
by (simp add: isCont_difg n) |
61076 | 114 |
show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0::nat) differentiable (at x)" |
29187 | 115 |
by (simp add: differentiable_difg n) |
116 |
qed |
|
117 |
next |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
118 |
case (Suc m') |
63569 | 119 |
then have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" |
120 |
by simp |
|
121 |
then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" |
|
122 |
by fast |
|
29187 | 123 |
have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0" |
124 |
proof (rule Rolle) |
|
125 |
show "0 < t" by fact |
|
126 |
show "difg (Suc m') 0 = difg (Suc m') t" |
|
60758 | 127 |
using t \<open>Suc m' < n\<close> by (simp add: difg_Suc_eq_0 difg_eq_0) |
29187 | 128 |
show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x" |
60758 | 129 |
using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: isCont_difg) |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
51489
diff
changeset
|
130 |
show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable (at x)" |
60758 | 131 |
using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: differentiable_difg) |
29187 | 132 |
qed |
63569 | 133 |
with \<open>t < h\<close> show ?case |
134 |
by auto |
|
29187 | 135 |
qed |
63569 | 136 |
then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" |
137 |
by fast |
|
138 |
with \<open>m < n\<close> have "difg (Suc m) t = 0" |
|
139 |
by (simp add: difg_Suc_eq_0) |
|
29187 | 140 |
show ?thesis |
141 |
proof (intro exI conjI) |
|
142 |
show "0 < t" by fact |
|
143 |
show "t < h" by fact |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
144 |
show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n" |
63569 | 145 |
using \<open>difg (Suc m) t = 0\<close> by (simp add: m f_h difg_def) |
29187 | 146 |
qed |
147 |
qed |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
148 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
149 |
lemma Maclaurin2: |
63569 | 150 |
fixes n :: nat |
151 |
and h :: real |
|
152 |
assumes INIT1: "0 < h" |
|
153 |
and INIT2: "diff 0 = f" |
|
154 |
and DERIV: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
155 |
shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / fact n * h ^ n" |
|
156 |
proof (cases n) |
|
157 |
case 0 |
|
158 |
with INIT1 INIT2 show ?thesis by fastforce |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
159 |
next |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
160 |
case Suc |
63569 | 161 |
then have "n > 0" by simp |
162 |
from INIT1 this INIT2 DERIV |
|
163 |
have "\<exists>t>0. t < h \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n" |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
164 |
by (rule Maclaurin) |
63569 | 165 |
then show ?thesis by fastforce |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
166 |
qed |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
167 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
168 |
lemma Maclaurin_minus: |
63569 | 169 |
fixes n :: nat and h :: real |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
170 |
assumes "h < 0" "0 < n" "diff 0 = f" |
63569 | 171 |
and DERIV: "\<forall>m t. m < n \<and> h \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
172 |
shows "\<exists>t. h < t \<and> t < 0 \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n" |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
173 |
proof - |
63569 | 174 |
txt \<open>Transform \<open>ABL'\<close> into \<open>derivative_intros\<close> format.\<close> |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
175 |
note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong] |
63569 | 176 |
let ?sum = "\<lambda>t. |
177 |
(\<Sum>m<n. (- 1) ^ m * diff m (- 0) / (fact m) * (- h) ^ m) + |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
178 |
(- 1) ^ n * diff n (- t) / (fact n) * (- h) ^ n" |
63569 | 179 |
from assms have "\<exists>t>0. t < - h \<and> f (- (- h)) = ?sum t" |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset
|
180 |
by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV') |
63569 | 181 |
then obtain t where "0 < t" "t < - h" "f (- (- h)) = ?sum t" |
182 |
by blast |
|
183 |
moreover have "(- 1) ^ n * diff n (- t) * (- h) ^ n / fact n = diff n (- t) * h ^ n / fact n" |
|
184 |
by (auto simp: power_mult_distrib[symmetric]) |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
185 |
moreover |
63569 | 186 |
have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / fact m) = (\<Sum>m<n. diff m 0 * h ^ m / fact m)" |
64267 | 187 |
by (auto intro: sum.cong simp add: power_mult_distrib[symmetric]) |
63569 | 188 |
ultimately have "h < - t \<and> - t < 0 \<and> |
189 |
f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n (- t) / (fact n) * h ^ n" |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
190 |
by auto |
63569 | 191 |
then show ?thesis .. |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
192 |
qed |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
193 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
194 |
|
63569 | 195 |
subsection \<open>More Convenient "Bidirectional" Version.\<close> |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
196 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
197 |
lemma Maclaurin_bi_le: |
63569 | 198 |
fixes n :: nat and x :: real |
199 |
assumes "diff 0 = f" |
|
200 |
and DERIV : "\<forall>m t. m < n \<and> \<bar>t\<bar> \<le> \<bar>x\<bar> \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
201 |
shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) + diff n t / (fact n) * x ^ n" |
|
202 |
(is "\<exists>t. _ \<and> f x = ?f x t") |
|
203 |
proof (cases "n = 0") |
|
204 |
case True |
|
205 |
with \<open>diff 0 = f\<close> show ?thesis by force |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
206 |
next |
63569 | 207 |
case False |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
208 |
show ?thesis |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
209 |
proof (cases rule: linorder_cases) |
63569 | 210 |
assume "x = 0" |
211 |
with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" |
|
68669 | 212 |
by auto |
63569 | 213 |
then show ?thesis .. |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
214 |
next |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
215 |
assume "x < 0" |
63569 | 216 |
with \<open>n \<noteq> 0\<close> DERIV have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t" |
217 |
by (intro Maclaurin_minus) auto |
|
218 |
then obtain t where "x < t" "t < 0" |
|
219 |
"diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n" |
|
220 |
by blast |
|
221 |
with \<open>x < 0\<close> \<open>diff 0 = f\<close> have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" |
|
222 |
by simp |
|
223 |
then show ?thesis .. |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
224 |
next |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
225 |
assume "x > 0" |
63569 | 226 |
with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t" |
227 |
by (intro Maclaurin) auto |
|
228 |
then obtain t where "0 < t" "t < x" |
|
229 |
"diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n" |
|
230 |
by blast |
|
60758 | 231 |
with \<open>x > 0\<close> \<open>diff 0 = f\<close> have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp |
63569 | 232 |
then show ?thesis .. |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
233 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
234 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
235 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
236 |
lemma Maclaurin_all_lt: |
63569 | 237 |
fixes x :: real |
238 |
assumes INIT1: "diff 0 = f" |
|
239 |
and INIT2: "0 < n" |
|
240 |
and INIT3: "x \<noteq> 0" |
|
241 |
and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x" |
|
242 |
shows "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = |
|
243 |
(\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n" |
|
244 |
(is "\<exists>t. _ \<and> _ \<and> f x = ?f x t") |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
245 |
proof (cases rule: linorder_cases) |
63569 | 246 |
assume "x = 0" |
247 |
with INIT3 show ?thesis .. |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
248 |
next |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
249 |
assume "x < 0" |
63569 | 250 |
with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t" |
251 |
by (intro Maclaurin_minus) auto |
|
252 |
then obtain t where "t > x" "t < 0" "f x = ?f x t" |
|
253 |
by blast |
|
254 |
with \<open>x < 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" |
|
255 |
by simp |
|
256 |
then show ?thesis .. |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
257 |
next |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
258 |
assume "x > 0" |
63569 | 259 |
with assms have "\<exists>t>0. t < x \<and> f x = ?f x t" |
260 |
by (intro Maclaurin) auto |
|
261 |
then obtain t where "t > 0" "t < x" "f x = ?f x t" |
|
262 |
by blast |
|
263 |
with \<open>x > 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" |
|
264 |
by simp |
|
265 |
then show ?thesis .. |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
266 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
267 |
|
63569 | 268 |
lemma Maclaurin_zero: "x = 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) = diff 0 0" |
269 |
for x :: real and n :: nat |
|
68669 | 270 |
by simp |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
271 |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
272 |
|
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
273 |
lemma Maclaurin_all_le: |
63569 | 274 |
fixes x :: real and n :: nat |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
275 |
assumes INIT: "diff 0 = f" |
63569 | 276 |
and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x" |
277 |
shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n" |
|
278 |
(is "\<exists>t. _ \<and> f x = ?f x t") |
|
279 |
proof (cases "n = 0") |
|
280 |
case True |
|
281 |
with INIT show ?thesis by force |
|
282 |
next |
|
283 |
case False |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
284 |
show ?thesis |
63569 | 285 |
proof (cases "x = 0") |
286 |
case True |
|
60758 | 287 |
with \<open>n \<noteq> 0\<close> have "(\<Sum>m<n. diff m 0 / (fact m) * x ^ m) = diff 0 0" |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
288 |
by (intro Maclaurin_zero) auto |
63569 | 289 |
with INIT \<open>x = 0\<close> \<open>n \<noteq> 0\<close> have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" |
290 |
by force |
|
291 |
then show ?thesis .. |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
292 |
next |
63569 | 293 |
case False |
60758 | 294 |
with INIT \<open>n \<noteq> 0\<close> DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
295 |
by (intro Maclaurin_all_lt) auto |
63569 | 296 |
then obtain t where "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" .. |
297 |
then have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" |
|
298 |
by simp |
|
299 |
then show ?thesis .. |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
300 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
301 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
302 |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
303 |
lemma Maclaurin_all_le_objl: |
63569 | 304 |
"diff 0 = f \<and> (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) \<longrightarrow> |
305 |
(\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n)" |
|
306 |
for x :: real and n :: nat |
|
307 |
by (blast intro: Maclaurin_all_le) |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
308 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
309 |
|
63569 | 310 |
subsection \<open>Version for Exponential Function\<close> |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
311 |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
312 |
lemma Maclaurin_exp_lt: |
63569 | 313 |
fixes x :: real and n :: nat |
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
314 |
shows |
63569 | 315 |
"x \<noteq> 0 \<Longrightarrow> n > 0 \<Longrightarrow> |
316 |
(\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n)" |
|
68669 | 317 |
using Maclaurin_all_lt [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
318 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
319 |
lemma Maclaurin_exp_le: |
63569 | 320 |
fixes x :: real and n :: nat |
321 |
shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n" |
|
322 |
using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto |
|
323 |
||
65273
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
324 |
corollary exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x" |
63569 | 325 |
for x :: real |
326 |
using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square) |
|
327 |
||
65273
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
328 |
corollary ln_2_less_1: "ln 2 < (1::real)" |
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
329 |
proof - |
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
330 |
have "2 < 5/(2::real)" by simp |
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
331 |
also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp |
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
332 |
finally have "exp (ln 2) < exp (1::real)" by simp |
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
333 |
thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp |
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
334 |
qed |
63569 | 335 |
|
336 |
subsection \<open>Version for Sine Function\<close> |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
337 |
|
67091 | 338 |
lemma mod_exhaust_less_4: "m mod 4 = 0 \<or> m mod 4 = 1 \<or> m mod 4 = 2 \<or> m mod 4 = 3" |
63569 | 339 |
for m :: nat |
340 |
by auto |
|
341 |
||
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
342 |
|
63569 | 343 |
text \<open>It is unclear why so many variant results are needed.\<close> |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
344 |
|
63569 | 345 |
lemma sin_expansion_lemma: "sin (x + real (Suc m) * pi / 2) = cos (x + real m * pi / 2)" |
346 |
by (auto simp: cos_add sin_add add_divide_distrib distrib_right) |
|
36974
b877866b5b00
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
huffman
parents:
32047
diff
changeset
|
347 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
348 |
lemma Maclaurin_sin_expansion2: |
63569 | 349 |
"\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> |
350 |
sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n" |
|
68669 | 351 |
proof (cases "n = 0 \<or> x = 0") |
352 |
case False |
|
353 |
let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)" |
|
354 |
have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> sin x = |
|
355 |
(\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n" |
|
356 |
proof (rule Maclaurin_all_lt) |
|
357 |
show "\<forall>m x. ((\<lambda>t. sin (t + 1/2 * real m * pi)) has_real_derivative |
|
358 |
sin (x + 1/2 * real (Suc m) * pi)) (at x)" |
|
359 |
by (rule allI derivative_eq_intros | use sin_expansion_lemma in force)+ |
|
360 |
qed (use False in auto) |
|
361 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
362 |
apply (rule ex_forward, simp) |
68669 | 363 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
364 |
apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc) |
68669 | 365 |
done |
366 |
qed auto |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
367 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
368 |
lemma Maclaurin_sin_expansion: |
63569 | 369 |
"\<exists>t. sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n" |
370 |
using Maclaurin_sin_expansion2 [of x n] by blast |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
371 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
372 |
lemma Maclaurin_sin_expansion3: |
68669 | 373 |
assumes "n > 0" "x > 0" |
374 |
shows "\<exists>t. 0 < t \<and> t < x \<and> |
|
375 |
sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n" |
|
376 |
proof - |
|
377 |
let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)" |
|
378 |
have "\<exists>t. 0 < t \<and> t < x \<and> sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n" |
|
379 |
proof (rule Maclaurin) |
|
380 |
show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> |
|
381 |
((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative |
|
382 |
sin (t + 1/2 * real (Suc m) * pi)) (at t)" |
|
383 |
apply (simp add: sin_expansion_lemma del: of_nat_Suc) |
|
384 |
apply (force intro!: derivative_eq_intros) |
|
385 |
done |
|
386 |
qed (use assms in auto) |
|
387 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
388 |
apply (rule ex_forward, simp) |
68669 | 389 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
390 |
apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc) |
68669 | 391 |
done |
392 |
qed |
|
63569 | 393 |
|
394 |
lemma Maclaurin_sin_expansion4: |
|
68669 | 395 |
assumes "0 < x" |
396 |
shows "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n" |
|
397 |
proof - |
|
398 |
let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)" |
|
399 |
have "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n" |
|
400 |
proof (rule Maclaurin2) |
|
401 |
show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> |
|
402 |
((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative |
|
403 |
sin (t + 1/2 * real (Suc m) * pi)) (at t)" |
|
404 |
apply (simp add: sin_expansion_lemma del: of_nat_Suc) |
|
405 |
apply (force intro!: derivative_eq_intros) |
|
406 |
done |
|
407 |
qed (use assms in auto) |
|
408 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
409 |
apply (rule ex_forward, simp) |
68669 | 410 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
411 |
apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc) |
68669 | 412 |
done |
413 |
qed |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
414 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
415 |
|
63569 | 416 |
subsection \<open>Maclaurin Expansion for Cosine Function\<close> |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
417 |
|
63569 | 418 |
lemma sumr_cos_zero_one [simp]: "(\<Sum>m<Suc n. cos_coeff m * 0 ^ m) = 1" |
419 |
by (induct n) auto |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
420 |
|
63569 | 421 |
lemma cos_expansion_lemma: "cos (x + real (Suc m) * pi / 2) = - sin (x + real m * pi / 2)" |
422 |
by (auto simp: cos_add sin_add distrib_right add_divide_distrib) |
|
36974
b877866b5b00
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
huffman
parents:
32047
diff
changeset
|
423 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
424 |
lemma Maclaurin_cos_expansion: |
63569 | 425 |
"\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> |
426 |
cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos(t + 1/2 * real n * pi) / fact n) * x ^ n" |
|
68669 | 427 |
proof (cases "n = 0 \<or> x = 0") |
428 |
case False |
|
429 |
let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)" |
|
430 |
have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> cos x = |
|
431 |
(\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n" |
|
432 |
proof (rule Maclaurin_all_lt) |
|
433 |
show "\<forall>m x. ((\<lambda>t. cos (t + 1/2 * real m * pi)) has_real_derivative |
|
434 |
cos (x + 1/2 * real (Suc m) * pi)) (at x)" |
|
435 |
apply (rule allI derivative_eq_intros | simp)+ |
|
436 |
using cos_expansion_lemma by force |
|
437 |
qed (use False in auto) |
|
438 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
439 |
apply (rule ex_forward, simp) |
68669 | 440 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
441 |
apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE simp del: of_nat_Suc) |
68669 | 442 |
done |
443 |
qed auto |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
444 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
445 |
lemma Maclaurin_cos_expansion2: |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
446 |
assumes "x > 0" "n > 0" |
68669 | 447 |
shows "\<exists>t. 0 < t \<and> t < x \<and> |
63569 | 448 |
cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos (t + 1/2 * real n * pi) / fact n) * x ^ n" |
68669 | 449 |
proof - |
450 |
let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)" |
|
451 |
have "\<exists>t. 0 < t \<and> t < x \<and> cos x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n" |
|
452 |
proof (rule Maclaurin) |
|
453 |
show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> |
|
454 |
((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative |
|
455 |
cos (t + 1 / 2 * real (Suc m) * pi)) (at t)" |
|
456 |
by (simp add: cos_expansion_lemma del: of_nat_Suc) |
|
457 |
qed (use assms in auto) |
|
458 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
459 |
apply (rule ex_forward, simp) |
68669 | 460 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
461 |
apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE) |
68669 | 462 |
done |
463 |
qed |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
464 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
465 |
lemma Maclaurin_minus_cos_expansion: |
68669 | 466 |
assumes "n > 0" "x < 0" |
467 |
shows "\<exists>t. x < t \<and> t < 0 \<and> |
|
468 |
cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + ((cos (t + 1/2 * real n * pi) / fact n) * x ^ n)" |
|
469 |
proof - |
|
470 |
let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)" |
|
471 |
have "\<exists>t. x < t \<and> t < 0 \<and> cos x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n" |
|
472 |
proof (rule Maclaurin_minus) |
|
473 |
show "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> |
|
474 |
((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative |
|
475 |
cos (t + 1 / 2 * real (Suc m) * pi)) (at t)" |
|
476 |
by (simp add: cos_expansion_lemma del: of_nat_Suc) |
|
477 |
qed (use assms in auto) |
|
478 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
479 |
apply (rule ex_forward, simp) |
68669 | 480 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
481 |
apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE) |
68669 | 482 |
done |
483 |
qed |
|
63569 | 484 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
485 |
|
63569 | 486 |
(* Version for ln(1 +/- x). Where is it?? *) |
487 |
||
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
488 |
|
63569 | 489 |
lemma sin_bound_lemma: "x = y \<Longrightarrow> \<bar>u\<bar> \<le> v \<Longrightarrow> \<bar>(x + u) - y\<bar> \<le> v" |
490 |
for x y u v :: real |
|
491 |
by auto |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
492 |
|
63569 | 493 |
lemma Maclaurin_sin_bound: "\<bar>sin x - (\<Sum>m<n. sin_coeff m * x ^ m)\<bar> \<le> inverse (fact n) * \<bar>x\<bar> ^ n" |
14738 | 494 |
proof - |
63569 | 495 |
have est: "x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" for x y :: real |
496 |
by (rule mult_right_mono) simp_all |
|
68157 | 497 |
let ?diff = "\<lambda>(n::nat) (x::real). |
63569 | 498 |
if n mod 4 = 0 then sin x |
499 |
else if n mod 4 = 1 then cos x |
|
500 |
else if n mod 4 = 2 then - sin x |
|
501 |
else - cos x" |
|
22985 | 502 |
have diff_0: "?diff 0 = sin" by simp |
68157 | 503 |
have "DERIV (?diff m) x :> ?diff (Suc m) x" for m and x |
504 |
using mod_exhaust_less_4 [of m] |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
505 |
by (auto simp: mod_Suc intro!: derivative_eq_intros) |
68157 | 506 |
then have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x" |
507 |
by blast |
|
22985 | 508 |
from Maclaurin_all_le [OF diff_0 DERIV_diff] |
63569 | 509 |
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" |
510 |
and t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / (fact n) * x ^ n" |
|
511 |
by fast |
|
68157 | 512 |
have diff_m_0: "?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))" for m |
513 |
using mod_exhaust_less_4 [of m] |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
514 |
by (auto simp: minus_one_power_iff even_even_mod_4_iff [of m] dest: even_mod_4_div_2 odd_mod_4_div_2) |
14738 | 515 |
show ?thesis |
44306
33572a766836
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
huffman
parents:
41166
diff
changeset
|
516 |
unfolding sin_coeff_def |
22985 | 517 |
apply (subst t2) |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
518 |
apply (rule sin_bound_lemma) |
64267 | 519 |
apply (rule sum.cong[OF refl]) |
63569 | 520 |
apply (subst diff_m_0, simp) |
521 |
using est |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
522 |
apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono |
63569 | 523 |
simp: ac_simps divide_inverse power_abs [symmetric] abs_mult) |
14738 | 524 |
done |
525 |
qed |
|
526 |
||
63570 | 527 |
|
528 |
section \<open>Taylor series\<close> |
|
529 |
||
530 |
text \<open> |
|
531 |
We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close> |
|
532 |
to prove Taylor's theorem. |
|
533 |
\<close> |
|
534 |
||
535 |
lemma taylor_up: |
|
536 |
assumes INIT: "n > 0" "diff 0 = f" |
|
537 |
and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)" |
|
538 |
and INTERV: "a \<le> c" "c < b" |
|
539 |
shows "\<exists>t::real. c < t \<and> t < b \<and> |
|
540 |
f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n" |
|
541 |
proof - |
|
542 |
from INTERV have "0 < b - c" by arith |
|
543 |
moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" |
|
544 |
by auto |
|
545 |
moreover |
|
546 |
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)" |
|
547 |
proof (intro strip) |
|
548 |
fix m t |
|
549 |
assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c" |
|
550 |
with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" |
|
551 |
by auto |
|
552 |
moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" |
|
553 |
by (rule DERIV_add) |
|
554 |
ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" |
|
555 |
by (rule DERIV_chain2) |
|
556 |
then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" |
|
557 |
by simp |
|
558 |
qed |
|
559 |
ultimately obtain x where |
|
560 |
"0 < x \<and> x < b - c \<and> |
|
561 |
f (b - c + c) = |
|
562 |
(\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" |
|
563 |
by (rule Maclaurin [THEN exE]) |
|
564 |
then have "c < x + c \<and> x + c < b \<and> f b = |
|
565 |
(\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" |
|
566 |
by fastforce |
|
567 |
then show ?thesis by fastforce |
|
568 |
qed |
|
569 |
||
570 |
lemma taylor_down: |
|
571 |
fixes a :: real and n :: nat |
|
572 |
assumes INIT: "n > 0" "diff 0 = f" |
|
573 |
and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)" |
|
574 |
and INTERV: "a < c" "c \<le> b" |
|
575 |
shows "\<exists>t. a < t \<and> t < c \<and> |
|
576 |
f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n" |
|
577 |
proof - |
|
578 |
from INTERV have "a-c < 0" by arith |
|
579 |
moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" |
|
580 |
by auto |
|
581 |
moreover |
|
582 |
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)" |
|
583 |
proof (rule allI impI)+ |
|
584 |
fix m t |
|
585 |
assume "m < n \<and> a - c \<le> t \<and> t \<le> 0" |
|
586 |
with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" |
|
587 |
by auto |
|
588 |
moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" |
|
589 |
by (rule DERIV_add) |
|
590 |
ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" |
|
591 |
by (rule DERIV_chain2) |
|
592 |
then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" |
|
593 |
by simp |
|
594 |
qed |
|
595 |
ultimately obtain x where |
|
596 |
"a - c < x \<and> x < 0 \<and> |
|
597 |
f (a - c + c) = |
|
598 |
(\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" |
|
599 |
by (rule Maclaurin_minus [THEN exE]) |
|
600 |
then have "a < x + c \<and> x + c < c \<and> |
|
601 |
f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" |
|
602 |
by fastforce |
|
603 |
then show ?thesis by fastforce |
|
604 |
qed |
|
605 |
||
606 |
theorem taylor: |
|
607 |
fixes a :: real and n :: nat |
|
608 |
assumes INIT: "n > 0" "diff 0 = f" |
|
609 |
and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
610 |
and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" |
|
611 |
shows "\<exists>t. |
|
612 |
(if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and> |
|
613 |
f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n" |
|
614 |
proof (cases "x < c") |
|
615 |
case True |
|
616 |
note INIT |
|
617 |
moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
618 |
using DERIV and INTERV by fastforce |
|
619 |
moreover note True |
|
620 |
moreover from INTERV have "c \<le> b" |
|
621 |
by simp |
|
622 |
ultimately have "\<exists>t>x. t < c \<and> f x = |
|
623 |
(\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" |
|
624 |
by (rule taylor_down) |
|
625 |
with True show ?thesis by simp |
|
626 |
next |
|
627 |
case False |
|
628 |
note INIT |
|
629 |
moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
630 |
using DERIV and INTERV by fastforce |
|
631 |
moreover from INTERV have "a \<le> c" |
|
632 |
by arith |
|
633 |
moreover from False and INTERV have "c < x" |
|
634 |
by arith |
|
635 |
ultimately have "\<exists>t>c. t < x \<and> f x = |
|
636 |
(\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" |
|
637 |
by (rule taylor_up) |
|
638 |
with False show ?thesis by simp |
|
639 |
qed |
|
640 |
||
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
641 |
end |