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