add L'Hôpital's rule
authorhoelzl
Mon Dec 03 18:19:07 2012 +0100 (2012-12-03)
changeset 50327bbea2e82871c
parent 50326 b5afeccab2db
child 50328 25b1e8686ce0
add L'Hôpital's rule
src/HOL/Deriv.thy
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Deriv.thy	Mon Dec 03 18:19:05 2012 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Mon Dec 03 18:19:07 2012 +0100
     1.3 @@ -1589,4 +1589,183 @@
     1.4  apply (drule (1) LIM_fun_gt_zero, force)
     1.5  done
     1.6  
     1.7 +lemma GMVT':
     1.8 +  fixes f g :: "real \<Rightarrow> real"
     1.9 +  assumes "a < b"
    1.10 +  assumes isCont_f: "\<And>z. a \<le> z \<Longrightarrow> z \<le> b \<Longrightarrow> isCont f z"
    1.11 +  assumes isCont_g: "\<And>z. a \<le> z \<Longrightarrow> z \<le> b \<Longrightarrow> isCont g z"
    1.12 +  assumes DERIV_g: "\<And>z. a < z \<Longrightarrow> z < b \<Longrightarrow> DERIV g z :> (g' z)"
    1.13 +  assumes DERIV_f: "\<And>z. a < z \<Longrightarrow> z < b \<Longrightarrow> DERIV f z :> (f' z)"
    1.14 +  shows "\<exists>c. a < c \<and> c < b \<and> (f b - f a) * g' c = (g b - g a) * f' c"
    1.15 +proof -
    1.16 +  have "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and>
    1.17 +    a < c \<and> c < b \<and> (f b - f a) * g'c = (g b - g a) * f'c"
    1.18 +    using assms by (intro GMVT) (force simp: differentiable_def)+
    1.19 +  then obtain c where "a < c" "c < b" "(f b - f a) * g' c = (g b - g a) * f' c"
    1.20 +    using DERIV_f DERIV_g by (force dest: DERIV_unique)
    1.21 +  then show ?thesis
    1.22 +    by auto
    1.23 +qed
    1.24 +
    1.25 +lemma lhopital_right_0:
    1.26 +  fixes f g :: "real \<Rightarrow> real"
    1.27 +  assumes f_0: "isCont f 0" "f 0 = 0"
    1.28 +  assumes g_0: "isCont g 0" "g 0 = 0"
    1.29 +  assumes ev:
    1.30 +    "eventually (\<lambda>x. g x \<noteq> 0) (at_right 0)"
    1.31 +    "eventually (\<lambda>x. g' x \<noteq> 0) (at_right 0)"
    1.32 +    "eventually (\<lambda>x. DERIV f x :> f' x) (at_right 0)"
    1.33 +    "eventually (\<lambda>x. DERIV g x :> g' x) (at_right 0)"
    1.34 +  assumes lim: "((\<lambda> x. (f' x / g' x)) ---> x) (at_right 0)"
    1.35 +  shows "((\<lambda> x. f x / g x) ---> x) (at_right 0)"
    1.36 +proof -
    1.37 +  from eventually_conj[OF eventually_conj[OF ev(1) ev(2)] eventually_conj[OF ev(3) ev(4)]]
    1.38 +  obtain a where [arith]: "0 < a"
    1.39 +    and g_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g x \<noteq> 0"
    1.40 +    and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0"
    1.41 +    and f: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f x :> (f' x)"
    1.42 +    and g: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g x :> (g' x)"
    1.43 +    unfolding eventually_within eventually_at by (auto simp: dist_real_def)
    1.44 +
    1.45 +  { fix x assume x: "0 \<le> x" "x < a"
    1.46 +    from `0 \<le> x` have "isCont f x"
    1.47 +      unfolding le_less
    1.48 +    proof
    1.49 +      assume "0 = x" with `isCont f 0` show "isCont f x" by simp
    1.50 +    next
    1.51 +      assume "0 < x" with f x show ?thesis by (auto intro!: DERIV_isCont)
    1.52 +    qed }
    1.53 +  note isCont_f = this
    1.54 +
    1.55 +  { fix x assume x: "0 \<le> x" "x < a"
    1.56 +    from `0 \<le> x` have "isCont g x"
    1.57 +      unfolding le_less
    1.58 +    proof
    1.59 +      assume "0 = x" with `isCont g 0` show "isCont g x" by simp
    1.60 +    next
    1.61 +      assume "0 < x" with g x show ?thesis by (auto intro!: DERIV_isCont)
    1.62 +    qed }
    1.63 +  note isCont_g = this
    1.64 +
    1.65 +  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)"
    1.66 +  proof (rule bchoice, rule)
    1.67 +    fix x assume "x \<in> {0 <..< a}"
    1.68 +    then have x[arith]: "0 < x" "x < a" by auto
    1.69 +    with g'_neq_0 g_neq_0 `g 0 = 0` have g': "\<And>x. 0 < x \<Longrightarrow> x < a  \<Longrightarrow> 0 \<noteq> g' x" "g 0 \<noteq> g x"
    1.70 +      by auto
    1.71 +
    1.72 +    have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c"
    1.73 +      using isCont_f isCont_g f g `x < a` by (intro GMVT') auto
    1.74 +    then guess c ..
    1.75 +    moreover
    1.76 +    with g'(1)[of c] g'(2) have "(f x - f 0)  / (g x - g 0) = f' c / g' c"
    1.77 +      by (simp add: field_simps)
    1.78 +    ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
    1.79 +      using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])
    1.80 +  qed
    1.81 +  then guess \<zeta> ..
    1.82 +  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)"
    1.83 +    unfolding eventually_within eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
    1.84 +  moreover
    1.85 +  from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)"
    1.86 +    by eventually_elim auto
    1.87 +  then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
    1.88 +    by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"])
    1.89 +       (auto intro: tendsto_const tendsto_ident_at_within)
    1.90 +  then have "(\<zeta> ---> 0) (at_right 0)"
    1.91 +    by (rule tendsto_norm_zero_cancel)
    1.92 +  with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
    1.93 +    by (auto elim!: eventually_elim1 simp: filterlim_within filterlim_at)
    1.94 +  from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
    1.95 +    by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
    1.96 +  ultimately show "((\<lambda>t. f t / g t) ---> x) (at_right 0)"
    1.97 +    apply (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
    1.98 +    apply (erule_tac eventually_elim1)
    1.99 +    apply simp_all
   1.100 +    done
   1.101 +qed
   1.102 +
   1.103 +lemma lhopital_right_0_at_top:
   1.104 +  fixes f g :: "real \<Rightarrow> real"
   1.105 +  assumes g_0: "LIM x at_right 0. g x :> at_top"
   1.106 +  assumes ev:
   1.107 +    "eventually (\<lambda>x. g' x \<noteq> 0) (at_right 0)"
   1.108 +    "eventually (\<lambda>x. DERIV f x :> f' x) (at_right 0)"
   1.109 +    "eventually (\<lambda>x. DERIV g x :> g' x) (at_right 0)"
   1.110 +  assumes lim: "((\<lambda> x. (f' x / g' x)) ---> x) (at_right 0)"
   1.111 +  shows "((\<lambda> x. f x / g x) ---> x) (at_right 0)"
   1.112 +  unfolding tendsto_iff
   1.113 +proof safe
   1.114 +  fix e :: real assume "0 < e"
   1.115 +
   1.116 +  with lim[unfolded tendsto_iff, rule_format, of "e / 4"]
   1.117 +  have "eventually (\<lambda>t. dist (f' t / g' t) x < e / 4) (at_right 0)" by simp
   1.118 +  from eventually_conj[OF eventually_conj[OF ev(1) ev(2)] eventually_conj[OF ev(3) this]]
   1.119 +  obtain a where [arith]: "0 < a"
   1.120 +    and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0"
   1.121 +    and f0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV f x :> (f' x)"
   1.122 +    and g0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV g x :> (g' x)"
   1.123 +    and Df: "\<And>t. 0 < t \<Longrightarrow> t < a \<Longrightarrow> dist (f' t / g' t) x < e / 4"
   1.124 +    unfolding eventually_within_le by (auto simp: dist_real_def)
   1.125 +
   1.126 +  from Df have
   1.127 +    "eventually (\<lambda>t. t < a) (at_right 0)"
   1.128 +    "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
   1.129 +    unfolding eventually_within eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
   1.130 +  moreover
   1.131 +
   1.132 +  have "eventually (\<lambda>t. 0 < g t) (at_right 0)"
   1.133 +    using g_0[unfolded filterlim_at_top, rule_format, of "1"] by eventually_elim auto
   1.134 +
   1.135 +  moreover
   1.136 +
   1.137 +  have "eventually (\<lambda>t. g a < g t) (at_right 0)"
   1.138 +    using g_0[unfolded filterlim_at_top, rule_format, of "g a + 1"] by eventually_elim auto
   1.139 +  moreover
   1.140 +  have inv_g: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"
   1.141 +    using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl]
   1.142 +    by (rule filterlim_compose)
   1.143 +  then have "((\<lambda>x. norm (1 - g a * inverse (g x))) ---> norm (1 - g a * 0)) (at_right 0)"
   1.144 +    by (intro tendsto_intros)
   1.145 +  then have "((\<lambda>x. norm (1 - g a / g x)) ---> 1) (at_right 0)"
   1.146 +    by (simp add: inverse_eq_divide)
   1.147 +  from this[unfolded tendsto_iff, rule_format, of 1]
   1.148 +  have "eventually (\<lambda>x. norm (1 - g a / g x) < 2) (at_right 0)"
   1.149 +    by (auto elim!: eventually_elim1 simp: dist_real_def)
   1.150 +
   1.151 +  moreover
   1.152 +  from inv_g have "((\<lambda>t. norm ((f a - x * g a) * inverse (g t))) ---> norm ((f a - x * g a) * 0)) (at_right 0)"
   1.153 +    by (intro tendsto_intros)
   1.154 +  then have "((\<lambda>t. norm (f a - x * g a) / norm (g t)) ---> 0) (at_right 0)"
   1.155 +    by (simp add: inverse_eq_divide)
   1.156 +  from this[unfolded tendsto_iff, rule_format, of "e / 2"] `0 < e`
   1.157 +  have "eventually (\<lambda>t. norm (f a - x * g a) / norm (g t) < e / 2) (at_right 0)"
   1.158 +    by (auto simp: dist_real_def)
   1.159 +
   1.160 +  ultimately show "eventually (\<lambda>t. dist (f t / g t) x < e) (at_right 0)"
   1.161 +  proof eventually_elim
   1.162 +    fix t assume t[arith]: "0 < t" "t < a" "g a < g t" "0 < g t"
   1.163 +    assume ineq: "norm (1 - g a / g t) < 2" "norm (f a - x * g a) / norm (g t) < e / 2"
   1.164 +
   1.165 +    have "\<exists>y. t < y \<and> y < a \<and> (g a - g t) * f' y = (f a - f t) * g' y"
   1.166 +      using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+
   1.167 +    then guess y ..
   1.168 +    from this
   1.169 +    have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
   1.170 +      using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps)
   1.171 +
   1.172 +    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"
   1.173 +      by (simp add: field_simps)
   1.174 +    have "norm (f t / g t - x) \<le>
   1.175 +        norm (((f t - f a) / (g t - g a) - x) * (1 - g a / g t)) + norm ((f a - x * g a) / g t)"
   1.176 +      unfolding * by (rule norm_triangle_ineq)
   1.177 +    also have "\<dots> = dist (f' y / g' y) x * norm (1 - g a / g t) + norm (f a - x * g a) / norm (g t)"
   1.178 +      by (simp add: abs_mult D_eq dist_real_def)
   1.179 +    also have "\<dots> < (e / 4) * 2 + e / 2"
   1.180 +      using ineq Df[of y] `0 < e` by (intro add_le_less_mono mult_mono) auto
   1.181 +    finally show "dist (f t / g t) x < e"
   1.182 +      by (simp add: dist_real_def)
   1.183 +  qed
   1.184 +qed
   1.185 +
   1.186  end
     2.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:19:05 2012 +0100
     2.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:07 2012 +0100
     2.3 @@ -445,6 +445,14 @@
     2.4    shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
     2.5  unfolding at_def eventually_within eventually_nhds_metric by auto
     2.6  
     2.7 +lemma eventually_within_less: (* COPY FROM Topo/eventually_within *)
     2.8 +  "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
     2.9 +  unfolding eventually_within eventually_at dist_nz by auto
    2.10 +
    2.11 +lemma eventually_within_le: (* COPY FROM Topo/eventually_within_le *)
    2.12 +  "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)"
    2.13 +  unfolding eventually_within_less by auto (metis dense order_le_less_trans)
    2.14 +
    2.15  lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
    2.16    unfolding trivial_limit_def eventually_at_topological
    2.17    by (safe, case_tac "S = {a}", simp, fast, fast)
    2.18 @@ -675,14 +683,18 @@
    2.19    "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
    2.20    unfolding filterlim_def le_filter_def eventually_filtermap ..
    2.21  
    2.22 -lemma filterlim_compose: 
    2.23 +lemma filterlim_compose:
    2.24    "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
    2.25    unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
    2.26  
    2.27 -lemma filterlim_mono: 
    2.28 +lemma filterlim_mono:
    2.29    "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
    2.30    unfolding filterlim_def by (metis filtermap_mono order_trans)
    2.31  
    2.32 +lemma filterlim_cong:
    2.33 +  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
    2.34 +  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
    2.35 +
    2.36  lemma filterlim_within:
    2.37    "(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))"
    2.38    unfolding filterlim_def