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