author | haftmann |
Wed, 29 Apr 2009 14:20:26 +0200 | |
changeset 31021 | 53642251a04f |
parent 30729 | 461ee3e49ad3 |
child 32960 | 69916a850301 |
permissions | -rw-r--r-- |
21776 | 1 |
(* Title : FrechetDeriv.thy |
2 |
Author : Brian Huffman |
|
3 |
*) |
|
4 |
||
5 |
header {* Frechet Derivative *} |
|
6 |
||
7 |
theory FrechetDeriv |
|
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
30273
diff
changeset
|
8 |
imports Lim Complex_Main |
21776 | 9 |
begin |
10 |
||
11 |
definition |
|
12 |
fderiv :: |
|
13 |
"['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool" |
|
14 |
-- {* Frechet derivative: D is derivative of function f at x *} |
|
15 |
("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where |
|
16 |
"FDERIV f x :> D = (bounded_linear D \<and> |
|
17 |
(\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)" |
|
18 |
||
19 |
lemma FDERIV_I: |
|
20 |
"\<lbrakk>bounded_linear D; (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\<rbrakk> |
|
21 |
\<Longrightarrow> FDERIV f x :> D" |
|
22 |
by (simp add: fderiv_def) |
|
23 |
||
24 |
lemma FDERIV_D: |
|
25 |
"FDERIV f x :> D \<Longrightarrow> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0" |
|
26 |
by (simp add: fderiv_def) |
|
27 |
||
28 |
lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D" |
|
29 |
by (simp add: fderiv_def) |
|
30 |
||
31 |
lemma bounded_linear_zero: |
|
32 |
"bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)" |
|
28823 | 33 |
proof |
21776 | 34 |
show "(0::'b) = 0 + 0" by simp |
35 |
fix r show "(0::'b) = scaleR r 0" by simp |
|
36 |
have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp |
|
37 |
thus "\<exists>K. \<forall>x::'a. norm (0::'b) \<le> norm x * K" .. |
|
38 |
qed |
|
39 |
||
40 |
lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)" |
|
41 |
by (simp add: fderiv_def bounded_linear_zero) |
|
42 |
||
43 |
lemma bounded_linear_ident: |
|
44 |
"bounded_linear (\<lambda>x::'a::real_normed_vector. x)" |
|
28823 | 45 |
proof |
21776 | 46 |
fix x y :: 'a show "x + y = x + y" by simp |
47 |
fix r and x :: 'a show "scaleR r x = scaleR r x" by simp |
|
48 |
have "\<forall>x::'a. norm x \<le> norm x * 1" by simp |
|
49 |
thus "\<exists>K. \<forall>x::'a. norm x \<le> norm x * K" .. |
|
50 |
qed |
|
51 |
||
52 |
lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)" |
|
53 |
by (simp add: fderiv_def bounded_linear_ident) |
|
54 |
||
55 |
subsection {* Addition *} |
|
56 |
||
57 |
lemma add_diff_add: |
|
58 |
fixes a b c d :: "'a::ab_group_add" |
|
59 |
shows "(a + c) - (b + d) = (a - b) + (c - d)" |
|
60 |
by simp |
|
61 |
||
62 |
lemma bounded_linear_add: |
|
27611 | 63 |
assumes "bounded_linear f" |
64 |
assumes "bounded_linear g" |
|
21776 | 65 |
shows "bounded_linear (\<lambda>x. f x + g x)" |
27611 | 66 |
proof - |
29233 | 67 |
interpret f: bounded_linear f by fact |
68 |
interpret g: bounded_linear g by fact |
|
27611 | 69 |
show ?thesis apply (unfold_locales) |
70 |
apply (simp only: f.add g.add add_ac) |
|
71 |
apply (simp only: f.scaleR g.scaleR scaleR_right_distrib) |
|
72 |
apply (rule f.pos_bounded [THEN exE], rename_tac Kf) |
|
73 |
apply (rule g.pos_bounded [THEN exE], rename_tac Kg) |
|
74 |
apply (rule_tac x="Kf + Kg" in exI, safe) |
|
75 |
apply (subst right_distrib) |
|
76 |
apply (rule order_trans [OF norm_triangle_ineq]) |
|
77 |
apply (rule add_mono, erule spec, erule spec) |
|
78 |
done |
|
79 |
qed |
|
21776 | 80 |
|
81 |
lemma norm_ratio_ineq: |
|
82 |
fixes x y :: "'a::real_normed_vector" |
|
83 |
fixes h :: "'b::real_normed_vector" |
|
84 |
shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h" |
|
85 |
apply (rule ord_le_eq_trans) |
|
86 |
apply (rule divide_right_mono) |
|
87 |
apply (rule norm_triangle_ineq) |
|
88 |
apply (rule norm_ge_zero) |
|
89 |
apply (rule add_divide_distrib) |
|
90 |
done |
|
91 |
||
92 |
lemma FDERIV_add: |
|
93 |
assumes f: "FDERIV f x :> F" |
|
94 |
assumes g: "FDERIV g x :> G" |
|
95 |
shows "FDERIV (\<lambda>x. f x + g x) x :> (\<lambda>h. F h + G h)" |
|
96 |
proof (rule FDERIV_I) |
|
97 |
show "bounded_linear (\<lambda>h. F h + G h)" |
|
98 |
apply (rule bounded_linear_add) |
|
99 |
apply (rule FDERIV_bounded_linear [OF f]) |
|
100 |
apply (rule FDERIV_bounded_linear [OF g]) |
|
101 |
done |
|
102 |
next |
|
103 |
have f': "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0" |
|
104 |
using f by (rule FDERIV_D) |
|
105 |
have g': "(\<lambda>h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0" |
|
106 |
using g by (rule FDERIV_D) |
|
107 |
from f' g' |
|
108 |
have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h |
|
109 |
+ norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0" |
|
110 |
by (rule LIM_add_zero) |
|
111 |
thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h)) |
|
112 |
/ norm h) -- 0 --> 0" |
|
113 |
apply (rule real_LIM_sandwich_zero) |
|
114 |
apply (simp add: divide_nonneg_pos) |
|
115 |
apply (simp only: add_diff_add) |
|
116 |
apply (rule norm_ratio_ineq) |
|
117 |
done |
|
118 |
qed |
|
119 |
||
120 |
subsection {* Subtraction *} |
|
121 |
||
122 |
lemma bounded_linear_minus: |
|
27611 | 123 |
assumes "bounded_linear f" |
21776 | 124 |
shows "bounded_linear (\<lambda>x. - f x)" |
27611 | 125 |
proof - |
29233 | 126 |
interpret f: bounded_linear f by fact |
27611 | 127 |
show ?thesis apply (unfold_locales) |
128 |
apply (simp add: f.add) |
|
129 |
apply (simp add: f.scaleR) |
|
130 |
apply (simp add: f.bounded) |
|
131 |
done |
|
132 |
qed |
|
21776 | 133 |
|
134 |
lemma FDERIV_minus: |
|
135 |
"FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)" |
|
136 |
apply (rule FDERIV_I) |
|
137 |
apply (rule bounded_linear_minus) |
|
138 |
apply (erule FDERIV_bounded_linear) |
|
139 |
apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel) |
|
140 |
done |
|
141 |
||
142 |
lemma FDERIV_diff: |
|
143 |
"\<lbrakk>FDERIV f x :> F; FDERIV g x :> G\<rbrakk> |
|
144 |
\<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)" |
|
145 |
by (simp only: diff_minus FDERIV_add FDERIV_minus) |
|
146 |
||
147 |
subsection {* Continuity *} |
|
148 |
||
149 |
lemma FDERIV_isCont: |
|
150 |
assumes f: "FDERIV f x :> F" |
|
151 |
shows "isCont f x" |
|
152 |
proof - |
|
29233 | 153 |
from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear) |
21776 | 154 |
have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0" |
155 |
by (rule FDERIV_D [OF f]) |
|
156 |
hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0" |
|
28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
157 |
by (intro LIM_mult_zero LIM_norm_zero LIM_ident) |
21776 | 158 |
hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0" |
159 |
by (simp cong: LIM_cong) |
|
160 |
hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0" |
|
161 |
by (rule LIM_norm_zero_cancel) |
|
162 |
hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0" |
|
28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
163 |
by (intro LIM_add_zero F.LIM_zero LIM_ident) |
21776 | 164 |
hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0" |
165 |
by simp |
|
166 |
thus "isCont f x" |
|
167 |
unfolding isCont_iff by (rule LIM_zero_cancel) |
|
168 |
qed |
|
169 |
||
170 |
subsection {* Composition *} |
|
171 |
||
172 |
lemma real_divide_cancel_lemma: |
|
173 |
fixes a b c :: real |
|
174 |
shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c" |
|
175 |
by simp |
|
176 |
||
177 |
lemma bounded_linear_compose: |
|
27611 | 178 |
assumes "bounded_linear f" |
179 |
assumes "bounded_linear g" |
|
21776 | 180 |
shows "bounded_linear (\<lambda>x. f (g x))" |
27611 | 181 |
proof - |
29233 | 182 |
interpret f: bounded_linear f by fact |
183 |
interpret g: bounded_linear g by fact |
|
27611 | 184 |
show ?thesis proof (unfold_locales) |
185 |
fix x y show "f (g (x + y)) = f (g x) + f (g y)" |
|
186 |
by (simp only: f.add g.add) |
|
187 |
next |
|
188 |
fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))" |
|
189 |
by (simp only: f.scaleR g.scaleR) |
|
190 |
next |
|
191 |
from f.pos_bounded |
|
192 |
obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast |
|
193 |
from g.pos_bounded |
|
194 |
obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast |
|
195 |
show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K" |
|
196 |
proof (intro exI allI) |
|
197 |
fix x |
|
198 |
have "norm (f (g x)) \<le> norm (g x) * Kf" |
|
199 |
using f . |
|
200 |
also have "\<dots> \<le> (norm x * Kg) * Kf" |
|
201 |
using g Kf [THEN order_less_imp_le] by (rule mult_right_mono) |
|
202 |
also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)" |
|
203 |
by (rule mult_assoc) |
|
204 |
finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" . |
|
205 |
qed |
|
21776 | 206 |
qed |
207 |
qed |
|
208 |
||
209 |
lemma FDERIV_compose: |
|
210 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
|
211 |
fixes g :: "'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector" |
|
212 |
assumes f: "FDERIV f x :> F" |
|
213 |
assumes g: "FDERIV g (f x) :> G" |
|
214 |
shows "FDERIV (\<lambda>x. g (f x)) x :> (\<lambda>h. G (F h))" |
|
215 |
proof (rule FDERIV_I) |
|
216 |
from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f] |
|
217 |
show "bounded_linear (\<lambda>h. G (F h))" |
|
218 |
by (rule bounded_linear_compose) |
|
219 |
next |
|
220 |
let ?Rf = "\<lambda>h. f (x + h) - f x - F h" |
|
221 |
let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k" |
|
222 |
let ?k = "\<lambda>h. f (x + h) - f x" |
|
223 |
let ?Nf = "\<lambda>h. norm (?Rf h) / norm h" |
|
224 |
let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)" |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
225 |
from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear) |
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
226 |
from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear) |
21776 | 227 |
from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast |
228 |
from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast |
|
229 |
||
230 |
let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)" |
|
231 |
||
232 |
show "(\<lambda>h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0" |
|
233 |
proof (rule real_LIM_sandwich_zero) |
|
234 |
have Nf: "?Nf -- 0 --> 0" |
|
235 |
using FDERIV_D [OF f] . |
|
236 |
||
237 |
have Ng1: "isCont (\<lambda>k. norm (?Rg k) / norm k) 0" |
|
238 |
by (simp add: isCont_def FDERIV_D [OF g]) |
|
239 |
have Ng2: "?k -- 0 --> 0" |
|
240 |
apply (rule LIM_zero) |
|
241 |
apply (fold isCont_iff) |
|
242 |
apply (rule FDERIV_isCont [OF f]) |
|
243 |
done |
|
244 |
have Ng: "?Ng -- 0 --> 0" |
|
245 |
using isCont_LIM_compose [OF Ng1 Ng2] by simp |
|
246 |
||
247 |
have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) |
|
248 |
-- 0 --> 0 * kG + 0 * (0 + kF)" |
|
249 |
by (intro LIM_add LIM_mult LIM_const Nf Ng) |
|
250 |
thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0" |
|
251 |
by simp |
|
252 |
next |
|
253 |
fix h::'a assume h: "h \<noteq> 0" |
|
254 |
thus "0 \<le> norm (g (f (x + h)) - g (f x) - G (F h)) / norm h" |
|
255 |
by (simp add: divide_nonneg_pos) |
|
256 |
next |
|
257 |
fix h::'a assume h: "h \<noteq> 0" |
|
258 |
have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)" |
|
259 |
by (simp add: G.diff) |
|
260 |
hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h |
|
261 |
= norm (G (?Rf h) + ?Rg (?k h)) / norm h" |
|
262 |
by (rule arg_cong) |
|
263 |
also have "\<dots> \<le> norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h" |
|
264 |
by (rule norm_ratio_ineq) |
|
265 |
also have "\<dots> \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" |
|
266 |
proof (rule add_mono) |
|
267 |
show "norm (G (?Rf h)) / norm h \<le> ?Nf h * kG" |
|
268 |
apply (rule ord_le_eq_trans) |
|
269 |
apply (rule divide_right_mono [OF kG norm_ge_zero]) |
|
270 |
apply simp |
|
271 |
done |
|
272 |
next |
|
273 |
have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)" |
|
274 |
apply (rule real_divide_cancel_lemma [symmetric]) |
|
275 |
apply (simp add: G.zero) |
|
276 |
done |
|
277 |
also have "\<dots> \<le> ?Ng h * (?Nf h + kF)" |
|
278 |
proof (rule mult_left_mono) |
|
279 |
have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h" |
|
280 |
by simp |
|
281 |
also have "\<dots> \<le> ?Nf h + norm (F h) / norm h" |
|
282 |
by (rule norm_ratio_ineq) |
|
283 |
also have "\<dots> \<le> ?Nf h + kF" |
|
284 |
apply (rule add_left_mono) |
|
285 |
apply (subst pos_divide_le_eq, simp add: h) |
|
286 |
apply (subst mult_commute) |
|
287 |
apply (rule kF) |
|
288 |
done |
|
289 |
finally show "norm (?k h) / norm h \<le> ?Nf h + kF" . |
|
290 |
next |
|
291 |
show "0 \<le> ?Ng h" |
|
292 |
apply (case_tac "f (x + h) - f x = 0", simp) |
|
293 |
apply (rule divide_nonneg_pos [OF norm_ge_zero]) |
|
294 |
apply simp |
|
295 |
done |
|
296 |
qed |
|
297 |
finally show "norm (?Rg (?k h)) / norm h \<le> ?Ng h * (?Nf h + kF)" . |
|
298 |
qed |
|
299 |
finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h |
|
300 |
\<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" . |
|
301 |
qed |
|
302 |
qed |
|
303 |
||
304 |
subsection {* Product Rule *} |
|
305 |
||
306 |
lemma (in bounded_bilinear) FDERIV_lemma: |
|
307 |
"a' ** b' - a ** b - (a ** B + A ** b) |
|
308 |
= a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)" |
|
309 |
by (simp add: diff_left diff_right) |
|
310 |
||
311 |
lemma (in bounded_bilinear) FDERIV: |
|
312 |
fixes x :: "'d::real_normed_vector" |
|
313 |
assumes f: "FDERIV f x :> F" |
|
314 |
assumes g: "FDERIV g x :> G" |
|
315 |
shows "FDERIV (\<lambda>x. f x ** g x) x :> (\<lambda>h. f x ** G h + F h ** g x)" |
|
316 |
proof (rule FDERIV_I) |
|
317 |
show "bounded_linear (\<lambda>h. f x ** G h + F h ** g x)" |
|
318 |
apply (rule bounded_linear_add) |
|
319 |
apply (rule bounded_linear_compose [OF bounded_linear_right]) |
|
320 |
apply (rule FDERIV_bounded_linear [OF g]) |
|
321 |
apply (rule bounded_linear_compose [OF bounded_linear_left]) |
|
322 |
apply (rule FDERIV_bounded_linear [OF f]) |
|
323 |
done |
|
324 |
next |
|
325 |
from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]] |
|
326 |
obtain KF where norm_F: "\<And>x. norm (F x) \<le> norm x * KF" by fast |
|
327 |
||
328 |
from pos_bounded obtain K where K: "0 < K" and norm_prod: |
|
329 |
"\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast |
|
330 |
||
331 |
let ?Rf = "\<lambda>h. f (x + h) - f x - F h" |
|
332 |
let ?Rg = "\<lambda>h. g (x + h) - g x - G h" |
|
333 |
||
334 |
let ?fun1 = "\<lambda>h. |
|
335 |
norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) / |
|
336 |
norm h" |
|
337 |
||
338 |
let ?fun2 = "\<lambda>h. |
|
339 |
norm (f x) * (norm (?Rg h) / norm h) * K + |
|
340 |
norm (?Rf h) / norm h * norm (g (x + h)) * K + |
|
341 |
KF * norm (g (x + h) - g x) * K" |
|
342 |
||
343 |
have "?fun1 -- 0 --> 0" |
|
344 |
proof (rule real_LIM_sandwich_zero) |
|
345 |
from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]] |
|
346 |
have "?fun2 -- 0 --> |
|
347 |
norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K" |
|
348 |
by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D) |
|
349 |
thus "?fun2 -- 0 --> 0" |
|
350 |
by simp |
|
351 |
next |
|
352 |
fix h::'d assume "h \<noteq> 0" |
|
353 |
thus "0 \<le> ?fun1 h" |
|
354 |
by (simp add: divide_nonneg_pos) |
|
355 |
next |
|
356 |
fix h::'d assume "h \<noteq> 0" |
|
357 |
have "?fun1 h \<le> (norm (f x) * norm (?Rg h) * K + |
|
358 |
norm (?Rf h) * norm (g (x + h)) * K + |
|
359 |
norm h * KF * norm (g (x + h) - g x) * K) / norm h" |
|
360 |
by (intro |
|
361 |
divide_right_mono mult_mono' |
|
362 |
order_trans [OF norm_triangle_ineq add_mono] |
|
363 |
order_trans [OF norm_prod mult_right_mono] |
|
364 |
mult_nonneg_nonneg order_refl norm_ge_zero norm_F |
|
365 |
K [THEN order_less_imp_le] |
|
366 |
) |
|
367 |
also have "\<dots> = ?fun2 h" |
|
368 |
by (simp add: add_divide_distrib) |
|
369 |
finally show "?fun1 h \<le> ?fun2 h" . |
|
370 |
qed |
|
371 |
thus "(\<lambda>h. |
|
372 |
norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x)) |
|
373 |
/ norm h) -- 0 --> 0" |
|
374 |
by (simp only: FDERIV_lemma) |
|
375 |
qed |
|
376 |
||
29233 | 377 |
lemmas FDERIV_mult = mult.FDERIV |
21776 | 378 |
|
29233 | 379 |
lemmas FDERIV_scaleR = scaleR.FDERIV |
28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
380 |
|
21776 | 381 |
|
382 |
subsection {* Powers *} |
|
383 |
||
384 |
lemma FDERIV_power_Suc: |
|
31021 | 385 |
fixes x :: "'a::{real_normed_algebra,comm_ring_1}" |
28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
386 |
shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)" |
21776 | 387 |
apply (induct n) |
388 |
apply (simp add: power_Suc FDERIV_ident) |
|
389 |
apply (drule FDERIV_mult [OF FDERIV_ident]) |
|
28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
390 |
apply (simp only: of_nat_Suc left_distrib mult_1_left) |
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
391 |
apply (simp only: power_Suc right_distrib add_ac mult_ac) |
21776 | 392 |
done |
393 |
||
394 |
lemma FDERIV_power: |
|
31021 | 395 |
fixes x :: "'a::{real_normed_algebra,comm_ring_1}" |
21776 | 396 |
shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)" |
28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
397 |
apply (cases n) |
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
398 |
apply (simp add: FDERIV_const) |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
29986
diff
changeset
|
399 |
apply (simp add: FDERIV_power_Suc del: power_Suc) |
28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
400 |
done |
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
401 |
|
21776 | 402 |
|
403 |
subsection {* Inverse *} |
|
404 |
||
405 |
lemma inverse_diff_inverse: |
|
406 |
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk> |
|
407 |
\<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)" |
|
408 |
by (simp add: right_diff_distrib left_diff_distrib mult_assoc) |
|
409 |
||
410 |
lemmas bounded_linear_mult_const = |
|
29233 | 411 |
mult.bounded_linear_left [THEN bounded_linear_compose] |
21776 | 412 |
|
413 |
lemmas bounded_linear_const_mult = |
|
29233 | 414 |
mult.bounded_linear_right [THEN bounded_linear_compose] |
21776 | 415 |
|
416 |
lemma FDERIV_inverse: |
|
417 |
fixes x :: "'a::real_normed_div_algebra" |
|
418 |
assumes x: "x \<noteq> 0" |
|
419 |
shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))" |
|
420 |
(is "FDERIV ?inv _ :> _") |
|
421 |
proof (rule FDERIV_I) |
|
422 |
show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))" |
|
423 |
apply (rule bounded_linear_minus) |
|
424 |
apply (rule bounded_linear_mult_const) |
|
425 |
apply (rule bounded_linear_const_mult) |
|
426 |
apply (rule bounded_linear_ident) |
|
427 |
done |
|
428 |
next |
|
429 |
show "(\<lambda>h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h) |
|
430 |
-- 0 --> 0" |
|
431 |
proof (rule LIM_equal2) |
|
432 |
show "0 < norm x" using x by simp |
|
433 |
next |
|
434 |
fix h::'a |
|
435 |
assume 1: "h \<noteq> 0" |
|
436 |
assume "norm (h - 0) < norm x" |
|
437 |
hence "h \<noteq> -x" by clarsimp |
|
438 |
hence 2: "x + h \<noteq> 0" |
|
439 |
apply (rule contrapos_nn) |
|
440 |
apply (rule sym) |
|
441 |
apply (erule equals_zero_I) |
|
442 |
done |
|
443 |
show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h |
|
444 |
= norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h" |
|
445 |
apply (subst inverse_diff_inverse [OF 2 x]) |
|
446 |
apply (subst minus_diff_minus) |
|
447 |
apply (subst norm_minus_cancel) |
|
448 |
apply (simp add: left_diff_distrib) |
|
449 |
done |
|
450 |
next |
|
451 |
show "(\<lambda>h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h) |
|
452 |
-- 0 --> 0" |
|
453 |
proof (rule real_LIM_sandwich_zero) |
|
454 |
show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x)) |
|
455 |
-- 0 --> 0" |
|
456 |
apply (rule LIM_mult_left_zero) |
|
457 |
apply (rule LIM_norm_zero) |
|
458 |
apply (rule LIM_zero) |
|
459 |
apply (rule LIM_offset_zero) |
|
460 |
apply (rule LIM_inverse) |
|
28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28823
diff
changeset
|
461 |
apply (rule LIM_ident) |
21776 | 462 |
apply (rule x) |
463 |
done |
|
464 |
next |
|
465 |
fix h::'a assume h: "h \<noteq> 0" |
|
466 |
show "0 \<le> norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h" |
|
467 |
apply (rule divide_nonneg_pos) |
|
468 |
apply (rule norm_ge_zero) |
|
469 |
apply (simp add: h) |
|
470 |
done |
|
471 |
next |
|
472 |
fix h::'a assume h: "h \<noteq> 0" |
|
473 |
have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h |
|
474 |
\<le> norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h" |
|
475 |
apply (rule divide_right_mono [OF _ norm_ge_zero]) |
|
476 |
apply (rule order_trans [OF norm_mult_ineq]) |
|
477 |
apply (rule mult_right_mono [OF _ norm_ge_zero]) |
|
478 |
apply (rule norm_mult_ineq) |
|
479 |
done |
|
480 |
also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)" |
|
481 |
by simp |
|
482 |
finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h |
|
483 |
\<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" . |
|
484 |
qed |
|
485 |
qed |
|
486 |
qed |
|
487 |
||
488 |
subsection {* Alternate definition *} |
|
489 |
||
490 |
lemma field_fderiv_def: |
|
491 |
fixes x :: "'a::real_normed_field" shows |
|
492 |
"FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D" |
|
493 |
apply (unfold fderiv_def) |
|
29233 | 494 |
apply (simp add: mult.bounded_linear_left) |
21776 | 495 |
apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) |
496 |
apply (subst diff_divide_distrib) |
|
497 |
apply (subst times_divide_eq_left [symmetric]) |
|
23398 | 498 |
apply (simp cong: LIM_cong) |
21776 | 499 |
apply (simp add: LIM_norm_zero_iff LIM_zero_iff) |
500 |
done |
|
501 |
||
502 |
end |