1(* Title: HOL/Deriv.thy 2 Author: Jacques D. Fleuriot, University of Cambridge, 1998 3 Author: Brian Huffman 4 Author: Lawrence C Paulson, 2004 5 Author: Benjamin Porter, 2005 6*) 7 8section \<open>Differentiation\<close> 9 10theory Deriv 11 imports Limits 12begin 13 14subsection \<open>Frechet derivative\<close> 15 16definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 17 ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> bool" (infix "(has'_derivative)" 50) 18 where "(f has_derivative f') F \<longleftrightarrow> 19 bounded_linear f' \<and> 20 ((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) \<longlongrightarrow> 0) F" 21 22text \<open> 23 Usually the filter @{term F} is @{term "at x within s"}. @{term "(f has_derivative D) 24 (at x within s)"} means: @{term D} is the derivative of function @{term f} at point @{term x} 25 within the set @{term s}. Where @{term s} is used to express left or right sided derivatives. In 26 most cases @{term s} is either a variable or @{term UNIV}. 27\<close> 28 29text \<open>These are the only cases we'll care about, probably.\<close> 30 31lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow> 32 bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)" 33 unfolding has_derivative_def tendsto_iff 34 by (subst eventually_Lim_ident_at) (auto simp add: field_simps) 35 36lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F" 37 by simp 38 39definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool" 40 (infix "(has'_field'_derivative)" 50) 41 where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative ( * ) D) F" 42 43lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F" 44 by simp 45 46definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool" 47 (infix "has'_vector'_derivative" 50) 48 where "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net" 49 50lemma has_vector_derivative_eq_rhs: 51 "(f has_vector_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_vector_derivative Y) F" 52 by simp 53 54named_theorems derivative_intros "structural introduction rules for derivatives" 55setup \<open> 56 let 57 val eq_thms = @{thms has_derivative_eq_rhs DERIV_cong has_vector_derivative_eq_rhs} 58 fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms 59 in 60 Global_Theory.add_thms_dynamic 61 (\<^binding>\<open>derivative_eq_intros\<close>, 62 fn context => 63 Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros} 64 |> map_filter eq_rule) 65 end; 66\<close> 67 68text \<open> 69 The following syntax is only used as a legacy syntax. 70\<close> 71abbreviation (input) 72 FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" 73 ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) 74 where "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)" 75 76lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'" 77 by (simp add: has_derivative_def) 78 79lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'" 80 using bounded_linear.linear[OF has_derivative_bounded_linear] . 81 82lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F" 83 by (simp add: has_derivative_def) 84 85lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) (at a)" 86 by (metis eq_id_iff has_derivative_ident) 87 88lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F" 89 by (simp add: has_derivative_def) 90 91lemma (in bounded_linear) bounded_linear: "bounded_linear f" .. 92 93lemma (in bounded_linear) has_derivative: 94 "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F" 95 unfolding has_derivative_def 96 by (auto simp add: bounded_linear_compose [OF bounded_linear] scaleR diff dest: tendsto) 97 98lemmas has_derivative_scaleR_right [derivative_intros] = 99 bounded_linear.has_derivative [OF bounded_linear_scaleR_right] 100 101lemmas has_derivative_scaleR_left [derivative_intros] = 102 bounded_linear.has_derivative [OF bounded_linear_scaleR_left] 103 104lemmas has_derivative_mult_right [derivative_intros] = 105 bounded_linear.has_derivative [OF bounded_linear_mult_right] 106 107lemmas has_derivative_mult_left [derivative_intros] = 108 bounded_linear.has_derivative [OF bounded_linear_mult_left] 109 110lemma has_derivative_add[simp, derivative_intros]: 111 assumes f: "(f has_derivative f') F" 112 and g: "(g has_derivative g') F" 113 shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F" 114 unfolding has_derivative_def 115proof safe 116 let ?x = "Lim F (\<lambda>x. x)" 117 let ?D = "\<lambda>f f' y. ((f y - f ?x) - f' (y - ?x)) /\<^sub>R norm (y - ?x)" 118 have "((\<lambda>x. ?D f f' x + ?D g g' x) \<longlongrightarrow> (0 + 0)) F" 119 using f g by (intro tendsto_add) (auto simp: has_derivative_def) 120 then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) \<longlongrightarrow> 0) F" 121 by (simp add: field_simps scaleR_add_right scaleR_diff_right) 122qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear) 123 124lemma has_derivative_sum[simp, derivative_intros]: 125 "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F) \<Longrightarrow> 126 ((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F" 127 by (induct I rule: infinite_finite_induct) simp_all 128 129lemma has_derivative_minus[simp, derivative_intros]: 130 "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F" 131 using has_derivative_scaleR_right[of f f' F "-1"] by simp 132 133lemma has_derivative_diff[simp, derivative_intros]: 134 "(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> 135 ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F" 136 by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus) 137 138lemma has_derivative_at_within: 139 "(f has_derivative f') (at x within s) \<longleftrightarrow> 140 (bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s))" 141 by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at) 142 143lemma has_derivative_iff_norm: 144 "(f has_derivative f') (at x within s) \<longleftrightarrow> 145 bounded_linear f' \<and> ((\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)" 146 using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric] 147 by (simp add: has_derivative_at_within divide_inverse ac_simps) 148 149lemma has_derivative_at: 150 "(f has_derivative D) (at x) \<longleftrightarrow> 151 (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) \<midarrow>0\<rightarrow> 0)" 152 unfolding has_derivative_iff_norm LIM_offset_zero_iff[of _ _ x] by simp 153 154lemma field_has_derivative_at: 155 fixes x :: "'a::real_normed_field" 156 shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs") 157proof - 158 have "?lhs = (\<lambda>h. norm (f (x + h) - f x - D * h) / norm h) \<midarrow>0 \<rightarrow> 0" 159 by (simp add: bounded_linear_mult_right has_derivative_at) 160 also have "... = (\<lambda>y. norm ((f (x + y) - f x - D * y) / y)) \<midarrow>0\<rightarrow> 0" 161 by (simp cong: LIM_cong flip: nonzero_norm_divide) 162 also have "... = (\<lambda>y. norm ((f (x + y) - f x) / y - D / y * y)) \<midarrow>0\<rightarrow> 0" 163 by (simp only: diff_divide_distrib times_divide_eq_left [symmetric]) 164 also have "... = ?rhs" 165 by (simp add: tendsto_norm_zero_iff LIM_zero_iff cong: LIM_cong) 166 finally show ?thesis . 167qed 168 169lemma has_derivativeI: 170 "bounded_linear f' \<Longrightarrow> 171 ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s) \<Longrightarrow> 172 (f has_derivative f') (at x within s)" 173 by (simp add: has_derivative_at_within) 174 175lemma has_derivativeI_sandwich: 176 assumes e: "0 < e" 177 and bounded: "bounded_linear f'" 178 and sandwich: "(\<And>y. y \<in> s \<Longrightarrow> y \<noteq> x \<Longrightarrow> dist y x < e \<Longrightarrow> 179 norm ((f y - f x) - f' (y - x)) / norm (y - x) \<le> H y)" 180 and "(H \<longlongrightarrow> 0) (at x within s)" 181 shows "(f has_derivative f') (at x within s)" 182 unfolding has_derivative_iff_norm 183proof safe 184 show "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)" 185 proof (rule tendsto_sandwich[where f="\<lambda>x. 0"]) 186 show "(H \<longlongrightarrow> 0) (at x within s)" by fact 187 show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> H n) (at x within s)" 188 unfolding eventually_at using e sandwich by auto 189 qed (auto simp: le_divide_eq) 190qed fact 191 192lemma has_derivative_subset: 193 "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)" 194 by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset) 195 196lemmas has_derivative_within_subset = has_derivative_subset 197 198lemma has_derivative_within_singleton_iff: 199 "(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g" 200 by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear) 201 202 203subsubsection \<open>Limit transformation for derivatives\<close> 204 205lemma has_derivative_transform_within: 206 assumes "(f has_derivative f') (at x within s)" 207 and "0 < d" 208 and "x \<in> s" 209 and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'" 210 shows "(g has_derivative f') (at x within s)" 211 using assms 212 unfolding has_derivative_within 213 by (force simp add: intro: Lim_transform_within) 214 215lemma has_derivative_transform_within_open: 216 assumes "(f has_derivative f') (at x within t)" 217 and "open s" 218 and "x \<in> s" 219 and "\<And>x. x\<in>s \<Longrightarrow> f x = g x" 220 shows "(g has_derivative f') (at x within t)" 221 using assms unfolding has_derivative_within 222 by (force simp add: intro: Lim_transform_within_open) 223 224lemma has_derivative_transform: 225 assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x" 226 assumes "(f has_derivative f') (at x within s)" 227 shows "(g has_derivative f') (at x within s)" 228 using assms 229 by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto 230 231lemma has_derivative_transform_eventually: 232 assumes "(f has_derivative f') (at x within s)" 233 "(\<forall>\<^sub>F x' in at x within s. f x' = g x')" 234 assumes "f x = g x" "x \<in> s" 235 shows "(g has_derivative f') (at x within s)" 236 using assms 237proof - 238 from assms(2,3) obtain d where "d > 0" "\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'" 239 by (force simp: eventually_at) 240 from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)] 241 show ?thesis . 242qed 243 244 245subsection \<open>Continuity\<close> 246 247lemma has_derivative_continuous: 248 assumes f: "(f has_derivative f') (at x within s)" 249 shows "continuous (at x within s) f" 250proof - 251 from f interpret F: bounded_linear f' 252 by (rule has_derivative_bounded_linear) 253 note F.tendsto[tendsto_intros] 254 let ?L = "\<lambda>f. (f \<longlongrightarrow> 0) (at x within s)" 255 have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x))" 256 using f unfolding has_derivative_iff_norm by blast 257 then have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m) 258 by (rule tendsto_mult_zero) (auto intro!: tendsto_eq_intros) 259 also have "?m \<longleftrightarrow> ?L (\<lambda>y. norm ((f y - f x) - f' (y - x)))" 260 by (intro filterlim_cong) (simp_all add: eventually_at_filter) 261 finally have "?L (\<lambda>y. (f y - f x) - f' (y - x))" 262 by (rule tendsto_norm_zero_cancel) 263 then have "?L (\<lambda>y. ((f y - f x) - f' (y - x)) + f' (y - x))" 264 by (rule tendsto_eq_intros) (auto intro!: tendsto_eq_intros simp: F.zero) 265 then have "?L (\<lambda>y. f y - f x)" 266 by simp 267 from tendsto_add[OF this tendsto_const, of "f x"] show ?thesis 268 by (simp add: continuous_within) 269qed 270 271 272subsection \<open>Composition\<close> 273 274lemma tendsto_at_iff_tendsto_nhds_within: 275 "f x = y \<Longrightarrow> (f \<longlongrightarrow> y) (at x within s) \<longleftrightarrow> (f \<longlongrightarrow> y) (inf (nhds x) (principal s))" 276 unfolding tendsto_def eventually_inf_principal eventually_at_filter 277 by (intro ext all_cong imp_cong) (auto elim!: eventually_mono) 278 279lemma has_derivative_in_compose: 280 assumes f: "(f has_derivative f') (at x within s)" 281 and g: "(g has_derivative g') (at (f x) within (f`s))" 282 shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)" 283proof - 284 from f interpret F: bounded_linear f' 285 by (rule has_derivative_bounded_linear) 286 from g interpret G: bounded_linear g' 287 by (rule has_derivative_bounded_linear) 288 from F.bounded obtain kF where kF: "\<And>x. norm (f' x) \<le> norm x * kF" 289 by fast 290 from G.bounded obtain kG where kG: "\<And>x. norm (g' x) \<le> norm x * kG" 291 by fast 292 note G.tendsto[tendsto_intros] 293 294 let ?L = "\<lambda>f. (f \<longlongrightarrow> 0) (at x within s)" 295 let ?D = "\<lambda>f f' x y. (f y - f x) - f' (y - x)" 296 let ?N = "\<lambda>f f' x y. norm (?D f f' x y) / norm (y - x)" 297 let ?gf = "\<lambda>x. g (f x)" and ?gf' = "\<lambda>x. g' (f' x)" 298 define Nf where "Nf = ?N f f' x" 299 define Ng where [abs_def]: "Ng y = ?N g g' (f x) (f y)" for y 300 301 show ?thesis 302 proof (rule has_derivativeI_sandwich[of 1]) 303 show "bounded_linear (\<lambda>x. g' (f' x))" 304 using f g by (blast intro: bounded_linear_compose has_derivative_bounded_linear) 305 next 306 fix y :: 'a 307 assume neq: "y \<noteq> x" 308 have "?N ?gf ?gf' x y = norm (g' (?D f f' x y) + ?D g g' (f x) (f y)) / norm (y - x)" 309 by (simp add: G.diff G.add field_simps) 310 also have "\<dots> \<le> norm (g' (?D f f' x y)) / norm (y - x) + Ng y * (norm (f y - f x) / norm (y - x))" 311 by (simp add: add_divide_distrib[symmetric] divide_right_mono norm_triangle_ineq G.zero Ng_def) 312 also have "\<dots> \<le> Nf y * kG + Ng y * (Nf y + kF)" 313 proof (intro add_mono mult_left_mono) 314 have "norm (f y - f x) = norm (?D f f' x y + f' (y - x))" 315 by simp 316 also have "\<dots> \<le> norm (?D f f' x y) + norm (f' (y - x))" 317 by (rule norm_triangle_ineq) 318 also have "\<dots> \<le> norm (?D f f' x y) + norm (y - x) * kF" 319 using kF by (intro add_mono) simp 320 finally show "norm (f y - f x) / norm (y - x) \<le> Nf y + kF" 321 by (simp add: neq Nf_def field_simps) 322 qed (use kG in \<open>simp_all add: Ng_def Nf_def neq zero_le_divide_iff field_simps\<close>) 323 finally show "?N ?gf ?gf' x y \<le> Nf y * kG + Ng y * (Nf y + kF)" . 324 next 325 have [tendsto_intros]: "?L Nf" 326 using f unfolding has_derivative_iff_norm Nf_def .. 327 from f have "(f \<longlongrightarrow> f x) (at x within s)" 328 by (blast intro: has_derivative_continuous continuous_within[THEN iffD1]) 329 then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))" 330 unfolding filterlim_def 331 by (simp add: eventually_filtermap eventually_at_filter le_principal) 332 333 have "((?N g g' (f x)) \<longlongrightarrow> 0) (at (f x) within f`s)" 334 using g unfolding has_derivative_iff_norm .. 335 then have g': "((?N g g' (f x)) \<longlongrightarrow> 0) (inf (nhds (f x)) (principal (f`s)))" 336 by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp 337 338 have [tendsto_intros]: "?L Ng" 339 unfolding Ng_def by (rule filterlim_compose[OF g' f']) 340 show "((\<lambda>y. Nf y * kG + Ng y * (Nf y + kF)) \<longlongrightarrow> 0) (at x within s)" 341 by (intro tendsto_eq_intros) auto 342 qed simp 343qed 344 345lemma has_derivative_compose: 346 "(f has_derivative f') (at x within s) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> 347 ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)" 348 by (blast intro: has_derivative_in_compose has_derivative_subset) 349 350lemma has_derivative_in_compose2: 351 assumes "\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)" 352 assumes "f ` s \<subseteq> t" "x \<in> s" 353 assumes "(f has_derivative f') (at x within s)" 354 shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)" 355 using assms 356 by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g]) 357 358lemma (in bounded_bilinear) FDERIV: 359 assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" 360 shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)" 361proof - 362 from bounded_linear.bounded [OF has_derivative_bounded_linear [OF f]] 363 obtain KF where norm_F: "\<And>x. norm (f' x) \<le> norm x * KF" by fast 364 365 from pos_bounded obtain K 366 where K: "0 < K" and norm_prod: "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" 367 by fast 368 let ?D = "\<lambda>f f' y. f y - f x - f' (y - x)" 369 let ?N = "\<lambda>f f' y. norm (?D f f' y) / norm (y - x)" 370 define Ng where "Ng = ?N g g'" 371 define Nf where "Nf = ?N f f'" 372 373 let ?fun1 = "\<lambda>y. norm (f y ** g y - f x ** g x - (f x ** g' (y - x) + f' (y - x) ** g x)) / norm (y - x)" 374 let ?fun2 = "\<lambda>y. norm (f x) * Ng y * K + Nf y * norm (g y) * K + KF * norm (g y - g x) * K" 375 let ?F = "at x within s" 376 377 show ?thesis 378 proof (rule has_derivativeI_sandwich[of 1]) 379 show "bounded_linear (\<lambda>h. f x ** g' h + f' h ** g x)" 380 by (intro bounded_linear_add 381 bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left] 382 has_derivative_bounded_linear [OF g] has_derivative_bounded_linear [OF f]) 383 next 384 from g have "(g \<longlongrightarrow> g x) ?F" 385 by (intro continuous_within[THEN iffD1] has_derivative_continuous) 386 moreover from f g have "(Nf \<longlongrightarrow> 0) ?F" "(Ng \<longlongrightarrow> 0) ?F" 387 by (simp_all add: has_derivative_iff_norm Ng_def Nf_def) 388 ultimately have "(?fun2 \<longlongrightarrow> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F" 389 by (intro tendsto_intros) (simp_all add: LIM_zero_iff) 390 then show "(?fun2 \<longlongrightarrow> 0) ?F" 391 by simp 392 next 393 fix y :: 'd 394 assume "y \<noteq> x" 395 have "?fun1 y = 396 norm (f x ** ?D g g' y + ?D f f' y ** g y + f' (y - x) ** (g y - g x)) / norm (y - x)" 397 by (simp add: diff_left diff_right add_left add_right field_simps) 398 also have "\<dots> \<le> (norm (f x) * norm (?D g g' y) * K + norm (?D f f' y) * norm (g y) * K + 399 norm (y - x) * KF * norm (g y - g x) * K) / norm (y - x)" 400 by (intro divide_right_mono mult_mono' 401 order_trans [OF norm_triangle_ineq add_mono] 402 order_trans [OF norm_prod mult_right_mono] 403 mult_nonneg_nonneg order_refl norm_ge_zero norm_F 404 K [THEN order_less_imp_le]) 405 also have "\<dots> = ?fun2 y" 406 by (simp add: add_divide_distrib Ng_def Nf_def) 407 finally show "?fun1 y \<le> ?fun2 y" . 408 qed simp 409qed 410 411lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult] 412lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR] 413 414lemma has_derivative_prod[simp, derivative_intros]: 415 fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_field" 416 shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within S)) \<Longrightarrow> 417 ((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within S)" 418proof (induct I rule: infinite_finite_induct) 419 case infinite 420 then show ?case by simp 421next 422 case empty 423 then show ?case by simp 424next 425 case (insert i I) 426 let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)" 427 have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within S)" 428 using insert by (intro has_derivative_mult) auto 429 also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))" 430 using insert(1,2) 431 by (auto simp add: sum_distrib_left insert_Diff_if intro!: ext sum.cong) 432 finally show ?case 433 using insert by simp 434qed 435 436lemma has_derivative_power[simp, derivative_intros]: 437 fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field" 438 assumes f: "(f has_derivative f') (at x within S)" 439 shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within S)" 440 using has_derivative_prod[OF f, of "{..< n}"] by (simp add: prod_constant ac_simps) 441 442lemma has_derivative_inverse': 443 fixes x :: "'a::real_normed_div_algebra" 444 assumes x: "x \<noteq> 0" 445 shows "(inverse has_derivative (\<lambda>h. - (inverse x * h * inverse x))) (at x within S)" 446 (is "(_ has_derivative ?f) _") 447proof (rule has_derivativeI_sandwich) 448 show "bounded_linear (\<lambda>h. - (inverse x * h * inverse x))" 449 by (simp add: bounded_linear_minus bounded_linear_mult_const bounded_linear_mult_right) 450 show "0 < norm x" using x by simp 451 have "(inverse \<longlongrightarrow> inverse x) (at x within S)" 452 using tendsto_inverse tendsto_ident_at x by auto 453 then show "((\<lambda>y. norm (inverse y - inverse x) * norm (inverse x)) \<longlongrightarrow> 0) (at x within S)" 454 by (simp add: LIM_zero_iff tendsto_mult_left_zero tendsto_norm_zero) 455next 456 fix y :: 'a 457 assume h: "y \<noteq> x" "dist y x < norm x" 458 then have "y \<noteq> 0" by auto 459 have "norm (inverse y - inverse x - ?f (y -x)) / norm (y - x) 460 = norm (- (inverse y * (y - x) * inverse x - inverse x * (y - x) * inverse x)) / 461 norm (y - x)" 462 by (simp add: \<open>y \<noteq> 0\<close> inverse_diff_inverse x) 463 also have "... = norm ((inverse y - inverse x) * (y - x) * inverse x) / norm (y - x)" 464 by (simp add: left_diff_distrib norm_minus_commute) 465 also have "\<dots> \<le> norm (inverse y - inverse x) * norm (y - x) * norm (inverse x) / norm (y - x)" 466 by (simp add: norm_mult) 467 also have "\<dots> = norm (inverse y - inverse x) * norm (inverse x)" 468 by simp 469 finally show "norm (inverse y - inverse x - ?f (y -x)) / norm (y - x) \<le> 470 norm (inverse y - inverse x) * norm (inverse x)" . 471qed 472 473lemma has_derivative_inverse[simp, derivative_intros]: 474 fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra" 475 assumes x: "f x \<noteq> 0" 476 and f: "(f has_derivative f') (at x within S)" 477 shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))) 478 (at x within S)" 479 using has_derivative_compose[OF f has_derivative_inverse', OF x] . 480 481lemma has_derivative_divide[simp, derivative_intros]: 482 fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra" 483 assumes f: "(f has_derivative f') (at x within S)" 484 and g: "(g has_derivative g') (at x within S)" 485 assumes x: "g x \<noteq> 0" 486 shows "((\<lambda>x. f x / g x) has_derivative 487 (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within S)" 488 using has_derivative_mult[OF f has_derivative_inverse[OF x g]] 489 by (simp add: field_simps) 490 491 492text \<open>Conventional form requires mult-AC laws. Types real and complex only.\<close> 493 494lemma has_derivative_divide'[derivative_intros]: 495 fixes f :: "_ \<Rightarrow> 'a::real_normed_field" 496 assumes f: "(f has_derivative f') (at x within S)" 497 and g: "(g has_derivative g') (at x within S)" 498 and x: "g x \<noteq> 0" 499 shows "((\<lambda>x. f x / g x) has_derivative (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within S)" 500proof - 501 have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) = 502 (f' h * g x - f x * g' h) / (g x * g x)" for h 503 by (simp add: field_simps x) 504 then show ?thesis 505 using has_derivative_divide [OF f g] x 506 by simp 507qed 508 509 510subsection \<open>Uniqueness\<close> 511 512text \<open> 513This can not generally shown for @{const has_derivative}, as we need to approach the point from 514all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>. 515\<close> 516 517lemma has_derivative_at2: "(f has_derivative f') (at x) \<longleftrightarrow> 518 bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)" 519 using has_derivative_within [of f f' x UNIV] 520 by simp 521lemma has_derivative_zero_unique: 522 assumes "((\<lambda>x. 0) has_derivative F) (at x)" 523 shows "F = (\<lambda>h. 0)" 524proof - 525 interpret F: bounded_linear F 526 using assms by (rule has_derivative_bounded_linear) 527 let ?r = "\<lambda>h. norm (F h) / norm h" 528 have *: "?r \<midarrow>0\<rightarrow> 0" 529 using assms unfolding has_derivative_at by simp 530 show "F = (\<lambda>h. 0)" 531 proof 532 show "F h = 0" for h 533 proof (rule ccontr) 534 assume **: "\<not> ?thesis" 535 then have h: "h \<noteq> 0" 536 by (auto simp add: F.zero) 537 with ** have "0 < ?r h" 538 by simp 539 from LIM_D [OF * this] obtain S 540 where S: "0 < S" and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < S \<Longrightarrow> ?r x < ?r h" 541 by auto 542 from dense [OF S] obtain t where t: "0 < t \<and> t < S" .. 543 let ?x = "scaleR (t / norm h) h" 544 have "?x \<noteq> 0" and "norm ?x < S" 545 using t h by simp_all 546 then have "?r ?x < ?r h" 547 by (rule r) 548 then show False 549 using t h by (simp add: F.scaleR) 550 qed 551 qed 552qed 553 554lemma has_derivative_unique: 555 assumes "(f has_derivative F) (at x)" 556 and "(f has_derivative F') (at x)" 557 shows "F = F'" 558proof - 559 have "((\<lambda>x. 0) has_derivative (\<lambda>h. F h - F' h)) (at x)" 560 using has_derivative_diff [OF assms] by simp 561 then have "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)" 562 by (rule has_derivative_zero_unique) 563 then show "F = F'" 564 unfolding fun_eq_iff right_minus_eq . 565qed 566 567 568subsection \<open>Differentiability predicate\<close> 569 570definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" 571 (infix "differentiable" 50) 572 where "f differentiable F \<longleftrightarrow> (\<exists>D. (f has_derivative D) F)" 573 574lemma differentiable_subset: 575 "f differentiable (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable (at x within t)" 576 unfolding differentiable_def by (blast intro: has_derivative_subset) 577 578lemmas differentiable_within_subset = differentiable_subset 579 580lemma differentiable_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable F" 581 unfolding differentiable_def by (blast intro: has_derivative_ident) 582 583lemma differentiable_const [simp, derivative_intros]: "(\<lambda>z. a) differentiable F" 584 unfolding differentiable_def by (blast intro: has_derivative_const) 585 586lemma differentiable_in_compose: 587 "f differentiable (at (g x) within (g`s)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> 588 (\<lambda>x. f (g x)) differentiable (at x within s)" 589 unfolding differentiable_def by (blast intro: has_derivative_in_compose) 590 591lemma differentiable_compose: 592 "f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> 593 (\<lambda>x. f (g x)) differentiable (at x within s)" 594 by (blast intro: differentiable_in_compose differentiable_subset) 595 596lemma differentiable_add [simp, derivative_intros]: 597 "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F" 598 unfolding differentiable_def by (blast intro: has_derivative_add) 599 600lemma differentiable_sum[simp, derivative_intros]: 601 assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net" 602 shows "(\<lambda>x. sum (\<lambda>a. f a x) s) differentiable net" 603proof - 604 from bchoice[OF assms(2)[unfolded differentiable_def]] 605 show ?thesis 606 by (auto intro!: has_derivative_sum simp: differentiable_def) 607qed 608 609lemma differentiable_minus [simp, derivative_intros]: 610 "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F" 611 unfolding differentiable_def by (blast intro: has_derivative_minus) 612 613lemma differentiable_diff [simp, derivative_intros]: 614 "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x - g x) differentiable F" 615 unfolding differentiable_def by (blast intro: has_derivative_diff) 616 617lemma differentiable_mult [simp, derivative_intros]: 618 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 619 shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> 620 (\<lambda>x. f x * g x) differentiable (at x within s)" 621 unfolding differentiable_def by (blast intro: has_derivative_mult) 622 623lemma differentiable_inverse [simp, derivative_intros]: 624 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field" 625 shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> 626 (\<lambda>x. inverse (f x)) differentiable (at x within s)" 627 unfolding differentiable_def by (blast intro: has_derivative_inverse) 628 629lemma differentiable_divide [simp, derivative_intros]: 630 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field" 631 shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> 632 g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)" 633 unfolding divide_inverse by simp 634 635lemma differentiable_power [simp, derivative_intros]: 636 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field" 637 shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)" 638 unfolding differentiable_def by (blast intro: has_derivative_power) 639 640lemma differentiable_scaleR [simp, derivative_intros]: 641 "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> 642 (\<lambda>x. f x *\<^sub>R g x) differentiable (at x within s)" 643 unfolding differentiable_def by (blast intro: has_derivative_scaleR) 644 645lemma has_derivative_imp_has_field_derivative: 646 "(f has_derivative D) F \<Longrightarrow> (\<And>x. x * D' = D x) \<Longrightarrow> (f has_field_derivative D') F" 647 unfolding has_field_derivative_def 648 by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult.commute) 649 650lemma has_field_derivative_imp_has_derivative: 651 "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative ( * ) D) F" 652 by (simp add: has_field_derivative_def) 653 654lemma DERIV_subset: 655 "(f has_field_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> 656 (f has_field_derivative f') (at x within t)" 657 by (simp add: has_field_derivative_def has_derivative_within_subset) 658 659lemma has_field_derivative_at_within: 660 "(f has_field_derivative f') (at x) \<Longrightarrow> (f has_field_derivative f') (at x within s)" 661 using DERIV_subset by blast 662 663abbreviation (input) 664 DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 665 ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) 666 where "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)" 667 668abbreviation has_real_derivative :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real filter \<Rightarrow> bool" 669 (infix "(has'_real'_derivative)" 50) 670 where "(f has_real_derivative D) F \<equiv> (f has_field_derivative D) F" 671 672lemma real_differentiable_def: 673 "f differentiable at x within s \<longleftrightarrow> (\<exists>D. (f has_real_derivative D) (at x within s))" 674proof safe 675 assume "f differentiable at x within s" 676 then obtain f' where *: "(f has_derivative f') (at x within s)" 677 unfolding differentiable_def by auto 678 then obtain c where "f' = (( * ) c)" 679 by (metis real_bounded_linear has_derivative_bounded_linear mult.commute fun_eq_iff) 680 with * show "\<exists>D. (f has_real_derivative D) (at x within s)" 681 unfolding has_field_derivative_def by auto 682qed (auto simp: differentiable_def has_field_derivative_def) 683 684lemma real_differentiableE [elim?]: 685 assumes f: "f differentiable (at x within s)" 686 obtains df where "(f has_real_derivative df) (at x within s)" 687 using assms by (auto simp: real_differentiable_def) 688 689lemma differentiableD: 690 "f differentiable (at x within s) \<Longrightarrow> \<exists>D. (f has_real_derivative D) (at x within s)" 691 by (auto elim: real_differentiableE) 692 693lemma differentiableI: 694 "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)" 695 by (force simp add: real_differentiable_def) 696 697lemma has_field_derivative_iff: 698 "(f has_field_derivative D) (at x within S) \<longleftrightarrow> 699 ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)" 700proof - 701 have "((\<lambda>y. norm (f y - f x - D * (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within S) 702 = ((\<lambda>y. (f y - f x) / (y - x) - D) \<longlongrightarrow> 0) (at x within S)" 703 apply (subst tendsto_norm_zero_iff[symmetric], rule filterlim_cong) 704 apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide) 705 done 706 then show ?thesis 707 by (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right LIM_zero_iff) 708qed 709 710lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" 711 unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff .. 712 713lemma mult_commute_abs: "(\<lambda>x. x * c) = ( * ) c" 714 for c :: "'a::ab_semigroup_mult" 715 by (simp add: fun_eq_iff mult.commute) 716 717lemma DERIV_compose_FDERIV: 718 fixes f::"real\<Rightarrow>real" 719 assumes "DERIV f (g x) :> f'" 720 assumes "(g has_derivative g') (at x within s)" 721 shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)" 722 using assms has_derivative_compose[of g g' x s f "( * ) f'"] 723 by (auto simp: has_field_derivative_def ac_simps) 724 725 726subsection \<open>Vector derivative\<close> 727 728lemma has_field_derivative_iff_has_vector_derivative: 729 "(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F" 730 unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs .. 731 732lemma has_field_derivative_subset: 733 "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> 734 (f has_field_derivative y) (at x within t)" 735 unfolding has_field_derivative_def by (rule has_derivative_subset) 736 737lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net" 738 by (auto simp: has_vector_derivative_def) 739 740lemma has_vector_derivative_id[simp, derivative_intros]: "((\<lambda>x. x) has_vector_derivative 1) net" 741 by (auto simp: has_vector_derivative_def) 742 743lemma has_vector_derivative_minus[derivative_intros]: 744 "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net" 745 by (auto simp: has_vector_derivative_def) 746 747lemma has_vector_derivative_add[derivative_intros]: 748 "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow> 749 ((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net" 750 by (auto simp: has_vector_derivative_def scaleR_right_distrib) 751 752lemma has_vector_derivative_sum[derivative_intros]: 753 "(\<And>i. i \<in> I \<Longrightarrow> (f i has_vector_derivative f' i) net) \<Longrightarrow> 754 ((\<lambda>x. \<Sum>i\<in>I. f i x) has_vector_derivative (\<Sum>i\<in>I. f' i)) net" 755 by (auto simp: has_vector_derivative_def fun_eq_iff scaleR_sum_right intro!: derivative_eq_intros) 756 757lemma has_vector_derivative_diff[derivative_intros]: 758 "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow> 759 ((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net" 760 by (auto simp: has_vector_derivative_def scaleR_diff_right) 761 762lemma has_vector_derivative_add_const: 763 "((\<lambda>t. g t + z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net" 764 apply (intro iffI) 765 apply (force dest: has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const]) 766 apply (force dest: has_vector_derivative_add [OF _ has_vector_derivative_const]) 767 done 768 769lemma has_vector_derivative_diff_const: 770 "((\<lambda>t. g t - z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net" 771 using has_vector_derivative_add_const [where z = "-z"] 772 by simp 773 774lemma (in bounded_linear) has_vector_derivative: 775 assumes "(g has_vector_derivative g') F" 776 shows "((\<lambda>x. f (g x)) has_vector_derivative f g') F" 777 using has_derivative[OF assms[unfolded has_vector_derivative_def]] 778 by (simp add: has_vector_derivative_def scaleR) 779 780lemma (in bounded_bilinear) has_vector_derivative: 781 assumes "(f has_vector_derivative f') (at x within s)" 782 and "(g has_vector_derivative g') (at x within s)" 783 shows "((\<lambda>x. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)" 784 using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]] 785 by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib) 786 787lemma has_vector_derivative_scaleR[derivative_intros]: 788 "(f has_field_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow> 789 ((\<lambda>x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)" 790 unfolding has_field_derivative_iff_has_vector_derivative 791 by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR]) 792 793lemma has_vector_derivative_mult[derivative_intros]: 794 "(f has_vector_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow> 795 ((\<lambda>x. f x * g x) has_vector_derivative (f x * g' + f' * g x)) (at x within s)" 796 for f g :: "real \<Rightarrow> 'a::real_normed_algebra" 797 by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult]) 798 799lemma has_vector_derivative_of_real[derivative_intros]: 800 "(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F" 801 by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real]) 802 (simp add: has_field_derivative_iff_has_vector_derivative) 803 804lemma has_vector_derivative_continuous: 805 "(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f" 806 by (auto intro: has_derivative_continuous simp: has_vector_derivative_def) 807 808lemma has_vector_derivative_mult_right[derivative_intros]: 809 fixes a :: "'a::real_normed_algebra" 810 shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. a * f x) has_vector_derivative (a * x)) F" 811 by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_right]) 812 813lemma has_vector_derivative_mult_left[derivative_intros]: 814 fixes a :: "'a::real_normed_algebra" 815 shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * a) has_vector_derivative (x * a)) F" 816 by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left]) 817 818 819subsection \<open>Derivatives\<close> 820 821lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" 822 by (simp add: DERIV_def) 823 824lemma has_field_derivativeD: 825 "(f has_field_derivative D) (at x within S) \<Longrightarrow> 826 ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)" 827 by (simp add: has_field_derivative_iff) 828 829lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F" 830 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto 831 832lemma DERIV_ident [simp, derivative_intros]: "((\<lambda>x. x) has_field_derivative 1) F" 833 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto 834 835lemma field_differentiable_add[derivative_intros]: 836 "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> 837 ((\<lambda>z. f z + g z) has_field_derivative f' + g') F" 838 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add]) 839 (auto simp: has_field_derivative_def field_simps mult_commute_abs) 840 841corollary DERIV_add: 842 "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow> 843 ((\<lambda>x. f x + g x) has_field_derivative D + E) (at x within s)" 844 by (rule field_differentiable_add) 845 846lemma field_differentiable_minus[derivative_intros]: 847 "(f has_field_derivative f') F \<Longrightarrow> ((\<lambda>z. - (f z)) has_field_derivative -f') F" 848 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus]) 849 (auto simp: has_field_derivative_def field_simps mult_commute_abs) 850 851corollary DERIV_minus: 852 "(f has_field_derivative D) (at x within s) \<Longrightarrow> 853 ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)" 854 by (rule field_differentiable_minus) 855 856lemma field_differentiable_diff[derivative_intros]: 857 "(f has_field_derivative f') F \<Longrightarrow> 858 (g has_field_derivative g') F \<Longrightarrow> ((\<lambda>z. f z - g z) has_field_derivative f' - g') F" 859 by (simp only: diff_conv_add_uminus field_differentiable_add field_differentiable_minus) 860 861corollary DERIV_diff: 862 "(f has_field_derivative D) (at x within s) \<Longrightarrow> 863 (g has_field_derivative E) (at x within s) \<Longrightarrow> 864 ((\<lambda>x. f x - g x) has_field_derivative D - E) (at x within s)" 865 by (rule field_differentiable_diff) 866 867lemma DERIV_continuous: "(f has_field_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f" 868 by (drule has_derivative_continuous[OF has_field_derivative_imp_has_derivative]) simp 869 870corollary DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x" 871 by (rule DERIV_continuous) 872 873lemma DERIV_continuous_on: 874 "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x within s)) \<Longrightarrow> continuous_on s f" 875 unfolding continuous_on_eq_continuous_within 876 by (intro continuous_at_imp_continuous_on ballI DERIV_continuous) 877 878lemma DERIV_mult': 879 "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow> 880 ((\<lambda>x. f x * g x) has_field_derivative f x * E + D * g x) (at x within s)" 881 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult]) 882 (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative) 883 884lemma DERIV_mult[derivative_intros]: 885 "(f has_field_derivative Da) (at x within s) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow> 886 ((\<lambda>x. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)" 887 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult]) 888 (auto simp: field_simps dest: has_field_derivative_imp_has_derivative) 889 890text \<open>Derivative of linear multiplication\<close> 891 892lemma DERIV_cmult: 893 "(f has_field_derivative D) (at x within s) \<Longrightarrow> 894 ((\<lambda>x. c * f x) has_field_derivative c * D) (at x within s)" 895 by (drule DERIV_mult' [OF DERIV_const]) simp 896 897lemma DERIV_cmult_right: 898 "(f has_field_derivative D) (at x within s) \<Longrightarrow> 899 ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)" 900 using DERIV_cmult by (auto simp add: ac_simps) 901 902lemma DERIV_cmult_Id [simp]: "(( * ) c has_field_derivative c) (at x within s)" 903 using DERIV_ident [THEN DERIV_cmult, where c = c and x = x] by simp 904 905lemma DERIV_cdivide: 906 "(f has_field_derivative D) (at x within s) \<Longrightarrow> 907 ((\<lambda>x. f x / c) has_field_derivative D / c) (at x within s)" 908 using DERIV_cmult_right[of f D x s "1 / c"] by simp 909 910lemma DERIV_unique: "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E" 911 unfolding DERIV_def by (rule LIM_unique) 912 913lemma DERIV_sum[derivative_intros]: 914 "(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow> 915 ((\<lambda>x. sum (f x) S) has_field_derivative sum (f' x) S) F" 916 by (rule has_derivative_imp_has_field_derivative [OF has_derivative_sum]) 917 (auto simp: sum_distrib_left mult_commute_abs dest: has_field_derivative_imp_has_derivative) 918 919lemma DERIV_inverse'[derivative_intros]: 920 assumes "(f has_field_derivative D) (at x within s)" 921 and "f x \<noteq> 0" 922 shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) 923 (at x within s)" 924proof - 925 have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative ( * ) D)" 926 by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff) 927 with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)" 928 by (auto dest!: has_field_derivative_imp_has_derivative) 929 then show ?thesis using \<open>f x \<noteq> 0\<close> 930 by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse) 931qed 932 933text \<open>Power of \<open>-1\<close>\<close> 934 935lemma DERIV_inverse: 936 "x \<noteq> 0 \<Longrightarrow> ((\<lambda>x. inverse(x)) has_field_derivative - (inverse x ^ Suc (Suc 0))) (at x within s)" 937 by (drule DERIV_inverse' [OF DERIV_ident]) simp 938 939text \<open>Derivative of inverse\<close> 940 941lemma DERIV_inverse_fun: 942 "(f has_field_derivative d) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> 943 ((\<lambda>x. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)" 944 by (drule (1) DERIV_inverse') (simp add: ac_simps nonzero_inverse_mult_distrib) 945 946text \<open>Derivative of quotient\<close> 947 948lemma DERIV_divide[derivative_intros]: 949 "(f has_field_derivative D) (at x within s) \<Longrightarrow> 950 (g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> 951 ((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)" 952 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_divide]) 953 (auto dest: has_field_derivative_imp_has_derivative simp: field_simps) 954 955lemma DERIV_quotient: 956 "(f has_field_derivative d) (at x within s) \<Longrightarrow> 957 (g has_field_derivative e) (at x within s)\<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> 958 ((\<lambda>y. f y / g y) has_field_derivative (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))) (at x within s)" 959 by (drule (2) DERIV_divide) (simp add: mult.commute) 960 961lemma DERIV_power_Suc: 962 "(f has_field_derivative D) (at x within s) \<Longrightarrow> 963 ((\<lambda>x. f x ^ Suc n) has_field_derivative (1 + of_nat n) * (D * f x ^ n)) (at x within s)" 964 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power]) 965 (auto simp: has_field_derivative_def) 966 967lemma DERIV_power[derivative_intros]: 968 "(f has_field_derivative D) (at x within s) \<Longrightarrow> 969 ((\<lambda>x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)" 970 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power]) 971 (auto simp: has_field_derivative_def) 972 973lemma DERIV_pow: "((\<lambda>x. x ^ n) has_field_derivative real n * (x ^ (n - Suc 0))) (at x within s)" 974 using DERIV_power [OF DERIV_ident] by simp 975 976lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow> 977 ((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)" 978 using has_derivative_compose[of f "( * ) D" x s g "( * ) E"] 979 by (simp only: has_field_derivative_def mult_commute_abs ac_simps) 980 981corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow> 982 ((\<lambda>x. f (g x)) has_field_derivative Da * Db) (at x within s)" 983 by (rule DERIV_chain') 984 985text \<open>Standard version\<close> 986 987lemma DERIV_chain: 988 "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow> 989 (f \<circ> g has_field_derivative Da * Db) (at x within s)" 990 by (drule (1) DERIV_chain', simp add: o_def mult.commute) 991 992lemma DERIV_image_chain: 993 "(f has_field_derivative Da) (at (g x) within (g ` s)) \<Longrightarrow> 994 (g has_field_derivative Db) (at x within s) \<Longrightarrow> 995 (f \<circ> g has_field_derivative Da * Db) (at x within s)" 996 using has_derivative_in_compose [of g "( * ) Db" x s f "( * ) Da "] 997 by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps) 998 999(*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*) 1000lemma DERIV_chain_s: 1001 assumes "(\<And>x. x \<in> s \<Longrightarrow> DERIV g x :> g'(x))" 1002 and "DERIV f x :> f'" 1003 and "f x \<in> s" 1004 shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)" 1005 by (metis (full_types) DERIV_chain' mult.commute assms) 1006 1007lemma DERIV_chain3: (*HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV*) 1008 assumes "(\<And>x. DERIV g x :> g'(x))" 1009 and "DERIV f x :> f'" 1010 shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)" 1011 by (metis UNIV_I DERIV_chain_s [of UNIV] assms) 1012 1013text \<open>Alternative definition for differentiability\<close> 1014 1015lemma DERIV_LIM_iff: 1016 fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" 1017 shows "((\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0\<rightarrow> D) = ((\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D)" (is "?lhs = ?rhs") 1018proof 1019 assume ?lhs 1020 then have "(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>0 - - a\<rightarrow> D" 1021 by (rule LIM_offset) 1022 then show ?rhs 1023 by simp 1024next 1025 assume ?rhs 1026 then have "(\<lambda>x. (f (x+a) - f a) / ((x+a) - a)) \<midarrow>a-a\<rightarrow> D" 1027 by (rule LIM_offset) 1028 then show ?lhs 1029 by (simp add: add.commute) 1030qed 1031 1032lemma has_field_derivative_cong_ev: 1033 assumes "x = y" 1034 and *: "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x = g x) (nhds x)" 1035 and "u = v" "S = t" "x \<in> S" 1036 shows "(f has_field_derivative u) (at x within S) = (g has_field_derivative v) (at y within t)" 1037 unfolding has_field_derivative_iff 1038proof (rule filterlim_cong) 1039 from assms have "f y = g y" 1040 by (auto simp: eventually_nhds) 1041 with * show "\<forall>\<^sub>F z in at x within S. (f z - f x) / (z - x) = (g z - g y) / (z - y)" 1042 unfolding eventually_at_filter 1043 by eventually_elim (auto simp: assms \<open>f y = g y\<close>) 1044qed (simp_all add: assms) 1045 1046lemma has_field_derivative_cong_eventually: 1047 assumes "eventually (\<lambda>x. f x = g x) (at x within S)" "f x = g x" 1048 shows "(f has_field_derivative u) (at x within S) = (g has_field_derivative u) (at x within S)" 1049 unfolding has_field_derivative_iff 1050proof (rule tendsto_cong) 1051 show "\<forall>\<^sub>F y in at x within S. (f y - f x) / (y - x) = (g y - g x) / (y - x)" 1052 using assms by (auto elim: eventually_mono) 1053qed 1054 1055lemma DERIV_cong_ev: 1056 "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow> 1057 DERIV f x :> u \<longleftrightarrow> DERIV g y :> v" 1058 by (rule has_field_derivative_cong_ev) simp_all 1059 1060lemma DERIV_shift: 1061 "(f has_field_derivative y) (at (x + z)) = ((\<lambda>x. f (x + z)) has_field_derivative y) (at x)" 1062 by (simp add: DERIV_def field_simps) 1063 1064lemma DERIV_mirror: "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x)) x :> - y)" 1065 for f :: "real \<Rightarrow> real" and x y :: real 1066 by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right 1067 tendsto_minus_cancel_left field_simps conj_commute) 1068 1069lemma floor_has_real_derivative: 1070 fixes f :: "real \<Rightarrow> 'a::{floor_ceiling,order_topology}" 1071 assumes "isCont f x" 1072 and "f x \<notin> \<int>" 1073 shows "((\<lambda>x. floor (f x)) has_real_derivative 0) (at x)" 1074proof (subst DERIV_cong_ev[OF refl _ refl]) 1075 show "((\<lambda>_. floor (f x)) has_real_derivative 0) (at x)" 1076 by simp 1077 have "\<forall>\<^sub>F y in at x. \<lfloor>f y\<rfloor> = \<lfloor>f x\<rfloor>" 1078 by (rule eventually_floor_eq[OF assms[unfolded continuous_at]]) 1079 then show "\<forall>\<^sub>F y in nhds x. real_of_int \<lfloor>f y\<rfloor> = real_of_int \<lfloor>f x\<rfloor>" 1080 unfolding eventually_at_filter 1081 by eventually_elim auto 1082qed 1083 1084lemmas has_derivative_floor[derivative_intros] = 1085 floor_has_real_derivative[THEN DERIV_compose_FDERIV] 1086 1087text \<open>Caratheodory formulation of derivative at a point\<close> 1088 1089lemma CARAT_DERIV: 1090 "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)" 1091 (is "?lhs = ?rhs") 1092proof 1093 assume ?lhs 1094 show "\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l" 1095 proof (intro exI conjI) 1096 let ?g = "(\<lambda>z. if z = x then l else (f z - f x) / (z-x))" 1097 show "\<forall>z. f z - f x = ?g z * (z - x)" 1098 by simp 1099 show "isCont ?g x" 1100 using \<open>?lhs\<close> by (simp add: isCont_iff DERIV_def cong: LIM_equal [rule_format]) 1101 show "?g x = l" 1102 by simp 1103 qed 1104next 1105 assume ?rhs 1106 then show ?lhs 1107 by (auto simp add: isCont_iff DERIV_def cong: LIM_cong) 1108qed 1109 1110 1111subsection \<open>Local extrema\<close> 1112 1113text \<open>If @{term "0 < f' x"} then @{term x} is Locally Strictly Increasing At The Right.\<close> 1114 1115lemma has_real_derivative_pos_inc_right: 1116 fixes f :: "real \<Rightarrow> real" 1117 assumes der: "(f has_real_derivative l) (at x within S)" 1118 and l: "0 < l" 1119 shows "\<exists>d > 0. \<forall>h > 0. x + h \<in> S \<longrightarrow> h < d \<longrightarrow> f x < f (x + h)" 1120 using assms 1121proof - 1122 from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at] 1123 obtain s where s: "0 < s" 1124 and all: "\<And>xa. xa\<in>S \<Longrightarrow> xa \<noteq> x \<and> dist xa x < s \<longrightarrow> \<bar>(f xa - f x) / (xa - x) - l\<bar> < l" 1125 by (auto simp: dist_real_def) 1126 then show ?thesis 1127 proof (intro exI conjI strip) 1128 show "0 < s" by (rule s) 1129 next 1130 fix h :: real 1131 assume "0 < h" "h < s" "x + h \<in> S" 1132 with all [of "x + h"] show "f x < f (x+h)" 1133 proof (simp add: abs_if dist_real_def pos_less_divide_eq split: if_split_asm) 1134 assume "\<not> (f (x + h) - f x) / h < l" and h: "0 < h" 1135 with l have "0 < (f (x + h) - f x) / h" 1136 by arith 1137 then show "f x < f (x + h)" 1138 by (simp add: pos_less_divide_eq h) 1139 qed 1140 qed 1141qed 1142 1143lemma DERIV_pos_inc_right: 1144 fixes f :: "real \<Rightarrow> real" 1145 assumes der: "DERIV f x :> l" 1146 and l: "0 < l" 1147 shows "\<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f x < f (x + h)" 1148 using has_real_derivative_pos_inc_right[OF assms] 1149 by auto 1150 1151lemma has_real_derivative_neg_dec_left: 1152 fixes f :: "real \<Rightarrow> real" 1153 assumes der: "(f has_real_derivative l) (at x within S)" 1154 and "l < 0" 1155 shows "\<exists>d > 0. \<forall>h > 0. x - h \<in> S \<longrightarrow> h < d \<longrightarrow> f x < f (x - h)" 1156proof - 1157 from \<open>l < 0\<close> have l: "- l > 0" 1158 by simp 1159 from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at] 1160 obtain s where s: "0 < s" 1161 and all: "\<And>xa. xa\<in>S \<Longrightarrow> xa \<noteq> x \<and> dist xa x < s \<longrightarrow> \<bar>(f xa - f x) / (xa - x) - l\<bar> < - l" 1162 by (auto simp: dist_real_def) 1163 then show ?thesis 1164 proof (intro exI conjI strip) 1165 show "0 < s" by (rule s) 1166 next 1167 fix h :: real 1168 assume "0 < h" "h < s" "x - h \<in> S" 1169 with all [of "x - h"] show "f x < f (x-h)" 1170 proof (simp add: abs_if pos_less_divide_eq dist_real_def split: if_split_asm) 1171 assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h" 1172 with l have "0 < (f (x-h) - f x) / h" 1173 by arith 1174 then show "f x < f (x - h)" 1175 by (simp add: pos_less_divide_eq h) 1176 qed 1177 qed 1178qed 1179 1180lemma DERIV_neg_dec_left: 1181 fixes f :: "real \<Rightarrow> real" 1182 assumes der: "DERIV f x :> l" 1183 and l: "l < 0" 1184 shows "\<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f x < f (x - h)" 1185 using has_real_derivative_neg_dec_left[OF assms] 1186 by auto 1187 1188lemma has_real_derivative_pos_inc_left: 1189 fixes f :: "real \<Rightarrow> real" 1190 shows "(f has_real_derivative l) (at x within S) \<Longrightarrow> 0 < l \<Longrightarrow> 1191 \<exists>d>0. \<forall>h>0. x - h \<in> S \<longrightarrow> h < d \<longrightarrow> f (x - h) < f x" 1192 by (rule has_real_derivative_neg_dec_left [of "\<lambda>x. - f x" "-l" x S, simplified]) 1193 (auto simp add: DERIV_minus) 1194 1195lemma DERIV_pos_inc_left: 1196 fixes f :: "real \<Rightarrow> real" 1197 shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f (x - h) < f x" 1198 using has_real_derivative_pos_inc_left 1199 by blast 1200 1201lemma has_real_derivative_neg_dec_right: 1202 fixes f :: "real \<Rightarrow> real" 1203 shows "(f has_real_derivative l) (at x within S) \<Longrightarrow> l < 0 \<Longrightarrow> 1204 \<exists>d > 0. \<forall>h > 0. x + h \<in> S \<longrightarrow> h < d \<longrightarrow> f x > f (x + h)" 1205 by (rule has_real_derivative_pos_inc_right [of "\<lambda>x. - f x" "-l" x S, simplified]) 1206 (auto simp add: DERIV_minus) 1207 1208lemma DERIV_neg_dec_right: 1209 fixes f :: "real \<Rightarrow> real" 1210 shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f x > f (x + h)" 1211 using has_real_derivative_neg_dec_right by blast 1212 1213lemma DERIV_local_max: 1214 fixes f :: "real \<Rightarrow> real" 1215 assumes der: "DERIV f x :> l" 1216 and d: "0 < d" 1217 and le: "\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f y \<le> f x" 1218 shows "l = 0" 1219proof (cases rule: linorder_cases [of l 0]) 1220 case equal 1221 then show ?thesis . 1222next 1223 case less 1224 from DERIV_neg_dec_left [OF der less] 1225 obtain d' where d': "0 < d'" and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x - h)" 1226 by blast 1227 obtain e where "0 < e \<and> e < d \<and> e < d'" 1228 using field_lbound_gt_zero [OF d d'] .. 1229 with lt le [THEN spec [where x="x - e"]] show ?thesis 1230 by (auto simp add: abs_if) 1231next 1232 case greater 1233 from DERIV_pos_inc_right [OF der greater] 1234 obtain d' where d': "0 < d'" and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" 1235 by blast 1236 obtain e where "0 < e \<and> e < d \<and> e < d'" 1237 using field_lbound_gt_zero [OF d d'] .. 1238 with lt le [THEN spec [where x="x + e"]] show ?thesis 1239 by (auto simp add: abs_if) 1240qed 1241 1242text \<open>Similar theorem for a local minimum\<close> 1243lemma DERIV_local_min: 1244 fixes f :: "real \<Rightarrow> real" 1245 shows "DERIV f x :> l \<Longrightarrow> 0 < d \<Longrightarrow> \<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f x \<le> f y \<Longrightarrow> l = 0" 1246 by (drule DERIV_minus [THEN DERIV_local_max]) auto 1247 1248 1249text\<open>In particular, if a function is locally flat\<close> 1250lemma DERIV_local_const: 1251 fixes f :: "real \<Rightarrow> real" 1252 shows "DERIV f x :> l \<Longrightarrow> 0 < d \<Longrightarrow> \<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f x = f y \<Longrightarrow> l = 0" 1253 by (auto dest!: DERIV_local_max) 1254 1255 1256subsection \<open>Rolle's Theorem\<close> 1257 1258text \<open>Lemma about introducing open ball in open interval\<close> 1259lemma lemma_interval_lt: 1260 fixes a b x :: real 1261 assumes "a < x" "x < b" 1262 shows "\<exists>d. 0 < d \<and> (\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a < y \<and> y < b)" 1263 using linorder_linear [of "x - a" "b - x"] 1264proof 1265 assume "x - a \<le> b - x" 1266 with assms show ?thesis 1267 by (rule_tac x = "x - a" in exI) auto 1268next 1269 assume "b - x \<le> x - a" 1270 with assms show ?thesis 1271 by (rule_tac x = "b - x" in exI) auto 1272qed 1273 1274lemma lemma_interval: "a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b)" 1275 for a b x :: real 1276 by (force dest: lemma_interval_lt) 1277 1278text \<open>Rolle's Theorem. 1279 If @{term f} is defined and continuous on the closed interval 1280 \<open>[a,b]\<close> and differentiable on the open interval \<open>(a,b)\<close>, 1281 and @{term "f a = f b"}, 1282 then there exists \<open>x0 \<in> (a,b)\<close> such that @{term "f' x0 = 0"}\<close> 1283theorem Rolle: 1284 fixes a b :: real 1285 assumes lt: "a < b" 1286 and eq: "f a = f b" 1287 and con: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x" 1288 and dif [rule_format]: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)" 1289 shows "\<exists>z. a < z \<and> z < b \<and> DERIV f z :> 0" 1290proof - 1291 have le: "a \<le> b" 1292 using lt by simp 1293 from isCont_eq_Ub [OF le con] 1294 obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x" and "a \<le> x" "x \<le> b" 1295 by blast 1296 from isCont_eq_Lb [OF le con] 1297 obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z" and "a \<le> x'" "x' \<le> b" 1298 by blast 1299 consider "a < x" "x < b" | "x = a \<or> x = b" 1300 using \<open>a \<le> x\<close> \<open>x \<le> b\<close> by arith 1301 then show ?thesis 1302 proof cases 1303 case 1 1304 \<comment> \<open>@{term f} attains its maximum within the interval\<close> 1305 obtain d where d: "0 < d" and bound: "\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" 1306 using lemma_interval [OF 1] by blast 1307 then have bound': "\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f y \<le> f x" 1308 using x_max by blast 1309 obtain l where der: "DERIV f x :> l" 1310 using differentiableD [OF dif [OF conjI [OF 1]]] .. 1311 \<comment> \<open>the derivative at a local maximum is zero\<close> 1312 have "l = 0" 1313 by (rule DERIV_local_max [OF der d bound']) 1314 with 1 der show ?thesis by auto 1315 next 1316 case 2 1317 then have fx: "f b = f x" by (auto simp add: eq) 1318 consider "a < x'" "x' < b" | "x' = a \<or> x' = b" 1319 using \<open>a \<le> x'\<close> \<open>x' \<le> b\<close> by arith 1320 then show ?thesis 1321 proof cases 1322 case 1 1323 \<comment> \<open>@{term f} attains its minimum within the interval\<close> 1324 from lemma_interval [OF 1] 1325 obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" 1326 by blast 1327 then have bound': "\<forall>y. \<bar>x' - y\<bar> < d \<longrightarrow> f x' \<le> f y" 1328 using x'_min by blast 1329 from differentiableD [OF dif [OF conjI [OF 1]]] 1330 obtain l where der: "DERIV f x' :> l" .. 1331 have "l = 0" by (rule DERIV_local_min [OF der d bound']) 1332 \<comment> \<open>the derivative at a local minimum is zero\<close> 1333 then show ?thesis using 1 der by auto 1334 next 1335 case 2 1336 \<comment> \<open>@{term f} is constant throughout the interval\<close> 1337 then have fx': "f b = f x'" by (auto simp: eq) 1338 from dense [OF lt] obtain r where r: "a < r" "r < b" by blast 1339 obtain d where d: "0 < d" and bound: "\<forall>y. \<bar>r - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" 1340 using lemma_interval [OF r] by blast 1341 have eq_fb: "f z = f b" if "a \<le> z" and "z \<le> b" for z 1342 proof (rule order_antisym) 1343 show "f z \<le> f b" by (simp add: fx x_max that) 1344 show "f b \<le> f z" by (simp add: fx' x'_min that) 1345 qed 1346 have bound': "\<forall>y. \<bar>r - y\<bar> < d \<longrightarrow> f r = f y" 1347 proof (intro strip) 1348 fix y :: real 1349 assume lt: "\<bar>r - y\<bar> < d" 1350 then have "f y = f b" by (simp add: eq_fb bound) 1351 then show "f r = f y" by (simp add: eq_fb r order_less_imp_le) 1352 qed 1353 obtain l where der: "DERIV f r :> l" 1354 using differentiableD [OF dif [OF conjI [OF r]]] .. 1355 have "l = 0" 1356 by (rule DERIV_local_const [OF der d bound']) 1357 \<comment> \<open>the derivative of a constant function is zero\<close> 1358 with r der show ?thesis by auto 1359 qed 1360 qed 1361qed 1362 1363 1364subsection \<open>Mean Value Theorem\<close> 1365 1366lemma lemma_MVT: "f a - (f b - f a) / (b - a) * a = f b - (f b - f a) / (b - a) * b" 1367 for a b :: real 1368 by (cases "a = b") (simp_all add: field_simps) 1369 1370theorem MVT: 1371 fixes a b :: real 1372 assumes lt: "a < b" 1373 and con: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 1374 and dif: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)" 1375 shows "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l" 1376proof - 1377 let ?F = "\<lambda>x. f x - ((f b - f a) / (b - a)) * x" 1378 have cont_f: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" 1379 using con by (fast intro: continuous_intros) 1380 have dif_f: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable (at x)" 1381 proof clarify 1382 fix x :: real 1383 assume x: "a < x" "x < b" 1384 obtain l where der: "DERIV f x :> l" 1385 using differentiableD [OF dif] x by blast 1386 show "?F differentiable (at x)" 1387 by (rule differentiableI [where D = "l - (f b - f a) / (b - a)"], 1388 blast intro: DERIV_diff DERIV_cmult_Id der) 1389 qed 1390 from Rolle [where f = ?F, OF lt lemma_MVT cont_f dif_f] 1391 obtain z where z: "a < z" "z < b" and der: "DERIV ?F z :> 0" 1392 by blast 1393 have "DERIV (\<lambda>x. ((f b - f a) / (b - a)) * x) z :> (f b - f a) / (b - a)" 1394 by (rule DERIV_cmult_Id) 1395 then have der_f: "DERIV (\<lambda>x. ?F x + (f b - f a) / (b - a) * x) z :> 0 + (f b - f a) / (b - a)" 1396 by (rule DERIV_add [OF der]) 1397 show ?thesis 1398 proof (intro exI conjI) 1399 show "a < z" and "z < b" using z . 1400 show "f b - f a = (b - a) * ((f b - f a) / (b - a))" by simp 1401 show "DERIV f z :> ((f b - f a) / (b - a))" using der_f by simp 1402 qed 1403qed 1404 1405corollary MVT2: 1406 assumes "a < b" and der: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> DERIV f x :> f' x" 1407 shows "\<exists>z::real. a < z \<and> z < b \<and> (f b - f a = (b - a) * f' z)" 1408proof - 1409 have "\<exists>l z. a < z \<and> 1410 z < b \<and> 1411 (f has_real_derivative l) (at z) \<and> 1412 f b - f a = (b - a) * l" 1413 proof (rule MVT [OF \<open>a < b\<close>]) 1414 show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 1415 using assms by (blast intro: DERIV_isCont) 1416 show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)" 1417 using assms by (force dest: order_less_imp_le simp add: real_differentiable_def) 1418 qed 1419 with assms show ?thesis 1420 by (blast dest: DERIV_unique order_less_imp_le) 1421qed 1422 1423lemma pos_deriv_imp_strict_mono: 1424 assumes "\<And>x. (f has_real_derivative f' x) (at x)" 1425 assumes "\<And>x. f' x > 0" 1426 shows "strict_mono f" 1427proof (rule strict_monoI) 1428 fix x y :: real assume xy: "x < y" 1429 from assms and xy have "\<exists>z>x. z < y \<and> f y - f x = (y - x) * f' z" 1430 by (intro MVT2) (auto dest: connectedD_interval) 1431 then obtain z where z: "z > x" "z < y" "f y - f x = (y - x) * f' z" by blast 1432 note \<open>f y - f x = (y - x) * f' z\<close> 1433 also have "(y - x) * f' z > 0" using xy assms by (intro mult_pos_pos) auto 1434 finally show "f x < f y" by simp 1435qed 1436 1437 1438subsubsection \<open>A function is constant if its derivative is 0 over an interval.\<close> 1439 1440lemma DERIV_isconst_end: 1441 fixes f :: "real \<Rightarrow> real" 1442 assumes "a < b" and contf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 1443 and 0: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0" 1444 shows "f b = f a" 1445 using MVT [OF \<open>a < b\<close>] "0" DERIV_unique contf real_differentiable_def by fastforce 1446 1447lemma DERIV_isconst2: 1448 fixes f :: "real \<Rightarrow> real" 1449 assumes "a < b" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0" 1450 and "a \<le> x" "x \<le> b" 1451shows "f x = f a" 1452proof (cases "x=a") 1453 case False 1454 show ?thesis 1455 by (rule DERIV_isconst_end [where f=f]) (use False assms in auto) 1456qed auto 1457 1458lemma DERIV_isconst3: 1459 fixes a b x y :: real 1460 assumes "a < b" 1461 and "x \<in> {a <..< b}" 1462 and "y \<in> {a <..< b}" 1463 and derivable: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> DERIV f x :> 0" 1464 shows "f x = f y" 1465proof (cases "x = y") 1466 case False 1467 let ?a = "min x y" 1468 let ?b = "max x y" 1469 1470 have "DERIV f z :> 0" if "?a \<le> z" "z \<le> ?b" for z 1471 proof - 1472 have "a < z" and "z < b" 1473 using that \<open>x \<in> {a <..< b}\<close> and \<open>y \<in> {a <..< b}\<close> by auto 1474 then have "z \<in> {a<..<b}" by auto 1475 then show "DERIV f z :> 0" by (rule derivable) 1476 qed 1477 then have isCont: "\<And>z. \<lbrakk>?a \<le> z; z \<le> ?b\<rbrakk> \<Longrightarrow> isCont f z" 1478 and DERIV: "\<And>z. \<lbrakk>?a < z; z < ?b\<rbrakk> \<Longrightarrow> DERIV f z :> 0" 1479 using DERIV_isCont by auto 1480 1481 have "?a < ?b" using \<open>x \<noteq> y\<close> by auto 1482 from DERIV_isconst2[OF this isCont DERIV, of x] and DERIV_isconst2[OF this isCont DERIV, of y] 1483 show ?thesis by auto 1484qed auto 1485 1486lemma DERIV_isconst_all: 1487 fixes f :: "real \<Rightarrow> real" 1488 shows "\<forall>x. DERIV f x :> 0 \<Longrightarrow> f x = f y" 1489 apply (rule linorder_cases [of x y]) 1490 apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+ 1491 done 1492 1493lemma DERIV_const_ratio_const: 1494 fixes f :: "real \<Rightarrow> real" 1495 assumes "a \<noteq> b" and df: "\<And>x. DERIV f x :> k" 1496 shows "f b - f a = (b - a) * k" 1497proof (cases a b rule: linorder_cases) 1498 case less 1499 show ?thesis 1500 using MVT [OF less] df by (auto dest: DERIV_isCont DERIV_unique simp: real_differentiable_def) 1501next 1502 case greater 1503 show ?thesis 1504 using MVT [OF greater] df 1505 by (fastforce dest: DERIV_continuous DERIV_unique simp: real_differentiable_def algebra_simps) 1506qed auto 1507 1508lemma DERIV_const_ratio_const2: 1509 fixes f :: "real \<Rightarrow> real" 1510 assumes "a \<noteq> b" and df: "\<And>x. DERIV f x :> k" 1511 shows "(f b - f a) / (b - a) = k" 1512 using DERIV_const_ratio_const [OF assms] \<open>a \<noteq> b\<close> by auto 1513 1514lemma real_average_minus_first [simp]: "(a + b) / 2 - a = (b - a) / 2" 1515 for a b :: real 1516 by simp 1517 1518lemma real_average_minus_second [simp]: "(b + a) / 2 - a = (b - a) / 2" 1519 for a b :: real 1520 by simp 1521 1522text \<open>Gallileo's "trick": average velocity = av. of end velocities.\<close> 1523 1524lemma DERIV_const_average: 1525 fixes v :: "real \<Rightarrow> real" 1526 and a b :: real 1527 assumes neq: "a \<noteq> b" 1528 and der: "\<And>x. DERIV v x :> k" 1529 shows "v ((a + b) / 2) = (v a + v b) / 2" 1530proof (cases rule: linorder_cases [of a b]) 1531 case equal 1532 with neq show ?thesis by simp 1533next 1534 case less 1535 have "(v b - v a) / (b - a) = k" 1536 by (rule DERIV_const_ratio_const2 [OF neq der]) 1537 then have "(b - a) * ((v b - v a) / (b - a)) = (b - a) * k" 1538 by simp 1539 moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k" 1540 by (rule DERIV_const_ratio_const2 [OF _ der]) (simp add: neq) 1541 ultimately show ?thesis 1542 using neq by force 1543next 1544 case greater 1545 have "(v b - v a) / (b - a) = k" 1546 by (rule DERIV_const_ratio_const2 [OF neq der]) 1547 then have "(b - a) * ((v b - v a) / (b - a)) = (b - a) * k" 1548 by simp 1549 moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k" 1550 by (rule DERIV_const_ratio_const2 [OF _ der]) (simp add: neq) 1551 ultimately show ?thesis 1552 using neq by (force simp add: add.commute) 1553qed 1554 1555subsubsection\<open>A function with positive derivative is increasing\<close> 1556text \<open>A simple proof using the MVT, by Jeremy Avigad. And variants.\<close> 1557lemma DERIV_pos_imp_increasing_open: 1558 fixes a b :: real 1559 and f :: "real \<Rightarrow> real" 1560 assumes "a < b" 1561 and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y > 0)" 1562 and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x" 1563 shows "f a < f b" 1564proof (rule ccontr) 1565 assume f: "\<not> ?thesis" 1566 have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l" 1567 by (rule MVT) (use assms Deriv.differentiableI in \<open>force+\<close>) 1568 then obtain l z where z: "a < z" "z < b" "DERIV f z :> l" and "f b - f a = (b - a) * l" 1569 by auto 1570 with assms f have "\<not> l > 0" 1571 by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le) 1572 with assms z show False 1573 by (metis DERIV_unique) 1574qed 1575 1576lemma DERIV_pos_imp_increasing: 1577 fixes a b :: real 1578 and f :: "real \<Rightarrow> real" 1579 assumes "a < b" 1580 and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y > 0)" 1581 shows "f a < f b" 1582 by (metis DERIV_pos_imp_increasing_open [of a b f] assms DERIV_continuous less_imp_le) 1583 1584lemma DERIV_nonneg_imp_nondecreasing: 1585 fixes a b :: real 1586 and f :: "real \<Rightarrow> real" 1587 assumes "a \<le> b" 1588 and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y \<ge> 0" 1589 shows "f a \<le> f b" 1590proof (rule ccontr, cases "a = b") 1591 assume "\<not> ?thesis" and "a = b" 1592 then show False by auto 1593next 1594 assume *: "\<not> ?thesis" 1595 assume "a \<noteq> b" 1596 with \<open>a \<le> b\<close> have "a < b" 1597 by linarith 1598 with assms have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l" 1599 by (metis (no_types) not_le not_less_iff_gr_or_eq 1600 MVT [OF \<open>a < b\<close>, of f] DERIV_isCont [of f] differentiableI) 1601 then obtain l z where lz: "a < z" "z < b" "DERIV f z :> l" and **: "f b - f a = (b - a) * l" 1602 by auto 1603 with * have "a < b" "f b < f a" by auto 1604 with ** have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps) 1605 (metis * add_le_cancel_right assms(1) less_eq_real_def mult_right_mono add_left_mono linear order_refl) 1606 with assms lz show False 1607 by (metis DERIV_unique order_less_imp_le) 1608qed 1609 1610lemma DERIV_neg_imp_decreasing_open: 1611 fixes a b :: real 1612 and f :: "real \<Rightarrow> real" 1613 assumes "a < b" 1614 and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0" 1615 and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x" 1616 shows "f a > f b" 1617proof - 1618 have "(\<lambda>x. -f x) a < (\<lambda>x. -f x) b" 1619 proof (rule DERIV_pos_imp_increasing_open [of a b]) 1620 show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> \<exists>y. ((\<lambda>x. - f x) has_real_derivative y) (at x) \<and> 0 < y" 1621 using assms 1622 by simp (metis field_differentiable_minus neg_0_less_iff_less) 1623 qed (use assms in auto) 1624 then show ?thesis 1625 by simp 1626qed 1627 1628lemma DERIV_neg_imp_decreasing: 1629 fixes a b :: real 1630 and f :: "real \<Rightarrow> real" 1631 assumes "a < b" 1632 and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0" 1633 shows "f a > f b" 1634 by (metis DERIV_neg_imp_decreasing_open [of a b f] assms DERIV_continuous less_imp_le) 1635 1636lemma DERIV_nonpos_imp_nonincreasing: 1637 fixes a b :: real 1638 and f :: "real \<Rightarrow> real" 1639 assumes "a \<le> b" 1640 and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y \<le> 0" 1641 shows "f a \<ge> f b" 1642proof - 1643 have "(\<lambda>x. -f x) a \<le> (\<lambda>x. -f x) b" 1644 using DERIV_nonneg_imp_nondecreasing [of a b "\<lambda>x. -f x"] assms DERIV_minus by fastforce 1645 then show ?thesis 1646 by simp 1647qed 1648 1649lemma DERIV_pos_imp_increasing_at_bot: 1650 fixes f :: "real \<Rightarrow> real" 1651 assumes "\<And>x. x \<le> b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y > 0)" 1652 and lim: "(f \<longlongrightarrow> flim) at_bot" 1653 shows "flim < f b" 1654proof - 1655 have "\<exists>N. \<forall>n\<le>N. f n \<le> f (b - 1)" 1656 by (rule_tac x="b - 2" in exI) (force intro: order.strict_implies_order DERIV_pos_imp_increasing assms) 1657 then have "flim \<le> f (b - 1)" 1658 by (auto simp: eventually_at_bot_linorder tendsto_upperbound [OF lim]) 1659 also have "\<dots> < f b" 1660 by (force intro: DERIV_pos_imp_increasing [where f=f] assms) 1661 finally show ?thesis . 1662qed 1663 1664lemma DERIV_neg_imp_decreasing_at_top: 1665 fixes f :: "real \<Rightarrow> real" 1666 assumes der: "\<And>x. x \<ge> b \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0" 1667 and lim: "(f \<longlongrightarrow> flim) at_top" 1668 shows "flim < f b" 1669 apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\<lambda>i. f (-i)" and b = "-b", simplified]) 1670 apply (metis DERIV_mirror der le_minus_iff neg_0_less_iff_less) 1671 apply (metis filterlim_at_top_mirror lim) 1672 done 1673 1674text \<open>Derivative of inverse function\<close> 1675 1676lemma DERIV_inverse_function: 1677 fixes f g :: "real \<Rightarrow> real" 1678 assumes der: "DERIV f (g x) :> D" 1679 and neq: "D \<noteq> 0" 1680 and x: "a < x" "x < b" 1681 and inj: "\<And>y. \<lbrakk>a < y; y < b\<rbrakk> \<Longrightarrow> f (g y) = y" 1682 and cont: "isCont g x" 1683 shows "DERIV g x :> inverse D" 1684unfolding has_field_derivative_iff 1685proof (rule LIM_equal2) 1686 show "0 < min (x - a) (b - x)" 1687 using x by arith 1688next 1689 fix y 1690 assume "norm (y - x) < min (x - a) (b - x)" 1691 then have "a < y" and "y < b" 1692 by (simp_all add: abs_less_iff) 1693 then show "(g y - g x) / (y - x) = inverse ((f (g y) - x) / (g y - g x))" 1694 by (simp add: inj) 1695next 1696 have "(\<lambda>z. (f z - f (g x)) / (z - g x)) \<midarrow>g x\<rightarrow> D" 1697 by (rule der [unfolded has_field_derivative_iff]) 1698 then have 1: "(\<lambda>z. (f z - x) / (z - g x)) \<midarrow>g x\<rightarrow> D" 1699 using inj x by simp 1700 have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x" 1701 proof (rule exI, safe) 1702 show "0 < min (x - a) (b - x)" 1703 using x by simp 1704 next 1705 fix y 1706 assume "norm (y - x) < min (x - a) (b - x)" 1707 then have y: "a < y" "y < b" 1708 by (simp_all add: abs_less_iff) 1709 assume "g y = g x" 1710 then have "f (g y) = f (g x)" by simp 1711 then have "y = x" using inj y x by simp 1712 also assume "y \<noteq> x" 1713 finally show False by simp 1714 qed 1715 have "(\<lambda>y. (f (g y) - x) / (g y - g x)) \<midarrow>x\<rightarrow> D" 1716 using cont 1 2 by (rule isCont_LIM_compose2) 1717 then show "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x))) \<midarrow>x\<rightarrow> inverse D" 1718 using neq by (rule tendsto_inverse) 1719qed 1720 1721subsection \<open>Generalized Mean Value Theorem\<close> 1722 1723theorem GMVT: 1724 fixes a b :: real 1725 assumes alb: "a < b" 1726 and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x" 1727 and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)" 1728 and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x" 1729 and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable (at x)" 1730 shows "\<exists>g'c f'c c. 1731 DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> (f b - f a) * g'c = (g b - g a) * f'c" 1732proof - 1733 let ?h = "\<lambda>x. (f b - f a) * g x - (g b - g a) * f x" 1734 have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" 1735 proof (rule MVT) 1736 from assms show "a < b" by simp 1737 show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont ?h x" 1738 using fc gc by simp 1739 show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> ?h differentiable (at x)" 1740 using fd gd by simp 1741 qed 1742 then obtain l where l: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" .. 1743 then obtain c where c: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" .. 1744 1745 from c have cint: "a < c \<and> c < b" by auto 1746 with gd have "g differentiable (at c)" by simp 1747 then have "\<exists>D. DERIV g c :> D" by (rule differentiableD) 1748 then obtain g'c where g'c: "DERIV g c :> g'c" .. 1749 1750 from c have "a < c \<and> c < b" by auto 1751 with fd have "f differentiable (at c)" by simp 1752 then have "\<exists>D. DERIV f c :> D" by (rule differentiableD) 1753 then obtain f'c where f'c: "DERIV f c :> f'c" .. 1754 1755 from c have "DERIV ?h c :> l" by auto 1756 moreover have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)" 1757 using g'c f'c by (auto intro!: derivative_eq_intros) 1758 ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique) 1759 1760 have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" 1761 proof - 1762 from c have "?h b - ?h a = (b - a) * l" by auto 1763 also from leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp 1764 finally show ?thesis by simp 1765 qed 1766 moreover have "?h b - ?h a = 0" 1767 proof - 1768 have "?h b - ?h a = 1769 ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) - 1770 ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))" 1771 by (simp add: algebra_simps) 1772 then show ?thesis by auto 1773 qed 1774 ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto 1775 with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp 1776 then have "g'c * (f b - f a) = f'c * (g b - g a)" by simp 1777 then have "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: ac_simps) 1778 with g'c f'c cint show ?thesis by auto 1779qed 1780 1781lemma GMVT': 1782 fixes f g :: "real \<Rightarrow> real" 1783 assumes "a < b" 1784 and isCont_f: "\<And>z. a \<le> z \<Longrightarrow> z \<le> b \<Longrightarrow> isCont f z" 1785 and isCont_g: "\<And>z. a \<le> z \<Longrightarrow> z \<le> b \<Longrightarrow> isCont g z" 1786 and DERIV_g: "\<And>z. a < z \<Longrightarrow> z < b \<Longrightarrow> DERIV g z :> (g' z)" 1787 and DERIV_f: "\<And>z. a < z \<Longrightarrow> z < b \<Longrightarrow> DERIV f z :> (f' z)" 1788 shows "\<exists>c. a < c \<and> c < b \<and> (f b - f a) * g' c = (g b - g a) * f' c" 1789proof - 1790 have "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> 1791 a < c \<and> c < b \<and> (f b - f a) * g'c = (g b - g a) * f'c" 1792 using assms by (intro GMVT) (force simp: real_differentiable_def)+ 1793 then obtain c where "a < c" "c < b" "(f b - f a) * g' c = (g b - g a) * f' c" 1794 using DERIV_f DERIV_g by (force dest: DERIV_unique) 1795 then show ?thesis 1796 by auto 1797qed 1798 1799 1800subsection \<open>L'Hopitals rule\<close> 1801 1802lemma isCont_If_ge: 1803 fixes a :: "'a :: linorder_topology" 1804 assumes "continuous (at_left a) g" and f: "(f \<longlongrightarrow> g a) (at_right a)" 1805 shows "isCont (\<lambda>x. if x \<le> a then g x else f x) a" (is "isCont ?gf a") 1806proof - 1807 have g: "(g \<longlongrightarrow> g a) (at_left a)" 1808 using assms continuous_within by blast 1809 show ?thesis 1810 unfolding isCont_def continuous_within 1811 proof (intro filterlim_split_at; simp) 1812 show "(?gf \<longlongrightarrow> g a) (at_left a)" 1813 by (subst filterlim_cong[OF refl refl, where g=g]) (simp_all add: eventually_at_filter less_le g) 1814 show "(?gf \<longlongrightarrow> g a) (at_right a)" 1815 by (subst filterlim_cong[OF refl refl, where g=f]) (simp_all add: eventually_at_filter less_le f) 1816 qed 1817qed 1818 1819lemma lhopital_right_0: 1820 fixes f0 g0 :: "real \<Rightarrow> real" 1821 assumes f_0: "(f0 \<longlongrightarrow> 0) (at_right 0)" 1822 and g_0: "(g0 \<longlongrightarrow> 0) (at_right 0)" 1823 and ev: 1824 "eventually (\<lambda>x. g0 x \<noteq> 0) (at_right 0)" 1825 "eventually (\<lambda>x. g' x \<noteq> 0) (at_right 0)" 1826 "eventually (\<lambda>x. DERIV f0 x :> f' x) (at_right 0)" 1827 "eventually (\<lambda>x. DERIV g0 x :> g' x) (at_right 0)" 1828 and lim: "filterlim (\<lambda> x. (f' x / g' x)) F (at_right 0)" 1829 shows "filterlim (\<lambda> x. f0 x / g0 x) F (at_right 0)" 1830proof - 1831 define f where [abs_def]: "f x = (if x \<le> 0 then 0 else f0 x)" for x 1832 then have "f 0 = 0" by simp 1833 1834 define g where [abs_def]: "g x = (if x \<le> 0 then 0 else g0 x)" for x 1835 then have "g 0 = 0" by simp 1836 1837 have "eventually (\<lambda>x. g0 x \<noteq> 0 \<and> g' x \<noteq> 0 \<and> 1838 DERIV f0 x :> (f' x) \<and> DERIV g0 x :> (g' x)) (at_right 0)" 1839 using ev by eventually_elim auto 1840 then obtain a where [arith]: "0 < a" 1841 and g0_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g0 x \<noteq> 0" 1842 and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0" 1843 and f0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f0 x :> (f' x)" 1844 and g0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g0 x :> (g' x)" 1845 unfolding eventually_at by (auto simp: dist_real_def) 1846 1847 have g_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g x \<noteq> 0" 1848 using g0_neq_0 by (simp add: g_def) 1849 1850 have f: "DERIV f x :> (f' x)" if x: "0 < x" "x < a" for x 1851 using that 1852 by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ f0[OF x]]) 1853 (auto simp: f_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) 1854 1855 have g: "DERIV g x :> (g' x)" if x: "0 < x" "x < a" for x 1856 using that 1857 by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ g0[OF x]]) 1858 (auto simp: g_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) 1859 1860 have "isCont f 0" 1861 unfolding f_def by (intro isCont_If_ge f_0 continuous_const) 1862 1863 have "isCont g 0" 1864 unfolding g_def by (intro isCont_If_ge g_0 continuous_const) 1865 1866 have "\<exists>\<zeta>. \<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)" 1867 proof (rule bchoice, rule ballI) 1868 fix x 1869 assume "x \<in> {0 <..< a}" 1870 then have x[arith]: "0 < x" "x < a" by auto 1871 with g'_neq_0 g_neq_0 \<open>g 0 = 0\<close> have g': "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> 0 \<noteq> g' x" "g 0 \<noteq> g x" 1872 by auto 1873 have "\<And>x. 0 \<le> x \<Longrightarrow> x < a \<Longrightarrow> isCont f x" 1874 using \<open>isCont f 0\<close> f by (auto intro: DERIV_isCont simp: le_less) 1875 moreover have "\<And>x. 0 \<le> x \<Longrightarrow> x < a \<Longrightarrow> isCont g x" 1876 using \<open>isCont g 0\<close> g by (auto intro: DERIV_isCont simp: le_less) 1877 ultimately have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c" 1878 using f g \<open>x < a\<close> by (intro GMVT') auto 1879 then obtain c where *: "0 < c" "c < x" "(f x - f 0) * g' c = (g x - g 0) * f' c" 1880 by blast 1881 moreover 1882 from * g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" 1883 by (simp add: field_simps) 1884 ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y" 1885 using \<open>f 0 = 0\<close> \<open>g 0 = 0\<close> by (auto intro!: exI[of _ c]) 1886 qed 1887 then obtain \<zeta> where "\<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)" .. 1888 then have \<zeta>: "eventually (\<lambda>x. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)) (at_right 0)" 1889 unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def) 1890 moreover 1891 from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)" 1892 by eventually_elim auto 1893 then have "((\<lambda>x. norm (\<zeta> x)) \<longlongrightarrow> 0) (at_right 0)" 1894 by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"]) auto 1895 then have "(\<zeta> \<longlongrightarrow> 0) (at_right 0)" 1896 by (rule tendsto_norm_zero_cancel) 1897 with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)" 1898 by (auto elim!: eventually_mono simp: filterlim_at) 1899 from this lim have "filterlim (\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) F (at_right 0)" 1900 by (rule_tac filterlim_compose[of _ _ _ \<zeta>]) 1901 ultimately have "filterlim (\<lambda>t. f t / g t) F (at_right 0)" (is ?P) 1902 by (rule_tac filterlim_cong[THEN iffD1, OF refl refl]) 1903 (auto elim: eventually_mono) 1904 also have "?P \<longleftrightarrow> ?thesis" 1905 by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter) 1906 finally show ?thesis . 1907qed 1908 1909lemma lhopital_right: 1910 "(f \<longlongrightarrow> 0) (at_right x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at_right x) \<Longrightarrow> 1911 eventually (\<lambda>x. g x \<noteq> 0) (at_right x) \<Longrightarrow> 1912 eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow> 1913 eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow> 1914 eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow> 1915 filterlim (\<lambda> x. (f' x / g' x)) F (at_right x) \<Longrightarrow> 1916 filterlim (\<lambda> x. f x / g x) F (at_right x)" 1917 for x :: real 1918 unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift 1919 by (rule lhopital_right_0) 1920 1921lemma lhopital_left: 1922 "(f \<longlongrightarrow> 0) (at_left x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at_left x) \<Longrightarrow> 1923 eventually (\<lambda>x. g x \<noteq> 0) (at_left x) \<Longrightarrow> 1924 eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow> 1925 eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow> 1926 eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow> 1927 filterlim (\<lambda> x. (f' x / g' x)) F (at_left x) \<Longrightarrow> 1928 filterlim (\<lambda> x. f x / g x) F (at_left x)" 1929 for x :: real 1930 unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror 1931 by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror) 1932 1933lemma lhopital: 1934 "(f \<longlongrightarrow> 0) (at x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at x) \<Longrightarrow> 1935 eventually (\<lambda>x. g x \<noteq> 0) (at x) \<Longrightarrow> 1936 eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow> 1937 eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow> 1938 eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow> 1939 filterlim (\<lambda> x. (f' x / g' x)) F (at x) \<Longrightarrow> 1940 filterlim (\<lambda> x. f x / g x) F (at x)" 1941 for x :: real 1942 unfolding eventually_at_split filterlim_at_split 1943 by (auto intro!: lhopital_right[of f x g g' f'] lhopital_left[of f x g g' f']) 1944 1945 1946lemma lhopital_right_0_at_top: 1947 fixes f g :: "real \<Rightarrow> real" 1948 assumes g_0: "LIM x at_right 0. g x :> at_top" 1949 and ev: 1950 "eventually (\<lambda>x. g' x \<noteq> 0) (at_right 0)" 1951 "eventually (\<lambda>x. DERIV f x :> f' x) (at_right 0)" 1952 "eventually (\<lambda>x. DERIV g x :> g' x) (at_right 0)" 1953 and lim: "((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> x) (at_right 0)" 1954 shows "((\<lambda> x. f x / g x) \<longlongrightarrow> x) (at_right 0)" 1955 unfolding tendsto_iff 1956proof safe 1957 fix e :: real 1958 assume "0 < e" 1959 with lim[unfolded tendsto_iff, rule_format, of "e / 4"] 1960 have "eventually (\<lambda>t. dist (f' t / g' t) x < e / 4) (at_right 0)" 1961 by simp 1962 from eventually_conj[OF eventually_conj[OF ev(1) ev(2)] eventually_conj[OF ev(3) this]] 1963 obtain a where [arith]: "0 < a" 1964 and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0" 1965 and f0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV f x :> (f' x)" 1966 and g0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV g x :> (g' x)" 1967 and Df: "\<And>t. 0 < t \<Longrightarrow> t < a \<Longrightarrow> dist (f' t / g' t) x < e / 4" 1968 unfolding eventually_at_le by (auto simp: dist_real_def) 1969 1970 from Df have "eventually (\<lambda>t. t < a) (at_right 0)" "eventually (\<lambda>t::real. 0 < t) (at_right 0)" 1971 unfolding eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def) 1972 1973 moreover 1974 have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)" 1975 using g_0 by (auto elim: eventually_mono simp: filterlim_at_top_dense) 1976 1977 moreover 1978 have inv_g: "((\<lambda>x. inverse (g x)) \<longlongrightarrow> 0) (at_right 0)" 1979 using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl] 1980 by (rule filterlim_compose) 1981 then have "((\<lambda>x. norm (1 - g a * inverse (g x))) \<longlongrightarrow> norm (1 - g a * 0)) (at_right 0)" 1982 by (intro tendsto_intros) 1983 then have "((\<lambda>x. norm (1 - g a / g x)) \<longlongrightarrow> 1) (at_right 0)" 1984 by (simp add: inverse_eq_divide) 1985 from this[unfolded tendsto_iff, rule_format, of 1] 1986 have "eventually (\<lambda>x. norm (1 - g a / g x) < 2) (at_right 0)" 1987 by (auto elim!: eventually_mono simp: dist_real_def) 1988 1989 moreover 1990 from inv_g have "((\<lambda>t. norm ((f a - x * g a) * inverse (g t))) \<longlongrightarrow> norm ((f a - x * g a) * 0)) 1991 (at_right 0)" 1992 by (intro tendsto_intros) 1993 then have "((\<lambda>t. norm (f a - x * g a) / norm (g t)) \<longlongrightarrow> 0) (at_right 0)" 1994 by (simp add: inverse_eq_divide) 1995 from this[unfolded tendsto_iff, rule_format, of "e / 2"] \<open>0 < e\<close> 1996 have "eventually (\<lambda>t. norm (f a - x * g a) / norm (g t) < e / 2) (at_right 0)" 1997 by (auto simp: dist_real_def) 1998 1999 ultimately show "eventually (\<lambda>t. dist (f t / g t) x < e) (at_right 0)" 2000 proof eventually_elim 2001 fix t assume t[arith]: "0 < t" "t < a" "g a < g t" "0 < g t" 2002 assume ineq: "norm (1 - g a / g t) < 2" "norm (f a - x * g a) / norm (g t) < e / 2" 2003 2004 have "\<exists>y. t < y \<and> y < a \<and> (g a - g t) * f' y = (f a - f t) * g' y" 2005 using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+ 2006 then obtain y where [arith]: "t < y" "y < a" 2007 and D_eq0: "(g a - g t) * f' y = (f a - f t) * g' y" 2008 by blast 2009 from D_eq0 have D_eq: "(f t - f a) / (g t - g a) = f' y / g' y" 2010 using \<open>g a < g t\<close> g'_neq_0[of y] by (auto simp add: field_simps) 2011 2012 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" 2013 by (simp add: field_simps) 2014 have "norm (f t / g t - x) \<le> 2015 norm (((f t - f a) / (g t - g a) - x) * (1 - g a / g t)) + norm ((f a - x * g a) / g t)" 2016 unfolding * by (rule norm_triangle_ineq) 2017 also have "\<dots> = dist (f' y / g' y) x * norm (1 - g a / g t) + norm (f a - x * g a) / norm (g t)" 2018 by (simp add: abs_mult D_eq dist_real_def) 2019 also have "\<dots> < (e / 4) * 2 + e / 2" 2020 using ineq Df[of y] \<open>0 < e\<close> by (intro add_le_less_mono mult_mono) auto 2021 finally show "dist (f t / g t) x < e" 2022 by (simp add: dist_real_def) 2023 qed 2024qed 2025 2026lemma lhopital_right_at_top: 2027 "LIM x at_right x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow> 2028 eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow> 2029 eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow> 2030 eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow> 2031 ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_right x) \<Longrightarrow> 2032 ((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at_right x)" 2033 unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift 2034 by (rule lhopital_right_0_at_top) 2035 2036lemma lhopital_left_at_top: 2037 "LIM x at_left x. g x :> at_top \<Longrightarrow> 2038 eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow> 2039 eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow> 2040 eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow> 2041 ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_left x) \<Longrightarrow> 2042 ((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at_left x)" 2043 for x :: real 2044 unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror 2045 by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror) 2046 2047lemma lhopital_at_top: 2048 "LIM x at x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow> 2049 eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow> 2050 eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow> 2051 eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow> 2052 ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at x) \<Longrightarrow> 2053 ((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at x)" 2054 unfolding eventually_at_split filterlim_at_split 2055 by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f']) 2056 2057lemma lhospital_at_top_at_top: 2058 fixes f g :: "real \<Rightarrow> real" 2059 assumes g_0: "LIM x at_top. g x :> at_top" 2060 and g': "eventually (\<lambda>x. g' x \<noteq> 0) at_top" 2061 and Df: "eventually (\<lambda>x. DERIV f x :> f' x) at_top" 2062 and Dg: "eventually (\<lambda>x. DERIV g x :> g' x) at_top" 2063 and lim: "((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> x) at_top" 2064 shows "((\<lambda> x. f x / g x) \<longlongrightarrow> x) at_top" 2065 unfolding filterlim_at_top_to_right 2066proof (rule lhopital_right_0_at_top) 2067 let ?F = "\<lambda>x. f (inverse x)" 2068 let ?G = "\<lambda>x. g (inverse x)" 2069 let ?R = "at_right (0::real)" 2070 let ?D = "\<lambda>f' x. f' (inverse x) * - (inverse x ^ Suc (Suc 0))" 2071 show "LIM x ?R. ?G x :> at_top" 2072 using g_0 unfolding filterlim_at_top_to_right . 2073 show "eventually (\<lambda>x. DERIV ?G x :> ?D g' x) ?R" 2074 unfolding eventually_at_right_to_top 2075 using Dg eventually_ge_at_top[where c=1] 2076 by eventually_elim (rule derivative_eq_intros DERIV_chain'[where f=inverse] | simp)+ 2077 show "eventually (\<lambda>x. DERIV ?F x :> ?D f' x) ?R" 2078 unfolding eventually_at_right_to_top 2079 using Df eventually_ge_at_top[where c=1] 2080 by eventually_elim (rule derivative_eq_intros DERIV_chain'[where f=inverse] | simp)+ 2081 show "eventually (\<lambda>x. ?D g' x \<noteq> 0) ?R" 2082 unfolding eventually_at_right_to_top 2083 using g' eventually_ge_at_top[where c=1] 2084 by eventually_elim auto 2085 show "((\<lambda>x. ?D f' x / ?D g' x) \<longlongrightarrow> x) ?R" 2086 unfolding filterlim_at_right_to_top 2087 apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim]) 2088 using eventually_ge_at_top[where c=1] 2089 by eventually_elim simp 2090qed 2091 2092lemma lhopital_right_at_top_at_top: 2093 fixes f g :: "real \<Rightarrow> real" 2094 assumes f_0: "LIM x at_right a. f x :> at_top" 2095 assumes g_0: "LIM x at_right a. g x :> at_top" 2096 and ev: 2097 "eventually (\<lambda>x. DERIV f x :> f' x) (at_right a)" 2098 "eventually (\<lambda>x. DERIV g x :> g' x) (at_right a)" 2099 and lim: "filterlim (\<lambda> x. (f' x / g' x)) at_top (at_right a)" 2100 shows "filterlim (\<lambda> x. f x / g x) at_top (at_right a)" 2101proof - 2102 from lim have pos: "eventually (\<lambda>x. f' x / g' x > 0) (at_right a)" 2103 unfolding filterlim_at_top_dense by blast 2104 have "((\<lambda>x. g x / f x) \<longlongrightarrow> 0) (at_right a)" 2105 proof (rule lhopital_right_at_top) 2106 from pos show "eventually (\<lambda>x. f' x \<noteq> 0) (at_right a)" by eventually_elim auto 2107 from tendsto_inverse_0_at_top[OF lim] 2108 show "((\<lambda>x. g' x / f' x) \<longlongrightarrow> 0) (at_right a)" by simp 2109 qed fact+ 2110 moreover from f_0 g_0 2111 have "eventually (\<lambda>x. f x > 0) (at_right a)" "eventually (\<lambda>x. g x > 0) (at_right a)" 2112 unfolding filterlim_at_top_dense by blast+ 2113 hence "eventually (\<lambda>x. g x / f x > 0) (at_right a)" by eventually_elim simp 2114 ultimately have "filterlim (\<lambda>x. inverse (g x / f x)) at_top (at_right a)" 2115 by (rule filterlim_inverse_at_top) 2116 thus ?thesis by simp 2117qed 2118 2119lemma lhopital_right_at_top_at_bot: 2120 fixes f g :: "real \<Rightarrow> real" 2121 assumes f_0: "LIM x at_right a. f x :> at_top" 2122 assumes g_0: "LIM x at_right a. g x :> at_bot" 2123 and ev: 2124 "eventually (\<lambda>x. DERIV f x :> f' x) (at_right a)" 2125 "eventually (\<lambda>x. DERIV g x :> g' x) (at_right a)" 2126 and lim: "filterlim (\<lambda> x. (f' x / g' x)) at_bot (at_right a)" 2127 shows "filterlim (\<lambda> x. f x / g x) at_bot (at_right a)" 2128proof - 2129 from ev(2) have ev': "eventually (\<lambda>x. DERIV (\<lambda>x. -g x) x :> -g' x) (at_right a)" 2130 by eventually_elim (auto intro: derivative_intros) 2131 have "filterlim (\<lambda>x. f x / (-g x)) at_top (at_right a)" 2132 by (rule lhopital_right_at_top_at_top[where f' = f' and g' = "\<lambda>x. -g' x"]) 2133 (insert assms ev', auto simp: filterlim_uminus_at_bot) 2134 hence "filterlim (\<lambda>x. -(f x / g x)) at_top (at_right a)" by simp 2135 thus ?thesis by (simp add: filterlim_uminus_at_bot) 2136qed 2137 2138lemma lhopital_left_at_top_at_top: 2139 fixes f g :: "real \<Rightarrow> real" 2140 assumes f_0: "LIM x at_left a. f x :> at_top" 2141 assumes g_0: "LIM x at_left a. g x :> at_top" 2142 and ev: 2143 "eventually (\<lambda>x. DERIV f x :> f' x) (at_left a)" 2144 "eventually (\<lambda>x. DERIV g x :> g' x) (at_left a)" 2145 and lim: "filterlim (\<lambda> x. (f' x / g' x)) at_top (at_left a)" 2146 shows "filterlim (\<lambda> x. f x / g x) at_top (at_left a)" 2147 by (insert assms, unfold eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror, 2148 rule lhopital_right_at_top_at_top[where f'="\<lambda>x. - f' (- x)"]) 2149 (insert assms, auto simp: DERIV_mirror) 2150 2151lemma lhopital_left_at_top_at_bot: 2152 fixes f g :: "real \<Rightarrow> real" 2153 assumes f_0: "LIM x at_left a. f x :> at_top" 2154 assumes g_0: "LIM x at_left a. g x :> at_bot" 2155 and ev: 2156 "eventually (\<lambda>x. DERIV f x :> f' x) (at_left a)" 2157 "eventually (\<lambda>x. DERIV g x :> g' x) (at_left a)" 2158 and lim: "filterlim (\<lambda> x. (f' x / g' x)) at_bot (at_left a)" 2159 shows "filterlim (\<lambda> x. f x / g x) at_bot (at_left a)" 2160 by (insert assms, unfold eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror, 2161 rule lhopital_right_at_top_at_bot[where f'="\<lambda>x. - f' (- x)"]) 2162 (insert assms, auto simp: DERIV_mirror) 2163 2164lemma lhopital_at_top_at_top: 2165 fixes f g :: "real \<Rightarrow> real" 2166 assumes f_0: "LIM x at a. f x :> at_top" 2167 assumes g_0: "LIM x at a. g x :> at_top" 2168 and ev: 2169 "eventually (\<lambda>x. DERIV f x :> f' x) (at a)" 2170 "eventually (\<lambda>x. DERIV g x :> g' x) (at a)" 2171 and lim: "filterlim (\<lambda> x. (f' x / g' x)) at_top (at a)" 2172 shows "filterlim (\<lambda> x. f x / g x) at_top (at a)" 2173 using assms unfolding eventually_at_split filterlim_at_split 2174 by (auto intro!: lhopital_right_at_top_at_top[of f a g f' g'] 2175 lhopital_left_at_top_at_top[of f a g f' g']) 2176 2177lemma lhopital_at_top_at_bot: 2178 fixes f g :: "real \<Rightarrow> real" 2179 assumes f_0: "LIM x at a. f x :> at_top" 2180 assumes g_0: "LIM x at a. g x :> at_bot" 2181 and ev: 2182 "eventually (\<lambda>x. DERIV f x :> f' x) (at a)" 2183 "eventually (\<lambda>x. DERIV g x :> g' x) (at a)" 2184 and lim: "filterlim (\<lambda> x. (f' x / g' x)) at_bot (at a)" 2185 shows "filterlim (\<lambda> x. f x / g x) at_bot (at a)" 2186 using assms unfolding eventually_at_split filterlim_at_split 2187 by (auto intro!: lhopital_right_at_top_at_bot[of f a g f' g'] 2188 lhopital_left_at_top_at_bot[of f a g f' g']) 2189 2190end 2191