conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
authorhoelzl
Mon Dec 03 18:19:11 2012 +0100 (2012-12-03)
changeset 50330d0b12171118e
parent 50329 9bd6b6b8a554
child 50331 4b6dc5077e98
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
src/HOL/Deriv.thy
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Deriv.thy	Mon Dec 03 18:19:09 2012 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Mon Dec 03 18:19:11 2012 +0100
     1.3 @@ -1618,23 +1618,14 @@
     1.4      by (auto simp: eventually_within at_def elim: eventually_elim1)
     1.5  qed simp_all
     1.6  
     1.7 -lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
     1.8 -  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
     1.9 -           elim: eventually_elim2 eventually_elim1)
    1.10 -
    1.11 -lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
    1.12 -  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
    1.13 +lemma DERIV_shift:
    1.14 +  "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
    1.15 +  by (simp add: DERIV_iff field_simps)
    1.16  
    1.17 -lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
    1.18 -  unfolding filterlim_def filtermap_filtermap ..
    1.19 -
    1.20 -lemma filterlim_sup:
    1.21 -  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
    1.22 -  unfolding filterlim_def filtermap_sup by auto
    1.23 -
    1.24 -lemma filterlim_split_at_real:
    1.25 -  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
    1.26 -  by (subst at_eq_sup_left_right) (rule filterlim_sup)
    1.27 +lemma DERIV_mirror:
    1.28 +  "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
    1.29 +  by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
    1.30 +                tendsto_minus_cancel_left field_simps conj_commute)
    1.31  
    1.32  lemma lhopital_right_0:
    1.33    fixes f0 g0 :: "real \<Rightarrow> real"
    1.34 @@ -1733,6 +1724,39 @@
    1.35    finally show ?thesis .
    1.36  qed
    1.37  
    1.38 +lemma lhopital_right:
    1.39 +  "((f::real \<Rightarrow> real) ---> 0) (at_right x) \<Longrightarrow> (g ---> 0) (at_right x) \<Longrightarrow>
    1.40 +    eventually (\<lambda>x. g x \<noteq> 0) (at_right x) \<Longrightarrow>
    1.41 +    eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow>
    1.42 +    eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow>
    1.43 +    eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow>
    1.44 +    ((\<lambda> x. (f' x / g' x)) ---> y) (at_right x) \<Longrightarrow>
    1.45 +  ((\<lambda> x. f x / g x) ---> y) (at_right x)"
    1.46 +  unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift
    1.47 +  by (rule lhopital_right_0)
    1.48 +
    1.49 +lemma lhopital_left:
    1.50 +  "((f::real \<Rightarrow> real) ---> 0) (at_left x) \<Longrightarrow> (g ---> 0) (at_left x) \<Longrightarrow>
    1.51 +    eventually (\<lambda>x. g x \<noteq> 0) (at_left x) \<Longrightarrow>
    1.52 +    eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow>
    1.53 +    eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow>
    1.54 +    eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow>
    1.55 +    ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
    1.56 +  ((\<lambda> x. f x / g x) ---> y) (at_left x)"
    1.57 +  unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
    1.58 +  by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
    1.59 +
    1.60 +lemma lhopital:
    1.61 +  "((f::real \<Rightarrow> real) ---> 0) (at x) \<Longrightarrow> (g ---> 0) (at x) \<Longrightarrow>
    1.62 +    eventually (\<lambda>x. g x \<noteq> 0) (at x) \<Longrightarrow>
    1.63 +    eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow>
    1.64 +    eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow>
    1.65 +    eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow>
    1.66 +    ((\<lambda> x. (f' x / g' x)) ---> y) (at x) \<Longrightarrow>
    1.67 +  ((\<lambda> x. f x / g x) ---> y) (at x)"
    1.68 +  unfolding eventually_at_split filterlim_at_split
    1.69 +  by (auto intro!: lhopital_right[of f x g g' f'] lhopital_left[of f x g g' f'])
    1.70 +
    1.71  lemma lhopital_right_0_at_top:
    1.72    fixes f g :: "real \<Rightarrow> real"
    1.73    assumes g_0: "LIM x at_right 0. g x :> at_top"
    1.74 @@ -1811,4 +1835,34 @@
    1.75    qed
    1.76  qed
    1.77  
    1.78 +lemma lhopital_right_at_top:
    1.79 +  "LIM x at_right x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
    1.80 +    eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow>
    1.81 +    eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow>
    1.82 +    eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow>
    1.83 +    ((\<lambda> x. (f' x / g' x)) ---> y) (at_right x) \<Longrightarrow>
    1.84 +    ((\<lambda> x. f x / g x) ---> y) (at_right x)"
    1.85 +  unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift
    1.86 +  by (rule lhopital_right_0_at_top)
    1.87 +
    1.88 +lemma lhopital_left_at_top:
    1.89 +  "LIM x at_left x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
    1.90 +    eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow>
    1.91 +    eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow>
    1.92 +    eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow>
    1.93 +    ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
    1.94 +    ((\<lambda> x. f x / g x) ---> y) (at_left x)"
    1.95 +  unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
    1.96 +  by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
    1.97 +
    1.98 +lemma lhopital_at_top:
    1.99 +  "LIM x at x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
   1.100 +    eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow>
   1.101 +    eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow>
   1.102 +    eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow>
   1.103 +    ((\<lambda> x. (f' x / g' x)) ---> y) (at x) \<Longrightarrow>
   1.104 +    ((\<lambda> x. f x / g x) ---> y) (at x)"
   1.105 +  unfolding eventually_at_split filterlim_at_split
   1.106 +  by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f'])
   1.107 +
   1.108  end
     2.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:19:09 2012 +0100
     2.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:11 2012 +0100
     2.3 @@ -280,6 +280,9 @@
     2.4  lemma filtermap_bot [simp]: "filtermap f bot = bot"
     2.5    by (simp add: filter_eq_iff eventually_filtermap)
     2.6  
     2.7 +lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
     2.8 +  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
     2.9 +
    2.10  subsection {* Order filters *}
    2.11  
    2.12  definition at_top :: "('a::order) filter"
    2.13 @@ -703,6 +706,13 @@
    2.14      by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
    2.15  qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
    2.16  
    2.17 +lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
    2.18 +  unfolding filterlim_def filtermap_filtermap ..
    2.19 +
    2.20 +lemma filterlim_sup:
    2.21 +  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
    2.22 +  unfolding filterlim_def filtermap_sup by auto
    2.23 +
    2.24  abbreviation (in topological_space)
    2.25    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
    2.26    "(f ---> l) F \<equiv> filterlim f (nhds l) F"
    2.27 @@ -915,6 +925,11 @@
    2.28    shows "((\<lambda>x. - f x) ---> - a) F \<Longrightarrow> (f ---> a) F"
    2.29    by (drule tendsto_minus, simp)
    2.30  
    2.31 +lemma tendsto_minus_cancel_left:
    2.32 +    "(f ---> - (y::_::real_normed_vector)) F \<longleftrightarrow> ((\<lambda>x. - f x) ---> y) F"
    2.33 +  using tendsto_minus_cancel[of f "- y" F]  tendsto_minus[of f "- y" F]
    2.34 +  by auto
    2.35 +
    2.36  lemma tendsto_diff [tendsto_intros]:
    2.37    fixes a b :: "'a::real_normed_vector"
    2.38    shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
    2.39 @@ -1367,5 +1382,79 @@
    2.40      by eventually_elim simp
    2.41  qed
    2.42  
    2.43 +subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
    2.44 +
    2.45 +text {*
    2.46 +
    2.47 +This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
    2.48 +@{term "at_right x"} and also @{term "at_right 0"}.
    2.49 +
    2.50 +*}
    2.51 +
    2.52 +lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
    2.53 +  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
    2.54 +           elim: eventually_elim2 eventually_elim1)
    2.55 +
    2.56 +lemma filterlim_split_at_real:
    2.57 +  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
    2.58 +  by (subst at_eq_sup_left_right) (rule filterlim_sup)
    2.59 +
    2.60 +lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
    2.61 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
    2.62 +  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
    2.63 +
    2.64 +lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
    2.65 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
    2.66 +  apply (intro allI ex_cong)
    2.67 +  apply (auto simp: dist_real_def field_simps)
    2.68 +  apply (erule_tac x="-x" in allE)
    2.69 +  apply simp
    2.70 +  done
    2.71 +
    2.72 +lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
    2.73 +  unfolding at_def filtermap_nhds_shift[symmetric]
    2.74 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.75 +
    2.76 +lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
    2.77 +  unfolding filtermap_at_shift[symmetric]
    2.78 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.79 +
    2.80 +lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
    2.81 +  using filtermap_at_right_shift[of "-a" 0] by simp
    2.82 +
    2.83 +lemma filterlim_at_right_to_0:
    2.84 +  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
    2.85 +  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
    2.86 +
    2.87 +lemma eventually_at_right_to_0:
    2.88 +  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
    2.89 +  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
    2.90 +
    2.91 +lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
    2.92 +  unfolding at_def filtermap_nhds_minus[symmetric]
    2.93 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.94 +
    2.95 +lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
    2.96 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
    2.97 +
    2.98 +lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
    2.99 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
   2.100 +
   2.101 +lemma filterlim_at_left_to_right:
   2.102 +  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   2.103 +  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
   2.104 +
   2.105 +lemma eventually_at_left_to_right:
   2.106 +  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
   2.107 +  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
   2.108 +
   2.109 +lemma filterlim_at_split:
   2.110 +  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
   2.111 +  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
   2.112 +
   2.113 +lemma eventually_at_split:
   2.114 +  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   2.115 +  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   2.116 +
   2.117  end
   2.118