src/HOL/Deriv.thy
 author wenzelm Tue Sep 03 01:12:40 2013 +0200 (2013-09-03) changeset 53374 a14d2a854c02 parent 51642 400ec5ae7f8f child 53381 355a4cac5440 permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
 huffman@21164 ` 1` ```(* Title : Deriv.thy ``` huffman@21164 ` 2` ``` Author : Jacques D. Fleuriot ``` huffman@21164 ` 3` ``` Copyright : 1998 University of Cambridge ``` hoelzl@51642 ` 4` ``` Author : Brian Huffman ``` huffman@21164 ` 5` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2004 ``` huffman@21164 ` 6` ``` GMVT by Benjamin Porter, 2005 ``` huffman@21164 ` 7` ```*) ``` huffman@21164 ` 8` huffman@21164 ` 9` ```header{* Differentiation *} ``` huffman@21164 ` 10` huffman@21164 ` 11` ```theory Deriv ``` hoelzl@51526 ` 12` ```imports Limits ``` huffman@21164 ` 13` ```begin ``` huffman@21164 ` 14` hoelzl@51642 ` 15` ```definition ``` hoelzl@51642 ` 16` ``` -- {* Frechet derivative: D is derivative of function f at x within s *} ``` hoelzl@51642 ` 17` ``` has_derivative :: "('a::real_normed_vector \ 'b::real_normed_vector) \ ('a \ 'b) \ 'a filter \ bool" ``` hoelzl@51642 ` 18` ``` (infixl "(has'_derivative)" 12) ``` hoelzl@51642 ` 19` ```where ``` hoelzl@51642 ` 20` ``` "(f has_derivative f') F \ ``` hoelzl@51642 ` 21` ``` (bounded_linear f' \ ``` hoelzl@51642 ` 22` ``` ((\y. ((f y - f (Lim F (\x. x))) - f' (y - Lim F (\x. x))) /\<^sub>R norm (y - Lim F (\x. x))) ---> 0) F)" ``` hoelzl@51642 ` 23` hoelzl@51642 ` 24` ```lemma FDERIV_eq_rhs: "(f has_derivative f') F \ f' = g' \ (f has_derivative g') F" ``` hoelzl@51642 ` 25` ``` by simp ``` hoelzl@51642 ` 26` hoelzl@51642 ` 27` ```ML {* ``` hoelzl@51642 ` 28` hoelzl@51642 ` 29` ```structure FDERIV_Intros = Named_Thms ``` hoelzl@51642 ` 30` ```( ``` hoelzl@51642 ` 31` ``` val name = @{binding FDERIV_intros} ``` hoelzl@51642 ` 32` ``` val description = "introduction rules for FDERIV" ``` hoelzl@51642 ` 33` ```) ``` hoelzl@51642 ` 34` hoelzl@51642 ` 35` ```*} ``` hoelzl@51642 ` 36` hoelzl@51642 ` 37` ```setup {* ``` hoelzl@51642 ` 38` ``` FDERIV_Intros.setup #> ``` hoelzl@51642 ` 39` ``` Global_Theory.add_thms_dynamic (@{binding FDERIV_eq_intros}, ``` hoelzl@51642 ` 40` ``` map_filter (try (fn thm => @{thm FDERIV_eq_rhs} OF [thm])) o FDERIV_Intros.get o Context.proof_of); ``` hoelzl@51642 ` 41` ```*} ``` hoelzl@51642 ` 42` hoelzl@51642 ` 43` ```lemma FDERIV_bounded_linear: "(f has_derivative f') F \ bounded_linear f'" ``` hoelzl@51642 ` 44` ``` by (simp add: has_derivative_def) ``` hoelzl@51642 ` 45` hoelzl@51642 ` 46` ```lemma FDERIV_ident[FDERIV_intros, simp]: "((\x. x) has_derivative (\x. x)) F" ``` hoelzl@51642 ` 47` ``` by (simp add: has_derivative_def tendsto_const) ``` hoelzl@51642 ` 48` hoelzl@51642 ` 49` ```lemma FDERIV_const[FDERIV_intros, simp]: "((\x. c) has_derivative (\x. 0)) F" ``` hoelzl@51642 ` 50` ``` by (simp add: has_derivative_def tendsto_const) ``` hoelzl@51642 ` 51` hoelzl@51642 ` 52` ```lemma (in bounded_linear) bounded_linear: "bounded_linear f" .. ``` hoelzl@51642 ` 53` hoelzl@51642 ` 54` ```lemma (in bounded_linear) FDERIV: ``` hoelzl@51642 ` 55` ``` "(g has_derivative g') F \ ((\x. f (g x)) has_derivative (\x. f (g' x))) F" ``` hoelzl@51642 ` 56` ``` using assms unfolding has_derivative_def ``` hoelzl@51642 ` 57` ``` apply safe ``` hoelzl@51642 ` 58` ``` apply (erule bounded_linear_compose [OF local.bounded_linear]) ``` hoelzl@51642 ` 59` ``` apply (drule local.tendsto) ``` hoelzl@51642 ` 60` ``` apply (simp add: local.scaleR local.diff local.add local.zero) ``` hoelzl@51642 ` 61` ``` done ``` hoelzl@51642 ` 62` hoelzl@51642 ` 63` ```lemmas FDERIV_scaleR_right [FDERIV_intros] = ``` hoelzl@51642 ` 64` ``` bounded_linear.FDERIV [OF bounded_linear_scaleR_right] ``` hoelzl@51642 ` 65` hoelzl@51642 ` 66` ```lemmas FDERIV_scaleR_left [FDERIV_intros] = ``` hoelzl@51642 ` 67` ``` bounded_linear.FDERIV [OF bounded_linear_scaleR_left] ``` hoelzl@51642 ` 68` hoelzl@51642 ` 69` ```lemmas FDERIV_mult_right [FDERIV_intros] = ``` hoelzl@51642 ` 70` ``` bounded_linear.FDERIV [OF bounded_linear_mult_right] ``` hoelzl@51642 ` 71` hoelzl@51642 ` 72` ```lemmas FDERIV_mult_left [FDERIV_intros] = ``` hoelzl@51642 ` 73` ``` bounded_linear.FDERIV [OF bounded_linear_mult_left] ``` hoelzl@51642 ` 74` hoelzl@51642 ` 75` ```lemma FDERIV_add[simp, FDERIV_intros]: ``` hoelzl@51642 ` 76` ``` assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F" ``` hoelzl@51642 ` 77` ``` shows "((\x. f x + g x) has_derivative (\x. f' x + g' x)) F" ``` hoelzl@51642 ` 78` ``` unfolding has_derivative_def ``` hoelzl@51642 ` 79` ```proof safe ``` hoelzl@51642 ` 80` ``` let ?x = "Lim F (\x. x)" ``` hoelzl@51642 ` 81` ``` let ?D = "\f f' y. ((f y - f ?x) - f' (y - ?x)) /\<^sub>R norm (y - ?x)" ``` hoelzl@51642 ` 82` ``` have "((\x. ?D f f' x + ?D g g' x) ---> (0 + 0)) F" ``` hoelzl@51642 ` 83` ``` using f g by (intro tendsto_add) (auto simp: has_derivative_def) ``` hoelzl@51642 ` 84` ``` then show "(?D (\x. f x + g x) (\x. f' x + g' x) ---> 0) F" ``` hoelzl@51642 ` 85` ``` by (simp add: field_simps scaleR_add_right scaleR_diff_right) ``` hoelzl@51642 ` 86` ```qed (blast intro: bounded_linear_add f g FDERIV_bounded_linear) ``` hoelzl@51642 ` 87` hoelzl@51642 ` 88` ```lemma FDERIV_setsum[simp, FDERIV_intros]: ``` hoelzl@51642 ` 89` ``` assumes f: "\i. i \ I \ (f i has_derivative f' i) F" ``` hoelzl@51642 ` 90` ``` shows "((\x. \i\I. f i x) has_derivative (\x. \i\I. f' i x)) F" ``` hoelzl@51642 ` 91` ```proof cases ``` hoelzl@51642 ` 92` ``` assume "finite I" from this f show ?thesis ``` hoelzl@51642 ` 93` ``` by induct (simp_all add: f) ``` hoelzl@51642 ` 94` ```qed simp ``` hoelzl@51642 ` 95` hoelzl@51642 ` 96` ```lemma FDERIV_minus[simp, FDERIV_intros]: "(f has_derivative f') F \ ((\x. - f x) has_derivative (\x. - f' x)) F" ``` hoelzl@51642 ` 97` ``` using FDERIV_scaleR_right[of f f' F "-1"] by simp ``` hoelzl@51642 ` 98` hoelzl@51642 ` 99` ```lemma FDERIV_diff[simp, FDERIV_intros]: ``` hoelzl@51642 ` 100` ``` "(f has_derivative f') F \ (g has_derivative g') F \ ((\x. f x - g x) has_derivative (\x. f' x - g' x)) F" ``` hoelzl@51642 ` 101` ``` by (simp only: diff_minus FDERIV_add FDERIV_minus) ``` hoelzl@51642 ` 102` hoelzl@51642 ` 103` ```abbreviation ``` hoelzl@51642 ` 104` ``` -- {* Frechet derivative: D is derivative of function f at x within s *} ``` hoelzl@51642 ` 105` ``` FDERIV :: "('a::real_normed_vector \ 'b::real_normed_vector) \ 'a \ 'a set \ ('a \ 'b) \ bool" ``` hoelzl@51642 ` 106` ``` ("(FDERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60) ``` hoelzl@51642 ` 107` ```where ``` hoelzl@51642 ` 108` ``` "FDERIV f x : s :> f' \ (f has_derivative f') (at x within s)" ``` hoelzl@51642 ` 109` hoelzl@51642 ` 110` ```abbreviation ``` hoelzl@51642 ` 111` ``` fderiv_at :: ``` hoelzl@51642 ` 112` ``` "('a::real_normed_vector \ 'b::real_normed_vector) \ 'a \ ('a \ 'b) \ bool" ``` hoelzl@51642 ` 113` ``` ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) ``` hoelzl@51642 ` 114` ```where ``` hoelzl@51642 ` 115` ``` "FDERIV f x :> D \ FDERIV f x : UNIV :> D" ``` hoelzl@51642 ` 116` hoelzl@51642 ` 117` ```lemma FDERIV_def: ``` hoelzl@51642 ` 118` ``` "FDERIV f x : s :> f' \ ``` hoelzl@51642 ` 119` ``` (bounded_linear f' \ ((\y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s))" ``` hoelzl@51642 ` 120` ``` by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at) ``` hoelzl@51642 ` 121` hoelzl@51642 ` 122` ```lemma FDERIV_iff_norm: ``` hoelzl@51642 ` 123` ``` "FDERIV f x : s :> f' \ ``` hoelzl@51642 ` 124` ``` (bounded_linear f' \ ((\y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) ---> 0) (at x within s))" ``` hoelzl@51642 ` 125` ``` using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric] ``` hoelzl@51642 ` 126` ``` by (simp add: FDERIV_def divide_inverse ac_simps) ``` hoelzl@51642 ` 127` hoelzl@51642 ` 128` ```lemma fderiv_def: ``` hoelzl@51642 ` 129` ``` "FDERIV f x :> D = (bounded_linear D \ (\h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)" ``` hoelzl@51642 ` 130` ``` unfolding FDERIV_iff_norm LIM_offset_zero_iff[of _ _ x] by simp ``` hoelzl@51642 ` 131` hoelzl@51642 ` 132` ```lemma field_fderiv_def: ``` hoelzl@51642 ` 133` ``` fixes x :: "'a::real_normed_field" ``` hoelzl@51642 ` 134` ``` shows "FDERIV f x :> (\h. h * D) = (\h. (f (x + h) - f x) / h) -- 0 --> D" ``` hoelzl@51642 ` 135` ``` apply (unfold fderiv_def) ``` hoelzl@51642 ` 136` ``` apply (simp add: bounded_linear_mult_left) ``` hoelzl@51642 ` 137` ``` apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) ``` hoelzl@51642 ` 138` ``` apply (subst diff_divide_distrib) ``` hoelzl@51642 ` 139` ``` apply (subst times_divide_eq_left [symmetric]) ``` hoelzl@51642 ` 140` ``` apply (simp cong: LIM_cong) ``` hoelzl@51642 ` 141` ``` apply (simp add: tendsto_norm_zero_iff LIM_zero_iff) ``` hoelzl@51642 ` 142` ``` done ``` hoelzl@51642 ` 143` hoelzl@51642 ` 144` ```lemma FDERIV_I: ``` hoelzl@51642 ` 145` ``` "bounded_linear f' \ ((\y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s) \ ``` hoelzl@51642 ` 146` ``` FDERIV f x : s :> f'" ``` hoelzl@51642 ` 147` ``` by (simp add: FDERIV_def) ``` hoelzl@51642 ` 148` hoelzl@51642 ` 149` ```lemma FDERIV_I_sandwich: ``` hoelzl@51642 ` 150` ``` assumes e: "0 < e" and bounded: "bounded_linear f'" ``` hoelzl@51642 ` 151` ``` and sandwich: "(\y. y \ s \ y \ x \ dist y x < e \ norm ((f y - f x) - f' (y - x)) / norm (y - x) \ H y)" ``` hoelzl@51642 ` 152` ``` and "(H ---> 0) (at x within s)" ``` hoelzl@51642 ` 153` ``` shows "FDERIV f x : s :> f'" ``` hoelzl@51642 ` 154` ``` unfolding FDERIV_iff_norm ``` hoelzl@51642 ` 155` ```proof safe ``` hoelzl@51642 ` 156` ``` show "((\y. norm (f y - f x - f' (y - x)) / norm (y - x)) ---> 0) (at x within s)" ``` hoelzl@51642 ` 157` ``` proof (rule tendsto_sandwich[where f="\x. 0"]) ``` hoelzl@51642 ` 158` ``` show "(H ---> 0) (at x within s)" by fact ``` hoelzl@51642 ` 159` ``` show "eventually (\n. norm (f n - f x - f' (n - x)) / norm (n - x) \ H n) (at x within s)" ``` hoelzl@51642 ` 160` ``` unfolding eventually_at using e sandwich by auto ``` hoelzl@51642 ` 161` ``` qed (auto simp: le_divide_eq tendsto_const) ``` hoelzl@51642 ` 162` ```qed fact ``` hoelzl@51642 ` 163` hoelzl@51642 ` 164` ```lemma FDERIV_subset: "FDERIV f x : s :> f' \ t \ s \ FDERIV f x : t :> f'" ``` hoelzl@51642 ` 165` ``` by (auto simp add: FDERIV_iff_norm intro: tendsto_within_subset) ``` hoelzl@51642 ` 166` hoelzl@51642 ` 167` ```subsection {* Continuity *} ``` hoelzl@51642 ` 168` hoelzl@51642 ` 169` ```lemma FDERIV_continuous: ``` hoelzl@51642 ` 170` ``` assumes f: "FDERIV f x : s :> f'" ``` hoelzl@51642 ` 171` ``` shows "continuous (at x within s) f" ``` hoelzl@51642 ` 172` ```proof - ``` hoelzl@51642 ` 173` ``` from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear) ``` hoelzl@51642 ` 174` ``` note F.tendsto[tendsto_intros] ``` hoelzl@51642 ` 175` ``` let ?L = "\f. (f ---> 0) (at x within s)" ``` hoelzl@51642 ` 176` ``` have "?L (\y. norm ((f y - f x) - f' (y - x)) / norm (y - x))" ``` hoelzl@51642 ` 177` ``` using f unfolding FDERIV_iff_norm by blast ``` hoelzl@51642 ` 178` ``` then have "?L (\y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m) ``` hoelzl@51642 ` 179` ``` by (rule tendsto_mult_zero) (auto intro!: tendsto_eq_intros) ``` hoelzl@51642 ` 180` ``` also have "?m \ ?L (\y. norm ((f y - f x) - f' (y - x)))" ``` hoelzl@51642 ` 181` ``` by (intro filterlim_cong) (simp_all add: eventually_at_filter) ``` hoelzl@51642 ` 182` ``` finally have "?L (\y. (f y - f x) - f' (y - x))" ``` hoelzl@51642 ` 183` ``` by (rule tendsto_norm_zero_cancel) ``` hoelzl@51642 ` 184` ``` then have "?L (\y. ((f y - f x) - f' (y - x)) + f' (y - x))" ``` hoelzl@51642 ` 185` ``` by (rule tendsto_eq_intros) (auto intro!: tendsto_eq_intros simp: F.zero) ``` hoelzl@51642 ` 186` ``` then have "?L (\y. f y - f x)" ``` hoelzl@51642 ` 187` ``` by simp ``` hoelzl@51642 ` 188` ``` from tendsto_add[OF this tendsto_const, of "f x"] show ?thesis ``` hoelzl@51642 ` 189` ``` by (simp add: continuous_within) ``` hoelzl@51642 ` 190` ```qed ``` hoelzl@51642 ` 191` hoelzl@51642 ` 192` ```subsection {* Composition *} ``` hoelzl@51642 ` 193` hoelzl@51642 ` 194` ```lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \ (f ---> y) (at x within s) \ (f ---> y) (inf (nhds x) (principal s))" ``` hoelzl@51642 ` 195` ``` unfolding tendsto_def eventually_inf_principal eventually_at_filter ``` hoelzl@51642 ` 196` ``` by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1) ``` hoelzl@51642 ` 197` hoelzl@51642 ` 198` ```lemma FDERIV_in_compose: ``` hoelzl@51642 ` 199` ``` assumes f: "FDERIV f x : s :> f'" ``` hoelzl@51642 ` 200` ``` assumes g: "FDERIV g (f x) : (f`s) :> g'" ``` hoelzl@51642 ` 201` ``` shows "FDERIV (\x. g (f x)) x : s :> (\x. g' (f' x))" ``` hoelzl@51642 ` 202` ```proof - ``` hoelzl@51642 ` 203` ``` from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear) ``` hoelzl@51642 ` 204` ``` from g interpret G: bounded_linear g' by (rule FDERIV_bounded_linear) ``` hoelzl@51642 ` 205` ``` from F.bounded obtain kF where kF: "\x. norm (f' x) \ norm x * kF" by fast ``` hoelzl@51642 ` 206` ``` from G.bounded obtain kG where kG: "\x. norm (g' x) \ norm x * kG" by fast ``` hoelzl@51642 ` 207` ``` note G.tendsto[tendsto_intros] ``` hoelzl@51642 ` 208` hoelzl@51642 ` 209` ``` let ?L = "\f. (f ---> 0) (at x within s)" ``` hoelzl@51642 ` 210` ``` let ?D = "\f f' x y. (f y - f x) - f' (y - x)" ``` hoelzl@51642 ` 211` ``` let ?N = "\f f' x y. norm (?D f f' x y) / norm (y - x)" ``` hoelzl@51642 ` 212` ``` let ?gf = "\x. g (f x)" and ?gf' = "\x. g' (f' x)" ``` hoelzl@51642 ` 213` ``` def Nf \ "?N f f' x" ``` hoelzl@51642 ` 214` ``` def Ng \ "\y. ?N g g' (f x) (f y)" ``` hoelzl@51642 ` 215` hoelzl@51642 ` 216` ``` show ?thesis ``` hoelzl@51642 ` 217` ``` proof (rule FDERIV_I_sandwich[of 1]) ``` hoelzl@51642 ` 218` ``` show "bounded_linear (\x. g' (f' x))" ``` hoelzl@51642 ` 219` ``` using f g by (blast intro: bounded_linear_compose FDERIV_bounded_linear) ``` hoelzl@51642 ` 220` ``` next ``` hoelzl@51642 ` 221` ``` fix y::'a assume neq: "y \ x" ``` hoelzl@51642 ` 222` ``` have "?N ?gf ?gf' x y = norm (g' (?D f f' x y) + ?D g g' (f x) (f y)) / norm (y - x)" ``` hoelzl@51642 ` 223` ``` by (simp add: G.diff G.add field_simps) ``` hoelzl@51642 ` 224` ``` also have "\ \ norm (g' (?D f f' x y)) / norm (y - x) + Ng y * (norm (f y - f x) / norm (y - x))" ``` hoelzl@51642 ` 225` ``` by (simp add: add_divide_distrib[symmetric] divide_right_mono norm_triangle_ineq G.zero Ng_def) ``` hoelzl@51642 ` 226` ``` also have "\ \ Nf y * kG + Ng y * (Nf y + kF)" ``` hoelzl@51642 ` 227` ``` proof (intro add_mono mult_left_mono) ``` hoelzl@51642 ` 228` ``` have "norm (f y - f x) = norm (?D f f' x y + f' (y - x))" ``` hoelzl@51642 ` 229` ``` by simp ``` hoelzl@51642 ` 230` ``` also have "\ \ norm (?D f f' x y) + norm (f' (y - x))" ``` hoelzl@51642 ` 231` ``` by (rule norm_triangle_ineq) ``` hoelzl@51642 ` 232` ``` also have "\ \ norm (?D f f' x y) + norm (y - x) * kF" ``` hoelzl@51642 ` 233` ``` using kF by (intro add_mono) simp ``` hoelzl@51642 ` 234` ``` finally show "norm (f y - f x) / norm (y - x) \ Nf y + kF" ``` hoelzl@51642 ` 235` ``` by (simp add: neq Nf_def field_simps) ``` hoelzl@51642 ` 236` ``` qed (insert kG, simp_all add: Ng_def Nf_def neq zero_le_divide_iff field_simps) ``` hoelzl@51642 ` 237` ``` finally show "?N ?gf ?gf' x y \ Nf y * kG + Ng y * (Nf y + kF)" . ``` hoelzl@51642 ` 238` ``` next ``` hoelzl@51642 ` 239` ``` have [tendsto_intros]: "?L Nf" ``` hoelzl@51642 ` 240` ``` using f unfolding FDERIV_iff_norm Nf_def .. ``` hoelzl@51642 ` 241` ``` from f have "(f ---> f x) (at x within s)" ``` hoelzl@51642 ` 242` ``` by (blast intro: FDERIV_continuous continuous_within[THEN iffD1]) ``` hoelzl@51642 ` 243` ``` then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))" ``` hoelzl@51642 ` 244` ``` unfolding filterlim_def ``` hoelzl@51642 ` 245` ``` by (simp add: eventually_filtermap eventually_at_filter le_principal) ``` hoelzl@51642 ` 246` hoelzl@51642 ` 247` ``` have "((?N g g' (f x)) ---> 0) (at (f x) within f`s)" ``` hoelzl@51642 ` 248` ``` using g unfolding FDERIV_iff_norm .. ``` hoelzl@51642 ` 249` ``` then have g': "((?N g g' (f x)) ---> 0) (inf (nhds (f x)) (principal (f`s)))" ``` hoelzl@51642 ` 250` ``` by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp ``` hoelzl@51642 ` 251` hoelzl@51642 ` 252` ``` have [tendsto_intros]: "?L Ng" ``` hoelzl@51642 ` 253` ``` unfolding Ng_def by (rule filterlim_compose[OF g' f']) ``` hoelzl@51642 ` 254` ``` show "((\y. Nf y * kG + Ng y * (Nf y + kF)) ---> 0) (at x within s)" ``` hoelzl@51642 ` 255` ``` by (intro tendsto_eq_intros) auto ``` hoelzl@51642 ` 256` ``` qed simp ``` hoelzl@51642 ` 257` ```qed ``` hoelzl@51642 ` 258` hoelzl@51642 ` 259` ```lemma FDERIV_compose: ``` hoelzl@51642 ` 260` ``` "FDERIV f x : s :> f' \ FDERIV g (f x) :> g' \ FDERIV (\x. g (f x)) x : s :> (\x. g' (f' x))" ``` hoelzl@51642 ` 261` ``` by (blast intro: FDERIV_in_compose FDERIV_subset) ``` hoelzl@51642 ` 262` hoelzl@51642 ` 263` ```lemma (in bounded_bilinear) FDERIV: ``` hoelzl@51642 ` 264` ``` assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" ``` hoelzl@51642 ` 265` ``` shows "FDERIV (\x. f x ** g x) x : s :> (\h. f x ** g' h + f' h ** g x)" ``` hoelzl@51642 ` 266` ```proof - ``` hoelzl@51642 ` 267` ``` from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]] ``` hoelzl@51642 ` 268` ``` obtain KF where norm_F: "\x. norm (f' x) \ norm x * KF" by fast ``` hoelzl@51642 ` 269` hoelzl@51642 ` 270` ``` from pos_bounded obtain K where K: "0 < K" and norm_prod: ``` hoelzl@51642 ` 271` ``` "\a b. norm (a ** b) \ norm a * norm b * K" by fast ``` hoelzl@51642 ` 272` ``` let ?D = "\f f' y. f y - f x - f' (y - x)" ``` hoelzl@51642 ` 273` ``` let ?N = "\f f' y. norm (?D f f' y) / norm (y - x)" ``` hoelzl@51642 ` 274` ``` def Ng =="?N g g'" and Nf =="?N f f'" ``` hoelzl@51642 ` 275` hoelzl@51642 ` 276` ``` let ?fun1 = "\y. norm (f y ** g y - f x ** g x - (f x ** g' (y - x) + f' (y - x) ** g x)) / norm (y - x)" ``` hoelzl@51642 ` 277` ``` let ?fun2 = "\y. norm (f x) * Ng y * K + Nf y * norm (g y) * K + KF * norm (g y - g x) * K" ``` hoelzl@51642 ` 278` ``` let ?F = "at x within s" ``` huffman@21164 ` 279` hoelzl@51642 ` 280` ``` show ?thesis ``` hoelzl@51642 ` 281` ``` proof (rule FDERIV_I_sandwich[of 1]) ``` hoelzl@51642 ` 282` ``` show "bounded_linear (\h. f x ** g' h + f' h ** g x)" ``` hoelzl@51642 ` 283` ``` by (intro bounded_linear_add ``` hoelzl@51642 ` 284` ``` bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left] ``` hoelzl@51642 ` 285` ``` FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]) ``` hoelzl@51642 ` 286` ``` next ``` hoelzl@51642 ` 287` ``` from g have "(g ---> g x) ?F" ``` hoelzl@51642 ` 288` ``` by (intro continuous_within[THEN iffD1] FDERIV_continuous) ``` hoelzl@51642 ` 289` ``` moreover from f g have "(Nf ---> 0) ?F" "(Ng ---> 0) ?F" ``` hoelzl@51642 ` 290` ``` by (simp_all add: FDERIV_iff_norm Ng_def Nf_def) ``` hoelzl@51642 ` 291` ``` ultimately have "(?fun2 ---> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F" ``` hoelzl@51642 ` 292` ``` by (intro tendsto_intros) (simp_all add: LIM_zero_iff) ``` hoelzl@51642 ` 293` ``` then show "(?fun2 ---> 0) ?F" ``` hoelzl@51642 ` 294` ``` by simp ``` hoelzl@51642 ` 295` ``` next ``` hoelzl@51642 ` 296` ``` fix y::'d assume "y \ x" ``` hoelzl@51642 ` 297` ``` have "?fun1 y = norm (f x ** ?D g g' y + ?D f f' y ** g y + f' (y - x) ** (g y - g x)) / norm (y - x)" ``` hoelzl@51642 ` 298` ``` by (simp add: diff_left diff_right add_left add_right field_simps) ``` hoelzl@51642 ` 299` ``` also have "\ \ (norm (f x) * norm (?D g g' y) * K + norm (?D f f' y) * norm (g y) * K + ``` hoelzl@51642 ` 300` ``` norm (y - x) * KF * norm (g y - g x) * K) / norm (y - x)" ``` hoelzl@51642 ` 301` ``` by (intro divide_right_mono mult_mono' ``` hoelzl@51642 ` 302` ``` order_trans [OF norm_triangle_ineq add_mono] ``` hoelzl@51642 ` 303` ``` order_trans [OF norm_prod mult_right_mono] ``` hoelzl@51642 ` 304` ``` mult_nonneg_nonneg order_refl norm_ge_zero norm_F ``` hoelzl@51642 ` 305` ``` K [THEN order_less_imp_le]) ``` hoelzl@51642 ` 306` ``` also have "\ = ?fun2 y" ``` hoelzl@51642 ` 307` ``` by (simp add: add_divide_distrib Ng_def Nf_def) ``` hoelzl@51642 ` 308` ``` finally show "?fun1 y \ ?fun2 y" . ``` hoelzl@51642 ` 309` ``` qed simp ``` hoelzl@51642 ` 310` ```qed ``` hoelzl@51642 ` 311` hoelzl@51642 ` 312` ```lemmas FDERIV_mult[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult] ``` hoelzl@51642 ` 313` ```lemmas FDERIV_scaleR[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR] ``` hoelzl@51642 ` 314` hoelzl@51642 ` 315` ```lemma FDERIV_setprod[simp, FDERIV_intros]: ``` hoelzl@51642 ` 316` ``` fixes f :: "'i \ 'a :: real_normed_vector \ 'b :: real_normed_field" ``` hoelzl@51642 ` 317` ``` assumes f: "\i. i \ I \ FDERIV (f i) x : s :> f' i" ``` hoelzl@51642 ` 318` ``` shows "FDERIV (\x. \i\I. f i x) x : s :> (\y. \i\I. f' i y * (\j\I - {i}. f j x))" ``` hoelzl@51642 ` 319` ```proof cases ``` hoelzl@51642 ` 320` ``` assume "finite I" from this f show ?thesis ``` hoelzl@51642 ` 321` ``` proof induct ``` hoelzl@51642 ` 322` ``` case (insert i I) ``` hoelzl@51642 ` 323` ``` let ?P = "\y. f i x * (\i\I. f' i y * (\j\I - {i}. f j x)) + (f' i y) * (\i\I. f i x)" ``` hoelzl@51642 ` 324` ``` have "FDERIV (\x. f i x * (\i\I. f i x)) x : s :> ?P" ``` hoelzl@51642 ` 325` ``` using insert by (intro FDERIV_mult) auto ``` hoelzl@51642 ` 326` ``` also have "?P = (\y. \i'\insert i I. f' i' y * (\j\insert i I - {i'}. f j x))" ``` hoelzl@51642 ` 327` ``` using insert(1,2) by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum_cong) ``` hoelzl@51642 ` 328` ``` finally show ?case ``` hoelzl@51642 ` 329` ``` using insert by simp ``` hoelzl@51642 ` 330` ``` qed simp ``` hoelzl@51642 ` 331` ```qed simp ``` hoelzl@51642 ` 332` hoelzl@51642 ` 333` ```lemma FDERIV_power[simp, FDERIV_intros]: ``` hoelzl@51642 ` 334` ``` fixes f :: "'a :: real_normed_vector \ 'b :: real_normed_field" ``` hoelzl@51642 ` 335` ``` assumes f: "FDERIV f x : s :> f'" ``` hoelzl@51642 ` 336` ``` shows "FDERIV (\x. f x^n) x : s :> (\y. of_nat n * f' y * f x^(n - 1))" ``` hoelzl@51642 ` 337` ``` using FDERIV_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps) ``` hoelzl@51642 ` 338` hoelzl@51642 ` 339` ```lemma FDERIV_inverse': ``` hoelzl@51642 ` 340` ``` fixes x :: "'a::real_normed_div_algebra" ``` hoelzl@51642 ` 341` ``` assumes x: "x \ 0" ``` hoelzl@51642 ` 342` ``` shows "FDERIV inverse x : s :> (\h. - (inverse x * h * inverse x))" ``` hoelzl@51642 ` 343` ``` (is "FDERIV ?inv x : s :> ?f") ``` hoelzl@51642 ` 344` ```proof (rule FDERIV_I_sandwich) ``` hoelzl@51642 ` 345` ``` show "bounded_linear (\h. - (?inv x * h * ?inv x))" ``` hoelzl@51642 ` 346` ``` apply (rule bounded_linear_minus) ``` hoelzl@51642 ` 347` ``` apply (rule bounded_linear_mult_const) ``` hoelzl@51642 ` 348` ``` apply (rule bounded_linear_const_mult) ``` hoelzl@51642 ` 349` ``` apply (rule bounded_linear_ident) ``` hoelzl@51642 ` 350` ``` done ``` hoelzl@51642 ` 351` ```next ``` hoelzl@51642 ` 352` ``` show "0 < norm x" using x by simp ``` hoelzl@51642 ` 353` ```next ``` hoelzl@51642 ` 354` ``` show "((\y. norm (?inv y - ?inv x) * norm (?inv x)) ---> 0) (at x within s)" ``` hoelzl@51642 ` 355` ``` apply (rule tendsto_mult_left_zero) ``` hoelzl@51642 ` 356` ``` apply (rule tendsto_norm_zero) ``` hoelzl@51642 ` 357` ``` apply (rule LIM_zero) ``` hoelzl@51642 ` 358` ``` apply (rule tendsto_inverse) ``` hoelzl@51642 ` 359` ``` apply (rule tendsto_ident_at) ``` hoelzl@51642 ` 360` ``` apply (rule x) ``` hoelzl@51642 ` 361` ``` done ``` hoelzl@51642 ` 362` ```next ``` hoelzl@51642 ` 363` ``` fix y::'a assume h: "y \ x" "dist y x < norm x" ``` hoelzl@51642 ` 364` ``` then have "y \ 0" ``` hoelzl@51642 ` 365` ``` by (auto simp: norm_conv_dist dist_commute) ``` hoelzl@51642 ` 366` ``` have "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) = norm ((?inv y - ?inv x) * (y - x) * ?inv x) / norm (y - x)" ``` hoelzl@51642 ` 367` ``` apply (subst inverse_diff_inverse [OF `y \ 0` x]) ``` hoelzl@51642 ` 368` ``` apply (subst minus_diff_minus) ``` hoelzl@51642 ` 369` ``` apply (subst norm_minus_cancel) ``` hoelzl@51642 ` 370` ``` apply (simp add: left_diff_distrib) ``` hoelzl@51642 ` 371` ``` done ``` hoelzl@51642 ` 372` ``` also have "\ \ norm (?inv y - ?inv x) * norm (y - x) * norm (?inv x) / norm (y - x)" ``` hoelzl@51642 ` 373` ``` apply (rule divide_right_mono [OF _ norm_ge_zero]) ``` hoelzl@51642 ` 374` ``` apply (rule order_trans [OF norm_mult_ineq]) ``` hoelzl@51642 ` 375` ``` apply (rule mult_right_mono [OF _ norm_ge_zero]) ``` hoelzl@51642 ` 376` ``` apply (rule norm_mult_ineq) ``` hoelzl@51642 ` 377` ``` done ``` hoelzl@51642 ` 378` ``` also have "\ = norm (?inv y - ?inv x) * norm (?inv x)" ``` hoelzl@51642 ` 379` ``` by simp ``` hoelzl@51642 ` 380` ``` finally show "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) \ ``` hoelzl@51642 ` 381` ``` norm (?inv y - ?inv x) * norm (?inv x)" . ``` hoelzl@51642 ` 382` ```qed ``` hoelzl@51642 ` 383` hoelzl@51642 ` 384` ```lemma FDERIV_inverse[simp, FDERIV_intros]: ``` hoelzl@51642 ` 385` ``` fixes f :: "_ \ 'a::real_normed_div_algebra" ``` hoelzl@51642 ` 386` ``` assumes x: "f x \ 0" and f: "FDERIV f x : s :> f'" ``` hoelzl@51642 ` 387` ``` shows "FDERIV (\x. inverse (f x)) x : s :> (\h. - (inverse (f x) * f' h * inverse (f x)))" ``` hoelzl@51642 ` 388` ``` using FDERIV_compose[OF f FDERIV_inverse', OF x] . ``` hoelzl@51642 ` 389` hoelzl@51642 ` 390` ```lemma FDERIV_divide[simp, FDERIV_intros]: ``` hoelzl@51642 ` 391` ``` fixes f :: "_ \ 'a::real_normed_div_algebra" ``` hoelzl@51642 ` 392` ``` assumes g: "FDERIV g x : s :> g'" ``` hoelzl@51642 ` 393` ``` assumes x: "f x \ 0" and f: "FDERIV f x : s :> f'" ``` hoelzl@51642 ` 394` ``` shows "FDERIV (\x. g x / f x) x : s :> (\h. - g x * (inverse (f x) * f' h * inverse (f x)) + g' h / f x)" ``` hoelzl@51642 ` 395` ``` using FDERIV_mult[OF g FDERIV_inverse[OF x f]] ``` hoelzl@51642 ` 396` ``` by (simp add: divide_inverse) ``` hoelzl@51642 ` 397` hoelzl@51642 ` 398` ```subsection {* Uniqueness *} ``` hoelzl@51642 ` 399` hoelzl@51642 ` 400` ```text {* ``` hoelzl@51642 ` 401` hoelzl@51642 ` 402` ```This can not generally shown for @{const FDERIV}, as we need to approach the point from ``` hoelzl@51642 ` 403` ```all directions. There is a proof in @{text Multivariate_Analysis} for @{text euclidean_space}. ``` hoelzl@51642 ` 404` hoelzl@51642 ` 405` ```*} ``` hoelzl@51642 ` 406` hoelzl@51642 ` 407` ```lemma FDERIV_zero_unique: ``` hoelzl@51642 ` 408` ``` assumes "FDERIV (\x. 0) x :> F" shows "F = (\h. 0)" ``` hoelzl@51642 ` 409` ```proof - ``` hoelzl@51642 ` 410` ``` interpret F: bounded_linear F ``` hoelzl@51642 ` 411` ``` using assms by (rule FDERIV_bounded_linear) ``` hoelzl@51642 ` 412` ``` let ?r = "\h. norm (F h) / norm h" ``` hoelzl@51642 ` 413` ``` have *: "?r -- 0 --> 0" ``` hoelzl@51642 ` 414` ``` using assms unfolding fderiv_def by simp ``` hoelzl@51642 ` 415` ``` show "F = (\h. 0)" ``` hoelzl@51642 ` 416` ``` proof ``` hoelzl@51642 ` 417` ``` fix h show "F h = 0" ``` hoelzl@51642 ` 418` ``` proof (rule ccontr) ``` wenzelm@53374 ` 419` ``` assume **: "F h \ 0" ``` wenzelm@53374 ` 420` ``` then have h: "h \ 0" ``` hoelzl@51642 ` 421` ``` by (clarsimp simp add: F.zero) ``` wenzelm@53374 ` 422` ``` with ** have "0 < ?r h" ``` hoelzl@51642 ` 423` ``` by (simp add: divide_pos_pos) ``` hoelzl@51642 ` 424` ``` from LIM_D [OF * this] obtain s where s: "0 < s" ``` hoelzl@51642 ` 425` ``` and r: "\x. x \ 0 \ norm x < s \ ?r x < ?r h" by auto ``` hoelzl@51642 ` 426` ``` from dense [OF s] obtain t where t: "0 < t \ t < s" .. ``` hoelzl@51642 ` 427` ``` let ?x = "scaleR (t / norm h) h" ``` hoelzl@51642 ` 428` ``` have "?x \ 0" and "norm ?x < s" using t h by simp_all ``` hoelzl@51642 ` 429` ``` hence "?r ?x < ?r h" by (rule r) ``` hoelzl@51642 ` 430` ``` thus "False" using t h by (simp add: F.scaleR) ``` hoelzl@51642 ` 431` ``` qed ``` hoelzl@51642 ` 432` ``` qed ``` hoelzl@51642 ` 433` ```qed ``` hoelzl@51642 ` 434` hoelzl@51642 ` 435` ```lemma FDERIV_unique: ``` hoelzl@51642 ` 436` ``` assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'" ``` hoelzl@51642 ` 437` ```proof - ``` hoelzl@51642 ` 438` ``` have "FDERIV (\x. 0) x :> (\h. F h - F' h)" ``` hoelzl@51642 ` 439` ``` using FDERIV_diff [OF assms] by simp ``` hoelzl@51642 ` 440` ``` hence "(\h. F h - F' h) = (\h. 0)" ``` hoelzl@51642 ` 441` ``` by (rule FDERIV_zero_unique) ``` hoelzl@51642 ` 442` ``` thus "F = F'" ``` hoelzl@51642 ` 443` ``` unfolding fun_eq_iff right_minus_eq . ``` hoelzl@51642 ` 444` ```qed ``` hoelzl@51642 ` 445` hoelzl@51642 ` 446` ```subsection {* Differentiability predicate *} ``` hoelzl@51642 ` 447` hoelzl@51642 ` 448` ```definition isDiff :: "'a filter \ ('a::real_normed_vector \ 'b::real_normed_vector) \ bool" where ``` hoelzl@51642 ` 449` ``` isDiff_def: "isDiff F f \ (\D. (f has_derivative D) F)" ``` hoelzl@51642 ` 450` hoelzl@51642 ` 451` ```abbreviation differentiable_in :: "('a::real_normed_vector \ 'b::real_normed_vector) \ 'a \ 'a set \ bool" ``` hoelzl@51642 ` 452` ``` ("(_) differentiable (_) in (_)" [1000, 1000, 60] 60) where ``` hoelzl@51642 ` 453` ``` "f differentiable x in s \ isDiff (at x within s) f" ``` hoelzl@51642 ` 454` hoelzl@51642 ` 455` ```abbreviation differentiable :: "('a::real_normed_vector \ 'b::real_normed_vector) \ 'a \ bool" ``` hoelzl@51642 ` 456` ``` (infixl "differentiable" 60) where ``` hoelzl@51642 ` 457` ``` "f differentiable x \ f differentiable x in UNIV" ``` hoelzl@51642 ` 458` hoelzl@51642 ` 459` ```lemma differentiable_subset: "f differentiable x in s \ t \ s \ f differentiable x in t" ``` hoelzl@51642 ` 460` ``` unfolding isDiff_def by (blast intro: FDERIV_subset) ``` hoelzl@51642 ` 461` hoelzl@51642 ` 462` ```lemma differentiable_ident [simp]: "isDiff F (\x. x)" ``` hoelzl@51642 ` 463` ``` unfolding isDiff_def by (blast intro: FDERIV_ident) ``` hoelzl@51642 ` 464` hoelzl@51642 ` 465` ```lemma differentiable_const [simp]: "isDiff F (\z. a)" ``` hoelzl@51642 ` 466` ``` unfolding isDiff_def by (blast intro: FDERIV_const) ``` hoelzl@51642 ` 467` hoelzl@51642 ` 468` ```lemma differentiable_in_compose: ``` hoelzl@51642 ` 469` ``` "f differentiable (g x) in (g`s) \ g differentiable x in s \ (\x. f (g x)) differentiable x in s" ``` hoelzl@51642 ` 470` ``` unfolding isDiff_def by (blast intro: FDERIV_in_compose) ``` hoelzl@51642 ` 471` hoelzl@51642 ` 472` ```lemma differentiable_compose: ``` hoelzl@51642 ` 473` ``` "f differentiable (g x) \ g differentiable x in s \ (\x. f (g x)) differentiable x in s" ``` hoelzl@51642 ` 474` ``` by (blast intro: differentiable_in_compose differentiable_subset) ``` hoelzl@51642 ` 475` hoelzl@51642 ` 476` ```lemma differentiable_sum [simp]: ``` hoelzl@51642 ` 477` ``` "isDiff F f \ isDiff F g \ isDiff F (\x. f x + g x)" ``` hoelzl@51642 ` 478` ``` unfolding isDiff_def by (blast intro: FDERIV_add) ``` hoelzl@51642 ` 479` hoelzl@51642 ` 480` ```lemma differentiable_minus [simp]: ``` hoelzl@51642 ` 481` ``` "isDiff F f \ isDiff F (\x. - f x)" ``` hoelzl@51642 ` 482` ``` unfolding isDiff_def by (blast intro: FDERIV_minus) ``` hoelzl@51642 ` 483` hoelzl@51642 ` 484` ```lemma differentiable_diff [simp]: ``` hoelzl@51642 ` 485` ``` "isDiff F f \ isDiff F g \ isDiff F (\x. f x - g x)" ``` hoelzl@51642 ` 486` ``` unfolding isDiff_def by (blast intro: FDERIV_diff) ``` hoelzl@51642 ` 487` hoelzl@51642 ` 488` ```lemma differentiable_mult [simp]: ``` hoelzl@51642 ` 489` ``` fixes f g :: "'a :: real_normed_vector \ 'b :: real_normed_algebra" ``` hoelzl@51642 ` 490` ``` shows "f differentiable x in s \ g differentiable x in s \ (\x. f x * g x) differentiable x in s" ``` hoelzl@51642 ` 491` ``` unfolding isDiff_def by (blast intro: FDERIV_mult) ``` hoelzl@51642 ` 492` hoelzl@51642 ` 493` ```lemma differentiable_inverse [simp]: ``` hoelzl@51642 ` 494` ``` fixes f :: "'a :: real_normed_vector \ 'b :: real_normed_field" ``` hoelzl@51642 ` 495` ``` shows "f differentiable x in s \ f x \ 0 \ (\x. inverse (f x)) differentiable x in s" ``` hoelzl@51642 ` 496` ``` unfolding isDiff_def by (blast intro: FDERIV_inverse) ``` hoelzl@51642 ` 497` hoelzl@51642 ` 498` ```lemma differentiable_divide [simp]: ``` hoelzl@51642 ` 499` ``` fixes f g :: "'a :: real_normed_vector \ 'b :: real_normed_field" ``` hoelzl@51642 ` 500` ``` shows "f differentiable x in s \ g differentiable x in s \ g x \ 0 \ (\x. f x / g x) differentiable x in s" ``` hoelzl@51642 ` 501` ``` unfolding divide_inverse using assms by simp ``` hoelzl@51642 ` 502` hoelzl@51642 ` 503` ```lemma differentiable_power [simp]: ``` hoelzl@51642 ` 504` ``` fixes f g :: "'a :: real_normed_vector \ 'b :: real_normed_field" ``` hoelzl@51642 ` 505` ``` shows "f differentiable x in s \ (\x. f x ^ n) differentiable x in s" ``` hoelzl@51642 ` 506` ``` unfolding isDiff_def by (blast intro: FDERIV_power) ``` hoelzl@51642 ` 507` hoelzl@51642 ` 508` ```lemma differentiable_scaleR [simp]: ``` hoelzl@51642 ` 509` ``` "f differentiable x in s \ g differentiable x in s \ (\x. f x *\<^sub>R g x) differentiable x in s" ``` hoelzl@51642 ` 510` ``` unfolding isDiff_def by (blast intro: FDERIV_scaleR) ``` hoelzl@51642 ` 511` hoelzl@51642 ` 512` ```definition ``` hoelzl@51642 ` 513` ``` -- {*Differentiation: D is derivative of function f at x*} ``` hoelzl@51642 ` 514` ``` deriv :: ``` hoelzl@51642 ` 515` ``` "('a::real_normed_field \ 'a) \ 'a \ 'a set \ 'a \ bool" ``` hoelzl@51642 ` 516` ``` ("(DERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60) ``` hoelzl@51642 ` 517` ```where ``` hoelzl@51642 ` 518` ``` deriv_fderiv: "DERIV f x : s :> D = FDERIV f x : s :> (\x. x * D)" ``` hoelzl@51642 ` 519` hoelzl@51642 ` 520` ```abbreviation ``` hoelzl@51642 ` 521` ``` -- {*Differentiation: D is derivative of function f at x*} ``` hoelzl@51642 ` 522` ``` deriv_at :: ``` hoelzl@51642 ` 523` ``` "('a::real_normed_field \ 'a) \ 'a \ 'a \ bool" ``` hoelzl@51642 ` 524` ``` ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) ``` hoelzl@51642 ` 525` ```where ``` hoelzl@51642 ` 526` ``` "DERIV f x :> D \ DERIV f x : UNIV :> D" ``` hoelzl@51642 ` 527` hoelzl@51642 ` 528` ```lemma differentiable_def: "(f::real \ real) differentiable x in s \ (\D. DERIV f x : s :> D)" ``` hoelzl@51642 ` 529` ```proof safe ``` hoelzl@51642 ` 530` ``` assume "f differentiable x in s" ``` wenzelm@53374 ` 531` ``` then obtain f' where *: "FDERIV f x : s :> f'" ``` hoelzl@51642 ` 532` ``` unfolding isDiff_def by auto ``` wenzelm@53374 ` 533` ``` then obtain c where "f' = (\x. x * c)" ``` hoelzl@51642 ` 534` ``` by (metis real_bounded_linear FDERIV_bounded_linear) ``` wenzelm@53374 ` 535` ``` with * show "\D. DERIV f x : s :> D" ``` hoelzl@51642 ` 536` ``` unfolding deriv_fderiv by auto ``` hoelzl@51642 ` 537` ```qed (auto simp: isDiff_def deriv_fderiv) ``` hoelzl@51642 ` 538` hoelzl@51642 ` 539` ```lemma differentiableE [elim?]: ``` hoelzl@51642 ` 540` ``` fixes f :: "real \ real" ``` hoelzl@51642 ` 541` ``` assumes f: "f differentiable x in s" obtains df where "DERIV f x : s :> df" ``` hoelzl@51642 ` 542` ``` using assms by (auto simp: differentiable_def) ``` hoelzl@51642 ` 543` hoelzl@51642 ` 544` ```lemma differentiableD: "(f::real \ real) differentiable x in s \ \D. DERIV f x : s :> D" ``` hoelzl@51642 ` 545` ``` by (auto elim: differentiableE) ``` hoelzl@51642 ` 546` hoelzl@51642 ` 547` ```lemma differentiableI: "DERIV f x : s :> D \ (f::real \ real) differentiable x in s" ``` hoelzl@51642 ` 548` ``` by (force simp add: differentiable_def) ``` hoelzl@51642 ` 549` hoelzl@51642 ` 550` ```lemma DERIV_I_FDERIV: "FDERIV f x : s :> F \ (\x. x * F' = F x) \ DERIV f x : s :> F'" ``` hoelzl@51642 ` 551` ``` by (simp add: deriv_fderiv) ``` hoelzl@51642 ` 552` hoelzl@51642 ` 553` ```lemma DERIV_D_FDERIV: "DERIV f x : s :> F \ FDERIV f x : s :> (\x. x * F)" ``` hoelzl@51642 ` 554` ``` by (simp add: deriv_fderiv) ``` hoelzl@51642 ` 555` hoelzl@51642 ` 556` ```lemma deriv_def: ``` hoelzl@51642 ` 557` ``` "DERIV f x :> D \ (\h. (f (x + h) - f x) / h) -- 0 --> D" ``` hoelzl@51642 ` 558` ``` apply (simp add: deriv_fderiv fderiv_def bounded_linear_mult_left LIM_zero_iff[symmetric, of _ D]) ``` hoelzl@51642 ` 559` ``` apply (subst (2) tendsto_norm_zero_iff[symmetric]) ``` hoelzl@51642 ` 560` ``` apply (rule filterlim_cong) ``` hoelzl@51642 ` 561` ``` apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide) ``` hoelzl@51642 ` 562` ``` done ``` huffman@21164 ` 563` huffman@21164 ` 564` ```subsection {* Derivatives *} ``` huffman@21164 ` 565` hoelzl@51642 ` 566` ```lemma DERIV_iff: "(DERIV f x :> D) \ (\h. (f (x + h) - f x) / h) -- 0 --> D" ``` hoelzl@51642 ` 567` ``` by (simp add: deriv_def) ``` huffman@21164 ` 568` hoelzl@51642 ` 569` ```lemma DERIV_D: "DERIV f x :> D \ (\h. (f (x + h) - f x) / h) -- 0 --> D" ``` hoelzl@51642 ` 570` ``` by (simp add: deriv_def) ``` huffman@21164 ` 571` hoelzl@51642 ` 572` ```lemma DERIV_const [simp]: "DERIV (\x. k) x : s :> 0" ``` hoelzl@51642 ` 573` ``` by (rule DERIV_I_FDERIV[OF FDERIV_const]) auto ``` huffman@21164 ` 574` hoelzl@51642 ` 575` ```lemma DERIV_ident [simp]: "DERIV (\x. x) x : s :> 1" ``` hoelzl@51642 ` 576` ``` by (rule DERIV_I_FDERIV[OF FDERIV_ident]) auto ``` huffman@21164 ` 577` hoelzl@51642 ` 578` ```lemma DERIV_add: "DERIV f x : s :> D \ DERIV g x : s :> E \ DERIV (\x. f x + g x) x : s :> D + E" ``` hoelzl@51642 ` 579` ``` by (rule DERIV_I_FDERIV[OF FDERIV_add]) (auto simp: field_simps dest: DERIV_D_FDERIV) ``` huffman@21164 ` 580` hoelzl@51642 ` 581` ```lemma DERIV_minus: "DERIV f x : s :> D \ DERIV (\x. - f x) x : s :> - D" ``` hoelzl@51642 ` 582` ``` by (rule DERIV_I_FDERIV[OF FDERIV_minus]) (auto simp: field_simps dest: DERIV_D_FDERIV) ``` huffman@21164 ` 583` hoelzl@51642 ` 584` ```lemma DERIV_diff: "DERIV f x : s :> D \ DERIV g x : s :> E \ DERIV (\x. f x - g x) x : s :> D - E" ``` hoelzl@51642 ` 585` ``` by (rule DERIV_I_FDERIV[OF FDERIV_diff]) (auto simp: field_simps dest: DERIV_D_FDERIV) ``` huffman@21164 ` 586` hoelzl@51642 ` 587` ```lemma DERIV_add_minus: "DERIV f x : s :> D \ DERIV g x : s :> E \ DERIV (\x. f x + - g x) x : s :> D + - E" ``` hoelzl@51642 ` 588` ``` by (simp only: DERIV_add DERIV_minus) ``` hoelzl@51642 ` 589` hoelzl@51642 ` 590` ```lemma DERIV_continuous: "DERIV f x : s :> D \ continuous (at x within s) f" ``` hoelzl@51642 ` 591` ``` by (drule FDERIV_continuous[OF DERIV_D_FDERIV]) simp ``` huffman@21164 ` 592` huffman@21164 ` 593` ```lemma DERIV_isCont: "DERIV f x :> D \ isCont f x" ``` hoelzl@51642 ` 594` ``` by (auto dest!: DERIV_continuous) ``` hoelzl@51642 ` 595` hoelzl@51642 ` 596` ```lemma DERIV_mult': "DERIV f x : s :> D \ DERIV g x : s :> E \ DERIV (\x. f x * g x) x : s :> f x * E + D * g x" ``` hoelzl@51642 ` 597` ``` by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV) ``` huffman@21164 ` 598` hoelzl@51642 ` 599` ```lemma DERIV_mult: "DERIV f x : s :> Da \ DERIV g x : s :> Db \ DERIV (\x. f x * g x) x : s :> Da * g x + Db * f x" ``` hoelzl@51642 ` 600` ``` by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV) ``` hoelzl@51642 ` 601` hoelzl@51642 ` 602` ```text {* Derivative of linear multiplication *} ``` huffman@21164 ` 603` hoelzl@51642 ` 604` ```lemma DERIV_cmult: ``` hoelzl@51642 ` 605` ``` "DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D" ``` hoelzl@51642 ` 606` ``` by (drule DERIV_mult' [OF DERIV_const], simp) ``` huffman@21164 ` 607` hoelzl@51642 ` 608` ```lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c" ``` hoelzl@51642 ` 609` ``` by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp) ``` hoelzl@51642 ` 610` hoelzl@51642 ` 611` ```lemma DERIV_cdivide: "DERIV f x : s :> D ==> DERIV (%x. f x / c) x : s :> D / c" ``` hoelzl@51642 ` 612` ``` apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x : s :> (1 / c) * D", force) ``` hoelzl@51642 ` 613` ``` apply (erule DERIV_cmult) ``` hoelzl@51642 ` 614` ``` done ``` huffman@21164 ` 615` huffman@21164 ` 616` ```lemma DERIV_unique: ``` hoelzl@51642 ` 617` ``` "DERIV f x :> D \ DERIV f x :> E \ D = E" ``` hoelzl@50331 ` 618` ``` unfolding deriv_def by (rule LIM_unique) ``` huffman@21164 ` 619` hoelzl@51642 ` 620` ```lemma DERIV_setsum': ``` hoelzl@51642 ` 621` ``` "(\ n. n \ S \ DERIV (%x. f x n) x : s :> (f' x n)) \ DERIV (\x. setsum (f x) S) x : s :> setsum (f' x) S" ``` hoelzl@51642 ` 622` ``` by (rule DERIV_I_FDERIV[OF FDERIV_setsum]) (auto simp: setsum_right_distrib dest: DERIV_D_FDERIV) ``` huffman@21164 ` 623` hoelzl@31880 ` 624` ```lemma DERIV_setsum: ``` hoelzl@51642 ` 625` ``` "finite S \ (\ n. n \ S \ DERIV (%x. f x n) x : s :> (f' x n)) \ DERIV (\x. setsum (f x) S) x : s :> setsum (f' x) S" ``` hoelzl@51642 ` 626` ``` by (rule DERIV_setsum') ``` hoelzl@51642 ` 627` hoelzl@51642 ` 628` ```lemma DERIV_sumr [rule_format (no_asm)]: (* REMOVE *) ``` hoelzl@51642 ` 629` ``` "(\r. m \ r & r < (m + n) --> DERIV (%x. f r x) x : s :> (f' r x)) ``` hoelzl@51642 ` 630` ``` --> DERIV (%x. \n=m.. (\r=m.. D \ f x \ 0 \ DERIV (\x. inverse (f x)) x : s :> - (inverse (f x) * D * inverse (f x))" ``` hoelzl@51642 ` 635` ``` by (rule DERIV_I_FDERIV[OF FDERIV_inverse]) (auto dest: DERIV_D_FDERIV) ``` hoelzl@51642 ` 636` hoelzl@51642 ` 637` ```text {* Power of @{text "-1"} *} ``` hoelzl@51642 ` 638` hoelzl@51642 ` 639` ```lemma DERIV_inverse: ``` hoelzl@51642 ` 640` ``` "x \ 0 \ DERIV (\x. inverse(x)) x : s :> - (inverse x ^ Suc (Suc 0))" ``` hoelzl@51642 ` 641` ``` by (drule DERIV_inverse' [OF DERIV_ident]) simp ``` hoelzl@51642 ` 642` hoelzl@51642 ` 643` ```text {* Derivative of inverse *} ``` hoelzl@51642 ` 644` hoelzl@51642 ` 645` ```lemma DERIV_inverse_fun: ``` hoelzl@51642 ` 646` ``` "DERIV f x : s :> d \ f x \ 0 \ DERIV (\x. inverse (f x)) x : s :> (- (d * inverse(f x ^ Suc (Suc 0))))" ``` hoelzl@51642 ` 647` ``` by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib) ``` hoelzl@51642 ` 648` hoelzl@51642 ` 649` ```text {* Derivative of quotient *} ``` hoelzl@51642 ` 650` hoelzl@51642 ` 651` ```lemma DERIV_divide: ``` hoelzl@51642 ` 652` ``` "DERIV f x : s :> D \ DERIV g x : s :> E \ g x \ 0 \ DERIV (\x. f x / g x) x : s :> (D * g x - f x * E) / (g x * g x)" ``` hoelzl@51642 ` 653` ``` by (rule DERIV_I_FDERIV[OF FDERIV_divide]) ``` hoelzl@51642 ` 654` ``` (auto dest: DERIV_D_FDERIV simp: field_simps nonzero_inverse_mult_distrib divide_inverse) ``` hoelzl@51642 ` 655` hoelzl@51642 ` 656` ```lemma DERIV_quotient: ``` hoelzl@51642 ` 657` ``` "DERIV f x : s :> d \ DERIV g x : s :> e \ g x \ 0 \ DERIV (\y. f y / g y) x : s :> (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))" ``` hoelzl@51642 ` 658` ``` by (drule (2) DERIV_divide) (simp add: mult_commute) ``` hoelzl@51642 ` 659` hoelzl@51642 ` 660` ```lemma DERIV_power_Suc: ``` hoelzl@51642 ` 661` ``` "DERIV f x : s :> D \ DERIV (\x. f x ^ Suc n) x : s :> (1 + of_nat n) * (D * f x ^ n)" ``` hoelzl@51642 ` 662` ``` by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv) ``` hoelzl@51642 ` 663` hoelzl@51642 ` 664` ```lemma DERIV_power: ``` hoelzl@51642 ` 665` ``` "DERIV f x : s :> D \ DERIV (\x. f x ^ n) x : s :> of_nat n * (D * f x ^ (n - Suc 0))" ``` hoelzl@51642 ` 666` ``` by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv) ``` hoelzl@31880 ` 667` hoelzl@51642 ` 668` ```lemma DERIV_pow: "DERIV (%x. x ^ n) x : s :> real n * (x ^ (n - Suc 0))" ``` hoelzl@51642 ` 669` ``` apply (cut_tac DERIV_power [OF DERIV_ident]) ``` hoelzl@51642 ` 670` ``` apply (simp add: real_of_nat_def) ``` hoelzl@51642 ` 671` ``` done ``` hoelzl@51642 ` 672` hoelzl@51642 ` 673` ```lemma DERIV_chain': "DERIV f x : s :> D \ DERIV g (f x) :> E \ DERIV (\x. g (f x)) x : s :> E * D" ``` hoelzl@51642 ` 674` ``` using FDERIV_compose[of f "\x. x * D" x s g "\x. x * E"] ``` hoelzl@51642 ` 675` ``` by (auto simp: deriv_fderiv ac_simps dest: FDERIV_subset) ``` hoelzl@51642 ` 676` hoelzl@51642 ` 677` ```text {* Standard version *} ``` hoelzl@51642 ` 678` hoelzl@51642 ` 679` ```lemma DERIV_chain: "DERIV f (g x) :> Da \ DERIV g x : s :> Db \ DERIV (f o g) x : s :> Da * Db" ``` hoelzl@51642 ` 680` ``` by (drule (1) DERIV_chain', simp add: o_def mult_commute) ``` hoelzl@51642 ` 681` hoelzl@51642 ` 682` ```lemma DERIV_chain2: "DERIV f (g x) :> Da \ DERIV g x : s :> Db \ DERIV (%x. f (g x)) x : s :> Da * Db" ``` hoelzl@51642 ` 683` ``` by (auto dest: DERIV_chain simp add: o_def) ``` hoelzl@51642 ` 684` hoelzl@51642 ` 685` ```subsubsection {* @{text "DERIV_intros"} *} ``` hoelzl@51642 ` 686` hoelzl@51642 ` 687` ```ML {* ``` hoelzl@51642 ` 688` ```structure Deriv_Intros = Named_Thms ``` hoelzl@51642 ` 689` ```( ``` hoelzl@51642 ` 690` ``` val name = @{binding DERIV_intros} ``` hoelzl@51642 ` 691` ``` val description = "DERIV introduction rules" ``` hoelzl@51642 ` 692` ```) ``` hoelzl@51642 ` 693` ```*} ``` hoelzl@51642 ` 694` hoelzl@51642 ` 695` ```setup Deriv_Intros.setup ``` hoelzl@51642 ` 696` hoelzl@51642 ` 697` ```lemma DERIV_cong: "DERIV f x : s :> X \ X = Y \ DERIV f x : s :> Y" ``` hoelzl@51642 ` 698` ``` by simp ``` hoelzl@51642 ` 699` hoelzl@51642 ` 700` ```declare ``` hoelzl@51642 ` 701` ``` DERIV_const[THEN DERIV_cong, DERIV_intros] ``` hoelzl@51642 ` 702` ``` DERIV_ident[THEN DERIV_cong, DERIV_intros] ``` hoelzl@51642 ` 703` ``` DERIV_add[THEN DERIV_cong, DERIV_intros] ``` hoelzl@51642 ` 704` ``` DERIV_minus[THEN DERIV_cong, DERIV_intros] ``` hoelzl@51642 ` 705` ``` DERIV_mult[THEN DERIV_cong, DERIV_intros] ``` hoelzl@51642 ` 706` ``` DERIV_diff[THEN DERIV_cong, DERIV_intros] ``` hoelzl@51642 ` 707` ``` DERIV_inverse'[THEN DERIV_cong, DERIV_intros] ``` hoelzl@51642 ` 708` ``` DERIV_divide[THEN DERIV_cong, DERIV_intros] ``` hoelzl@51642 ` 709` ``` DERIV_power[where 'a=real, THEN DERIV_cong, ``` hoelzl@51642 ` 710` ``` unfolded real_of_nat_def[symmetric], DERIV_intros] ``` hoelzl@51642 ` 711` ``` DERIV_setsum[THEN DERIV_cong, DERIV_intros] ``` huffman@21164 ` 712` huffman@21164 ` 713` ```text{*Alternative definition for differentiability*} ``` huffman@21164 ` 714` huffman@21164 ` 715` ```lemma DERIV_LIM_iff: ``` huffman@31338 ` 716` ``` fixes f :: "'a::{real_normed_vector,inverse} \ 'a" shows ``` huffman@21784 ` 717` ``` "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) = ``` huffman@21164 ` 718` ``` ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)" ``` huffman@21164 ` 719` ```apply (rule iffI) ``` huffman@21164 ` 720` ```apply (drule_tac k="- a" in LIM_offset) ``` huffman@21164 ` 721` ```apply (simp add: diff_minus) ``` huffman@21164 ` 722` ```apply (drule_tac k="a" in LIM_offset) ``` huffman@21164 ` 723` ```apply (simp add: add_commute) ``` huffman@21164 ` 724` ```done ``` huffman@21164 ` 725` hoelzl@51642 ` 726` ```lemma DERIV_iff2: "(DERIV f x :> D) \ (\z. (f z - f x) / (z - x)) --x --> D" ``` hoelzl@51642 ` 727` ``` by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff) ``` huffman@21164 ` 728` hoelzl@51642 ` 729` ```lemma DERIV_cong_ev: "x = y \ eventually (\x. f x = g x) (nhds x) \ u = v \ ``` hoelzl@51642 ` 730` ``` DERIV f x :> u \ DERIV g y :> v" ``` hoelzl@51642 ` 731` ``` unfolding DERIV_iff2 ``` hoelzl@51642 ` 732` ```proof (rule filterlim_cong) ``` wenzelm@53374 ` 733` ``` assume *: "eventually (\x. f x = g x) (nhds x)" ``` wenzelm@53374 ` 734` ``` moreover from * have "f x = g x" by (auto simp: eventually_nhds) ``` hoelzl@51642 ` 735` ``` moreover assume "x = y" "u = v" ``` hoelzl@51642 ` 736` ``` ultimately show "eventually (\xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)" ``` hoelzl@51642 ` 737` ``` by (auto simp: eventually_at_filter elim: eventually_elim1) ``` hoelzl@51642 ` 738` ```qed simp_all ``` huffman@21164 ` 739` hoelzl@51642 ` 740` ```lemma DERIV_shift: ``` hoelzl@51642 ` 741` ``` "(DERIV f (x + z) :> y) \ (DERIV (\x. f (x + z)) x :> y)" ``` hoelzl@51642 ` 742` ``` by (simp add: DERIV_iff field_simps) ``` huffman@21164 ` 743` hoelzl@51642 ` 744` ```lemma DERIV_mirror: ``` hoelzl@51642 ` 745` ``` "(DERIV f (- x) :> y) \ (DERIV (\x. f (- x::real) :: real) x :> - y)" ``` hoelzl@51642 ` 746` ``` by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right ``` hoelzl@51642 ` 747` ``` tendsto_minus_cancel_left field_simps conj_commute) ``` huffman@21164 ` 748` huffman@29975 ` 749` ```text {* Caratheodory formulation of derivative at a point *} ``` huffman@21164 ` 750` huffman@21164 ` 751` ```lemma CARAT_DERIV: ``` hoelzl@51642 ` 752` ``` "(DERIV f x :> l) \ (\g. (\z. f z - f x = g z * (z - x)) \ isCont g x \ g x = l)" ``` huffman@21164 ` 753` ``` (is "?lhs = ?rhs") ``` huffman@21164 ` 754` ```proof ``` huffman@21164 ` 755` ``` assume der: "DERIV f x :> l" ``` huffman@21784 ` 756` ``` show "\g. (\z. f z - f x = g z * (z-x)) \ isCont g x \ g x = l" ``` huffman@21164 ` 757` ``` proof (intro exI conjI) ``` huffman@21784 ` 758` ``` let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))" ``` nipkow@23413 ` 759` ``` show "\z. f z - f x = ?g z * (z-x)" by simp ``` huffman@21164 ` 760` ``` show "isCont ?g x" using der ``` huffman@21164 ` 761` ``` by (simp add: isCont_iff DERIV_iff diff_minus ``` huffman@21164 ` 762` ``` cong: LIM_equal [rule_format]) ``` huffman@21164 ` 763` ``` show "?g x = l" by simp ``` huffman@21164 ` 764` ``` qed ``` huffman@21164 ` 765` ```next ``` huffman@21164 ` 766` ``` assume "?rhs" ``` huffman@21164 ` 767` ``` then obtain g where ``` huffman@21784 ` 768` ``` "(\z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast ``` huffman@21164 ` 769` ``` thus "(DERIV f x :> l)" ``` nipkow@23413 ` 770` ``` by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong) ``` huffman@21164 ` 771` ```qed ``` huffman@21164 ` 772` wenzelm@31899 ` 773` ```text {* ``` wenzelm@31899 ` 774` ``` Let's do the standard proof, though theorem ``` wenzelm@31899 ` 775` ``` @{text "LIM_mult2"} follows from a NS proof ``` wenzelm@31899 ` 776` ```*} ``` huffman@21164 ` 777` huffman@29975 ` 778` ```subsection {* Local extrema *} ``` huffman@29975 ` 779` huffman@21164 ` 780` ```text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*} ``` huffman@21164 ` 781` paulson@33654 ` 782` ```lemma DERIV_pos_inc_right: ``` huffman@21164 ` 783` ``` fixes f :: "real => real" ``` huffman@21164 ` 784` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 785` ``` and l: "0 < l" ``` huffman@21164 ` 786` ``` shows "\d > 0. \h > 0. h < d --> f(x) < f(x + h)" ``` huffman@21164 ` 787` ```proof - ``` huffman@21164 ` 788` ``` from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]] ``` huffman@21164 ` 789` ``` have "\s > 0. (\z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < l)" ``` huffman@21164 ` 790` ``` by (simp add: diff_minus) ``` huffman@21164 ` 791` ``` then obtain s ``` huffman@21164 ` 792` ``` where s: "0 < s" ``` huffman@21164 ` 793` ``` and all: "!!z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < l" ``` huffman@21164 ` 794` ``` by auto ``` huffman@21164 ` 795` ``` thus ?thesis ``` huffman@21164 ` 796` ``` proof (intro exI conjI strip) ``` huffman@23441 ` 797` ``` show "0 real" ``` huffman@21164 ` 814` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 815` ``` and l: "l < 0" ``` huffman@21164 ` 816` ``` shows "\d > 0. \h > 0. h < d --> f(x) < f(x-h)" ``` huffman@21164 ` 817` ```proof - ``` huffman@21164 ` 818` ``` from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]] ``` huffman@21164 ` 819` ``` have "\s > 0. (\z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < -l)" ``` huffman@21164 ` 820` ``` by (simp add: diff_minus) ``` huffman@21164 ` 821` ``` then obtain s ``` huffman@21164 ` 822` ``` where s: "0 < s" ``` huffman@21164 ` 823` ``` and all: "!!z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < -l" ``` huffman@21164 ` 824` ``` by auto ``` huffman@21164 ` 825` ``` thus ?thesis ``` huffman@21164 ` 826` ``` proof (intro exI conjI strip) ``` huffman@23441 ` 827` ``` show "0 real" ``` paulson@33654 ` 844` ``` shows "DERIV f x :> l \ 0 < l \ \d > 0. \h > 0. h < d --> f(x - h) < f(x)" ``` paulson@33654 ` 845` ``` apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified]) ``` hoelzl@41368 ` 846` ``` apply (auto simp add: DERIV_minus) ``` paulson@33654 ` 847` ``` done ``` paulson@33654 ` 848` paulson@33654 ` 849` ```lemma DERIV_neg_dec_right: ``` paulson@33654 ` 850` ``` fixes f :: "real => real" ``` paulson@33654 ` 851` ``` shows "DERIV f x :> l \ l < 0 \ \d > 0. \h > 0. h < d --> f(x) > f(x + h)" ``` paulson@33654 ` 852` ``` apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified]) ``` hoelzl@41368 ` 853` ``` apply (auto simp add: DERIV_minus) ``` paulson@33654 ` 854` ``` done ``` paulson@33654 ` 855` huffman@21164 ` 856` ```lemma DERIV_local_max: ``` huffman@21164 ` 857` ``` fixes f :: "real => real" ``` huffman@21164 ` 858` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 859` ``` and d: "0 < d" ``` huffman@21164 ` 860` ``` and le: "\y. \x-y\ < d --> f(y) \ f(x)" ``` huffman@21164 ` 861` ``` shows "l = 0" ``` huffman@21164 ` 862` ```proof (cases rule: linorder_cases [of l 0]) ``` huffman@23441 ` 863` ``` case equal thus ?thesis . ``` huffman@21164 ` 864` ```next ``` huffman@21164 ` 865` ``` case less ``` paulson@33654 ` 866` ``` from DERIV_neg_dec_left [OF der less] ``` huffman@21164 ` 867` ``` obtain d' where d': "0 < d'" ``` huffman@21164 ` 868` ``` and lt: "\h > 0. h < d' \ f x < f (x-h)" by blast ``` huffman@21164 ` 869` ``` from real_lbound_gt_zero [OF d d'] ``` huffman@21164 ` 870` ``` obtain e where "0 < e \ e < d \ e < d'" .. ``` huffman@21164 ` 871` ``` with lt le [THEN spec [where x="x-e"]] ``` huffman@21164 ` 872` ``` show ?thesis by (auto simp add: abs_if) ``` huffman@21164 ` 873` ```next ``` huffman@21164 ` 874` ``` case greater ``` paulson@33654 ` 875` ``` from DERIV_pos_inc_right [OF der greater] ``` huffman@21164 ` 876` ``` obtain d' where d': "0 < d'" ``` huffman@21164 ` 877` ``` and lt: "\h > 0. h < d' \ f x < f (x + h)" by blast ``` huffman@21164 ` 878` ``` from real_lbound_gt_zero [OF d d'] ``` huffman@21164 ` 879` ``` obtain e where "0 < e \ e < d \ e < d'" .. ``` huffman@21164 ` 880` ``` with lt le [THEN spec [where x="x+e"]] ``` huffman@21164 ` 881` ``` show ?thesis by (auto simp add: abs_if) ``` huffman@21164 ` 882` ```qed ``` huffman@21164 ` 883` huffman@21164 ` 884` huffman@21164 ` 885` ```text{*Similar theorem for a local minimum*} ``` huffman@21164 ` 886` ```lemma DERIV_local_min: ``` huffman@21164 ` 887` ``` fixes f :: "real => real" ``` huffman@21164 ` 888` ``` shows "[| DERIV f x :> l; 0 < d; \y. \x-y\ < d --> f(x) \ f(y) |] ==> l = 0" ``` huffman@21164 ` 889` ```by (drule DERIV_minus [THEN DERIV_local_max], auto) ``` huffman@21164 ` 890` huffman@21164 ` 891` huffman@21164 ` 892` ```text{*In particular, if a function is locally flat*} ``` huffman@21164 ` 893` ```lemma DERIV_local_const: ``` huffman@21164 ` 894` ``` fixes f :: "real => real" ``` huffman@21164 ` 895` ``` shows "[| DERIV f x :> l; 0 < d; \y. \x-y\ < d --> f(x) = f(y) |] ==> l = 0" ``` huffman@21164 ` 896` ```by (auto dest!: DERIV_local_max) ``` huffman@21164 ` 897` huffman@29975 ` 898` huffman@29975 ` 899` ```subsection {* Rolle's Theorem *} ``` huffman@29975 ` 900` huffman@21164 ` 901` ```text{*Lemma about introducing open ball in open interval*} ``` huffman@21164 ` 902` ```lemma lemma_interval_lt: ``` huffman@21164 ` 903` ``` "[| a < x; x < b |] ``` huffman@21164 ` 904` ``` ==> \d::real. 0 < d & (\y. \x-y\ < d --> a < y & y < b)" ``` chaieb@27668 ` 905` huffman@22998 ` 906` ```apply (simp add: abs_less_iff) ``` huffman@21164 ` 907` ```apply (insert linorder_linear [of "x-a" "b-x"], safe) ``` huffman@21164 ` 908` ```apply (rule_tac x = "x-a" in exI) ``` huffman@21164 ` 909` ```apply (rule_tac [2] x = "b-x" in exI, auto) ``` huffman@21164 ` 910` ```done ``` huffman@21164 ` 911` huffman@21164 ` 912` ```lemma lemma_interval: "[| a < x; x < b |] ==> ``` huffman@21164 ` 913` ``` \d::real. 0 < d & (\y. \x-y\ < d --> a \ y & y \ b)" ``` huffman@21164 ` 914` ```apply (drule lemma_interval_lt, auto) ``` huffman@44921 ` 915` ```apply force ``` huffman@21164 ` 916` ```done ``` huffman@21164 ` 917` huffman@21164 ` 918` ```text{*Rolle's Theorem. ``` huffman@21164 ` 919` ``` If @{term f} is defined and continuous on the closed interval ``` huffman@21164 ` 920` ``` @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"}, ``` huffman@21164 ` 921` ``` and @{term "f(a) = f(b)"}, ``` huffman@21164 ` 922` ``` then there exists @{text "x0 \ (a,b)"} such that @{term "f'(x0) = 0"}*} ``` huffman@21164 ` 923` ```theorem Rolle: ``` huffman@21164 ` 924` ``` assumes lt: "a < b" ``` huffman@21164 ` 925` ``` and eq: "f(a) = f(b)" ``` huffman@21164 ` 926` ``` and con: "\x. a \ x & x \ b --> isCont f x" ``` huffman@21164 ` 927` ``` and dif [rule_format]: "\x. a < x & x < b --> f differentiable x" ``` huffman@21784 ` 928` ``` shows "\z::real. a < z & z < b & DERIV f z :> 0" ``` huffman@21164 ` 929` ```proof - ``` huffman@21164 ` 930` ``` have le: "a \ b" using lt by simp ``` huffman@21164 ` 931` ``` from isCont_eq_Ub [OF le con] ``` huffman@21164 ` 932` ``` obtain x where x_max: "\z. a \ z \ z \ b \ f z \ f x" ``` huffman@21164 ` 933` ``` and alex: "a \ x" and xleb: "x \ b" ``` huffman@21164 ` 934` ``` by blast ``` huffman@21164 ` 935` ``` from isCont_eq_Lb [OF le con] ``` huffman@21164 ` 936` ``` obtain x' where x'_min: "\z. a \ z \ z \ b \ f x' \ f z" ``` huffman@21164 ` 937` ``` and alex': "a \ x'" and x'leb: "x' \ b" ``` huffman@21164 ` 938` ``` by blast ``` huffman@21164 ` 939` ``` show ?thesis ``` huffman@21164 ` 940` ``` proof cases ``` huffman@21164 ` 941` ``` assume axb: "a < x & x < b" ``` huffman@21164 ` 942` ``` --{*@{term f} attains its maximum within the interval*} ``` chaieb@27668 ` 943` ``` hence ax: "ay. \x-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 946` ``` by blast ``` huffman@21164 ` 947` ``` hence bound': "\y. \x-y\ < d \ f y \ f x" using x_max ``` huffman@21164 ` 948` ``` by blast ``` huffman@21164 ` 949` ``` from differentiableD [OF dif [OF axb]] ``` huffman@21164 ` 950` ``` obtain l where der: "DERIV f x :> l" .. ``` huffman@21164 ` 951` ``` have "l=0" by (rule DERIV_local_max [OF der d bound']) ``` huffman@21164 ` 952` ``` --{*the derivative at a local maximum is zero*} ``` huffman@21164 ` 953` ``` thus ?thesis using ax xb der by auto ``` huffman@21164 ` 954` ``` next ``` huffman@21164 ` 955` ``` assume notaxb: "~ (a < x & x < b)" ``` huffman@21164 ` 956` ``` hence xeqab: "x=a | x=b" using alex xleb by arith ``` huffman@21164 ` 957` ``` hence fb_eq_fx: "f b = f x" by (auto simp add: eq) ``` huffman@21164 ` 958` ``` show ?thesis ``` huffman@21164 ` 959` ``` proof cases ``` huffman@21164 ` 960` ``` assume ax'b: "a < x' & x' < b" ``` huffman@21164 ` 961` ``` --{*@{term f} attains its minimum within the interval*} ``` chaieb@27668 ` 962` ``` hence ax': "ay. \x'-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 965` ``` by blast ``` huffman@21164 ` 966` ``` hence bound': "\y. \x'-y\ < d \ f x' \ f y" using x'_min ``` huffman@21164 ` 967` ``` by blast ``` huffman@21164 ` 968` ``` from differentiableD [OF dif [OF ax'b]] ``` huffman@21164 ` 969` ``` obtain l where der: "DERIV f x' :> l" .. ``` huffman@21164 ` 970` ``` have "l=0" by (rule DERIV_local_min [OF der d bound']) ``` huffman@21164 ` 971` ``` --{*the derivative at a local minimum is zero*} ``` huffman@21164 ` 972` ``` thus ?thesis using ax' x'b der by auto ``` huffman@21164 ` 973` ``` next ``` huffman@21164 ` 974` ``` assume notax'b: "~ (a < x' & x' < b)" ``` huffman@21164 ` 975` ``` --{*@{term f} is constant througout the interval*} ``` huffman@21164 ` 976` ``` hence x'eqab: "x'=a | x'=b" using alex' x'leb by arith ``` huffman@21164 ` 977` ``` hence fb_eq_fx': "f b = f x'" by (auto simp add: eq) ``` huffman@21164 ` 978` ``` from dense [OF lt] ``` huffman@21164 ` 979` ``` obtain r where ar: "a < r" and rb: "r < b" by blast ``` huffman@21164 ` 980` ``` from lemma_interval [OF ar rb] ``` huffman@21164 ` 981` ``` obtain d where d: "0y. \r-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 982` ``` by blast ``` huffman@21164 ` 983` ``` have eq_fb: "\z. a \ z --> z \ b --> f z = f b" ``` huffman@21164 ` 984` ``` proof (clarify) ``` huffman@21164 ` 985` ``` fix z::real ``` huffman@21164 ` 986` ``` assume az: "a \ z" and zb: "z \ b" ``` huffman@21164 ` 987` ``` show "f z = f b" ``` huffman@21164 ` 988` ``` proof (rule order_antisym) ``` huffman@21164 ` 989` ``` show "f z \ f b" by (simp add: fb_eq_fx x_max az zb) ``` huffman@21164 ` 990` ``` show "f b \ f z" by (simp add: fb_eq_fx' x'_min az zb) ``` huffman@21164 ` 991` ``` qed ``` huffman@21164 ` 992` ``` qed ``` huffman@21164 ` 993` ``` have bound': "\y. \r-y\ < d \ f r = f y" ``` huffman@21164 ` 994` ``` proof (intro strip) ``` huffman@21164 ` 995` ``` fix y::real ``` huffman@21164 ` 996` ``` assume lt: "\r-y\ < d" ``` huffman@21164 ` 997` ``` hence "f y = f b" by (simp add: eq_fb bound) ``` huffman@21164 ` 998` ``` thus "f r = f y" by (simp add: eq_fb ar rb order_less_imp_le) ``` huffman@21164 ` 999` ``` qed ``` huffman@21164 ` 1000` ``` from differentiableD [OF dif [OF conjI [OF ar rb]]] ``` huffman@21164 ` 1001` ``` obtain l where der: "DERIV f r :> l" .. ``` huffman@21164 ` 1002` ``` have "l=0" by (rule DERIV_local_const [OF der d bound']) ``` huffman@21164 ` 1003` ``` --{*the derivative of a constant function is zero*} ``` huffman@21164 ` 1004` ``` thus ?thesis using ar rb der by auto ``` huffman@21164 ` 1005` ``` qed ``` huffman@21164 ` 1006` ``` qed ``` huffman@21164 ` 1007` ```qed ``` huffman@21164 ` 1008` huffman@21164 ` 1009` huffman@21164 ` 1010` ```subsection{*Mean Value Theorem*} ``` huffman@21164 ` 1011` huffman@21164 ` 1012` ```lemma lemma_MVT: ``` huffman@21164 ` 1013` ``` "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)" ``` hoelzl@51481 ` 1014` ``` by (cases "a = b") (simp_all add: field_simps) ``` huffman@21164 ` 1015` huffman@21164 ` 1016` ```theorem MVT: ``` huffman@21164 ` 1017` ``` assumes lt: "a < b" ``` huffman@21164 ` 1018` ``` and con: "\x. a \ x & x \ b --> isCont f x" ``` huffman@21164 ` 1019` ``` and dif [rule_format]: "\x. a < x & x < b --> f differentiable x" ``` huffman@21784 ` 1020` ``` shows "\l z::real. a < z & z < b & DERIV f z :> l & ``` huffman@21164 ` 1021` ``` (f(b) - f(a) = (b-a) * l)" ``` huffman@21164 ` 1022` ```proof - ``` huffman@21164 ` 1023` ``` let ?F = "%x. f x - ((f b - f a) / (b-a)) * x" ``` huffman@44233 ` 1024` ``` have contF: "\x. a \ x \ x \ b \ isCont ?F x" ``` huffman@44233 ` 1025` ``` using con by (fast intro: isCont_intros) ``` huffman@21164 ` 1026` ``` have difF: "\x. a < x \ x < b \ ?F differentiable x" ``` huffman@21164 ` 1027` ``` proof (clarify) ``` huffman@21164 ` 1028` ``` fix x::real ``` huffman@21164 ` 1029` ``` assume ax: "a < x" and xb: "x < b" ``` huffman@21164 ` 1030` ``` from differentiableD [OF dif [OF conjI [OF ax xb]]] ``` huffman@21164 ` 1031` ``` obtain l where der: "DERIV f x :> l" .. ``` huffman@21164 ` 1032` ``` show "?F differentiable x" ``` huffman@21164 ` 1033` ``` by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"], ``` huffman@21164 ` 1034` ``` blast intro: DERIV_diff DERIV_cmult_Id der) ``` huffman@21164 ` 1035` ``` qed ``` huffman@21164 ` 1036` ``` from Rolle [where f = ?F, OF lt lemma_MVT contF difF] ``` huffman@21164 ` 1037` ``` obtain z where az: "a < z" and zb: "z < b" and der: "DERIV ?F z :> 0" ``` huffman@21164 ` 1038` ``` by blast ``` huffman@21164 ` 1039` ``` have "DERIV (%x. ((f b - f a)/(b-a)) * x) z :> (f b - f a)/(b-a)" ``` huffman@21164 ` 1040` ``` by (rule DERIV_cmult_Id) ``` huffman@21164 ` 1041` ``` hence derF: "DERIV (\x. ?F x + (f b - f a) / (b - a) * x) z ``` huffman@21164 ` 1042` ``` :> 0 + (f b - f a) / (b - a)" ``` huffman@21164 ` 1043` ``` by (rule DERIV_add [OF der]) ``` huffman@21164 ` 1044` ``` show ?thesis ``` huffman@21164 ` 1045` ``` proof (intro exI conjI) ``` huffman@23441 ` 1046` ``` show "a < z" using az . ``` huffman@23441 ` 1047` ``` show "z < b" using zb . ``` huffman@21164 ` 1048` ``` show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp) ``` huffman@21164 ` 1049` ``` show "DERIV f z :> ((f b - f a)/(b-a))" using derF by simp ``` huffman@21164 ` 1050` ``` qed ``` huffman@21164 ` 1051` ```qed ``` huffman@21164 ` 1052` hoelzl@29803 ` 1053` ```lemma MVT2: ``` hoelzl@29803 ` 1054` ``` "[| a < b; \x. a \ x & x \ b --> DERIV f x :> f'(x) |] ``` hoelzl@29803 ` 1055` ``` ==> \z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))" ``` hoelzl@29803 ` 1056` ```apply (drule MVT) ``` hoelzl@29803 ` 1057` ```apply (blast intro: DERIV_isCont) ``` hoelzl@29803 ` 1058` ```apply (force dest: order_less_imp_le simp add: differentiable_def) ``` hoelzl@29803 ` 1059` ```apply (blast dest: DERIV_unique order_less_imp_le) ``` hoelzl@29803 ` 1060` ```done ``` hoelzl@29803 ` 1061` huffman@21164 ` 1062` huffman@21164 ` 1063` ```text{*A function is constant if its derivative is 0 over an interval.*} ``` huffman@21164 ` 1064` huffman@21164 ` 1065` ```lemma DERIV_isconst_end: ``` huffman@21164 ` 1066` ``` fixes f :: "real => real" ``` huffman@21164 ` 1067` ``` shows "[| a < b; ``` huffman@21164 ` 1068` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 1069` ``` \x. a < x & x < b --> DERIV f x :> 0 |] ``` huffman@21164 ` 1070` ``` ==> f b = f a" ``` huffman@21164 ` 1071` ```apply (drule MVT, assumption) ``` huffman@21164 ` 1072` ```apply (blast intro: differentiableI) ``` huffman@21164 ` 1073` ```apply (auto dest!: DERIV_unique simp add: diff_eq_eq) ``` huffman@21164 ` 1074` ```done ``` huffman@21164 ` 1075` huffman@21164 ` 1076` ```lemma DERIV_isconst1: ``` huffman@21164 ` 1077` ``` fixes f :: "real => real" ``` huffman@21164 ` 1078` ``` shows "[| a < b; ``` huffman@21164 ` 1079` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 1080` ``` \x. a < x & x < b --> DERIV f x :> 0 |] ``` huffman@21164 ` 1081` ``` ==> \x. a \ x & x \ b --> f x = f a" ``` huffman@21164 ` 1082` ```apply safe ``` huffman@21164 ` 1083` ```apply (drule_tac x = a in order_le_imp_less_or_eq, safe) ``` huffman@21164 ` 1084` ```apply (drule_tac b = x in DERIV_isconst_end, auto) ``` huffman@21164 ` 1085` ```done ``` huffman@21164 ` 1086` huffman@21164 ` 1087` ```lemma DERIV_isconst2: ``` huffman@21164 ` 1088` ``` fixes f :: "real => real" ``` huffman@21164 ` 1089` ``` shows "[| a < b; ``` huffman@21164 ` 1090` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 1091` ``` \x. a < x & x < b --> DERIV f x :> 0; ``` huffman@21164 ` 1092` ``` a \ x; x \ b |] ``` huffman@21164 ` 1093` ``` ==> f x = f a" ``` huffman@21164 ` 1094` ```apply (blast dest: DERIV_isconst1) ``` huffman@21164 ` 1095` ```done ``` huffman@21164 ` 1096` hoelzl@29803 ` 1097` ```lemma DERIV_isconst3: fixes a b x y :: real ``` hoelzl@29803 ` 1098` ``` assumes "a < b" and "x \ {a <..< b}" and "y \ {a <..< b}" ``` hoelzl@29803 ` 1099` ``` assumes derivable: "\x. x \ {a <..< b} \ DERIV f x :> 0" ``` hoelzl@29803 ` 1100` ``` shows "f x = f y" ``` hoelzl@29803 ` 1101` ```proof (cases "x = y") ``` hoelzl@29803 ` 1102` ``` case False ``` hoelzl@29803 ` 1103` ``` let ?a = "min x y" ``` hoelzl@29803 ` 1104` ``` let ?b = "max x y" ``` hoelzl@29803 ` 1105` ``` ``` hoelzl@29803 ` 1106` ``` have "\z. ?a \ z \ z \ ?b \ DERIV f z :> 0" ``` hoelzl@29803 ` 1107` ``` proof (rule allI, rule impI) ``` hoelzl@29803 ` 1108` ``` fix z :: real assume "?a \ z \ z \ ?b" ``` hoelzl@29803 ` 1109` ``` hence "a < z" and "z < b" using `x \ {a <..< b}` and `y \ {a <..< b}` by auto ``` hoelzl@29803 ` 1110` ``` hence "z \ {a<.. 0" by (rule derivable) ``` hoelzl@29803 ` 1112` ``` qed ``` hoelzl@29803 ` 1113` ``` hence isCont: "\z. ?a \ z \ z \ ?b \ isCont f z" ``` hoelzl@29803 ` 1114` ``` and DERIV: "\z. ?a < z \ z < ?b \ DERIV f z :> 0" using DERIV_isCont by auto ``` hoelzl@29803 ` 1115` hoelzl@29803 ` 1116` ``` have "?a < ?b" using `x \ y` by auto ``` hoelzl@29803 ` 1117` ``` from DERIV_isconst2[OF this isCont DERIV, of x] and DERIV_isconst2[OF this isCont DERIV, of y] ``` hoelzl@29803 ` 1118` ``` show ?thesis by auto ``` hoelzl@29803 ` 1119` ```qed auto ``` hoelzl@29803 ` 1120` huffman@21164 ` 1121` ```lemma DERIV_isconst_all: ``` huffman@21164 ` 1122` ``` fixes f :: "real => real" ``` huffman@21164 ` 1123` ``` shows "\x. DERIV f x :> 0 ==> f(x) = f(y)" ``` huffman@21164 ` 1124` ```apply (rule linorder_cases [of x y]) ``` huffman@21164 ` 1125` ```apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+ ``` huffman@21164 ` 1126` ```done ``` huffman@21164 ` 1127` huffman@21164 ` 1128` ```lemma DERIV_const_ratio_const: ``` huffman@21784 ` 1129` ``` fixes f :: "real => real" ``` huffman@21784 ` 1130` ``` shows "[|a \ b; \x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b-a) * k" ``` huffman@21164 ` 1131` ```apply (rule linorder_cases [of a b], auto) ``` huffman@21164 ` 1132` ```apply (drule_tac [!] f = f in MVT) ``` huffman@21164 ` 1133` ```apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def) ``` nipkow@23477 ` 1134` ```apply (auto dest: DERIV_unique simp add: ring_distribs diff_minus) ``` huffman@21164 ` 1135` ```done ``` huffman@21164 ` 1136` huffman@21164 ` 1137` ```lemma DERIV_const_ratio_const2: ``` huffman@21784 ` 1138` ``` fixes f :: "real => real" ``` huffman@21784 ` 1139` ``` shows "[|a \ b; \x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k" ``` huffman@21164 ` 1140` ```apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1]) ``` huffman@21164 ` 1141` ```apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc) ``` huffman@21164 ` 1142` ```done ``` huffman@21164 ` 1143` huffman@21164 ` 1144` ```lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)" ``` huffman@21164 ` 1145` ```by (simp) ``` huffman@21164 ` 1146` huffman@21164 ` 1147` ```lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)" ``` huffman@21164 ` 1148` ```by (simp) ``` huffman@21164 ` 1149` huffman@21164 ` 1150` ```text{*Gallileo's "trick": average velocity = av. of end velocities*} ``` huffman@21164 ` 1151` huffman@21164 ` 1152` ```lemma DERIV_const_average: ``` huffman@21164 ` 1153` ``` fixes v :: "real => real" ``` huffman@21164 ` 1154` ``` assumes neq: "a \ (b::real)" ``` huffman@21164 ` 1155` ``` and der: "\x. DERIV v x :> k" ``` huffman@21164 ` 1156` ``` shows "v ((a + b)/2) = (v a + v b)/2" ``` huffman@21164 ` 1157` ```proof (cases rule: linorder_cases [of a b]) ``` huffman@21164 ` 1158` ``` case equal with neq show ?thesis by simp ``` huffman@21164 ` 1159` ```next ``` huffman@21164 ` 1160` ``` case less ``` huffman@21164 ` 1161` ``` have "(v b - v a) / (b - a) = k" ``` huffman@21164 ` 1162` ``` by (rule DERIV_const_ratio_const2 [OF neq der]) ``` huffman@21164 ` 1163` ``` hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp ``` huffman@21164 ` 1164` ``` moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k" ``` huffman@21164 ` 1165` ``` by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq) ``` huffman@21164 ` 1166` ``` ultimately show ?thesis using neq by force ``` huffman@21164 ` 1167` ```next ``` huffman@21164 ` 1168` ``` case greater ``` huffman@21164 ` 1169` ``` have "(v b - v a) / (b - a) = k" ``` huffman@21164 ` 1170` ``` by (rule DERIV_const_ratio_const2 [OF neq der]) ``` huffman@21164 ` 1171` ``` hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp ``` huffman@21164 ` 1172` ``` moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k" ``` huffman@21164 ` 1173` ``` by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq) ``` huffman@21164 ` 1174` ``` ultimately show ?thesis using neq by (force simp add: add_commute) ``` huffman@21164 ` 1175` ```qed ``` huffman@21164 ` 1176` paulson@33654 ` 1177` ```(* A function with positive derivative is increasing. ``` paulson@33654 ` 1178` ``` A simple proof using the MVT, by Jeremy Avigad. And variants. ``` paulson@33654 ` 1179` ```*) ``` paulson@33654 ` 1180` ```lemma DERIV_pos_imp_increasing: ``` paulson@33654 ` 1181` ``` fixes a::real and b::real and f::"real => real" ``` paulson@33654 ` 1182` ``` assumes "a < b" and "\x. a \ x & x \ b --> (EX y. DERIV f x :> y & y > 0)" ``` paulson@33654 ` 1183` ``` shows "f a < f b" ``` paulson@33654 ` 1184` ```proof (rule ccontr) ``` wenzelm@41550 ` 1185` ``` assume f: "~ f a < f b" ``` wenzelm@33690 ` 1186` ``` have "EX l z. a < z & z < b & DERIV f z :> l ``` paulson@33654 ` 1187` ``` & f b - f a = (b - a) * l" ``` wenzelm@33690 ` 1188` ``` apply (rule MVT) ``` wenzelm@33690 ` 1189` ``` using assms ``` wenzelm@33690 ` 1190` ``` apply auto ``` wenzelm@33690 ` 1191` ``` apply (metis DERIV_isCont) ``` huffman@36777 ` 1192` ``` apply (metis differentiableI less_le) ``` wenzelm@33690 ` 1193` ``` done ``` wenzelm@41550 ` 1194` ``` then obtain l z where z: "a < z" "z < b" "DERIV f z :> l" ``` paulson@33654 ` 1195` ``` and "f b - f a = (b - a) * l" ``` paulson@33654 ` 1196` ``` by auto ``` wenzelm@41550 ` 1197` ``` with assms f have "~(l > 0)" ``` huffman@36777 ` 1198` ``` by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le) ``` wenzelm@41550 ` 1199` ``` with assms z show False ``` huffman@36777 ` 1200` ``` by (metis DERIV_unique less_le) ``` paulson@33654 ` 1201` ```qed ``` paulson@33654 ` 1202` noschinl@45791 ` 1203` ```lemma DERIV_nonneg_imp_nondecreasing: ``` paulson@33654 ` 1204` ``` fixes a::real and b::real and f::"real => real" ``` paulson@33654 ` 1205` ``` assumes "a \ b" and ``` paulson@33654 ` 1206` ``` "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y \ 0)" ``` paulson@33654 ` 1207` ``` shows "f a \ f b" ``` paulson@33654 ` 1208` ```proof (rule ccontr, cases "a = b") ``` wenzelm@41550 ` 1209` ``` assume "~ f a \ f b" and "a = b" ``` wenzelm@41550 ` 1210` ``` then show False by auto ``` haftmann@37891 ` 1211` ```next ``` haftmann@37891 ` 1212` ``` assume A: "~ f a \ f b" ``` haftmann@37891 ` 1213` ``` assume B: "a ~= b" ``` paulson@33654 ` 1214` ``` with assms have "EX l z. a < z & z < b & DERIV f z :> l ``` paulson@33654 ` 1215` ``` & f b - f a = (b - a) * l" ``` wenzelm@33690 ` 1216` ``` apply - ``` wenzelm@33690 ` 1217` ``` apply (rule MVT) ``` wenzelm@33690 ` 1218` ``` apply auto ``` wenzelm@33690 ` 1219` ``` apply (metis DERIV_isCont) ``` huffman@36777 ` 1220` ``` apply (metis differentiableI less_le) ``` paulson@33654 ` 1221` ``` done ``` wenzelm@41550 ` 1222` ``` then obtain l z where z: "a < z" "z < b" "DERIV f z :> l" ``` haftmann@37891 ` 1223` ``` and C: "f b - f a = (b - a) * l" ``` paulson@33654 ` 1224` ``` by auto ``` haftmann@37891 ` 1225` ``` with A have "a < b" "f b < f a" by auto ``` haftmann@37891 ` 1226` ``` with C have "\ l \ 0" by (auto simp add: not_le algebra_simps) ``` huffman@45051 ` 1227` ``` (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono add_left_mono linear order_refl) ``` wenzelm@41550 ` 1228` ``` with assms z show False ``` paulson@33654 ` 1229` ``` by (metis DERIV_unique order_less_imp_le) ``` paulson@33654 ` 1230` ```qed ``` paulson@33654 ` 1231` paulson@33654 ` 1232` ```lemma DERIV_neg_imp_decreasing: ``` paulson@33654 ` 1233` ``` fixes a::real and b::real and f::"real => real" ``` paulson@33654 ` 1234` ``` assumes "a < b" and ``` paulson@33654 ` 1235` ``` "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y < 0)" ``` paulson@33654 ` 1236` ``` shows "f a > f b" ``` paulson@33654 ` 1237` ```proof - ``` paulson@33654 ` 1238` ``` have "(%x. -f x) a < (%x. -f x) b" ``` paulson@33654 ` 1239` ``` apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"]) ``` wenzelm@33690 ` 1240` ``` using assms ``` wenzelm@33690 ` 1241` ``` apply auto ``` paulson@33654 ` 1242` ``` apply (metis DERIV_minus neg_0_less_iff_less) ``` paulson@33654 ` 1243` ``` done ``` paulson@33654 ` 1244` ``` thus ?thesis ``` paulson@33654 ` 1245` ``` by simp ``` paulson@33654 ` 1246` ```qed ``` paulson@33654 ` 1247` paulson@33654 ` 1248` ```lemma DERIV_nonpos_imp_nonincreasing: ``` paulson@33654 ` 1249` ``` fixes a::real and b::real and f::"real => real" ``` paulson@33654 ` 1250` ``` assumes "a \ b" and ``` paulson@33654 ` 1251` ``` "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y \ 0)" ``` paulson@33654 ` 1252` ``` shows "f a \ f b" ``` paulson@33654 ` 1253` ```proof - ``` paulson@33654 ` 1254` ``` have "(%x. -f x) a \ (%x. -f x) b" ``` noschinl@45791 ` 1255` ``` apply (rule DERIV_nonneg_imp_nondecreasing [of a b "%x. -f x"]) ``` wenzelm@33690 ` 1256` ``` using assms ``` wenzelm@33690 ` 1257` ``` apply auto ``` paulson@33654 ` 1258` ``` apply (metis DERIV_minus neg_0_le_iff_le) ``` paulson@33654 ` 1259` ``` done ``` paulson@33654 ` 1260` ``` thus ?thesis ``` paulson@33654 ` 1261` ``` by simp ``` paulson@33654 ` 1262` ```qed ``` huffman@21164 ` 1263` huffman@23041 ` 1264` ```text {* Derivative of inverse function *} ``` huffman@23041 ` 1265` huffman@23041 ` 1266` ```lemma DERIV_inverse_function: ``` huffman@23041 ` 1267` ``` fixes f g :: "real \ real" ``` huffman@23041 ` 1268` ``` assumes der: "DERIV f (g x) :> D" ``` huffman@23041 ` 1269` ``` assumes neq: "D \ 0" ``` huffman@23044 ` 1270` ``` assumes a: "a < x" and b: "x < b" ``` huffman@23044 ` 1271` ``` assumes inj: "\y. a < y \ y < b \ f (g y) = y" ``` huffman@23041 ` 1272` ``` assumes cont: "isCont g x" ``` huffman@23041 ` 1273` ``` shows "DERIV g x :> inverse D" ``` huffman@23041 ` 1274` ```unfolding DERIV_iff2 ``` huffman@23044 ` 1275` ```proof (rule LIM_equal2) ``` huffman@23044 ` 1276` ``` show "0 < min (x - a) (b - x)" ``` chaieb@27668 ` 1277` ``` using a b by arith ``` huffman@23044 ` 1278` ```next ``` huffman@23041 ` 1279` ``` fix y ``` huffman@23044 ` 1280` ``` assume "norm (y - x) < min (x - a) (b - x)" ``` chaieb@27668 ` 1281` ``` hence "a < y" and "y < b" ``` huffman@23044 ` 1282` ``` by (simp_all add: abs_less_iff) ``` huffman@23041 ` 1283` ``` thus "(g y - g x) / (y - x) = ``` huffman@23041 ` 1284` ``` inverse ((f (g y) - x) / (g y - g x))" ``` huffman@23041 ` 1285` ``` by (simp add: inj) ``` huffman@23041 ` 1286` ```next ``` huffman@23041 ` 1287` ``` have "(\z. (f z - f (g x)) / (z - g x)) -- g x --> D" ``` huffman@23041 ` 1288` ``` by (rule der [unfolded DERIV_iff2]) ``` huffman@23041 ` 1289` ``` hence 1: "(\z. (f z - x) / (z - g x)) -- g x --> D" ``` huffman@23044 ` 1290` ``` using inj a b by simp ``` huffman@23041 ` 1291` ``` have 2: "\d>0. \y. y \ x \ norm (y - x) < d \ g y \ g x" ``` huffman@23041 ` 1292` ``` proof (safe intro!: exI) ``` huffman@23044 ` 1293` ``` show "0 < min (x - a) (b - x)" ``` huffman@23044 ` 1294` ``` using a b by simp ``` huffman@23041 ` 1295` ``` next ``` huffman@23041 ` 1296` ``` fix y ``` huffman@23044 ` 1297` ``` assume "norm (y - x) < min (x - a) (b - x)" ``` huffman@23044 ` 1298` ``` hence y: "a < y" "y < b" ``` huffman@23044 ` 1299` ``` by (simp_all add: abs_less_iff) ``` huffman@23041 ` 1300` ``` assume "g y = g x" ``` huffman@23041 ` 1301` ``` hence "f (g y) = f (g x)" by simp ``` huffman@23044 ` 1302` ``` hence "y = x" using inj y a b by simp ``` huffman@23041 ` 1303` ``` also assume "y \ x" ``` huffman@23041 ` 1304` ``` finally show False by simp ``` huffman@23041 ` 1305` ``` qed ``` huffman@23041 ` 1306` ``` have "(\y. (f (g y) - x) / (g y - g x)) -- x --> D" ``` huffman@23041 ` 1307` ``` using cont 1 2 by (rule isCont_LIM_compose2) ``` huffman@23041 ` 1308` ``` thus "(\y. inverse ((f (g y) - x) / (g y - g x))) ``` huffman@23041 ` 1309` ``` -- x --> inverse D" ``` huffman@44568 ` 1310` ``` using neq by (rule tendsto_inverse) ``` huffman@23041 ` 1311` ```qed ``` huffman@23041 ` 1312` huffman@29975 ` 1313` ```subsection {* Generalized Mean Value Theorem *} ``` huffman@29975 ` 1314` huffman@21164 ` 1315` ```theorem GMVT: ``` huffman@21784 ` 1316` ``` fixes a b :: real ``` huffman@21164 ` 1317` ``` assumes alb: "a < b" ``` wenzelm@41550 ` 1318` ``` and fc: "\x. a \ x \ x \ b \ isCont f x" ``` wenzelm@41550 ` 1319` ``` and fd: "\x. a < x \ x < b \ f differentiable x" ``` wenzelm@41550 ` 1320` ``` and gc: "\x. a \ x \ x \ b \ isCont g x" ``` wenzelm@41550 ` 1321` ``` and gd: "\x. a < x \ x < b \ g differentiable x" ``` huffman@21164 ` 1322` ``` shows "\g'c f'c c. DERIV g c :> g'c \ DERIV f c :> f'c \ a < c \ c < b \ ((f b - f a) * g'c) = ((g b - g a) * f'c)" ``` huffman@21164 ` 1323` ```proof - ``` huffman@21164 ` 1324` ``` let ?h = "\x. (f b - f a)*(g x) - (g b - g a)*(f x)" ``` wenzelm@41550 ` 1325` ``` from assms have "a < b" by simp ``` huffman@21164 ` 1326` ``` moreover have "\x. a \ x \ x \ b \ isCont ?h x" ``` huffman@44233 ` 1327` ``` using fc gc by simp ``` huffman@44233 ` 1328` ``` moreover have "\x. a < x \ x < b \ ?h differentiable x" ``` huffman@44233 ` 1329` ``` using fd gd by simp ``` huffman@21164 ` 1330` ``` ultimately have "\l z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" by (rule MVT) ``` huffman@21164 ` 1331` ``` then obtain l where ldef: "\z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" .. ``` huffman@21164 ` 1332` ``` then obtain c where cdef: "a < c \ c < b \ DERIV ?h c :> l \ ?h b - ?h a = (b - a) * l" .. ``` huffman@21164 ` 1333` huffman@21164 ` 1334` ``` from cdef have cint: "a < c \ c < b" by auto ``` huffman@21164 ` 1335` ``` with gd have "g differentiable c" by simp ``` huffman@21164 ` 1336` ``` hence "\D. DERIV g c :> D" by (rule differentiableD) ``` huffman@21164 ` 1337` ``` then obtain g'c where g'cdef: "DERIV g c :> g'c" .. ``` huffman@21164 ` 1338` huffman@21164 ` 1339` ``` from cdef have "a < c \ c < b" by auto ``` huffman@21164 ` 1340` ``` with fd have "f differentiable c" by simp ``` huffman@21164 ` 1341` ``` hence "\D. DERIV f c :> D" by (rule differentiableD) ``` huffman@21164 ` 1342` ``` then obtain f'c where f'cdef: "DERIV f c :> f'c" .. ``` huffman@21164 ` 1343` huffman@21164 ` 1344` ``` from cdef have "DERIV ?h c :> l" by auto ``` hoelzl@41368 ` 1345` ``` moreover have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)" ``` hoelzl@41368 ` 1346` ``` using g'cdef f'cdef by (auto intro!: DERIV_intros) ``` huffman@21164 ` 1347` ``` ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique) ``` huffman@21164 ` 1348` huffman@21164 ` 1349` ``` { ``` huffman@21164 ` 1350` ``` from cdef have "?h b - ?h a = (b - a) * l" by auto ``` wenzelm@53374 ` 1351` ``` also from leq have "\ = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp ``` huffman@21164 ` 1352` ``` finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp ``` huffman@21164 ` 1353` ``` } ``` huffman@21164 ` 1354` ``` moreover ``` huffman@21164 ` 1355` ``` { ``` huffman@21164 ` 1356` ``` have "?h b - ?h a = ``` huffman@21164 ` 1357` ``` ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) - ``` huffman@21164 ` 1358` ``` ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))" ``` nipkow@29667 ` 1359` ``` by (simp add: algebra_simps) ``` huffman@21164 ` 1360` ``` hence "?h b - ?h a = 0" by auto ``` huffman@21164 ` 1361` ``` } ``` huffman@21164 ` 1362` ``` ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto ``` huffman@21164 ` 1363` ``` with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp ``` huffman@21164 ` 1364` ``` hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp ``` huffman@21164 ` 1365` ``` hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac) ``` huffman@21164 ` 1366` huffman@21164 ` 1367` ``` with g'cdef f'cdef cint show ?thesis by auto ``` huffman@21164 ` 1368` ```qed ``` huffman@21164 ` 1369` hoelzl@50327 ` 1370` ```lemma GMVT': ``` hoelzl@50327 ` 1371` ``` fixes f g :: "real \ real" ``` hoelzl@50327 ` 1372` ``` assumes "a < b" ``` hoelzl@50327 ` 1373` ``` assumes isCont_f: "\z. a \ z \ z \ b \ isCont f z" ``` hoelzl@50327 ` 1374` ``` assumes isCont_g: "\z. a \ z \ z \ b \ isCont g z" ``` hoelzl@50327 ` 1375` ``` assumes DERIV_g: "\z. a < z \ z < b \ DERIV g z :> (g' z)" ``` hoelzl@50327 ` 1376` ``` assumes DERIV_f: "\z. a < z \ z < b \ DERIV f z :> (f' z)" ``` hoelzl@50327 ` 1377` ``` shows "\c. a < c \ c < b \ (f b - f a) * g' c = (g b - g a) * f' c" ``` hoelzl@50327 ` 1378` ```proof - ``` hoelzl@50327 ` 1379` ``` have "\g'c f'c c. DERIV g c :> g'c \ DERIV f c :> f'c \ ``` hoelzl@50327 ` 1380` ``` a < c \ c < b \ (f b - f a) * g'c = (g b - g a) * f'c" ``` hoelzl@50327 ` 1381` ``` using assms by (intro GMVT) (force simp: differentiable_def)+ ``` hoelzl@50327 ` 1382` ``` then obtain c where "a < c" "c < b" "(f b - f a) * g' c = (g b - g a) * f' c" ``` hoelzl@50327 ` 1383` ``` using DERIV_f DERIV_g by (force dest: DERIV_unique) ``` hoelzl@50327 ` 1384` ``` then show ?thesis ``` hoelzl@50327 ` 1385` ``` by auto ``` hoelzl@50327 ` 1386` ```qed ``` hoelzl@50327 ` 1387` hoelzl@51529 ` 1388` hoelzl@51529 ` 1389` ```subsection {* L'Hopitals rule *} ``` hoelzl@51529 ` 1390` hoelzl@51641 ` 1391` ```lemma isCont_If_ge: ``` hoelzl@51641 ` 1392` ``` fixes a :: "'a :: linorder_topology" ``` hoelzl@51641 ` 1393` ``` shows "continuous (at_left a) g \ (f ---> g a) (at_right a) \ isCont (\x. if x \ a then g x else f x) a" ``` hoelzl@51641 ` 1394` ``` unfolding isCont_def continuous_within ``` hoelzl@51641 ` 1395` ``` apply (intro filterlim_split_at) ``` hoelzl@51641 ` 1396` ``` apply (subst filterlim_cong[OF refl refl, where g=g]) ``` hoelzl@51641 ` 1397` ``` apply (simp_all add: eventually_at_filter less_le) ``` hoelzl@51641 ` 1398` ``` apply (subst filterlim_cong[OF refl refl, where g=f]) ``` hoelzl@51641 ` 1399` ``` apply (simp_all add: eventually_at_filter less_le) ``` hoelzl@51641 ` 1400` ``` done ``` hoelzl@51641 ` 1401` hoelzl@50327 ` 1402` ```lemma lhopital_right_0: ``` hoelzl@50329 ` 1403` ``` fixes f0 g0 :: "real \ real" ``` hoelzl@50329 ` 1404` ``` assumes f_0: "(f0 ---> 0) (at_right 0)" ``` hoelzl@50329 ` 1405` ``` assumes g_0: "(g0 ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1406` ``` assumes ev: ``` hoelzl@50329 ` 1407` ``` "eventually (\x. g0 x \ 0) (at_right 0)" ``` hoelzl@50327 ` 1408` ``` "eventually (\x. g' x \ 0) (at_right 0)" ``` hoelzl@50329 ` 1409` ``` "eventually (\x. DERIV f0 x :> f' x) (at_right 0)" ``` hoelzl@50329 ` 1410` ``` "eventually (\x. DERIV g0 x :> g' x) (at_right 0)" ``` hoelzl@50327 ` 1411` ``` assumes lim: "((\ x. (f' x / g' x)) ---> x) (at_right 0)" ``` hoelzl@50329 ` 1412` ``` shows "((\ x. f0 x / g0 x) ---> x) (at_right 0)" ``` hoelzl@50327 ` 1413` ```proof - ``` hoelzl@50329 ` 1414` ``` def f \ "\x. if x \ 0 then 0 else f0 x" ``` hoelzl@50329 ` 1415` ``` then have "f 0 = 0" by simp ``` hoelzl@50329 ` 1416` hoelzl@50329 ` 1417` ``` def g \ "\x. if x \ 0 then 0 else g0 x" ``` hoelzl@50329 ` 1418` ``` then have "g 0 = 0" by simp ``` hoelzl@50329 ` 1419` hoelzl@50329 ` 1420` ``` have "eventually (\x. g0 x \ 0 \ g' x \ 0 \ ``` hoelzl@50329 ` 1421` ``` DERIV f0 x :> (f' x) \ DERIV g0 x :> (g' x)) (at_right 0)" ``` hoelzl@50329 ` 1422` ``` using ev by eventually_elim auto ``` hoelzl@50329 ` 1423` ``` then obtain a where [arith]: "0 < a" ``` hoelzl@50329 ` 1424` ``` and g0_neq_0: "\x. 0 < x \ x < a \ g0 x \ 0" ``` hoelzl@50327 ` 1425` ``` and g'_neq_0: "\x. 0 < x \ x < a \ g' x \ 0" ``` hoelzl@50329 ` 1426` ``` and f0: "\x. 0 < x \ x < a \ DERIV f0 x :> (f' x)" ``` hoelzl@50329 ` 1427` ``` and g0: "\x. 0 < x \ x < a \ DERIV g0 x :> (g' x)" ``` hoelzl@51641 ` 1428` ``` unfolding eventually_at eventually_at by (auto simp: dist_real_def) ``` hoelzl@50327 ` 1429` hoelzl@50329 ` 1430` ``` have g_neq_0: "\x. 0 < x \ x < a \ g x \ 0" ``` hoelzl@50329 ` 1431` ``` using g0_neq_0 by (simp add: g_def) ``` hoelzl@50329 ` 1432` hoelzl@50329 ` 1433` ``` { fix x assume x: "0 < x" "x < a" then have "DERIV f x :> (f' x)" ``` hoelzl@50329 ` 1434` ``` by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ f0[OF x]]) ``` hoelzl@50329 ` 1435` ``` (auto simp: f_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) } ``` hoelzl@50329 ` 1436` ``` note f = this ``` hoelzl@50329 ` 1437` hoelzl@50329 ` 1438` ``` { fix x assume x: "0 < x" "x < a" then have "DERIV g x :> (g' x)" ``` hoelzl@50329 ` 1439` ``` by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ g0[OF x]]) ``` hoelzl@50329 ` 1440` ``` (auto simp: g_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) } ``` hoelzl@50329 ` 1441` ``` note g = this ``` hoelzl@50329 ` 1442` hoelzl@50329 ` 1443` ``` have "isCont f 0" ``` hoelzl@51641 ` 1444` ``` unfolding f_def by (intro isCont_If_ge f_0 continuous_const) ``` hoelzl@51641 ` 1445` hoelzl@50329 ` 1446` ``` have "isCont g 0" ``` hoelzl@51641 ` 1447` ``` unfolding g_def by (intro isCont_If_ge g_0 continuous_const) ``` hoelzl@50329 ` 1448` hoelzl@50327 ` 1449` ``` have "\\. \x\{0 <..< a}. 0 < \ x \ \ x < x \ f x / g x = f' (\ x) / g' (\ x)" ``` hoelzl@50327 ` 1450` ``` proof (rule bchoice, rule) ``` hoelzl@50327 ` 1451` ``` fix x assume "x \ {0 <..< a}" ``` hoelzl@50327 ` 1452` ``` then have x[arith]: "0 < x" "x < a" by auto ``` hoelzl@50327 ` 1453` ``` with g'_neq_0 g_neq_0 `g 0 = 0` have g': "\x. 0 < x \ x < a \ 0 \ g' x" "g 0 \ g x" ``` hoelzl@50327 ` 1454` ``` by auto ``` hoelzl@50328 ` 1455` ``` have "\x. 0 \ x \ x < a \ isCont f x" ``` hoelzl@50328 ` 1456` ``` using `isCont f 0` f by (auto intro: DERIV_isCont simp: le_less) ``` hoelzl@50328 ` 1457` ``` moreover have "\x. 0 \ x \ x < a \ isCont g x" ``` hoelzl@50328 ` 1458` ``` using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less) ``` hoelzl@50328 ` 1459` ``` ultimately have "\c. 0 < c \ c < x \ (f x - f 0) * g' c = (g x - g 0) * f' c" ``` hoelzl@50328 ` 1460` ``` using f g `x < a` by (intro GMVT') auto ``` wenzelm@53374 ` 1461` ``` then obtain c where *: "0 < c" "c < x" "(f x - f 0) * g' c = (g x - g 0) * f' c" ``` wenzelm@53374 ` 1462` ``` by blast ``` hoelzl@50327 ` 1463` ``` moreover ``` wenzelm@53374 ` 1464` ``` from * g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" ``` hoelzl@50327 ` 1465` ``` by (simp add: field_simps) ``` hoelzl@50327 ` 1466` ``` ultimately show "\y. 0 < y \ y < x \ f x / g x = f' y / g' y" ``` hoelzl@50327 ` 1467` ``` using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c]) ``` hoelzl@50327 ` 1468` ``` qed ``` hoelzl@50327 ` 1469` ``` then guess \ .. ``` hoelzl@50327 ` 1470` ``` then have \: "eventually (\x. 0 < \ x \ \ x < x \ f x / g x = f' (\ x) / g' (\ x)) (at_right 0)" ``` hoelzl@51641 ` 1471` ``` unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def) ``` hoelzl@50327 ` 1472` ``` moreover ``` hoelzl@50327 ` 1473` ``` from \ have "eventually (\x. norm (\ x) \ x) (at_right 0)" ``` hoelzl@50327 ` 1474` ``` by eventually_elim auto ``` hoelzl@50327 ` 1475` ``` then have "((\x. norm (\ x)) ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1476` ``` by (rule_tac real_tendsto_sandwich[where f="\x. 0" and h="\x. x"]) ``` hoelzl@51641 ` 1477` ``` (auto intro: tendsto_const tendsto_ident_at) ``` hoelzl@50327 ` 1478` ``` then have "(\ ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1479` ``` by (rule tendsto_norm_zero_cancel) ``` hoelzl@50327 ` 1480` ``` with \ have "filterlim \ (at_right 0) (at_right 0)" ``` hoelzl@51641 ` 1481` ``` by (auto elim!: eventually_elim1 simp: filterlim_at) ``` hoelzl@50327 ` 1482` ``` from this lim have "((\t. f' (\ t) / g' (\ t)) ---> x) (at_right 0)" ``` hoelzl@50327 ` 1483` ``` by (rule_tac filterlim_compose[of _ _ _ \]) ``` hoelzl@50329 ` 1484` ``` ultimately have "((\t. f t / g t) ---> x) (at_right 0)" (is ?P) ``` hoelzl@50328 ` 1485` ``` by (rule_tac filterlim_cong[THEN iffD1, OF refl refl]) ``` hoelzl@50328 ` 1486` ``` (auto elim: eventually_elim1) ``` hoelzl@50329 ` 1487` ``` also have "?P \ ?thesis" ``` hoelzl@51641 ` 1488` ``` by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter) ``` hoelzl@50329 ` 1489` ``` finally show ?thesis . ``` hoelzl@50327 ` 1490` ```qed ``` hoelzl@50327 ` 1491` hoelzl@50330 ` 1492` ```lemma lhopital_right: ``` hoelzl@50330 ` 1493` ``` "((f::real \ real) ---> 0) (at_right x) \ (g ---> 0) (at_right x) \ ``` hoelzl@50330 ` 1494` ``` eventually (\x. g x \ 0) (at_right x) \ ``` hoelzl@50330 ` 1495` ``` eventually (\x. g' x \ 0) (at_right x) \ ``` hoelzl@50330 ` 1496` ``` eventually (\x. DERIV f x :> f' x) (at_right x) \ ``` hoelzl@50330 ` 1497` ``` eventually (\x. DERIV g x :> g' x) (at_right x) \ ``` hoelzl@50330 ` 1498` ``` ((\ x. (f' x / g' x)) ---> y) (at_right x) \ ``` hoelzl@50330 ` 1499` ``` ((\ x. f x / g x) ---> y) (at_right x)" ``` hoelzl@50330 ` 1500` ``` unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift ``` hoelzl@50330 ` 1501` ``` by (rule lhopital_right_0) ``` hoelzl@50330 ` 1502` hoelzl@50330 ` 1503` ```lemma lhopital_left: ``` hoelzl@50330 ` 1504` ``` "((f::real \ real) ---> 0) (at_left x) \ (g ---> 0) (at_left x) \ ``` hoelzl@50330 ` 1505` ``` eventually (\x. g x \ 0) (at_left x) \ ``` hoelzl@50330 ` 1506` ``` eventually (\x. g' x \ 0) (at_left x) \ ``` hoelzl@50330 ` 1507` ``` eventually (\x. DERIV f x :> f' x) (at_left x) \ ``` hoelzl@50330 ` 1508` ``` eventually (\x. DERIV g x :> g' x) (at_left x) \ ``` hoelzl@50330 ` 1509` ``` ((\ x. (f' x / g' x)) ---> y) (at_left x) \ ``` hoelzl@50330 ` 1510` ``` ((\ x. f x / g x) ---> y) (at_left x)" ``` hoelzl@50330 ` 1511` ``` unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror ``` hoelzl@50330 ` 1512` ``` by (rule lhopital_right[where f'="\x. - f' (- x)"]) (auto simp: DERIV_mirror) ``` hoelzl@50330 ` 1513` hoelzl@50330 ` 1514` ```lemma lhopital: ``` hoelzl@50330 ` 1515` ``` "((f::real \ real) ---> 0) (at x) \ (g ---> 0) (at x) \ ``` hoelzl@50330 ` 1516` ``` eventually (\x. g x \ 0) (at x) \ ``` hoelzl@50330 ` 1517` ``` eventually (\x. g' x \ 0) (at x) \ ``` hoelzl@50330 ` 1518` ``` eventually (\x. DERIV f x :> f' x) (at x) \ ``` hoelzl@50330 ` 1519` ``` eventually (\x. DERIV g x :> g' x) (at x) \ ``` hoelzl@50330 ` 1520` ``` ((\ x. (f' x / g' x)) ---> y) (at x) \ ``` hoelzl@50330 ` 1521` ``` ((\ x. f x / g x) ---> y) (at x)" ``` hoelzl@50330 ` 1522` ``` unfolding eventually_at_split filterlim_at_split ``` hoelzl@50330 ` 1523` ``` by (auto intro!: lhopital_right[of f x g g' f'] lhopital_left[of f x g g' f']) ``` hoelzl@50330 ` 1524` hoelzl@50327 ` 1525` ```lemma lhopital_right_0_at_top: ``` hoelzl@50327 ` 1526` ``` fixes f g :: "real \ real" ``` hoelzl@50327 ` 1527` ``` assumes g_0: "LIM x at_right 0. g x :> at_top" ``` hoelzl@50327 ` 1528` ``` assumes ev: ``` hoelzl@50327 ` 1529` ``` "eventually (\x. g' x \ 0) (at_right 0)" ``` hoelzl@50327 ` 1530` ``` "eventually (\x. DERIV f x :> f' x) (at_right 0)" ``` hoelzl@50327 ` 1531` ``` "eventually (\x. DERIV g x :> g' x) (at_right 0)" ``` hoelzl@50327 ` 1532` ``` assumes lim: "((\ x. (f' x / g' x)) ---> x) (at_right 0)" ``` hoelzl@50327 ` 1533` ``` shows "((\ x. f x / g x) ---> x) (at_right 0)" ``` hoelzl@50327 ` 1534` ``` unfolding tendsto_iff ``` hoelzl@50327 ` 1535` ```proof safe ``` hoelzl@50327 ` 1536` ``` fix e :: real assume "0 < e" ``` hoelzl@50327 ` 1537` hoelzl@50327 ` 1538` ``` with lim[unfolded tendsto_iff, rule_format, of "e / 4"] ``` hoelzl@50327 ` 1539` ``` have "eventually (\t. dist (f' t / g' t) x < e / 4) (at_right 0)" by simp ``` hoelzl@50327 ` 1540` ``` from eventually_conj[OF eventually_conj[OF ev(1) ev(2)] eventually_conj[OF ev(3) this]] ``` hoelzl@50327 ` 1541` ``` obtain a where [arith]: "0 < a" ``` hoelzl@50327 ` 1542` ``` and g'_neq_0: "\x. 0 < x \ x < a \ g' x \ 0" ``` hoelzl@50327 ` 1543` ``` and f0: "\x. 0 < x \ x \ a \ DERIV f x :> (f' x)" ``` hoelzl@50327 ` 1544` ``` and g0: "\x. 0 < x \ x \ a \ DERIV g x :> (g' x)" ``` hoelzl@50327 ` 1545` ``` and Df: "\t. 0 < t \ t < a \ dist (f' t / g' t) x < e / 4" ``` hoelzl@51641 ` 1546` ``` unfolding eventually_at_le by (auto simp: dist_real_def) ``` hoelzl@51641 ` 1547` ``` ``` hoelzl@50327 ` 1548` hoelzl@50327 ` 1549` ``` from Df have ``` hoelzl@50328 ` 1550` ``` "eventually (\t. t < a) (at_right 0)" "eventually (\t::real. 0 < t) (at_right 0)" ``` hoelzl@51641 ` 1551` ``` unfolding eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def) ``` hoelzl@50327 ` 1552` hoelzl@50327 ` 1553` ``` moreover ``` hoelzl@50328 ` 1554` ``` have "eventually (\t. 0 < g t) (at_right 0)" "eventually (\t. g a < g t) (at_right 0)" ``` hoelzl@50346 ` 1555` ``` using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top_dense) ``` hoelzl@50327 ` 1556` hoelzl@50327 ` 1557` ``` moreover ``` hoelzl@50327 ` 1558` ``` have inv_g: "((\x. inverse (g x)) ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1559` ``` using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl] ``` hoelzl@50327 ` 1560` ``` by (rule filterlim_compose) ``` hoelzl@50327 ` 1561` ``` then have "((\x. norm (1 - g a * inverse (g x))) ---> norm (1 - g a * 0)) (at_right 0)" ``` hoelzl@50327 ` 1562` ``` by (intro tendsto_intros) ``` hoelzl@50327 ` 1563` ``` then have "((\x. norm (1 - g a / g x)) ---> 1) (at_right 0)" ``` hoelzl@50327 ` 1564` ``` by (simp add: inverse_eq_divide) ``` hoelzl@50327 ` 1565` ``` from this[unfolded tendsto_iff, rule_format, of 1] ``` hoelzl@50327 ` 1566` ``` have "eventually (\x. norm (1 - g a / g x) < 2) (at_right 0)" ``` hoelzl@50327 ` 1567` ``` by (auto elim!: eventually_elim1 simp: dist_real_def) ``` hoelzl@50327 ` 1568` hoelzl@50327 ` 1569` ``` moreover ``` hoelzl@50327 ` 1570` ``` from inv_g have "((\t. norm ((f a - x * g a) * inverse (g t))) ---> norm ((f a - x * g a) * 0)) (at_right 0)" ``` hoelzl@50327 ` 1571` ``` by (intro tendsto_intros) ``` hoelzl@50327 ` 1572` ``` then have "((\t. norm (f a - x * g a) / norm (g t)) ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1573` ``` by (simp add: inverse_eq_divide) ``` hoelzl@50327 ` 1574` ``` from this[unfolded tendsto_iff, rule_format, of "e / 2"] `0 < e` ``` hoelzl@50327 ` 1575` ``` have "eventually (\t. norm (f a - x * g a) / norm (g t) < e / 2) (at_right 0)" ``` hoelzl@50327 ` 1576` ``` by (auto simp: dist_real_def) ``` hoelzl@50327 ` 1577` hoelzl@50327 ` 1578` ``` ultimately show "eventually (\t. dist (f t / g t) x < e) (at_right 0)" ``` hoelzl@50327 ` 1579` ``` proof eventually_elim ``` hoelzl@50327 ` 1580` ``` fix t assume t[arith]: "0 < t" "t < a" "g a < g t" "0 < g t" ``` hoelzl@50327 ` 1581` ``` assume ineq: "norm (1 - g a / g t) < 2" "norm (f a - x * g a) / norm (g t) < e / 2" ``` hoelzl@50327 ` 1582` hoelzl@50327 ` 1583` ``` have "\y. t < y \ y < a \ (g a - g t) * f' y = (f a - f t) * g' y" ``` hoelzl@50327 ` 1584` ``` using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+ ``` hoelzl@50327 ` 1585` ``` then guess y .. ``` hoelzl@50327 ` 1586` ``` from this ``` hoelzl@50327 ` 1587` ``` have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y" ``` hoelzl@50327 ` 1588` ``` using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps) ``` hoelzl@50327 ` 1589` hoelzl@50327 ` 1590` ``` have *: "f t / g t - x = ((f t - f a) / (g t - g a) - x) * (1 - g a / g t) + (f a - x * g a) / g t" ``` hoelzl@50327 ` 1591` ``` by (simp add: field_simps) ``` hoelzl@50327 ` 1592` ``` have "norm (f t / g t - x) \ ``` hoelzl@50327 ` 1593` ``` norm (((f t - f a) / (g t - g a) - x) * (1 - g a / g t)) + norm ((f a - x * g a) / g t)" ``` hoelzl@50327 ` 1594` ``` unfolding * by (rule norm_triangle_ineq) ``` hoelzl@50327 ` 1595` ``` also have "\ = dist (f' y / g' y) x * norm (1 - g a / g t) + norm (f a - x * g a) / norm (g t)" ``` hoelzl@50327 ` 1596` ``` by (simp add: abs_mult D_eq dist_real_def) ``` hoelzl@50327 ` 1597` ``` also have "\ < (e / 4) * 2 + e / 2" ``` hoelzl@50327 ` 1598` ``` using ineq Df[of y] `0 < e` by (intro add_le_less_mono mult_mono) auto ``` hoelzl@50327 ` 1599` ``` finally show "dist (f t / g t) x < e" ``` hoelzl@50327 ` 1600` ``` by (simp add: dist_real_def) ``` hoelzl@50327 ` 1601` ``` qed ``` hoelzl@50327 ` 1602` ```qed ``` hoelzl@50327 ` 1603` hoelzl@50330 ` 1604` ```lemma lhopital_right_at_top: ``` hoelzl@50330 ` 1605` ``` "LIM x at_right x. (g::real \ real) x :> at_top \ ``` hoelzl@50330 ` 1606` ``` eventually (\x. g' x \ 0) (at_right x) \ ``` hoelzl@50330 ` 1607` ``` eventually (\x. DERIV f x :> f' x) (at_right x) \ ``` hoelzl@50330 ` 1608` ``` eventually (\x. DERIV g x :> g' x) (at_right x) \ ``` hoelzl@50330 ` 1609` ``` ((\ x. (f' x / g' x)) ---> y) (at_right x) \ ``` hoelzl@50330 ` 1610` ``` ((\ x. f x / g x) ---> y) (at_right x)" ``` hoelzl@50330 ` 1611` ``` unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift ``` hoelzl@50330 ` 1612` ``` by (rule lhopital_right_0_at_top) ``` hoelzl@50330 ` 1613` hoelzl@50330 ` 1614` ```lemma lhopital_left_at_top: ``` hoelzl@50330 ` 1615` ``` "LIM x at_left x. (g::real \ real) x :> at_top \ ``` hoelzl@50330 ` 1616` ``` eventually (\x. g' x \ 0) (at_left x) \ ``` hoelzl@50330 ` 1617` ``` eventually (\x. DERIV f x :> f' x) (at_left x) \ ``` hoelzl@50330 ` 1618` ``` eventually (\x. DERIV g x :> g' x) (at_left x) \ ``` hoelzl@50330 ` 1619` ``` ((\ x. (f' x / g' x)) ---> y) (at_left x) \ ``` hoelzl@50330 ` 1620` ``` ((\ x. f x / g x) ---> y) (at_left x)" ``` hoelzl@50330 ` 1621` ``` unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror ``` hoelzl@50330 ` 1622` ``` by (rule lhopital_right_at_top[where f'="\x. - f' (- x)"]) (auto simp: DERIV_mirror) ``` hoelzl@50330 ` 1623` hoelzl@50330 ` 1624` ```lemma lhopital_at_top: ``` hoelzl@50330 ` 1625` ``` "LIM x at x. (g::real \ real) x :> at_top \ ``` hoelzl@50330 ` 1626` ``` eventually (\x. g' x \ 0) (at x) \ ``` hoelzl@50330 ` 1627` ``` eventually (\x. DERIV f x :> f' x) (at x) \ ``` hoelzl@50330 ` 1628` ``` eventually (\x. DERIV g x :> g' x) (at x) \ ``` hoelzl@50330 ` 1629` ``` ((\ x. (f' x / g' x)) ---> y) (at x) \ ``` hoelzl@50330 ` 1630` ``` ((\ x. f x / g x) ---> y) (at x)" ``` hoelzl@50330 ` 1631` ``` unfolding eventually_at_split filterlim_at_split ``` hoelzl@50330 ` 1632` ``` by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f']) ``` hoelzl@50330 ` 1633` hoelzl@50347 ` 1634` ```lemma lhospital_at_top_at_top: ``` hoelzl@50347 ` 1635` ``` fixes f g :: "real \ real" ``` hoelzl@50347 ` 1636` ``` assumes g_0: "LIM x at_top. g x :> at_top" ``` hoelzl@50347 ` 1637` ``` assumes g': "eventually (\x. g' x \ 0) at_top" ``` hoelzl@50347 ` 1638` ``` assumes Df: "eventually (\x. DERIV f x :> f' x) at_top" ``` hoelzl@50347 ` 1639` ``` assumes Dg: "eventually (\x. DERIV g x :> g' x) at_top" ``` hoelzl@50347 ` 1640` ``` assumes lim: "((\ x. (f' x / g' x)) ---> x) at_top" ``` hoelzl@50347 ` 1641` ``` shows "((\ x. f x / g x) ---> x) at_top" ``` hoelzl@50347 ` 1642` ``` unfolding filterlim_at_top_to_right ``` hoelzl@50347 ` 1643` ```proof (rule lhopital_right_0_at_top) ``` hoelzl@50347 ` 1644` ``` let ?F = "\x. f (inverse x)" ``` hoelzl@50347 ` 1645` ``` let ?G = "\x. g (inverse x)" ``` hoelzl@50347 ` 1646` ``` let ?R = "at_right (0::real)" ``` hoelzl@50347 ` 1647` ``` let ?D = "\f' x. f' (inverse x) * - (inverse x ^ Suc (Suc 0))" ``` hoelzl@50347 ` 1648` hoelzl@50347 ` 1649` ``` show "LIM x ?R. ?G x :> at_top" ``` hoelzl@50347 ` 1650` ``` using g_0 unfolding filterlim_at_top_to_right . ``` hoelzl@50347 ` 1651` hoelzl@50347 ` 1652` ``` show "eventually (\x. DERIV ?G x :> ?D g' x) ?R" ``` hoelzl@50347 ` 1653` ``` unfolding eventually_at_right_to_top ``` hoelzl@50347 ` 1654` ``` using Dg eventually_ge_at_top[where c="1::real"] ``` hoelzl@50347 ` 1655` ``` apply eventually_elim ``` hoelzl@50347 ` 1656` ``` apply (rule DERIV_cong) ``` hoelzl@50347 ` 1657` ``` apply (rule DERIV_chain'[where f=inverse]) ``` hoelzl@50347 ` 1658` ``` apply (auto intro!: DERIV_inverse) ``` hoelzl@50347 ` 1659` ``` done ``` hoelzl@50347 ` 1660` hoelzl@50347 ` 1661` ``` show "eventually (\x. DERIV ?F x :> ?D f' x) ?R" ``` hoelzl@50347 ` 1662` ``` unfolding eventually_at_right_to_top ``` hoelzl@50347 ` 1663` ``` using Df eventually_ge_at_top[where c="1::real"] ``` hoelzl@50347 ` 1664` ``` apply eventually_elim ``` hoelzl@50347 ` 1665` ``` apply (rule DERIV_cong) ``` hoelzl@50347 ` 1666` ``` apply (rule DERIV_chain'[where f=inverse]) ``` hoelzl@50347 ` 1667` ``` apply (auto intro!: DERIV_inverse) ``` hoelzl@50347 ` 1668` ``` done ``` hoelzl@50347 ` 1669` hoelzl@50347 ` 1670` ``` show "eventually (\x. ?D g' x \ 0) ?R" ``` hoelzl@50347 ` 1671` ``` unfolding eventually_at_right_to_top ``` hoelzl@50347 ` 1672` ``` using g' eventually_ge_at_top[where c="1::real"] ``` hoelzl@50347 ` 1673` ``` by eventually_elim auto ``` hoelzl@50347 ` 1674` ``` ``` hoelzl@50347 ` 1675` ``` show "((\x. ?D f' x / ?D g' x) ---> x) ?R" ``` hoelzl@50347 ` 1676` ``` unfolding filterlim_at_right_to_top ``` hoelzl@50347 ` 1677` ``` apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim]) ``` hoelzl@50347 ` 1678` ``` using eventually_ge_at_top[where c="1::real"] ``` hoelzl@50347 ` 1679` ``` by eventually_elim simp ``` hoelzl@50347 ` 1680` ```qed ``` hoelzl@50347 ` 1681` huffman@21164 ` 1682` ```end ```