some slight generalizations
authorimmler
Tue May 10 15:48:37 2016 +0200 (2016-05-10 ago)
changeset 63079e9ad90ce926c
parent 63078 e49dc94eb624
child 63080 8326aa594273
some slight generalizations
src/HOL/Deriv.thy
src/HOL/Multivariate_Analysis/Derivative.thy
     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.28  lemma has_vector_derivative_add_const:
    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.44    by (simp add: DERIV_def)
    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.55  apply (simp add: add.commute)
    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.73 +qed (simp_all add: assms)
    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.156 -    proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm)
   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.160 +    proof (simp add: abs_if pos_less_divide_eq dist_real_def split add: if_split_asm)
   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.190 -    proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm)
   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>