src/HOL/Library/FrechetDeriv.thy
 author Christian Sternagel Wed Aug 29 12:23:14 2012 +0900 (2012-08-29) changeset 49083 01081bca31b6 parent 44568 e6f291cb5810 child 49962 a8cc904a6820 permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
1 (*  Title       : FrechetDeriv.thy
2     Author      : Brian Huffman
3 *)
5 header {* Frechet Derivative *}
7 theory FrechetDeriv
8 imports Complex_Main
9 begin
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)"
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"
24 lemma FDERIV_D:
25   "FDERIV f x :> D \<Longrightarrow> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0"
28 lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
31 lemma bounded_linear_zero: "bounded_linear (\<lambda>x. 0)"
32   by (rule bounded_linear_intro [where K=0], simp_all)
34 lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
35   by (simp add: fderiv_def bounded_linear_zero tendsto_const)
37 lemma bounded_linear_ident: "bounded_linear (\<lambda>x. x)"
38   by (rule bounded_linear_intro [where K=1], simp_all)
40 lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
41   by (simp add: fderiv_def bounded_linear_ident tendsto_const)
46   assumes "bounded_linear f"
47   assumes "bounded_linear g"
48   shows "bounded_linear (\<lambda>x. f x + g x)"
49 proof -
50   interpret f: bounded_linear f by fact
51   interpret g: bounded_linear g by fact
52   show ?thesis apply (unfold_locales)
54     apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
55     apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
56     apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
57     apply (rule_tac x="Kf + Kg" in exI, safe)
58     apply (subst right_distrib)
59     apply (rule order_trans [OF norm_triangle_ineq])
60     apply (rule add_mono, erule spec, erule spec)
61     done
62 qed
64 lemma norm_ratio_ineq:
65   fixes x y :: "'a::real_normed_vector"
66   fixes h :: "'b::real_normed_vector"
67   shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h"
68 apply (rule ord_le_eq_trans)
69 apply (rule divide_right_mono)
70 apply (rule norm_triangle_ineq)
71 apply (rule norm_ge_zero)
73 done
76   assumes f: "FDERIV f x :> F"
77   assumes g: "FDERIV g x :> G"
78   shows "FDERIV (\<lambda>x. f x + g x) x :> (\<lambda>h. F h + G h)"
79 proof (rule FDERIV_I)
80   show "bounded_linear (\<lambda>h. F h + G h)"
82     apply (rule FDERIV_bounded_linear [OF f])
83     apply (rule FDERIV_bounded_linear [OF g])
84     done
85 next
86   have f': "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
87     using f by (rule FDERIV_D)
88   have g': "(\<lambda>h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
89     using g by (rule FDERIV_D)
90   from f' g'
91   have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h
92            + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
94   thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
95            / norm h) -- 0 --> 0"
96     apply (rule real_LIM_sandwich_zero)
99     apply (rule norm_ratio_ineq)
100     done
101 qed
103 subsection {* Subtraction *}
105 lemma bounded_linear_minus:
106   assumes "bounded_linear f"
107   shows "bounded_linear (\<lambda>x. - f x)"
108 proof -
109   interpret f: bounded_linear f by fact
110   show ?thesis apply (unfold_locales)
114     done
115 qed
117 lemma FDERIV_minus:
118   "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
119 apply (rule FDERIV_I)
120 apply (rule bounded_linear_minus)
121 apply (erule FDERIV_bounded_linear)
122 apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel)
123 done
125 lemma FDERIV_diff:
126   "\<lbrakk>FDERIV f x :> F; FDERIV g x :> G\<rbrakk>
127    \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
128 by (simp only: diff_minus FDERIV_add FDERIV_minus)
130 subsection {* Uniqueness *}
132 lemma FDERIV_zero_unique:
133   assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
134 proof -
135   interpret F: bounded_linear F
136     using assms by (rule FDERIV_bounded_linear)
137   let ?r = "\<lambda>h. norm (F h) / norm h"
138   have *: "?r -- 0 --> 0"
139     using assms unfolding fderiv_def by simp
140   show "F = (\<lambda>h. 0)"
141   proof
142     fix h show "F h = 0"
143     proof (rule ccontr)
144       assume "F h \<noteq> 0"
145       moreover from this have h: "h \<noteq> 0"
146         by (clarsimp simp add: F.zero)
147       ultimately have "0 < ?r h"
149       from LIM_D [OF * this] obtain s where s: "0 < s"
150         and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
151       from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
152       let ?x = "scaleR (t / norm h) h"
153       have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
154       hence "?r ?x < ?r h" by (rule r)
155       thus "False" using t h by (simp add: F.scaleR)
156     qed
157   qed
158 qed
160 lemma FDERIV_unique:
161   assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
162 proof -
163   have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
164     using FDERIV_diff [OF assms] by simp
165   hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
166     by (rule FDERIV_zero_unique)
167   thus "F = F'"
168     unfolding fun_eq_iff right_minus_eq .
169 qed
171 subsection {* Continuity *}
173 lemma FDERIV_isCont:
174   assumes f: "FDERIV f x :> F"
175   shows "isCont f x"
176 proof -
177   from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
178   have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
179     by (rule FDERIV_D [OF f])
180   hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
181     by (intro tendsto_mult_zero tendsto_norm_zero tendsto_ident_at)
182   hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
183     by (simp cong: LIM_cong)
184   hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
185     by (rule tendsto_norm_zero_cancel)
186   hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
187     by (intro tendsto_add_zero F.tendsto_zero tendsto_ident_at)
188   hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
189     by simp
190   thus "isCont f x"
191     unfolding isCont_iff by (rule LIM_zero_cancel)
192 qed
194 subsection {* Composition *}
196 lemma real_divide_cancel_lemma:
197   fixes a b c :: real
198   shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c"
199 by simp
201 lemma bounded_linear_compose:
202   assumes "bounded_linear f"
203   assumes "bounded_linear g"
204   shows "bounded_linear (\<lambda>x. f (g x))"
205 proof -
206   interpret f: bounded_linear f by fact
207   interpret g: bounded_linear g by fact
208   show ?thesis proof (unfold_locales)
209     fix x y show "f (g (x + y)) = f (g x) + f (g y)"
211   next
212     fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
213       by (simp only: f.scaleR g.scaleR)
214   next
215     from f.pos_bounded
216     obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
217     from g.pos_bounded
218     obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
219     show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
220     proof (intro exI allI)
221       fix x
222       have "norm (f (g x)) \<le> norm (g x) * Kf"
223         using f .
224       also have "\<dots> \<le> (norm x * Kg) * Kf"
225         using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
226       also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
227         by (rule mult_assoc)
228       finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
229     qed
230   qed
231 qed
233 lemma FDERIV_compose:
234   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
235   fixes g :: "'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
236   assumes f: "FDERIV f x :> F"
237   assumes g: "FDERIV g (f x) :> G"
238   shows "FDERIV (\<lambda>x. g (f x)) x :> (\<lambda>h. G (F h))"
239 proof (rule FDERIV_I)
240   from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]
241   show "bounded_linear (\<lambda>h. G (F h))"
242     by (rule bounded_linear_compose)
243 next
244   let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
245   let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k"
246   let ?k = "\<lambda>h. f (x + h) - f x"
247   let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
248   let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
249   from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
250   from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear)
251   from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
252   from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
254   let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)"
256   show "(\<lambda>h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0"
257   proof (rule real_LIM_sandwich_zero)
258     have Nf: "?Nf -- 0 --> 0"
259       using FDERIV_D [OF f] .
261     have Ng1: "isCont (\<lambda>k. norm (?Rg k) / norm k) 0"
262       by (simp add: isCont_def FDERIV_D [OF g])
263     have Ng2: "?k -- 0 --> 0"
264       apply (rule LIM_zero)
265       apply (fold isCont_iff)
266       apply (rule FDERIV_isCont [OF f])
267       done
268     have Ng: "?Ng -- 0 --> 0"
269       using isCont_tendsto_compose [OF Ng1 Ng2] by simp
271     have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF))
272            -- 0 --> 0 * kG + 0 * (0 + kF)"
273       by (intro tendsto_intros Nf Ng)
274     thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
275       by simp
276   next
277     fix h::'a assume h: "h \<noteq> 0"
278     thus "0 \<le> norm (g (f (x + h)) - g (f x) - G (F h)) / norm h"
280   next
281     fix h::'a assume h: "h \<noteq> 0"
282     have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)"
284     hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
285            = norm (G (?Rf h) + ?Rg (?k h)) / norm h"
286       by (rule arg_cong)
287     also have "\<dots> \<le> norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h"
288       by (rule norm_ratio_ineq)
289     also have "\<dots> \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)"
291       show "norm (G (?Rf h)) / norm h \<le> ?Nf h * kG"
292         apply (rule ord_le_eq_trans)
293         apply (rule divide_right_mono [OF kG norm_ge_zero])
294         apply simp
295         done
296     next
297       have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)"
298         apply (rule real_divide_cancel_lemma [symmetric])
300         done
301       also have "\<dots> \<le> ?Ng h * (?Nf h + kF)"
302       proof (rule mult_left_mono)
303         have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h"
304           by simp
305         also have "\<dots> \<le> ?Nf h + norm (F h) / norm h"
306           by (rule norm_ratio_ineq)
307         also have "\<dots> \<le> ?Nf h + kF"
309           apply (subst pos_divide_le_eq, simp add: h)
310           apply (subst mult_commute)
311           apply (rule kF)
312           done
313         finally show "norm (?k h) / norm h \<le> ?Nf h + kF" .
314       next
315         show "0 \<le> ?Ng h"
316         apply (case_tac "f (x + h) - f x = 0", simp)
317         apply (rule divide_nonneg_pos [OF norm_ge_zero])
318         apply simp
319         done
320       qed
321       finally show "norm (?Rg (?k h)) / norm h \<le> ?Ng h * (?Nf h + kF)" .
322     qed
323     finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
324         \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" .
325   qed
326 qed
328 subsection {* Product Rule *}
330 lemma (in bounded_bilinear) FDERIV_lemma:
331   "a' ** b' - a ** b - (a ** B + A ** b)
332    = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)"
333 by (simp add: diff_left diff_right)
335 lemma (in bounded_bilinear) FDERIV:
336   fixes x :: "'d::real_normed_vector"
337   assumes f: "FDERIV f x :> F"
338   assumes g: "FDERIV g x :> G"
339   shows "FDERIV (\<lambda>x. f x ** g x) x :> (\<lambda>h. f x ** G h + F h ** g x)"
340 proof (rule FDERIV_I)
341   show "bounded_linear (\<lambda>h. f x ** G h + F h ** g x)"
343     apply (rule bounded_linear_compose [OF bounded_linear_right])
344     apply (rule FDERIV_bounded_linear [OF g])
345     apply (rule bounded_linear_compose [OF bounded_linear_left])
346     apply (rule FDERIV_bounded_linear [OF f])
347     done
348 next
349   from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
350   obtain KF where norm_F: "\<And>x. norm (F x) \<le> norm x * KF" by fast
352   from pos_bounded obtain K where K: "0 < K" and norm_prod:
353     "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
355   let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
356   let ?Rg = "\<lambda>h. g (x + h) - g x - G h"
358   let ?fun1 = "\<lambda>h.
359         norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) /
360         norm h"
362   let ?fun2 = "\<lambda>h.
363         norm (f x) * (norm (?Rg h) / norm h) * K +
364         norm (?Rf h) / norm h * norm (g (x + h)) * K +
365         KF * norm (g (x + h) - g x) * K"
367   have "?fun1 -- 0 --> 0"
368   proof (rule real_LIM_sandwich_zero)
369     from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
370     have "?fun2 -- 0 -->
371           norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
372       by (intro tendsto_intros LIM_zero FDERIV_D)
373     thus "?fun2 -- 0 --> 0"
374       by simp
375   next
376     fix h::'d assume "h \<noteq> 0"
377     thus "0 \<le> ?fun1 h"
379   next
380     fix h::'d assume "h \<noteq> 0"
381     have "?fun1 h \<le> (norm (f x) * norm (?Rg h) * K +
382          norm (?Rf h) * norm (g (x + h)) * K +
383          norm h * KF * norm (g (x + h) - g x) * K) / norm h"
384       by (intro
385         divide_right_mono mult_mono'
387         order_trans [OF norm_prod mult_right_mono]
388         mult_nonneg_nonneg order_refl norm_ge_zero norm_F
389         K [THEN order_less_imp_le]
390       )
391     also have "\<dots> = ?fun2 h"
393     finally show "?fun1 h \<le> ?fun2 h" .
394   qed
395   thus "(\<lambda>h.
396     norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x))
397     / norm h) -- 0 --> 0"
398     by (simp only: FDERIV_lemma)
399 qed
401 lemmas FDERIV_mult =
402   bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
404 lemmas FDERIV_scaleR =
405   bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
408 subsection {* Powers *}
410 lemma FDERIV_power_Suc:
411   fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
412   shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
413  apply (induct n)
415  apply (drule FDERIV_mult [OF FDERIV_ident])
416  apply (simp only: of_nat_Suc left_distrib mult_1_left)
417  apply (simp only: power_Suc right_distrib add_ac mult_ac)
418 done
420 lemma FDERIV_power:
421   fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
422   shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
423   apply (cases n)
425   apply (simp add: FDERIV_power_Suc del: power_Suc)
426   done
429 subsection {* Inverse *}
431 lemmas bounded_linear_mult_const =
432   bounded_linear_mult_left [THEN bounded_linear_compose]
434 lemmas bounded_linear_const_mult =
435   bounded_linear_mult_right [THEN bounded_linear_compose]
437 lemma FDERIV_inverse:
438   fixes x :: "'a::real_normed_div_algebra"
439   assumes x: "x \<noteq> 0"
440   shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))"
441         (is "FDERIV ?inv _ :> _")
442 proof (rule FDERIV_I)
443   show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
444     apply (rule bounded_linear_minus)
445     apply (rule bounded_linear_mult_const)
446     apply (rule bounded_linear_const_mult)
447     apply (rule bounded_linear_ident)
448     done
449 next
450   show "(\<lambda>h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h)
451         -- 0 --> 0"
452   proof (rule LIM_equal2)
453     show "0 < norm x" using x by simp
454   next
455     fix h::'a
456     assume 1: "h \<noteq> 0"
457     assume "norm (h - 0) < norm x"
458     hence "h \<noteq> -x" by clarsimp
459     hence 2: "x + h \<noteq> 0"
460       apply (rule contrapos_nn)
461       apply (rule sym)
462       apply (erule minus_unique)
463       done
464     show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
465           = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
466       apply (subst inverse_diff_inverse [OF 2 x])
467       apply (subst minus_diff_minus)
468       apply (subst norm_minus_cancel)
470       done
471   next
472     show "(\<lambda>h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h)
473           -- 0 --> 0"
474     proof (rule real_LIM_sandwich_zero)
475       show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x))
476             -- 0 --> 0"
477         apply (rule tendsto_mult_left_zero)
478         apply (rule tendsto_norm_zero)
479         apply (rule LIM_zero)
480         apply (rule LIM_offset_zero)
481         apply (rule tendsto_inverse)
482         apply (rule tendsto_ident_at)
483         apply (rule x)
484         done
485     next
486       fix h::'a assume h: "h \<noteq> 0"
487       show "0 \<le> norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
488         apply (rule divide_nonneg_pos)
489         apply (rule norm_ge_zero)
491         done
492     next
493       fix h::'a assume h: "h \<noteq> 0"
494       have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
495             \<le> norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h"
496         apply (rule divide_right_mono [OF _ norm_ge_zero])
497         apply (rule order_trans [OF norm_mult_ineq])
498         apply (rule mult_right_mono [OF _ norm_ge_zero])
499         apply (rule norm_mult_ineq)
500         done
501       also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
502         by simp
503       finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
504             \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
505     qed
506   qed
507 qed
509 subsection {* Alternate definition *}
511 lemma field_fderiv_def:
512   fixes x :: "'a::real_normed_field" shows
513   "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
514  apply (unfold fderiv_def)