author | paulson <lp15@cam.ac.uk> |
Thu, 24 Aug 2023 21:40:24 +0100 | |
changeset 78522 | 918a9ed06898 |
parent 77280 | 8543e6b10a56 |
child 80769 | 77f7aa898ced |
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))" |
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
69529
diff
changeset
|
60 |
using \<open>0 < n - m\<close> by (simp add: field_split_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)" |
69022
e2858770997a
removal of more redundancies, and fixes
paulson <lp15@cam.ac.uk>
parents:
69020
diff
changeset
|
98 |
using difg_Suc real_differentiable_def by auto |
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) |
|
69020
4f94e262976d
elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents:
68671
diff
changeset
|
112 |
show "continuous_on {0..h} (difg 0)" |
4f94e262976d
elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents:
68671
diff
changeset
|
113 |
by (simp add: continuous_at_imp_continuous_on isCont_difg n) |
69022
e2858770997a
removal of more redundancies, and fixes
paulson <lp15@cam.ac.uk>
parents:
69020
diff
changeset
|
114 |
qed (simp add: differentiable_difg n) |
29187 | 115 |
next |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
116 |
case (Suc m') |
63569 | 117 |
then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" |
77280 | 118 |
by force |
29187 | 119 |
have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0" |
120 |
proof (rule Rolle) |
|
121 |
show "0 < t" by fact |
|
122 |
show "difg (Suc m') 0 = difg (Suc m') t" |
|
60758 | 123 |
using t \<open>Suc m' < n\<close> by (simp add: difg_Suc_eq_0 difg_eq_0) |
69020
4f94e262976d
elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents:
68671
diff
changeset
|
124 |
have "\<And>x. 0 \<le> x \<and> x \<le> t \<Longrightarrow> isCont (difg (Suc m')) x" |
60758 | 125 |
using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: isCont_difg) |
69020
4f94e262976d
elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents:
68671
diff
changeset
|
126 |
then show "continuous_on {0..t} (difg (Suc m'))" |
4f94e262976d
elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents:
68671
diff
changeset
|
127 |
by (simp add: continuous_at_imp_continuous_on) |
69022
e2858770997a
removal of more redundancies, and fixes
paulson <lp15@cam.ac.uk>
parents:
69020
diff
changeset
|
128 |
qed (use \<open>t < h\<close> \<open>Suc m' < n\<close> in \<open>simp add: differentiable_difg\<close>) |
63569 | 129 |
with \<open>t < h\<close> show ?case |
130 |
by auto |
|
29187 | 131 |
qed |
77280 | 132 |
then obtain t where "0 < t" "t < h" "difg (Suc m) t = 0" |
133 |
using \<open>m < n\<close> difg_Suc_eq_0 by force |
|
29187 | 134 |
show ?thesis |
135 |
proof (intro exI conjI) |
|
77280 | 136 |
show "0 < t" "t < h" by fact+ |
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
137 |
show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n" |
63569 | 138 |
using \<open>difg (Suc m) t = 0\<close> by (simp add: m f_h difg_def) |
29187 | 139 |
qed |
140 |
qed |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
141 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
142 |
lemma Maclaurin2: |
63569 | 143 |
fixes n :: nat |
144 |
and h :: real |
|
145 |
assumes INIT1: "0 < h" |
|
146 |
and INIT2: "diff 0 = f" |
|
147 |
and DERIV: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
148 |
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" |
|
149 |
proof (cases n) |
|
150 |
case 0 |
|
151 |
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
|
152 |
next |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
153 |
case Suc |
63569 | 154 |
then have "n > 0" by simp |
77280 | 155 |
from Maclaurin [OF INIT1 this INIT2 DERIV] |
156 |
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
|
157 |
qed |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
158 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
159 |
lemma Maclaurin_minus: |
63569 | 160 |
fixes n :: nat and h :: real |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
161 |
assumes "h < 0" "0 < n" "diff 0 = f" |
63569 | 162 |
and DERIV: "\<forall>m t. m < n \<and> h \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
163 |
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
|
164 |
proof - |
63569 | 165 |
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
|
166 |
note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong] |
63569 | 167 |
let ?sum = "\<lambda>t. |
168 |
(\<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
|
169 |
(- 1) ^ n * diff n (- t) / (fact n) * (- h) ^ n" |
63569 | 170 |
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
|
171 |
by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV') |
63569 | 172 |
then obtain t where "0 < t" "t < - h" "f (- (- h)) = ?sum t" |
173 |
by blast |
|
174 |
moreover have "(- 1) ^ n * diff n (- t) * (- h) ^ n / fact n = diff n (- t) * h ^ n / fact n" |
|
175 |
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
|
176 |
moreover |
63569 | 177 |
have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / fact m) = (\<Sum>m<n. diff m 0 * h ^ m / fact m)" |
64267 | 178 |
by (auto intro: sum.cong simp add: power_mult_distrib[symmetric]) |
63569 | 179 |
ultimately have "h < - t \<and> - t < 0 \<and> |
180 |
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
|
181 |
by auto |
63569 | 182 |
then show ?thesis .. |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
183 |
qed |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
184 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
185 |
|
63569 | 186 |
subsection \<open>More Convenient "Bidirectional" Version.\<close> |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
187 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
188 |
lemma Maclaurin_bi_le: |
63569 | 189 |
fixes n :: nat and x :: real |
190 |
assumes "diff 0 = f" |
|
191 |
and DERIV : "\<forall>m t. m < n \<and> \<bar>t\<bar> \<le> \<bar>x\<bar> \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
192 |
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" |
|
193 |
(is "\<exists>t. _ \<and> f x = ?f x t") |
|
194 |
proof (cases "n = 0") |
|
195 |
case True |
|
196 |
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
|
197 |
next |
63569 | 198 |
case False |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
199 |
show ?thesis |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
200 |
proof (cases rule: linorder_cases) |
63569 | 201 |
assume "x = 0" |
202 |
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 | 203 |
by auto |
63569 | 204 |
then show ?thesis .. |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
205 |
next |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
206 |
assume "x < 0" |
63569 | 207 |
with \<open>n \<noteq> 0\<close> DERIV have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t" |
208 |
by (intro Maclaurin_minus) auto |
|
209 |
then obtain t where "x < t" "t < 0" |
|
210 |
"diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n" |
|
211 |
by blast |
|
77280 | 212 |
with \<open>x < 0\<close> \<open>diff 0 = f\<close> show ?thesis by force |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
213 |
next |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
214 |
assume "x > 0" |
63569 | 215 |
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" |
216 |
by (intro Maclaurin) auto |
|
217 |
then obtain t where "0 < t" "t < x" |
|
218 |
"diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n" |
|
219 |
by blast |
|
60758 | 220 |
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 | 221 |
then show ?thesis .. |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
222 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
223 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
224 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
225 |
lemma Maclaurin_all_lt: |
63569 | 226 |
fixes x :: real |
227 |
assumes INIT1: "diff 0 = f" |
|
228 |
and INIT2: "0 < n" |
|
229 |
and INIT3: "x \<noteq> 0" |
|
230 |
and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x" |
|
231 |
shows "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = |
|
232 |
(\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n" |
|
233 |
(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
|
234 |
proof (cases rule: linorder_cases) |
63569 | 235 |
assume "x = 0" |
236 |
with INIT3 show ?thesis .. |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
237 |
next |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
238 |
assume "x < 0" |
63569 | 239 |
with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t" |
240 |
by (intro Maclaurin_minus) auto |
|
77280 | 241 |
then show ?thesis by force |
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
242 |
next |
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
243 |
assume "x > 0" |
63569 | 244 |
with assms have "\<exists>t>0. t < x \<and> f x = ?f x t" |
245 |
by (intro Maclaurin) auto |
|
77280 | 246 |
then 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
|
247 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
248 |
|
63569 | 249 |
lemma Maclaurin_zero: "x = 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) = diff 0 0" |
250 |
for x :: real and n :: nat |
|
68669 | 251 |
by simp |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
252 |
|
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
253 |
|
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
254 |
lemma Maclaurin_all_le: |
63569 | 255 |
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
|
256 |
assumes INIT: "diff 0 = f" |
63569 | 257 |
and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x" |
258 |
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" |
|
259 |
(is "\<exists>t. _ \<and> f x = ?f x t") |
|
260 |
proof (cases "n = 0") |
|
261 |
case True |
|
262 |
with INIT show ?thesis by force |
|
263 |
next |
|
264 |
case False |
|
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset
|
265 |
show ?thesis |
77280 | 266 |
using DERIV INIT Maclaurin_bi_le by auto |
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
267 |
qed |
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset
|
268 |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
269 |
lemma Maclaurin_all_le_objl: |
63569 | 270 |
"diff 0 = f \<and> (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) \<longrightarrow> |
271 |
(\<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)" |
|
272 |
for x :: real and n :: nat |
|
273 |
by (blast intro: Maclaurin_all_le) |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
274 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
275 |
|
63569 | 276 |
subsection \<open>Version for Exponential Function\<close> |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
277 |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
278 |
lemma Maclaurin_exp_lt: |
63569 | 279 |
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
|
280 |
shows |
63569 | 281 |
"x \<noteq> 0 \<Longrightarrow> n > 0 \<Longrightarrow> |
282 |
(\<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 | 283 |
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
|
284 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
285 |
lemma Maclaurin_exp_le: |
63569 | 286 |
fixes x :: real and n :: nat |
287 |
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" |
|
288 |
using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto |
|
289 |
||
69529 | 290 |
corollary exp_lower_Taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x" |
63569 | 291 |
for x :: real |
292 |
using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square) |
|
293 |
||
65273
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64267
diff
changeset
|
294 |
corollary ln_2_less_1: "ln 2 < (1::real)" |
77280 | 295 |
by (smt (verit) ln_eq_minus_one ln_le_minus_one) |
63569 | 296 |
|
297 |
subsection \<open>Version for Sine Function\<close> |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
298 |
|
67091 | 299 |
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 | 300 |
for m :: nat |
301 |
by auto |
|
302 |
||
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
303 |
|
63569 | 304 |
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
|
305 |
|
63569 | 306 |
lemma sin_expansion_lemma: "sin (x + real (Suc m) * pi / 2) = cos (x + real m * pi / 2)" |
307 |
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
|
308 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
309 |
lemma Maclaurin_sin_expansion2: |
63569 | 310 |
"\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> |
311 |
sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n" |
|
68669 | 312 |
proof (cases "n = 0 \<or> x = 0") |
313 |
case False |
|
314 |
let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)" |
|
315 |
have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> sin x = |
|
316 |
(\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n" |
|
317 |
proof (rule Maclaurin_all_lt) |
|
318 |
show "\<forall>m x. ((\<lambda>t. sin (t + 1/2 * real m * pi)) has_real_derivative |
|
319 |
sin (x + 1/2 * real (Suc m) * pi)) (at x)" |
|
320 |
by (rule allI derivative_eq_intros | use sin_expansion_lemma in force)+ |
|
321 |
qed (use False in auto) |
|
322 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
323 |
apply (rule ex_forward, simp) |
68669 | 324 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
325 |
apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc) |
68669 | 326 |
done |
327 |
qed auto |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
328 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
329 |
lemma Maclaurin_sin_expansion: |
63569 | 330 |
"\<exists>t. sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n" |
331 |
using Maclaurin_sin_expansion2 [of x n] by blast |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
332 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
333 |
lemma Maclaurin_sin_expansion3: |
68669 | 334 |
assumes "n > 0" "x > 0" |
335 |
shows "\<exists>t. 0 < t \<and> t < x \<and> |
|
336 |
sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n" |
|
337 |
proof - |
|
338 |
let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)" |
|
339 |
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" |
|
340 |
proof (rule Maclaurin) |
|
341 |
show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> |
|
342 |
((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative |
|
343 |
sin (t + 1/2 * real (Suc m) * pi)) (at t)" |
|
344 |
apply (simp add: sin_expansion_lemma del: of_nat_Suc) |
|
345 |
apply (force intro!: derivative_eq_intros) |
|
346 |
done |
|
347 |
qed (use assms in auto) |
|
348 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
349 |
apply (rule ex_forward, simp) |
68669 | 350 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
351 |
apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc) |
68669 | 352 |
done |
353 |
qed |
|
63569 | 354 |
|
355 |
lemma Maclaurin_sin_expansion4: |
|
68669 | 356 |
assumes "0 < x" |
357 |
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" |
|
358 |
proof - |
|
359 |
let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)" |
|
360 |
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" |
|
361 |
proof (rule Maclaurin2) |
|
362 |
show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> |
|
363 |
((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative |
|
364 |
sin (t + 1/2 * real (Suc m) * pi)) (at t)" |
|
365 |
apply (simp add: sin_expansion_lemma del: of_nat_Suc) |
|
366 |
apply (force intro!: derivative_eq_intros) |
|
367 |
done |
|
368 |
qed (use assms in auto) |
|
369 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
370 |
apply (rule ex_forward, simp) |
68669 | 371 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
372 |
apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc) |
68669 | 373 |
done |
374 |
qed |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
375 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
376 |
|
63569 | 377 |
subsection \<open>Maclaurin Expansion for Cosine Function\<close> |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
378 |
|
63569 | 379 |
lemma sumr_cos_zero_one [simp]: "(\<Sum>m<Suc n. cos_coeff m * 0 ^ m) = 1" |
380 |
by (induct n) auto |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
381 |
|
63569 | 382 |
lemma cos_expansion_lemma: "cos (x + real (Suc m) * pi / 2) = - sin (x + real m * pi / 2)" |
383 |
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
|
384 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
385 |
lemma Maclaurin_cos_expansion: |
63569 | 386 |
"\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> |
387 |
cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos(t + 1/2 * real n * pi) / fact n) * x ^ n" |
|
68669 | 388 |
proof (cases "n = 0 \<or> x = 0") |
389 |
case False |
|
390 |
let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)" |
|
391 |
have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> cos x = |
|
392 |
(\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n" |
|
393 |
proof (rule Maclaurin_all_lt) |
|
394 |
show "\<forall>m x. ((\<lambda>t. cos (t + 1/2 * real m * pi)) has_real_derivative |
|
395 |
cos (x + 1/2 * real (Suc m) * pi)) (at x)" |
|
77280 | 396 |
using cos_expansion_lemma |
397 |
by (intro allI derivative_eq_intros | simp)+ |
|
68669 | 398 |
qed (use False in auto) |
399 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
400 |
apply (rule ex_forward, simp) |
68669 | 401 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
402 |
apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE simp del: of_nat_Suc) |
68669 | 403 |
done |
404 |
qed auto |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
405 |
|
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
406 |
lemma Maclaurin_cos_expansion2: |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
407 |
assumes "x > 0" "n > 0" |
68669 | 408 |
shows "\<exists>t. 0 < t \<and> t < x \<and> |
63569 | 409 |
cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos (t + 1/2 * real n * pi) / fact n) * x ^ n" |
68669 | 410 |
proof - |
411 |
let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)" |
|
412 |
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" |
|
413 |
proof (rule Maclaurin) |
|
414 |
show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> |
|
415 |
((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative |
|
416 |
cos (t + 1 / 2 * real (Suc m) * pi)) (at t)" |
|
417 |
by (simp add: cos_expansion_lemma del: of_nat_Suc) |
|
418 |
qed (use assms in auto) |
|
419 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
420 |
apply (rule ex_forward, simp) |
68669 | 421 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
422 |
apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE) |
68669 | 423 |
done |
424 |
qed |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
425 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
426 |
lemma Maclaurin_minus_cos_expansion: |
68669 | 427 |
assumes "n > 0" "x < 0" |
428 |
shows "\<exists>t. x < t \<and> t < 0 \<and> |
|
429 |
cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + ((cos (t + 1/2 * real n * pi) / fact n) * x ^ n)" |
|
430 |
proof - |
|
431 |
let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)" |
|
432 |
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" |
|
433 |
proof (rule Maclaurin_minus) |
|
434 |
show "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> |
|
435 |
((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative |
|
436 |
cos (t + 1 / 2 * real (Suc m) * pi)) (at t)" |
|
437 |
by (simp add: cos_expansion_lemma del: of_nat_Suc) |
|
438 |
qed (use assms in auto) |
|
439 |
then show ?thesis |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
440 |
apply (rule ex_forward, simp) |
68669 | 441 |
apply (rule sum.cong[OF refl]) |
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
442 |
apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE) |
68669 | 443 |
done |
444 |
qed |
|
63569 | 445 |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
446 |
|
63569 | 447 |
(* Version for ln(1 +/- x). Where is it?? *) |
448 |
||
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
449 |
|
63569 | 450 |
lemma sin_bound_lemma: "x = y \<Longrightarrow> \<bar>u\<bar> \<le> v \<Longrightarrow> \<bar>(x + u) - y\<bar> \<le> v" |
451 |
for x y u v :: real |
|
452 |
by auto |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
453 |
|
63569 | 454 |
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 | 455 |
proof - |
63569 | 456 |
have est: "x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" for x y :: real |
457 |
by (rule mult_right_mono) simp_all |
|
68157 | 458 |
let ?diff = "\<lambda>(n::nat) (x::real). |
63569 | 459 |
if n mod 4 = 0 then sin x |
460 |
else if n mod 4 = 1 then cos x |
|
461 |
else if n mod 4 = 2 then - sin x |
|
462 |
else - cos x" |
|
22985 | 463 |
have diff_0: "?diff 0 = sin" by simp |
68157 | 464 |
have "DERIV (?diff m) x :> ?diff (Suc m) x" for m and x |
465 |
using mod_exhaust_less_4 [of m] |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
466 |
by (auto simp: mod_Suc intro!: derivative_eq_intros) |
68157 | 467 |
then have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x" |
468 |
by blast |
|
22985 | 469 |
from Maclaurin_all_le [OF diff_0 DERIV_diff] |
63569 | 470 |
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" |
471 |
and t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / (fact n) * x ^ n" |
|
472 |
by fast |
|
68157 | 473 |
have diff_m_0: "?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))" for m |
474 |
using mod_exhaust_less_4 [of m] |
|
68671
205749fba102
fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents:
68669
diff
changeset
|
475 |
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 | 476 |
show ?thesis |
22985 | 477 |
apply (subst t2) |
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
478 |
apply (rule sin_bound_lemma) |
64267 | 479 |
apply (rule sum.cong[OF refl]) |
77280 | 480 |
unfolding sin_coeff_def |
63569 | 481 |
apply (subst diff_m_0, simp) |
482 |
using est |
|
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
483 |
apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono |
63569 | 484 |
simp: ac_simps divide_inverse power_abs [symmetric] abs_mult) |
14738 | 485 |
done |
486 |
qed |
|
487 |
||
63570 | 488 |
|
489 |
section \<open>Taylor series\<close> |
|
490 |
||
491 |
text \<open> |
|
492 |
We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close> |
|
493 |
to prove Taylor's theorem. |
|
494 |
\<close> |
|
495 |
||
69529 | 496 |
lemma Taylor_up: |
63570 | 497 |
assumes INIT: "n > 0" "diff 0 = f" |
498 |
and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)" |
|
499 |
and INTERV: "a \<le> c" "c < b" |
|
500 |
shows "\<exists>t::real. c < t \<and> t < b \<and> |
|
501 |
f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n" |
|
502 |
proof - |
|
503 |
from INTERV have "0 < b - c" by arith |
|
504 |
moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" |
|
505 |
by auto |
|
506 |
moreover |
|
507 |
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)" |
|
508 |
proof (intro strip) |
|
509 |
fix m t |
|
510 |
assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c" |
|
511 |
with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" |
|
512 |
by auto |
|
513 |
moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" |
|
514 |
by (rule DERIV_add) |
|
515 |
ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)" |
|
516 |
by (rule DERIV_chain2) |
|
517 |
then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" |
|
518 |
by simp |
|
519 |
qed |
|
520 |
ultimately obtain x where |
|
521 |
"0 < x \<and> x < b - c \<and> |
|
522 |
f (b - c + c) = |
|
523 |
(\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n" |
|
524 |
by (rule Maclaurin [THEN exE]) |
|
77280 | 525 |
then show ?thesis |
526 |
by (smt (verit) sum.cong) |
|
63570 | 527 |
qed |
528 |
||
69529 | 529 |
lemma Taylor_down: |
63570 | 530 |
fixes a :: real and n :: nat |
531 |
assumes INIT: "n > 0" "diff 0 = f" |
|
532 |
and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)" |
|
533 |
and INTERV: "a < c" "c \<le> b" |
|
534 |
shows "\<exists>t. a < t \<and> t < c \<and> |
|
535 |
f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n" |
|
536 |
proof - |
|
537 |
from INTERV have "a-c < 0" by arith |
|
538 |
moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))" |
|
539 |
by auto |
|
540 |
moreover |
|
541 |
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)" |
|
542 |
proof (rule allI impI)+ |
|
543 |
fix m t |
|
544 |
assume "m < n \<and> a - c \<le> t \<and> t \<le> 0" |
|
545 |
with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" |
|
546 |
by auto |
|
547 |
moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0" |
|
548 |
by (rule DERIV_add) |
|
77280 | 549 |
ultimately show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)" |
550 |
using DERIV_chain2 DERIV_shift by blast |
|
63570 | 551 |
qed |
552 |
ultimately obtain x where |
|
553 |
"a - c < x \<and> x < 0 \<and> |
|
554 |
f (a - c + c) = |
|
555 |
(\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" |
|
556 |
by (rule Maclaurin_minus [THEN exE]) |
|
557 |
then have "a < x + c \<and> x + c < c \<and> |
|
558 |
f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n" |
|
559 |
by fastforce |
|
560 |
then show ?thesis by fastforce |
|
561 |
qed |
|
562 |
||
69529 | 563 |
theorem Taylor: |
63570 | 564 |
fixes a :: real and n :: nat |
565 |
assumes INIT: "n > 0" "diff 0 = f" |
|
566 |
and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
567 |
and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" |
|
568 |
shows "\<exists>t. |
|
569 |
(if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and> |
|
570 |
f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n" |
|
571 |
proof (cases "x < c") |
|
572 |
case True |
|
573 |
note INIT |
|
574 |
moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
575 |
using DERIV and INTERV by fastforce |
|
77280 | 576 |
ultimately show ?thesis |
577 |
using True INTERV Taylor_down by simp |
|
63570 | 578 |
next |
579 |
case False |
|
580 |
note INIT |
|
581 |
moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" |
|
582 |
using DERIV and INTERV by fastforce |
|
77280 | 583 |
ultimately show ?thesis |
584 |
using Taylor_up INTERV False by simp |
|
63570 | 585 |
qed |
586 |
||
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset
|
587 |
end |