--- a/src/HOL/Deriv.thy Tue May 10 14:04:44 2016 +0100
+++ b/src/HOL/Deriv.thy Tue May 10 15:48:37 2016 +0200
@@ -599,13 +599,19 @@
lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
by (force simp add: real_differentiable_def)
-lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
- apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
+lemma has_field_derivative_iff:
+ "(f has_field_derivative D) (at x within S) \<longleftrightarrow>
+ ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)"
+ apply (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right
+ LIM_zero_iff[symmetric, of _ D])
apply (subst (2) tendsto_norm_zero_iff[symmetric])
apply (rule filterlim_cong)
apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
done
+lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
+ unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
+
lemma mult_commute_abs: "(\<lambda>x. x * c) = op * (c::'a::ab_semigroup_mult)"
by (simp add: fun_eq_iff mult.commute)
@@ -645,14 +651,14 @@
by (auto simp: has_vector_derivative_def scaleR_diff_right)
lemma has_vector_derivative_add_const:
- "((\<lambda>t. g t + z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
+ "((\<lambda>t. g t + z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net"
apply (intro iffI)
apply (drule has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const], simp)
apply (drule has_vector_derivative_add [OF _ has_vector_derivative_const], simp)
done
lemma has_vector_derivative_diff_const:
- "((\<lambda>t. g t - z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
+ "((\<lambda>t. g t - z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net"
using has_vector_derivative_add_const [where z = "-z"]
by simp
@@ -704,6 +710,11 @@
lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
by (simp add: DERIV_def)
+lemma has_field_derivativeD:
+ "(f has_field_derivative D) (at x within S) \<Longrightarrow>
+ ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)"
+ by (simp add: has_field_derivative_iff)
+
lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto
@@ -892,22 +903,27 @@
apply (simp add: add.commute)
done
-lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) \<midarrow>x\<rightarrow> D"
- by (simp add: DERIV_def DERIV_LIM_iff)
+lemmas DERIV_iff2 = has_field_derivative_iff
+
+lemma has_field_derivative_cong_ev:
+ assumes "x = y"
+ and *: "eventually (\<lambda>x. x \<in> s \<longrightarrow> f x = g x) (nhds x)"
+ and "u = v" "s = t" "x \<in> s"
+ shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative v) (at y within t)"
+ unfolding DERIV_iff2
+proof (rule filterlim_cong)
+ from assms have "f y = g y" by (auto simp: eventually_nhds)
+ with * show "\<forall>\<^sub>F xa in at x within s. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)"
+ unfolding eventually_at_filter
+ by eventually_elim (auto simp: assms \<open>f y = g y\<close>)
+qed (simp_all add: assms)
lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
- unfolding DERIV_iff2
-proof (rule filterlim_cong)
- assume *: "eventually (\<lambda>x. f x = g x) (nhds x)"
- moreover from * have "f x = g x" by (auto simp: eventually_nhds)
- moreover assume "x = y" "u = v"
- ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
- by (auto simp: eventually_at_filter elim: eventually_mono)
-qed simp_all
+ by (rule has_field_derivative_cong_ev) simp_all
lemma DERIV_shift:
- "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
+ "(f has_field_derivative y) (at (x + z)) = ((\<lambda>x. f (x + z)) has_field_derivative y) (at x)"
by (simp add: DERIV_def field_simps)
lemma DERIV_mirror:
@@ -943,31 +959,64 @@
text\<open>If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right\<close>
+lemma has_real_derivative_pos_inc_right:
+ fixes f :: "real => real"
+ assumes der: "(f has_real_derivative l) (at x within S)"
+ and l: "0 < l"
+ shows "\<exists>d > 0. \<forall>h > 0. x + h \<in> S \<longrightarrow> h < d \<longrightarrow> f x < f (x + h)"
+ using assms
+proof -
+ from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at]
+ obtain s where s: "0 < s"
+ 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"
+ by (auto simp: dist_real_def)
+ then show ?thesis
+ proof (intro exI conjI strip)
+ show "0<s" using s .
+ fix h::real
+ assume "0 < h" "h < s" "x + h \<in> S"
+ with all [of "x + h"] show "f x < f (x+h)"
+ proof (simp add: abs_if dist_real_def pos_less_divide_eq split: if_split_asm)
+ assume "\<not> (f (x+h) - f x) / h < l" and h: "0 < h"
+ with l
+ have "0 < (f (x+h) - f x) / h" by arith
+ thus "f x < f (x+h)"
+ by (simp add: pos_less_divide_eq h)
+ qed
+ qed
+qed
+
lemma DERIV_pos_inc_right:
fixes f :: "real => real"
assumes der: "DERIV f x :> l"
and l: "0 < l"
shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x + h)"
+ using has_real_derivative_pos_inc_right[OF assms]
+ by auto
+
+lemma has_real_derivative_neg_dec_left:
+ fixes f :: "real => real"
+ assumes der: "(f has_real_derivative l) (at x within S)"
+ and "l < 0"
+ shows "\<exists>d > 0. \<forall>h > 0. x - h \<in> S \<longrightarrow> h < d \<longrightarrow> f x < f (x - h)"
proof -
- from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
- 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)"
- by simp
- then obtain s
- where s: "0 < s"
- and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
- by auto
+ from \<open>l < 0\<close> have l: "- l > 0" by simp
+ from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at]
+ obtain s where s: "0 < s"
+ 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"
+ by (auto simp: dist_real_def)
thus ?thesis
proof (intro exI conjI strip)
show "0<s" using s .
fix h::real
- assume "0 < h" "h < s"
- with all [of h] show "f x < f (x+h)"
- proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm)
- assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
+ assume "0 < h" "h < s" "x - h \<in> S"
+ with all [of "x - h"] show "f x < f (x-h)"
+ proof (simp add: abs_if pos_less_divide_eq dist_real_def split add: if_split_asm)
+ assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
with l
- have "0 < (f (x+h) - f x) / h" by arith
- thus "f x < f (x+h)"
- by (simp add: pos_less_divide_eq h)
+ have "0 < (f (x-h) - f x) / h" by arith
+ thus "f x < f (x-h)"
+ by (simp add: pos_less_divide_eq h)
qed
qed
qed
@@ -977,43 +1026,31 @@
assumes der: "DERIV f x :> l"
and l: "l < 0"
shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x-h)"
-proof -
- from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
- 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)"
- by simp
- then obtain s
- where s: "0 < s"
- and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
- by auto
- thus ?thesis
- proof (intro exI conjI strip)
- show "0<s" using s .
- fix h::real
- assume "0 < h" "h < s"
- with all [of "-h"] show "f x < f (x-h)"
- proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm)
- assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
- with l
- have "0 < (f (x-h) - f x) / h" by arith
- thus "f x < f (x-h)"
- by (simp add: pos_less_divide_eq h)
- qed
- qed
-qed
+ using has_real_derivative_neg_dec_left[OF assms]
+ by auto
+
+lemma has_real_derivative_pos_inc_left:
+ fixes f :: "real => real"
+ 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"
+ by (rule has_real_derivative_neg_dec_left [of "%x. - f x" "-l" x S, simplified])
+ (auto simp add: DERIV_minus)
lemma DERIV_pos_inc_left:
fixes f :: "real => real"
shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
- apply (rule DERIV_neg_dec_left [of "%x. - f x" "-l" x, simplified])
- apply (auto simp add: DERIV_minus)
- done
+ using has_real_derivative_pos_inc_left
+ by blast
+
+lemma has_real_derivative_neg_dec_right:
+ fixes f :: "real => real"
+ 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)"
+ by (rule has_real_derivative_pos_inc_right [of "%x. - f x" "-l" x S, simplified])
+ (auto simp add: DERIV_minus)
lemma DERIV_neg_dec_right:
fixes f :: "real => real"
shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
- apply (rule DERIV_pos_inc_right [of "%x. - f x" "-l" x, simplified])
- apply (auto simp add: DERIV_minus)
- done
+ using has_real_derivative_neg_dec_right by blast
lemma DERIV_local_max:
fixes f :: "real => real"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue May 10 14:04:44 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue May 10 15:48:37 2016 +0200
@@ -126,19 +126,7 @@
subsubsection \<open>Caratheodory characterization\<close>
-lemma DERIV_within_iff:
- "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) \<longlongrightarrow> D) (at a within s)"
-proof -
- have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
- by (metis divide_diff_eq_iff eq_iff_diff_eq_0 mult.commute)
- show ?thesis
- apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
- apply (simp add: LIM_zero_iff [where l = D, symmetric])
- apply (simp add: Lim_within dist_norm)
- apply (simp add: nonzero_norm_divide [symmetric])
- apply (simp add: 1 diff_diff_eq ac_simps)
- done
-qed
+lemmas DERIV_within_iff = has_field_derivative_iff
lemma DERIV_caratheodory_within:
"(f has_field_derivative l) (at x within s) \<longleftrightarrow>