author immler Tue May 10 15:48:37 2016 +0200 (2016-05-10 ago) changeset 63079 e9ad90ce926c parent 63078 e49dc94eb624 child 63080 8326aa594273
some slight generalizations
 src/HOL/Deriv.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Derivative.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Deriv.thy	Tue May 10 14:04:44 2016 +0100
1.2 +++ b/src/HOL/Deriv.thy	Tue May 10 15:48:37 2016 +0200
1.3 @@ -599,13 +599,19 @@
1.4  lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
1.5    by (force simp add: real_differentiable_def)
1.6
1.7 -lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
1.8 -  apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
1.9 +lemma has_field_derivative_iff:
1.10 +  "(f has_field_derivative D) (at x within S) \<longleftrightarrow>
1.11 +    ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)"
1.12 +  apply (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right
1.13 +    LIM_zero_iff[symmetric, of _ D])
1.14    apply (subst (2) tendsto_norm_zero_iff[symmetric])
1.15    apply (rule filterlim_cong)
1.16    apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
1.17    done
1.18
1.19 +lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
1.20 +  unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
1.21 +
1.22  lemma mult_commute_abs: "(\<lambda>x. x * c) = op * (c::'a::ab_semigroup_mult)"
1.23    by (simp add: fun_eq_iff mult.commute)
1.24
1.25 @@ -645,14 +651,14 @@
1.26    by (auto simp: has_vector_derivative_def scaleR_diff_right)
1.27
1.29 -     "((\<lambda>t. g t + z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
1.30 +     "((\<lambda>t. g t + z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net"
1.31  apply (intro iffI)
1.32  apply (drule has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const], simp)
1.33  apply (drule has_vector_derivative_add [OF _ has_vector_derivative_const], simp)
1.34  done
1.35
1.36  lemma has_vector_derivative_diff_const:
1.37 -     "((\<lambda>t. g t - z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
1.38 +     "((\<lambda>t. g t - z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net"
1.39  using has_vector_derivative_add_const [where z = "-z"]
1.40  by simp
1.41
1.42 @@ -704,6 +710,11 @@
1.43  lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
1.45
1.46 +lemma has_field_derivativeD:
1.47 +  "(f has_field_derivative D) (at x within S) \<Longrightarrow>
1.48 +    ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)"
1.49 +  by (simp add: has_field_derivative_iff)
1.50 +
1.51  lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F"
1.52    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto
1.53
1.54 @@ -892,22 +903,27 @@
1.56  done
1.57
1.58 -lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) \<midarrow>x\<rightarrow> D"
1.59 -  by (simp add: DERIV_def DERIV_LIM_iff)
1.60 +lemmas DERIV_iff2 = has_field_derivative_iff
1.61 +
1.62 +lemma has_field_derivative_cong_ev:
1.63 +  assumes "x = y"
1.64 +    and *: "eventually (\<lambda>x. x \<in> s \<longrightarrow> f x = g x) (nhds x)"
1.65 +    and "u = v" "s = t" "x \<in> s"
1.66 +    shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative v) (at y within t)"
1.67 +  unfolding DERIV_iff2
1.68 +proof (rule filterlim_cong)
1.69 +  from assms have "f y = g y" by (auto simp: eventually_nhds)
1.70 +  with * show "\<forall>\<^sub>F xa in at x within s. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)"
1.71 +    unfolding eventually_at_filter
1.72 +    by eventually_elim (auto simp: assms \<open>f y = g y\<close>)
1.74
1.75  lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
1.76      DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
1.77 -  unfolding DERIV_iff2
1.78 -proof (rule filterlim_cong)
1.79 -  assume *: "eventually (\<lambda>x. f x = g x) (nhds x)"
1.80 -  moreover from * have "f x = g x" by (auto simp: eventually_nhds)
1.81 -  moreover assume "x = y" "u = v"
1.82 -  ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
1.83 -    by (auto simp: eventually_at_filter elim: eventually_mono)
1.84 -qed simp_all
1.85 +  by (rule has_field_derivative_cong_ev) simp_all
1.86
1.87  lemma DERIV_shift:
1.88 -  "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
1.89 +  "(f has_field_derivative y) (at (x + z)) = ((\<lambda>x. f (x + z)) has_field_derivative y) (at x)"
1.90    by (simp add: DERIV_def field_simps)
1.91
1.92  lemma DERIV_mirror:
1.93 @@ -943,31 +959,64 @@
1.94
1.95  text\<open>If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right\<close>
1.96
1.97 +lemma has_real_derivative_pos_inc_right:
1.98 +  fixes f :: "real => real"
1.99 +  assumes der: "(f has_real_derivative l) (at x within S)"
1.100 +      and l:   "0 < l"
1.101 +  shows "\<exists>d > 0. \<forall>h > 0. x + h \<in> S \<longrightarrow> h < d \<longrightarrow> f x < f (x + h)"
1.102 +  using assms
1.103 +proof -
1.104 +  from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at]
1.105 +  obtain s where s:   "0 < s"
1.106 +    and all: "\<And>xa. xa\<in>S \<Longrightarrow> xa \<noteq> x \<and> dist xa x < s \<longrightarrow> abs ((f xa - f x) / (xa - x) - l) < l"
1.107 +    by (auto simp: dist_real_def)
1.108 +  then show ?thesis
1.109 +  proof (intro exI conjI strip)
1.110 +    show "0<s" using s .
1.111 +    fix h::real
1.112 +    assume "0 < h" "h < s" "x + h \<in> S"
1.113 +    with all [of "x + h"] show "f x < f (x+h)"
1.114 +    proof (simp add: abs_if dist_real_def pos_less_divide_eq split: if_split_asm)
1.115 +      assume "\<not> (f (x+h) - f x) / h < l" and h: "0 < h"
1.116 +      with l
1.117 +      have "0 < (f (x+h) - f x) / h" by arith
1.118 +      thus "f x < f (x+h)"
1.119 +        by (simp add: pos_less_divide_eq h)
1.120 +    qed
1.121 +  qed
1.122 +qed
1.123 +
1.124  lemma DERIV_pos_inc_right:
1.125    fixes f :: "real => real"
1.126    assumes der: "DERIV f x :> l"
1.127        and l:   "0 < l"
1.128    shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x + h)"
1.129 +  using has_real_derivative_pos_inc_right[OF assms]
1.130 +  by auto
1.131 +
1.132 +lemma has_real_derivative_neg_dec_left:
1.133 +  fixes f :: "real => real"
1.134 +  assumes der: "(f has_real_derivative l) (at x within S)"
1.135 +      and "l < 0"
1.136 +  shows "\<exists>d > 0. \<forall>h > 0. x - h \<in> S \<longrightarrow> h < d \<longrightarrow> f x < f (x - h)"
1.137  proof -
1.138 -  from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
1.139 -  have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
1.140 -    by simp
1.141 -  then obtain s
1.142 -        where s:   "0 < s"
1.143 -          and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
1.144 -    by auto
1.145 +  from \<open>l < 0\<close> have l: "- l > 0" by simp
1.146 +  from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at]
1.147 +  obtain s where s:   "0 < s"
1.148 +    and all: "\<And>xa. xa\<in>S \<Longrightarrow> xa \<noteq> x \<and> dist xa x < s \<longrightarrow> abs ((f xa - f x) / (xa - x) - l) < - l"
1.149 +    by (auto simp: dist_real_def)
1.150    thus ?thesis
1.151    proof (intro exI conjI strip)
1.152      show "0<s" using s .
1.153      fix h::real
1.154 -    assume "0 < h" "h < s"
1.155 -    with all [of h] show "f x < f (x+h)"
1.157 -      assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
1.158 +    assume "0 < h" "h < s" "x - h \<in> S"
1.159 +    with all [of "x - h"] show "f x < f (x-h)"
1.161 +      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
1.162        with l
1.163 -      have "0 < (f (x+h) - f x) / h" by arith
1.164 -      thus "f x < f (x+h)"
1.165 -  by (simp add: pos_less_divide_eq h)
1.166 +      have "0 < (f (x-h) - f x) / h" by arith
1.167 +      thus "f x < f (x-h)"
1.168 +        by (simp add: pos_less_divide_eq h)
1.169      qed
1.170    qed
1.171  qed
1.172 @@ -977,43 +1026,31 @@
1.173    assumes der: "DERIV f x :> l"
1.174        and l:   "l < 0"
1.175    shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x-h)"
1.176 -proof -
1.177 -  from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
1.178 -  have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
1.179 -    by simp
1.180 -  then obtain s
1.181 -        where s:   "0 < s"
1.182 -          and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
1.183 -    by auto
1.184 -  thus ?thesis
1.185 -  proof (intro exI conjI strip)
1.186 -    show "0<s" using s .
1.187 -    fix h::real
1.188 -    assume "0 < h" "h < s"
1.189 -    with all [of "-h"] show "f x < f (x-h)"
1.191 -      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
1.192 -      with l
1.193 -      have "0 < (f (x-h) - f x) / h" by arith
1.194 -      thus "f x < f (x-h)"
1.195 -  by (simp add: pos_less_divide_eq h)
1.196 -    qed
1.197 -  qed
1.198 -qed
1.199 +  using has_real_derivative_neg_dec_left[OF assms]
1.200 +  by auto
1.201 +
1.202 +lemma has_real_derivative_pos_inc_left:
1.203 +  fixes f :: "real => real"
1.204 +  shows "(f has_real_derivative l) (at x within S) \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d>0. \<forall>h>0. x - h \<in> S \<longrightarrow> h < d \<longrightarrow> f (x - h) < f x"
1.205 +  by (rule has_real_derivative_neg_dec_left [of "%x. - f x" "-l" x S, simplified])
1.206 +      (auto simp add: DERIV_minus)
1.207
1.208  lemma DERIV_pos_inc_left:
1.209    fixes f :: "real => real"
1.210    shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
1.211 -  apply (rule DERIV_neg_dec_left [of "%x. - f x" "-l" x, simplified])
1.212 -  apply (auto simp add: DERIV_minus)
1.213 -  done
1.214 +  using has_real_derivative_pos_inc_left
1.215 +  by blast
1.216 +
1.217 +lemma has_real_derivative_neg_dec_right:
1.218 +  fixes f :: "real => real"
1.219 +  shows "(f has_real_derivative l) (at x within S) \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. x + h \<in> S \<longrightarrow> h < d \<longrightarrow> f(x) > f(x + h)"
1.220 +  by (rule has_real_derivative_pos_inc_right [of "%x. - f x" "-l" x S, simplified])
1.221 +      (auto simp add: DERIV_minus)
1.222
1.223  lemma DERIV_neg_dec_right:
1.224    fixes f :: "real => real"
1.225    shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
1.226 -  apply (rule DERIV_pos_inc_right [of "%x. - f x" "-l" x, simplified])
1.227 -  apply (auto simp add: DERIV_minus)
1.228 -  done
1.229 +  using has_real_derivative_neg_dec_right by blast
1.230
1.231  lemma DERIV_local_max:
1.232    fixes f :: "real => real"
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 10 14:04:44 2016 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 10 15:48:37 2016 +0200
2.3 @@ -126,19 +126,7 @@
2.4
2.5  subsubsection \<open>Caratheodory characterization\<close>
2.6
2.7 -lemma DERIV_within_iff:
2.8 -  "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) \<longlongrightarrow> D) (at a within s)"
2.9 -proof -
2.10 -  have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
2.11 -    by (metis divide_diff_eq_iff eq_iff_diff_eq_0 mult.commute)
2.12 -  show ?thesis
2.13 -    apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
2.14 -    apply (simp add: LIM_zero_iff [where l = D, symmetric])
2.15 -    apply (simp add: Lim_within dist_norm)
2.16 -    apply (simp add: nonzero_norm_divide [symmetric])
2.17 -    apply (simp add: 1 diff_diff_eq ac_simps)
2.18 -    done
2.19 -qed
2.20 +lemmas DERIV_within_iff = has_field_derivative_iff
2.21
2.22  lemma DERIV_caratheodory_within:
2.23    "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
```