move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
--- a/src/HOL/Deriv.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Deriv.thy Tue Apr 09 14:04:47 2013 +0200
@@ -1,6 +1,7 @@
(* Title : Deriv.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
+ Author : Brian Huffman
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
GMVT by Benjamin Porter, 2005
*)
@@ -11,102 +12,703 @@
imports Limits
begin
-text{*Standard Definitions*}
+definition
+ -- {* Frechet derivative: D is derivative of function f at x within s *}
+ has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> bool"
+ (infixl "(has'_derivative)" 12)
+where
+ "(f has_derivative f') F \<longleftrightarrow>
+ (bounded_linear f' \<and>
+ ((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) ---> 0) F)"
+
+lemma FDERIV_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
+ by simp
+
+ML {*
+
+structure FDERIV_Intros = Named_Thms
+(
+ val name = @{binding FDERIV_intros}
+ val description = "introduction rules for FDERIV"
+)
+
+*}
+
+setup {*
+ FDERIV_Intros.setup #>
+ Global_Theory.add_thms_dynamic (@{binding FDERIV_eq_intros},
+ map_filter (try (fn thm => @{thm FDERIV_eq_rhs} OF [thm])) o FDERIV_Intros.get o Context.proof_of);
+*}
+
+lemma FDERIV_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
+ by (simp add: has_derivative_def)
+
+lemma FDERIV_ident[FDERIV_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
+ by (simp add: has_derivative_def tendsto_const)
+
+lemma FDERIV_const[FDERIV_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
+ by (simp add: has_derivative_def tendsto_const)
+
+lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
+
+lemma (in bounded_linear) FDERIV:
+ "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
+ using assms unfolding has_derivative_def
+ apply safe
+ apply (erule bounded_linear_compose [OF local.bounded_linear])
+ apply (drule local.tendsto)
+ apply (simp add: local.scaleR local.diff local.add local.zero)
+ done
+
+lemmas FDERIV_scaleR_right [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_scaleR_right]
+
+lemmas FDERIV_scaleR_left [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_scaleR_left]
+
+lemmas FDERIV_mult_right [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_mult_right]
+
+lemmas FDERIV_mult_left [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_mult_left]
+
+lemma FDERIV_add[simp, FDERIV_intros]:
+ assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F"
+ shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"
+ unfolding has_derivative_def
+proof safe
+ let ?x = "Lim F (\<lambda>x. x)"
+ let ?D = "\<lambda>f f' y. ((f y - f ?x) - f' (y - ?x)) /\<^sub>R norm (y - ?x)"
+ have "((\<lambda>x. ?D f f' x + ?D g g' x) ---> (0 + 0)) F"
+ using f g by (intro tendsto_add) (auto simp: has_derivative_def)
+ then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) ---> 0) F"
+ by (simp add: field_simps scaleR_add_right scaleR_diff_right)
+qed (blast intro: bounded_linear_add f g FDERIV_bounded_linear)
+
+lemma FDERIV_setsum[simp, FDERIV_intros]:
+ assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
+ shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
+proof cases
+ assume "finite I" from this f show ?thesis
+ by induct (simp_all add: f)
+qed simp
+
+lemma FDERIV_minus[simp, FDERIV_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
+ using FDERIV_scaleR_right[of f f' F "-1"] by simp
+
+lemma FDERIV_diff[simp, FDERIV_intros]:
+ "(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F"
+ by (simp only: diff_minus FDERIV_add FDERIV_minus)
+
+abbreviation
+ -- {* Frechet derivative: D is derivative of function f at x within s *}
+ FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ ("(FDERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60)
+where
+ "FDERIV f x : s :> f' \<equiv> (f has_derivative f') (at x within s)"
+
+abbreviation
+ fderiv_at ::
+ "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+where
+ "FDERIV f x :> D \<equiv> FDERIV f x : UNIV :> D"
+
+lemma FDERIV_def:
+ "FDERIV f x : s :> f' \<longleftrightarrow>
+ (bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s))"
+ by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at)
+
+lemma FDERIV_iff_norm:
+ "FDERIV f x : s :> f' \<longleftrightarrow>
+ (bounded_linear f' \<and> ((\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) ---> 0) (at x within s))"
+ using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric]
+ by (simp add: FDERIV_def divide_inverse ac_simps)
+
+lemma fderiv_def:
+ "FDERIV f x :> D = (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
+ unfolding FDERIV_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
+
+lemma field_fderiv_def:
+ fixes x :: "'a::real_normed_field"
+ shows "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ apply (unfold fderiv_def)
+ apply (simp add: bounded_linear_mult_left)
+ apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
+ apply (subst diff_divide_distrib)
+ apply (subst times_divide_eq_left [symmetric])
+ apply (simp cong: LIM_cong)
+ apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
+ done
+
+lemma FDERIV_I:
+ "bounded_linear f' \<Longrightarrow> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s) \<Longrightarrow>
+ FDERIV f x : s :> f'"
+ by (simp add: FDERIV_def)
+
+lemma FDERIV_I_sandwich:
+ assumes e: "0 < e" and bounded: "bounded_linear f'"
+ and sandwich: "(\<And>y. y \<in> s \<Longrightarrow> y \<noteq> x \<Longrightarrow> dist y x < e \<Longrightarrow> norm ((f y - f x) - f' (y - x)) / norm (y - x) \<le> H y)"
+ and "(H ---> 0) (at x within s)"
+ shows "FDERIV f x : s :> f'"
+ unfolding FDERIV_iff_norm
+proof safe
+ show "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) ---> 0) (at x within s)"
+ proof (rule tendsto_sandwich[where f="\<lambda>x. 0"])
+ show "(H ---> 0) (at x within s)" by fact
+ show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> H n) (at x within s)"
+ unfolding eventually_at using e sandwich by auto
+ qed (auto simp: le_divide_eq tendsto_const)
+qed fact
+
+lemma FDERIV_subset: "FDERIV f x : s :> f' \<Longrightarrow> t \<subseteq> s \<Longrightarrow> FDERIV f x : t :> f'"
+ by (auto simp add: FDERIV_iff_norm intro: tendsto_within_subset)
+
+subsection {* Continuity *}
+
+lemma FDERIV_continuous:
+ assumes f: "FDERIV f x : s :> f'"
+ shows "continuous (at x within s) f"
+proof -
+ from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
+ note F.tendsto[tendsto_intros]
+ let ?L = "\<lambda>f. (f ---> 0) (at x within s)"
+ have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x))"
+ using f unfolding FDERIV_iff_norm by blast
+ then have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m)
+ by (rule tendsto_mult_zero) (auto intro!: tendsto_eq_intros)
+ also have "?m \<longleftrightarrow> ?L (\<lambda>y. norm ((f y - f x) - f' (y - x)))"
+ by (intro filterlim_cong) (simp_all add: eventually_at_filter)
+ finally have "?L (\<lambda>y. (f y - f x) - f' (y - x))"
+ by (rule tendsto_norm_zero_cancel)
+ then have "?L (\<lambda>y. ((f y - f x) - f' (y - x)) + f' (y - x))"
+ by (rule tendsto_eq_intros) (auto intro!: tendsto_eq_intros simp: F.zero)
+ then have "?L (\<lambda>y. f y - f x)"
+ by simp
+ from tendsto_add[OF this tendsto_const, of "f x"] show ?thesis
+ by (simp add: continuous_within)
+qed
+
+subsection {* Composition *}
+
+lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \<Longrightarrow> (f ---> y) (at x within s) \<longleftrightarrow> (f ---> y) (inf (nhds x) (principal s))"
+ unfolding tendsto_def eventually_inf_principal eventually_at_filter
+ by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+
+lemma FDERIV_in_compose:
+ assumes f: "FDERIV f x : s :> f'"
+ assumes g: "FDERIV g (f x) : (f`s) :> g'"
+ shows "FDERIV (\<lambda>x. g (f x)) x : s :> (\<lambda>x. g' (f' x))"
+proof -
+ from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
+ from g interpret G: bounded_linear g' by (rule FDERIV_bounded_linear)
+ from F.bounded obtain kF where kF: "\<And>x. norm (f' x) \<le> norm x * kF" by fast
+ from G.bounded obtain kG where kG: "\<And>x. norm (g' x) \<le> norm x * kG" by fast
+ note G.tendsto[tendsto_intros]
+
+ let ?L = "\<lambda>f. (f ---> 0) (at x within s)"
+ let ?D = "\<lambda>f f' x y. (f y - f x) - f' (y - x)"
+ let ?N = "\<lambda>f f' x y. norm (?D f f' x y) / norm (y - x)"
+ let ?gf = "\<lambda>x. g (f x)" and ?gf' = "\<lambda>x. g' (f' x)"
+ def Nf \<equiv> "?N f f' x"
+ def Ng \<equiv> "\<lambda>y. ?N g g' (f x) (f y)"
+
+ show ?thesis
+ proof (rule FDERIV_I_sandwich[of 1])
+ show "bounded_linear (\<lambda>x. g' (f' x))"
+ using f g by (blast intro: bounded_linear_compose FDERIV_bounded_linear)
+ next
+ fix y::'a assume neq: "y \<noteq> x"
+ have "?N ?gf ?gf' x y = norm (g' (?D f f' x y) + ?D g g' (f x) (f y)) / norm (y - x)"
+ by (simp add: G.diff G.add field_simps)
+ also have "\<dots> \<le> norm (g' (?D f f' x y)) / norm (y - x) + Ng y * (norm (f y - f x) / norm (y - x))"
+ by (simp add: add_divide_distrib[symmetric] divide_right_mono norm_triangle_ineq G.zero Ng_def)
+ also have "\<dots> \<le> Nf y * kG + Ng y * (Nf y + kF)"
+ proof (intro add_mono mult_left_mono)
+ have "norm (f y - f x) = norm (?D f f' x y + f' (y - x))"
+ by simp
+ also have "\<dots> \<le> norm (?D f f' x y) + norm (f' (y - x))"
+ by (rule norm_triangle_ineq)
+ also have "\<dots> \<le> norm (?D f f' x y) + norm (y - x) * kF"
+ using kF by (intro add_mono) simp
+ finally show "norm (f y - f x) / norm (y - x) \<le> Nf y + kF"
+ by (simp add: neq Nf_def field_simps)
+ qed (insert kG, simp_all add: Ng_def Nf_def neq zero_le_divide_iff field_simps)
+ finally show "?N ?gf ?gf' x y \<le> Nf y * kG + Ng y * (Nf y + kF)" .
+ next
+ have [tendsto_intros]: "?L Nf"
+ using f unfolding FDERIV_iff_norm Nf_def ..
+ from f have "(f ---> f x) (at x within s)"
+ by (blast intro: FDERIV_continuous continuous_within[THEN iffD1])
+ then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))"
+ unfolding filterlim_def
+ by (simp add: eventually_filtermap eventually_at_filter le_principal)
+
+ have "((?N g g' (f x)) ---> 0) (at (f x) within f`s)"
+ using g unfolding FDERIV_iff_norm ..
+ then have g': "((?N g g' (f x)) ---> 0) (inf (nhds (f x)) (principal (f`s)))"
+ by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp
+
+ have [tendsto_intros]: "?L Ng"
+ unfolding Ng_def by (rule filterlim_compose[OF g' f'])
+ show "((\<lambda>y. Nf y * kG + Ng y * (Nf y + kF)) ---> 0) (at x within s)"
+ by (intro tendsto_eq_intros) auto
+ qed simp
+qed
+
+lemma FDERIV_compose:
+ "FDERIV f x : s :> f' \<Longrightarrow> FDERIV g (f x) :> g' \<Longrightarrow> FDERIV (\<lambda>x. g (f x)) x : s :> (\<lambda>x. g' (f' x))"
+ by (blast intro: FDERIV_in_compose FDERIV_subset)
+
+lemma (in bounded_bilinear) FDERIV:
+ assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
+ shows "FDERIV (\<lambda>x. f x ** g x) x : s :> (\<lambda>h. f x ** g' h + f' h ** g x)"
+proof -
+ from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
+ obtain KF where norm_F: "\<And>x. norm (f' x) \<le> norm x * KF" by fast
+
+ from pos_bounded obtain K where K: "0 < K" and norm_prod:
+ "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
+ let ?D = "\<lambda>f f' y. f y - f x - f' (y - x)"
+ let ?N = "\<lambda>f f' y. norm (?D f f' y) / norm (y - x)"
+ def Ng =="?N g g'" and Nf =="?N f f'"
+
+ let ?fun1 = "\<lambda>y. norm (f y ** g y - f x ** g x - (f x ** g' (y - x) + f' (y - x) ** g x)) / norm (y - x)"
+ let ?fun2 = "\<lambda>y. norm (f x) * Ng y * K + Nf y * norm (g y) * K + KF * norm (g y - g x) * K"
+ let ?F = "at x within s"
-definition
- deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
- --{*Differentiation: D is derivative of function f at x*}
- ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
- "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"
+ show ?thesis
+ proof (rule FDERIV_I_sandwich[of 1])
+ show "bounded_linear (\<lambda>h. f x ** g' h + f' h ** g x)"
+ by (intro bounded_linear_add
+ bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left]
+ FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f])
+ next
+ from g have "(g ---> g x) ?F"
+ by (intro continuous_within[THEN iffD1] FDERIV_continuous)
+ moreover from f g have "(Nf ---> 0) ?F" "(Ng ---> 0) ?F"
+ by (simp_all add: FDERIV_iff_norm Ng_def Nf_def)
+ ultimately have "(?fun2 ---> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F"
+ by (intro tendsto_intros) (simp_all add: LIM_zero_iff)
+ then show "(?fun2 ---> 0) ?F"
+ by simp
+ next
+ fix y::'d assume "y \<noteq> x"
+ have "?fun1 y = norm (f x ** ?D g g' y + ?D f f' y ** g y + f' (y - x) ** (g y - g x)) / norm (y - x)"
+ by (simp add: diff_left diff_right add_left add_right field_simps)
+ also have "\<dots> \<le> (norm (f x) * norm (?D g g' y) * K + norm (?D f f' y) * norm (g y) * K +
+ norm (y - x) * KF * norm (g y - g x) * K) / norm (y - x)"
+ by (intro divide_right_mono mult_mono'
+ order_trans [OF norm_triangle_ineq add_mono]
+ order_trans [OF norm_prod mult_right_mono]
+ mult_nonneg_nonneg order_refl norm_ge_zero norm_F
+ K [THEN order_less_imp_le])
+ also have "\<dots> = ?fun2 y"
+ by (simp add: add_divide_distrib Ng_def Nf_def)
+ finally show "?fun1 y \<le> ?fun2 y" .
+ qed simp
+qed
+
+lemmas FDERIV_mult[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
+lemmas FDERIV_scaleR[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
+
+lemma FDERIV_setprod[simp, FDERIV_intros]:
+ fixes f :: "'i \<Rightarrow> 'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ assumes f: "\<And>i. i \<in> I \<Longrightarrow> FDERIV (f i) x : s :> f' i"
+ shows "FDERIV (\<lambda>x. \<Prod>i\<in>I. f i x) x : s :> (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))"
+proof cases
+ assume "finite I" from this f show ?thesis
+ proof induct
+ case (insert i I)
+ let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)"
+ have "FDERIV (\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) x : s :> ?P"
+ using insert by (intro FDERIV_mult) auto
+ also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
+ using insert(1,2) by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum_cong)
+ finally show ?case
+ using insert by simp
+ qed simp
+qed simp
+
+lemma FDERIV_power[simp, FDERIV_intros]:
+ fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ assumes f: "FDERIV f x : s :> f'"
+ shows "FDERIV (\<lambda>x. f x^n) x : s :> (\<lambda>y. of_nat n * f' y * f x^(n - 1))"
+ using FDERIV_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
+
+lemma FDERIV_inverse':
+ fixes x :: "'a::real_normed_div_algebra"
+ assumes x: "x \<noteq> 0"
+ shows "FDERIV inverse x : s :> (\<lambda>h. - (inverse x * h * inverse x))"
+ (is "FDERIV ?inv x : s :> ?f")
+proof (rule FDERIV_I_sandwich)
+ show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
+ apply (rule bounded_linear_minus)
+ apply (rule bounded_linear_mult_const)
+ apply (rule bounded_linear_const_mult)
+ apply (rule bounded_linear_ident)
+ done
+next
+ show "0 < norm x" using x by simp
+next
+ show "((\<lambda>y. norm (?inv y - ?inv x) * norm (?inv x)) ---> 0) (at x within s)"
+ apply (rule tendsto_mult_left_zero)
+ apply (rule tendsto_norm_zero)
+ apply (rule LIM_zero)
+ apply (rule tendsto_inverse)
+ apply (rule tendsto_ident_at)
+ apply (rule x)
+ done
+next
+ fix y::'a assume h: "y \<noteq> x" "dist y x < norm x"
+ then have "y \<noteq> 0"
+ by (auto simp: norm_conv_dist dist_commute)
+ have "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) = norm ((?inv y - ?inv x) * (y - x) * ?inv x) / norm (y - x)"
+ apply (subst inverse_diff_inverse [OF `y \<noteq> 0` x])
+ apply (subst minus_diff_minus)
+ apply (subst norm_minus_cancel)
+ apply (simp add: left_diff_distrib)
+ done
+ also have "\<dots> \<le> norm (?inv y - ?inv x) * norm (y - x) * norm (?inv x) / norm (y - x)"
+ apply (rule divide_right_mono [OF _ norm_ge_zero])
+ apply (rule order_trans [OF norm_mult_ineq])
+ apply (rule mult_right_mono [OF _ norm_ge_zero])
+ apply (rule norm_mult_ineq)
+ done
+ also have "\<dots> = norm (?inv y - ?inv x) * norm (?inv x)"
+ by simp
+ finally show "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) \<le>
+ norm (?inv y - ?inv x) * norm (?inv x)" .
+qed
+
+lemma FDERIV_inverse[simp, FDERIV_intros]:
+ fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
+ assumes x: "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
+ shows "FDERIV (\<lambda>x. inverse (f x)) x : s :> (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))"
+ using FDERIV_compose[OF f FDERIV_inverse', OF x] .
+
+lemma FDERIV_divide[simp, FDERIV_intros]:
+ fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
+ assumes g: "FDERIV g x : s :> g'"
+ assumes x: "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
+ shows "FDERIV (\<lambda>x. g x / f x) x : s :> (\<lambda>h. - g x * (inverse (f x) * f' h * inverse (f x)) + g' h / f x)"
+ using FDERIV_mult[OF g FDERIV_inverse[OF x f]]
+ by (simp add: divide_inverse)
+
+subsection {* Uniqueness *}
+
+text {*
+
+This can not generally shown for @{const FDERIV}, as we need to approach the point from
+all directions. There is a proof in @{text Multivariate_Analysis} for @{text euclidean_space}.
+
+*}
+
+lemma FDERIV_zero_unique:
+ assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
+proof -
+ interpret F: bounded_linear F
+ using assms by (rule FDERIV_bounded_linear)
+ let ?r = "\<lambda>h. norm (F h) / norm h"
+ have *: "?r -- 0 --> 0"
+ using assms unfolding fderiv_def by simp
+ show "F = (\<lambda>h. 0)"
+ proof
+ fix h show "F h = 0"
+ proof (rule ccontr)
+ assume "F h \<noteq> 0"
+ moreover from this have h: "h \<noteq> 0"
+ by (clarsimp simp add: F.zero)
+ ultimately have "0 < ?r h"
+ by (simp add: divide_pos_pos)
+ from LIM_D [OF * this] obtain s where s: "0 < s"
+ and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
+ from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
+ let ?x = "scaleR (t / norm h) h"
+ have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
+ hence "?r ?x < ?r h" by (rule r)
+ thus "False" using t h by (simp add: F.scaleR)
+ qed
+ qed
+qed
+
+lemma FDERIV_unique:
+ assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
+proof -
+ have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
+ using FDERIV_diff [OF assms] by simp
+ hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
+ by (rule FDERIV_zero_unique)
+ thus "F = F'"
+ unfolding fun_eq_iff right_minus_eq .
+qed
+
+subsection {* Differentiability predicate *}
+
+definition isDiff :: "'a filter \<Rightarrow> ('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool" where
+ isDiff_def: "isDiff F f \<longleftrightarrow> (\<exists>D. (f has_derivative D) F)"
+
+abbreviation differentiable_in :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool"
+ ("(_) differentiable (_) in (_)" [1000, 1000, 60] 60) where
+ "f differentiable x in s \<equiv> isDiff (at x within s) f"
+
+abbreviation differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
+ (infixl "differentiable" 60) where
+ "f differentiable x \<equiv> f differentiable x in UNIV"
+
+lemma differentiable_subset: "f differentiable x in s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable x in t"
+ unfolding isDiff_def by (blast intro: FDERIV_subset)
+
+lemma differentiable_ident [simp]: "isDiff F (\<lambda>x. x)"
+ unfolding isDiff_def by (blast intro: FDERIV_ident)
+
+lemma differentiable_const [simp]: "isDiff F (\<lambda>z. a)"
+ unfolding isDiff_def by (blast intro: FDERIV_const)
+
+lemma differentiable_in_compose:
+ "f differentiable (g x) in (g`s) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_in_compose)
+
+lemma differentiable_compose:
+ "f differentiable (g x) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
+ by (blast intro: differentiable_in_compose differentiable_subset)
+
+lemma differentiable_sum [simp]:
+ "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x + g x)"
+ unfolding isDiff_def by (blast intro: FDERIV_add)
+
+lemma differentiable_minus [simp]:
+ "isDiff F f \<Longrightarrow> isDiff F (\<lambda>x. - f x)"
+ unfolding isDiff_def by (blast intro: FDERIV_minus)
+
+lemma differentiable_diff [simp]:
+ "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x - g x)"
+ unfolding isDiff_def by (blast intro: FDERIV_diff)
+
+lemma differentiable_mult [simp]:
+ fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_algebra"
+ shows "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f x * g x) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_mult)
+
+lemma differentiable_inverse [simp]:
+ fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ shows "f differentiable x in s \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_inverse)
+
+lemma differentiable_divide [simp]:
+ fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ shows "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable x in s"
+ unfolding divide_inverse using assms by simp
+
+lemma differentiable_power [simp]:
+ fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ shows "f differentiable x in s \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_power)
+
+lemma differentiable_scaleR [simp]:
+ "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_scaleR)
+
+definition
+ -- {*Differentiation: D is derivative of function f at x*}
+ deriv ::
+ "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool"
+ ("(DERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60)
+where
+ deriv_fderiv: "DERIV f x : s :> D = FDERIV f x : s :> (\<lambda>x. x * D)"
+
+abbreviation
+ -- {*Differentiation: D is derivative of function f at x*}
+ deriv_at ::
+ "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+where
+ "DERIV f x :> D \<equiv> DERIV f x : UNIV :> D"
+
+lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>D. DERIV f x : s :> D)"
+proof safe
+ assume "f differentiable x in s"
+ then obtain f' where "FDERIV f x : s :> f'"
+ unfolding isDiff_def by auto
+ moreover then obtain c where "f' = (\<lambda>x. x * c)"
+ by (metis real_bounded_linear FDERIV_bounded_linear)
+ ultimately show "\<exists>D. DERIV f x : s :> D"
+ unfolding deriv_fderiv by auto
+qed (auto simp: isDiff_def deriv_fderiv)
+
+lemma differentiableE [elim?]:
+ fixes f :: "real \<Rightarrow> real"
+ assumes f: "f differentiable x in s" obtains df where "DERIV f x : s :> df"
+ using assms by (auto simp: differentiable_def)
+
+lemma differentiableD: "(f::real \<Rightarrow> real) differentiable x in s \<Longrightarrow> \<exists>D. DERIV f x : s :> D"
+ by (auto elim: differentiableE)
+
+lemma differentiableI: "DERIV f x : s :> D \<Longrightarrow> (f::real \<Rightarrow> real) differentiable x in s"
+ by (force simp add: differentiable_def)
+
+lemma DERIV_I_FDERIV: "FDERIV f x : s :> F \<Longrightarrow> (\<And>x. x * F' = F x) \<Longrightarrow> DERIV f x : s :> F'"
+ by (simp add: deriv_fderiv)
+
+lemma DERIV_D_FDERIV: "DERIV f x : s :> F \<Longrightarrow> FDERIV f x : s :> (\<lambda>x. x * F)"
+ by (simp add: deriv_fderiv)
+
+lemma deriv_def:
+ "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ apply (simp add: deriv_fderiv fderiv_def bounded_linear_mult_left 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
subsection {* Derivatives *}
-lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"
-by (simp add: deriv_def)
+lemma DERIV_iff: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ by (simp add: deriv_def)
-lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --> D"
-by (simp add: deriv_def)
+lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ by (simp add: deriv_def)
-lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x :> 0"
- by (simp add: deriv_def tendsto_const)
+lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x : s :> 0"
+ by (rule DERIV_I_FDERIV[OF FDERIV_const]) auto
-lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
- by (simp add: deriv_def tendsto_const cong: LIM_cong)
+lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x : s :> 1"
+ by (rule DERIV_I_FDERIV[OF FDERIV_ident]) auto
-lemma DERIV_add:
- "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x :> D + E"
- by (simp only: deriv_def add_diff_add add_divide_distrib tendsto_add)
+lemma DERIV_add: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x : s :> D + E"
+ by (rule DERIV_I_FDERIV[OF FDERIV_add]) (auto simp: field_simps dest: DERIV_D_FDERIV)
-lemma DERIV_minus:
- "DERIV f x :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x :> - D"
- by (simp only: deriv_def minus_diff_minus divide_minus_left tendsto_minus)
+lemma DERIV_minus: "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x : s :> - D"
+ by (rule DERIV_I_FDERIV[OF FDERIV_minus]) (auto simp: field_simps dest: DERIV_D_FDERIV)
-lemma DERIV_diff:
- "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
-by (simp only: diff_minus DERIV_add DERIV_minus)
+lemma DERIV_diff: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x : s :> D - E"
+ by (rule DERIV_I_FDERIV[OF FDERIV_diff]) (auto simp: field_simps dest: DERIV_D_FDERIV)
-lemma DERIV_add_minus:
- "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x :> D + - E"
-by (simp only: DERIV_add DERIV_minus)
+lemma DERIV_add_minus: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x : s :> D + - E"
+ by (simp only: DERIV_add DERIV_minus)
+
+lemma DERIV_continuous: "DERIV f x : s :> D \<Longrightarrow> continuous (at x within s) f"
+ by (drule FDERIV_continuous[OF DERIV_D_FDERIV]) simp
lemma DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
-proof (unfold isCont_iff)
- assume "DERIV f x :> D"
- hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
- by (rule DERIV_D)
- hence "(\<lambda>h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0"
- by (intro tendsto_mult tendsto_ident_at)
- hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
- by simp
- hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
- by (simp cong: LIM_cong)
- thus "(\<lambda>h. f(x+h)) -- 0 --> f(x)"
- by (simp add: LIM_def dist_norm)
-qed
+ by (auto dest!: DERIV_continuous)
+
+lemma DERIV_mult': "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x : s :> f x * E + D * g x"
+ by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV)
-lemma DERIV_mult_lemma:
- fixes a b c d :: "'a::real_field"
- shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d"
- by (simp add: field_simps diff_divide_distrib)
+lemma DERIV_mult: "DERIV f x : s :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x : s :> Da * g x + Db * f x"
+ by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV)
+
+text {* Derivative of linear multiplication *}
-lemma DERIV_mult':
- assumes f: "DERIV f x :> D"
- assumes g: "DERIV g x :> E"
- shows "DERIV (\<lambda>x. f x * g x) x :> f x * E + D * g x"
-proof (unfold deriv_def)
- from f have "isCont f x"
- by (rule DERIV_isCont)
- hence "(\<lambda>h. f(x+h)) -- 0 --> f x"
- by (simp only: isCont_iff)
- hence "(\<lambda>h. f(x+h) * ((g(x+h) - g x) / h) +
- ((f(x+h) - f x) / h) * g x)
- -- 0 --> f x * E + D * g x"
- by (intro tendsto_intros DERIV_D f g)
- thus "(\<lambda>h. (f(x+h) * g(x+h) - f x * g x) / h)
- -- 0 --> f x * E + D * g x"
- by (simp only: DERIV_mult_lemma)
-qed
+lemma DERIV_cmult:
+ "DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D"
+ by (drule DERIV_mult' [OF DERIV_const], simp)
-lemma DERIV_mult:
- "DERIV f x :> Da \<Longrightarrow> DERIV g x :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x :> Da * g x + Db * f x"
- by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
+lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c"
+ by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
+
+lemma DERIV_cdivide: "DERIV f x : s :> D ==> DERIV (%x. f x / c) x : s :> D / c"
+ apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x : s :> (1 / c) * D", force)
+ apply (erule DERIV_cmult)
+ done
lemma DERIV_unique:
- "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
+ "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
unfolding deriv_def by (rule LIM_unique)
-text{*Differentiation of finite sum*}
+lemma DERIV_setsum':
+ "(\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x : s :> (f' x n)) \<Longrightarrow> DERIV (\<lambda>x. setsum (f x) S) x : s :> setsum (f' x) S"
+ by (rule DERIV_I_FDERIV[OF FDERIV_setsum]) (auto simp: setsum_right_distrib dest: DERIV_D_FDERIV)
lemma DERIV_setsum:
- assumes "finite S"
- and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
- shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
- using assms by induct (auto intro!: DERIV_add)
+ "finite S \<Longrightarrow> (\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x : s :> (f' x n)) \<Longrightarrow> DERIV (\<lambda>x. setsum (f x) S) x : s :> setsum (f' x) S"
+ by (rule DERIV_setsum')
+
+lemma DERIV_sumr [rule_format (no_asm)]: (* REMOVE *)
+ "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x : s :> (f' r x))
+ --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x : s :> (\<Sum>r=m..<n. f' r x)"
+ by (auto intro: DERIV_setsum)
+
+lemma DERIV_inverse':
+ "DERIV f x : s :> D \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x : s :> - (inverse (f x) * D * inverse (f x))"
+ by (rule DERIV_I_FDERIV[OF FDERIV_inverse]) (auto dest: DERIV_D_FDERIV)
+
+text {* Power of @{text "-1"} *}
+
+lemma DERIV_inverse:
+ "x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse(x)) x : s :> - (inverse x ^ Suc (Suc 0))"
+ by (drule DERIV_inverse' [OF DERIV_ident]) simp
+
+text {* Derivative of inverse *}
+
+lemma DERIV_inverse_fun:
+ "DERIV f x : s :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x : s :> (- (d * inverse(f x ^ Suc (Suc 0))))"
+ by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
+
+text {* Derivative of quotient *}
+
+lemma DERIV_divide:
+ "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. f x / g x) x : s :> (D * g x - f x * E) / (g x * g x)"
+ by (rule DERIV_I_FDERIV[OF FDERIV_divide])
+ (auto dest: DERIV_D_FDERIV simp: field_simps nonzero_inverse_mult_distrib divide_inverse)
+
+lemma DERIV_quotient:
+ "DERIV f x : s :> d \<Longrightarrow> DERIV g x : s :> e \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>y. f y / g y) x : s :> (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))"
+ by (drule (2) DERIV_divide) (simp add: mult_commute)
+
+lemma DERIV_power_Suc:
+ "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. f x ^ Suc n) x : s :> (1 + of_nat n) * (D * f x ^ n)"
+ by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv)
+
+lemma DERIV_power:
+ "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. f x ^ n) x : s :> of_nat n * (D * f x ^ (n - Suc 0))"
+ by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv)
-lemma DERIV_sumr [rule_format (no_asm)]:
- "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
- --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
- by (auto intro: DERIV_setsum)
+lemma DERIV_pow: "DERIV (%x. x ^ n) x : s :> real n * (x ^ (n - Suc 0))"
+ apply (cut_tac DERIV_power [OF DERIV_ident])
+ apply (simp add: real_of_nat_def)
+ done
+
+lemma DERIV_chain': "DERIV f x : s :> D \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow> DERIV (\<lambda>x. g (f x)) x : s :> E * D"
+ using FDERIV_compose[of f "\<lambda>x. x * D" x s g "\<lambda>x. x * E"]
+ by (auto simp: deriv_fderiv ac_simps dest: FDERIV_subset)
+
+text {* Standard version *}
+
+lemma DERIV_chain: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
+ by (drule (1) DERIV_chain', simp add: o_def mult_commute)
+
+lemma DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
+ by (auto dest: DERIV_chain simp add: o_def)
+
+subsubsection {* @{text "DERIV_intros"} *}
+
+ML {*
+structure Deriv_Intros = Named_Thms
+(
+ val name = @{binding DERIV_intros}
+ val description = "DERIV introduction rules"
+)
+*}
+
+setup Deriv_Intros.setup
+
+lemma DERIV_cong: "DERIV f x : s :> X \<Longrightarrow> X = Y \<Longrightarrow> DERIV f x : s :> Y"
+ by simp
+
+declare
+ DERIV_const[THEN DERIV_cong, DERIV_intros]
+ DERIV_ident[THEN DERIV_cong, DERIV_intros]
+ DERIV_add[THEN DERIV_cong, DERIV_intros]
+ DERIV_minus[THEN DERIV_cong, DERIV_intros]
+ DERIV_mult[THEN DERIV_cong, DERIV_intros]
+ DERIV_diff[THEN DERIV_cong, DERIV_intros]
+ DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
+ DERIV_divide[THEN DERIV_cong, DERIV_intros]
+ DERIV_power[where 'a=real, THEN DERIV_cong,
+ unfolded real_of_nat_def[symmetric], DERIV_intros]
+ DERIV_setsum[THEN DERIV_cong, DERIV_intros]
text{*Alternative definition for differentiability*}
@@ -121,86 +723,33 @@
apply (simp add: add_commute)
done
-lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)"
-by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
-
-lemma DERIV_inverse_lemma:
- "\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk>
- \<Longrightarrow> (inverse a - inverse b) / h
- = - (inverse a * ((a - b) / h) * inverse b)"
-by (simp add: inverse_diff_inverse)
-
-lemma DERIV_inverse':
- assumes der: "DERIV f x :> D"
- assumes neq: "f x \<noteq> 0"
- shows "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * D * inverse (f x))"
- (is "DERIV _ _ :> ?E")
-proof (unfold DERIV_iff2)
- from der have lim_f: "f -- x --> f x"
- by (rule DERIV_isCont [unfolded isCont_def])
-
- from neq have "0 < norm (f x)" by simp
- with LIM_D [OF lim_f] obtain s
- where s: "0 < s"
- and less_fx: "\<And>z. \<lbrakk>z \<noteq> x; norm (z - x) < s\<rbrakk>
- \<Longrightarrow> norm (f z - f x) < norm (f x)"
- by fast
+lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
+ by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
- show "(\<lambda>z. (inverse (f z) - inverse (f x)) / (z - x)) -- x --> ?E"
- proof (rule LIM_equal2 [OF s])
- fix z
- assume "z \<noteq> x" "norm (z - x) < s"
- hence "norm (f z - f x) < norm (f x)" by (rule less_fx)
- hence "f z \<noteq> 0" by auto
- thus "(inverse (f z) - inverse (f x)) / (z - x) =
- - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x))"
- using neq by (rule DERIV_inverse_lemma)
- next
- from der have "(\<lambda>z. (f z - f x) / (z - x)) -- x --> D"
- by (unfold DERIV_iff2)
- thus "(\<lambda>z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x)))
- -- x --> ?E"
- by (intro tendsto_intros lim_f neq)
- qed
-qed
+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 then 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_elim1)
+qed simp_all
-lemma DERIV_divide:
- "\<lbrakk>DERIV f x :> D; DERIV g x :> E; g x \<noteq> 0\<rbrakk>
- \<Longrightarrow> DERIV (\<lambda>x. f x / g x) x :> (D * g x - f x * E) / (g x * g x)"
-apply (subgoal_tac "f x * - (inverse (g x) * E * inverse (g x)) +
- D * inverse (g x) = (D * g x - f x * E) / (g x * g x)")
-apply (erule subst)
-apply (unfold divide_inverse)
-apply (erule DERIV_mult')
-apply (erule (1) DERIV_inverse')
-apply (simp add: ring_distribs nonzero_inverse_mult_distrib)
-done
+lemma DERIV_shift:
+ "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
+ by (simp add: DERIV_iff field_simps)
-lemma DERIV_power_Suc:
- fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
- assumes f: "DERIV f x :> D"
- shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
-proof (induct n)
-case 0
- show ?case by (simp add: f)
-case (Suc k)
- from DERIV_mult' [OF f Suc] show ?case
- apply (simp only: of_nat_Suc ring_distribs mult_1_left)
- apply (simp only: power_Suc algebra_simps)
- done
-qed
-
-lemma DERIV_power:
- fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
- assumes f: "DERIV f x :> D"
- shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
-by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
+lemma DERIV_mirror:
+ "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
+ by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
+ tendsto_minus_cancel_left field_simps conj_commute)
text {* Caratheodory formulation of derivative at a point *}
lemma CARAT_DERIV:
- "(DERIV f x :> l) =
- (\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isCont g x & g x = l)"
+ "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
(is "?lhs = ?rhs")
proof
assume der: "DERIV f x :> l"
@@ -221,207 +770,11 @@
by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong)
qed
-lemma DERIV_chain':
- assumes f: "DERIV f x :> D"
- assumes g: "DERIV g (f x) :> E"
- shows "DERIV (\<lambda>x. g (f x)) x :> E * D"
-proof (unfold DERIV_iff2)
- obtain d where d: "\<forall>y. g y - g (f x) = d y * (y - f x)"
- and cont_d: "isCont d (f x)" and dfx: "d (f x) = E"
- using CARAT_DERIV [THEN iffD1, OF g] by fast
- from f have "f -- x --> f x"
- by (rule DERIV_isCont [unfolded isCont_def])
- with cont_d have "(\<lambda>z. d (f z)) -- x --> d (f x)"
- by (rule isCont_tendsto_compose)
- hence "(\<lambda>z. d (f z) * ((f z - f x) / (z - x)))
- -- x --> d (f x) * D"
- by (rule tendsto_mult [OF _ f [unfolded DERIV_iff2]])
- thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D"
- by (simp add: d dfx)
-qed
-
text {*
Let's do the standard proof, though theorem
@{text "LIM_mult2"} follows from a NS proof
*}
-lemma DERIV_cmult:
- "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
-by (drule DERIV_mult' [OF DERIV_const], simp)
-
-lemma DERIV_cdivide: "DERIV f x :> D ==> DERIV (%x. f x / c) x :> D / c"
- apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x :> (1 / c) * D", force)
- apply (erule DERIV_cmult)
- done
-
-text {* Standard version *}
-lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
-by (drule (1) DERIV_chain', simp add: o_def mult_commute)
-
-lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
-by (auto dest: DERIV_chain simp add: o_def)
-
-text {* Derivative of linear multiplication *}
-lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
-by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
-
-lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
-apply (cut_tac DERIV_power [OF DERIV_ident])
-apply (simp add: real_of_nat_def)
-done
-
-text {* Power of @{text "-1"} *}
-
-lemma DERIV_inverse:
- fixes x :: "'a::{real_normed_field}"
- shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
-by (drule DERIV_inverse' [OF DERIV_ident]) simp
-
-text {* Derivative of inverse *}
-lemma DERIV_inverse_fun:
- fixes x :: "'a::{real_normed_field}"
- shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
- ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
-by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
-
-text {* Derivative of quotient *}
-lemma DERIV_quotient:
- fixes x :: "'a::{real_normed_field}"
- shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
- ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
-by (drule (2) DERIV_divide) (simp add: mult_commute)
-
-text {* @{text "DERIV_intros"} *}
-ML {*
-structure Deriv_Intros = Named_Thms
-(
- val name = @{binding DERIV_intros}
- val description = "DERIV introduction rules"
-)
-*}
-
-setup Deriv_Intros.setup
-
-lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
- by simp
-
-declare
- DERIV_const[THEN DERIV_cong, DERIV_intros]
- DERIV_ident[THEN DERIV_cong, DERIV_intros]
- DERIV_add[THEN DERIV_cong, DERIV_intros]
- DERIV_minus[THEN DERIV_cong, DERIV_intros]
- DERIV_mult[THEN DERIV_cong, DERIV_intros]
- DERIV_diff[THEN DERIV_cong, DERIV_intros]
- DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
- DERIV_divide[THEN DERIV_cong, DERIV_intros]
- DERIV_power[where 'a=real, THEN DERIV_cong,
- unfolded real_of_nat_def[symmetric], DERIV_intros]
- DERIV_setsum[THEN DERIV_cong, DERIV_intros]
-
-
-subsection {* Differentiability predicate *}
-
-definition
- differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
- (infixl "differentiable" 60) where
- "f differentiable x = (\<exists>D. DERIV f x :> D)"
-
-lemma differentiableE [elim?]:
- assumes "f differentiable x"
- obtains df where "DERIV f x :> df"
- using assms unfolding differentiable_def ..
-
-lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
-by (simp add: differentiable_def)
-
-lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
-by (force simp add: differentiable_def)
-
-lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable x"
- by (rule DERIV_ident [THEN differentiableI])
-
-lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable x"
- by (rule DERIV_const [THEN differentiableI])
-
-lemma differentiable_compose:
- assumes f: "f differentiable (g x)"
- assumes g: "g differentiable x"
- shows "(\<lambda>x. f (g x)) differentiable x"
-proof -
- from `f differentiable (g x)` obtain df where "DERIV f (g x) :> df" ..
- moreover
- from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
- ultimately
- have "DERIV (\<lambda>x. f (g x)) x :> df * dg" by (rule DERIV_chain2)
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_sum [simp]:
- assumes "f differentiable x"
- and "g differentiable x"
- shows "(\<lambda>x. f x + g x) differentiable x"
-proof -
- from `f differentiable x` obtain df where "DERIV f x :> df" ..
- moreover
- from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
- ultimately
- have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_minus [simp]:
- assumes "f differentiable x"
- shows "(\<lambda>x. - f x) differentiable x"
-proof -
- from `f differentiable x` obtain df where "DERIV f x :> df" ..
- hence "DERIV (\<lambda>x. - f x) x :> - df" by (rule DERIV_minus)
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_diff [simp]:
- assumes "f differentiable x"
- assumes "g differentiable x"
- shows "(\<lambda>x. f x - g x) differentiable x"
- unfolding diff_minus using assms by simp
-
-lemma differentiable_mult [simp]:
- assumes "f differentiable x"
- assumes "g differentiable x"
- shows "(\<lambda>x. f x * g x) differentiable x"
-proof -
- from `f differentiable x` obtain df where "DERIV f x :> df" ..
- moreover
- from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
- ultimately
- have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (rule DERIV_mult)
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_inverse [simp]:
- assumes "f differentiable x" and "f x \<noteq> 0"
- shows "(\<lambda>x. inverse (f x)) differentiable x"
-proof -
- from `f differentiable x` obtain df where "DERIV f x :> df" ..
- hence "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * df * inverse (f x))"
- using `f x \<noteq> 0` by (rule DERIV_inverse')
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_divide [simp]:
- assumes "f differentiable x"
- assumes "g differentiable x" and "g x \<noteq> 0"
- shows "(\<lambda>x. f x / g x) differentiable x"
- unfolding divide_inverse using assms by simp
-
-lemma differentiable_power [simp]:
- fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
- assumes "f differentiable x"
- shows "(\<lambda>x. f x ^ n) differentiable x"
- apply (induct n)
- apply simp
- apply (simp add: assms)
- done
-
subsection {* Local extrema *}
text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
@@ -1035,26 +1388,6 @@
subsection {* L'Hopitals rule *}
-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 then 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_elim1)
-qed simp_all
-
-lemma DERIV_shift:
- "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
- by (simp add: DERIV_iff field_simps)
-
-lemma DERIV_mirror:
- "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
- by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
- tendsto_minus_cancel_left field_simps conj_commute)
-
lemma isCont_If_ge:
fixes a :: "'a :: linorder_topology"
shows "continuous (at_left a) g \<Longrightarrow> (f ---> g a) (at_right a) \<Longrightarrow> isCont (\<lambda>x. if x \<le> a then g x else f x) a"
--- a/src/HOL/Library/Convex.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Library/Convex.thy Tue Apr 09 14:04:47 2013 +0200
@@ -669,7 +669,7 @@
proof -
have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
- using DERIV_minus by auto
+ by (auto simp: DERIV_minus)
have "\<And>z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
--- a/src/HOL/Library/FrechetDeriv.thy Tue Apr 09 14:04:41 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,523 +0,0 @@
-(* Title : FrechetDeriv.thy
- Author : Brian Huffman
-*)
-
-header {* Frechet Derivative *}
-
-theory FrechetDeriv
-imports Complex_Main
-begin
-
-definition
- fderiv ::
- "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
- -- {* Frechet derivative: D is derivative of function f at x *}
- ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
- "FDERIV f x :> D = (bounded_linear D \<and>
- (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
-
-lemma FDERIV_I:
- "\<lbrakk>bounded_linear D; (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\<rbrakk>
- \<Longrightarrow> FDERIV f x :> D"
-by (simp add: fderiv_def)
-
-lemma FDERIV_D:
- "FDERIV f x :> D \<Longrightarrow> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0"
-by (simp add: fderiv_def)
-
-lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
-by (simp add: fderiv_def)
-
-lemma bounded_linear_zero: "bounded_linear (\<lambda>x. 0)"
- by (rule bounded_linear_intro [where K=0], simp_all)
-
-lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
- by (simp add: fderiv_def bounded_linear_zero tendsto_const)
-
-lemma bounded_linear_ident: "bounded_linear (\<lambda>x. x)"
- by (rule bounded_linear_intro [where K=1], simp_all)
-
-lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
- by (simp add: fderiv_def bounded_linear_ident tendsto_const)
-
-subsection {* Addition *}
-
-lemma bounded_linear_add:
- assumes "bounded_linear f"
- assumes "bounded_linear g"
- shows "bounded_linear (\<lambda>x. f x + g x)"
-proof -
- interpret f: bounded_linear f by fact
- interpret g: bounded_linear g by fact
- show ?thesis apply (unfold_locales)
- apply (simp only: f.add g.add add_ac)
- apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
- apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
- apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
- apply (rule_tac x="Kf + Kg" in exI, safe)
- apply (subst distrib_left)
- apply (rule order_trans [OF norm_triangle_ineq])
- apply (rule add_mono, erule spec, erule spec)
- done
-qed
-
-lemma norm_ratio_ineq:
- fixes x y :: "'a::real_normed_vector"
- fixes h :: "'b::real_normed_vector"
- shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h"
-apply (rule ord_le_eq_trans)
-apply (rule divide_right_mono)
-apply (rule norm_triangle_ineq)
-apply (rule norm_ge_zero)
-apply (rule add_divide_distrib)
-done
-
-lemma FDERIV_add:
- assumes f: "FDERIV f x :> F"
- assumes g: "FDERIV g x :> G"
- shows "FDERIV (\<lambda>x. f x + g x) x :> (\<lambda>h. F h + G h)"
-proof (rule FDERIV_I)
- show "bounded_linear (\<lambda>h. F h + G h)"
- apply (rule bounded_linear_add)
- apply (rule FDERIV_bounded_linear [OF f])
- apply (rule FDERIV_bounded_linear [OF g])
- done
-next
- have f': "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
- using f by (rule FDERIV_D)
- have g': "(\<lambda>h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
- using g by (rule FDERIV_D)
- from f' g'
- have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h
- + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
- by (rule tendsto_add_zero)
- thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
- / norm h) -- 0 --> 0"
- apply (rule real_LIM_sandwich_zero)
- apply (simp add: divide_nonneg_pos)
- apply (simp only: add_diff_add)
- apply (rule norm_ratio_ineq)
- done
-qed
-
-subsection {* Subtraction *}
-
-lemma bounded_linear_minus:
- assumes "bounded_linear f"
- shows "bounded_linear (\<lambda>x. - f x)"
-proof -
- interpret f: bounded_linear f by fact
- show ?thesis apply (unfold_locales)
- apply (simp add: f.add)
- apply (simp add: f.scaleR)
- apply (simp add: f.bounded)
- done
-qed
-
-lemma FDERIV_minus:
- "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
-apply (rule FDERIV_I)
-apply (rule bounded_linear_minus)
-apply (erule FDERIV_bounded_linear)
-apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel)
-done
-
-lemma FDERIV_diff:
- "\<lbrakk>FDERIV f x :> F; FDERIV g x :> G\<rbrakk>
- \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
-by (simp only: diff_minus FDERIV_add FDERIV_minus)
-
-subsection {* Uniqueness *}
-
-lemma FDERIV_zero_unique:
- assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
-proof -
- interpret F: bounded_linear F
- using assms by (rule FDERIV_bounded_linear)
- let ?r = "\<lambda>h. norm (F h) / norm h"
- have *: "?r -- 0 --> 0"
- using assms unfolding fderiv_def by simp
- show "F = (\<lambda>h. 0)"
- proof
- fix h show "F h = 0"
- proof (rule ccontr)
- assume "F h \<noteq> 0"
- moreover from this have h: "h \<noteq> 0"
- by (clarsimp simp add: F.zero)
- ultimately have "0 < ?r h"
- by (simp add: divide_pos_pos)
- from LIM_D [OF * this] obtain s where s: "0 < s"
- and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
- from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
- let ?x = "scaleR (t / norm h) h"
- have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
- hence "?r ?x < ?r h" by (rule r)
- thus "False" using t h by (simp add: F.scaleR)
- qed
- qed
-qed
-
-lemma FDERIV_unique:
- assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
-proof -
- have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
- using FDERIV_diff [OF assms] by simp
- hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
- by (rule FDERIV_zero_unique)
- thus "F = F'"
- unfolding fun_eq_iff right_minus_eq .
-qed
-
-subsection {* Continuity *}
-
-lemma FDERIV_isCont:
- assumes f: "FDERIV f x :> F"
- shows "isCont f x"
-proof -
- from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
- have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
- by (rule FDERIV_D [OF f])
- hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
- by (intro tendsto_mult_zero tendsto_norm_zero tendsto_ident_at)
- hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
- by (simp cong: LIM_cong)
- hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
- by (rule tendsto_norm_zero_cancel)
- hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
- by (intro tendsto_add_zero F.tendsto_zero tendsto_ident_at)
- hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
- by simp
- thus "isCont f x"
- unfolding isCont_iff by (rule LIM_zero_cancel)
-qed
-
-subsection {* Composition *}
-
-lemma real_divide_cancel_lemma:
- fixes a b c :: real
- shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c"
-by simp
-
-lemma bounded_linear_compose:
- assumes "bounded_linear f"
- assumes "bounded_linear g"
- shows "bounded_linear (\<lambda>x. f (g x))"
-proof -
- interpret f: bounded_linear f by fact
- interpret g: bounded_linear g by fact
- show ?thesis proof (unfold_locales)
- fix x y show "f (g (x + y)) = f (g x) + f (g y)"
- by (simp only: f.add g.add)
- next
- fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
- by (simp only: f.scaleR g.scaleR)
- next
- from f.pos_bounded
- obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
- from g.pos_bounded
- obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
- show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
- proof (intro exI allI)
- fix x
- have "norm (f (g x)) \<le> norm (g x) * Kf"
- using f .
- also have "\<dots> \<le> (norm x * Kg) * Kf"
- using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
- also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
- by (rule mult_assoc)
- finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
- qed
- qed
-qed
-
-lemma FDERIV_compose:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- fixes g :: "'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
- assumes f: "FDERIV f x :> F"
- assumes g: "FDERIV g (f x) :> G"
- shows "FDERIV (\<lambda>x. g (f x)) x :> (\<lambda>h. G (F h))"
-proof (rule FDERIV_I)
- from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]
- show "bounded_linear (\<lambda>h. G (F h))"
- by (rule bounded_linear_compose)
-next
- let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
- let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k"
- let ?k = "\<lambda>h. f (x + h) - f x"
- let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
- let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
- from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
- from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear)
- from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
- from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
-
- let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)"
-
- show "(\<lambda>h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0"
- proof (rule real_LIM_sandwich_zero)
- have Nf: "?Nf -- 0 --> 0"
- using FDERIV_D [OF f] .
-
- have Ng1: "isCont (\<lambda>k. norm (?Rg k) / norm k) 0"
- by (simp add: isCont_def FDERIV_D [OF g])
- have Ng2: "?k -- 0 --> 0"
- apply (rule LIM_zero)
- apply (fold isCont_iff)
- apply (rule FDERIV_isCont [OF f])
- done
- have Ng: "?Ng -- 0 --> 0"
- using isCont_tendsto_compose [OF Ng1 Ng2] by simp
-
- have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF))
- -- 0 --> 0 * kG + 0 * (0 + kF)"
- by (intro tendsto_intros Nf Ng)
- thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
- by simp
- next
- fix h::'a assume h: "h \<noteq> 0"
- thus "0 \<le> norm (g (f (x + h)) - g (f x) - G (F h)) / norm h"
- by (simp add: divide_nonneg_pos)
- next
- fix h::'a assume h: "h \<noteq> 0"
- have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)"
- by (simp add: G.diff)
- hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
- = norm (G (?Rf h) + ?Rg (?k h)) / norm h"
- by (rule arg_cong)
- also have "\<dots> \<le> norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h"
- by (rule norm_ratio_ineq)
- also have "\<dots> \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)"
- proof (rule add_mono)
- show "norm (G (?Rf h)) / norm h \<le> ?Nf h * kG"
- apply (rule ord_le_eq_trans)
- apply (rule divide_right_mono [OF kG norm_ge_zero])
- apply simp
- done
- next
- have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)"
- apply (rule real_divide_cancel_lemma [symmetric])
- apply (simp add: G.zero)
- done
- also have "\<dots> \<le> ?Ng h * (?Nf h + kF)"
- proof (rule mult_left_mono)
- have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h"
- by simp
- also have "\<dots> \<le> ?Nf h + norm (F h) / norm h"
- by (rule norm_ratio_ineq)
- also have "\<dots> \<le> ?Nf h + kF"
- apply (rule add_left_mono)
- apply (subst pos_divide_le_eq, simp add: h)
- apply (subst mult_commute)
- apply (rule kF)
- done
- finally show "norm (?k h) / norm h \<le> ?Nf h + kF" .
- next
- show "0 \<le> ?Ng h"
- apply (case_tac "f (x + h) - f x = 0", simp)
- apply (rule divide_nonneg_pos [OF norm_ge_zero])
- apply simp
- done
- qed
- finally show "norm (?Rg (?k h)) / norm h \<le> ?Ng h * (?Nf h + kF)" .
- qed
- finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
- \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" .
- qed
-qed
-
-subsection {* Product Rule *}
-
-lemma (in bounded_bilinear) FDERIV_lemma:
- "a' ** b' - a ** b - (a ** B + A ** b)
- = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)"
-by (simp add: diff_left diff_right)
-
-lemma (in bounded_bilinear) FDERIV:
- fixes x :: "'d::real_normed_vector"
- assumes f: "FDERIV f x :> F"
- assumes g: "FDERIV g x :> G"
- shows "FDERIV (\<lambda>x. f x ** g x) x :> (\<lambda>h. f x ** G h + F h ** g x)"
-proof (rule FDERIV_I)
- show "bounded_linear (\<lambda>h. f x ** G h + F h ** g x)"
- apply (rule bounded_linear_add)
- apply (rule bounded_linear_compose [OF bounded_linear_right])
- apply (rule FDERIV_bounded_linear [OF g])
- apply (rule bounded_linear_compose [OF bounded_linear_left])
- apply (rule FDERIV_bounded_linear [OF f])
- done
-next
- from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
- obtain KF where norm_F: "\<And>x. norm (F x) \<le> norm x * KF" by fast
-
- from pos_bounded obtain K where K: "0 < K" and norm_prod:
- "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
-
- let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
- let ?Rg = "\<lambda>h. g (x + h) - g x - G h"
-
- let ?fun1 = "\<lambda>h.
- norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) /
- norm h"
-
- let ?fun2 = "\<lambda>h.
- norm (f x) * (norm (?Rg h) / norm h) * K +
- norm (?Rf h) / norm h * norm (g (x + h)) * K +
- KF * norm (g (x + h) - g x) * K"
-
- have "?fun1 -- 0 --> 0"
- proof (rule real_LIM_sandwich_zero)
- from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
- have "?fun2 -- 0 -->
- norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
- by (intro tendsto_intros LIM_zero FDERIV_D)
- thus "?fun2 -- 0 --> 0"
- by simp
- next
- fix h::'d assume "h \<noteq> 0"
- thus "0 \<le> ?fun1 h"
- by (simp add: divide_nonneg_pos)
- next
- fix h::'d assume "h \<noteq> 0"
- have "?fun1 h \<le> (norm (f x) * norm (?Rg h) * K +
- norm (?Rf h) * norm (g (x + h)) * K +
- norm h * KF * norm (g (x + h) - g x) * K) / norm h"
- by (intro
- divide_right_mono mult_mono'
- order_trans [OF norm_triangle_ineq add_mono]
- order_trans [OF norm_prod mult_right_mono]
- mult_nonneg_nonneg order_refl norm_ge_zero norm_F
- K [THEN order_less_imp_le]
- )
- also have "\<dots> = ?fun2 h"
- by (simp add: add_divide_distrib)
- finally show "?fun1 h \<le> ?fun2 h" .
- qed
- thus "(\<lambda>h.
- norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x))
- / norm h) -- 0 --> 0"
- by (simp only: FDERIV_lemma)
-qed
-
-lemmas FDERIV_mult =
- bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
-
-lemmas FDERIV_scaleR =
- bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
-
-
-subsection {* Powers *}
-
-lemma FDERIV_power_Suc:
- fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
- shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
- apply (induct n)
- apply (simp add: FDERIV_ident)
- apply (drule FDERIV_mult [OF FDERIV_ident])
- apply (simp only: of_nat_Suc distrib_right mult_1_left)
- apply (simp only: power_Suc distrib_left add_ac mult_ac)
-done
-
-lemma FDERIV_power:
- fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
- shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
- apply (cases n)
- apply (simp add: FDERIV_const)
- apply (simp add: FDERIV_power_Suc del: power_Suc)
- done
-
-
-subsection {* Inverse *}
-
-lemmas bounded_linear_mult_const =
- bounded_linear_mult_left [THEN bounded_linear_compose]
-
-lemmas bounded_linear_const_mult =
- bounded_linear_mult_right [THEN bounded_linear_compose]
-
-lemma FDERIV_inverse:
- fixes x :: "'a::real_normed_div_algebra"
- assumes x: "x \<noteq> 0"
- shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))"
- (is "FDERIV ?inv _ :> _")
-proof (rule FDERIV_I)
- show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
- apply (rule bounded_linear_minus)
- apply (rule bounded_linear_mult_const)
- apply (rule bounded_linear_const_mult)
- apply (rule bounded_linear_ident)
- done
-next
- show "(\<lambda>h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h)
- -- 0 --> 0"
- proof (rule LIM_equal2)
- show "0 < norm x" using x by simp
- next
- fix h::'a
- assume 1: "h \<noteq> 0"
- assume "norm (h - 0) < norm x"
- hence "h \<noteq> -x" by clarsimp
- hence 2: "x + h \<noteq> 0"
- apply (rule contrapos_nn)
- apply (rule sym)
- apply (erule minus_unique)
- done
- show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
- = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
- apply (subst inverse_diff_inverse [OF 2 x])
- apply (subst minus_diff_minus)
- apply (subst norm_minus_cancel)
- apply (simp add: left_diff_distrib)
- done
- next
- show "(\<lambda>h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h)
- -- 0 --> 0"
- proof (rule real_LIM_sandwich_zero)
- show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x))
- -- 0 --> 0"
- apply (rule tendsto_mult_left_zero)
- apply (rule tendsto_norm_zero)
- apply (rule LIM_zero)
- apply (rule LIM_offset_zero)
- apply (rule tendsto_inverse)
- apply (rule tendsto_ident_at)
- apply (rule x)
- done
- next
- fix h::'a assume h: "h \<noteq> 0"
- show "0 \<le> norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
- apply (rule divide_nonneg_pos)
- apply (rule norm_ge_zero)
- apply (simp add: h)
- done
- next
- fix h::'a assume h: "h \<noteq> 0"
- have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
- \<le> norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h"
- apply (rule divide_right_mono [OF _ norm_ge_zero])
- apply (rule order_trans [OF norm_mult_ineq])
- apply (rule mult_right_mono [OF _ norm_ge_zero])
- apply (rule norm_mult_ineq)
- done
- also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
- by simp
- finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
- \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
- qed
- qed
-qed
-
-subsection {* Alternate definition *}
-
-lemma field_fderiv_def:
- fixes x :: "'a::real_normed_field" shows
- "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
- apply (unfold fderiv_def)
- apply (simp add: bounded_linear_mult_left)
- apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
- apply (subst diff_divide_distrib)
- apply (subst times_divide_eq_left [symmetric])
- apply (simp cong: LIM_cong)
- apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
-done
-
-end
--- a/src/HOL/Library/Inner_Product.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Library/Inner_Product.thy Tue Apr 09 14:04:47 2013 +0200
@@ -5,7 +5,7 @@
header {* Inner Product Spaces and the Gradient Derivative *}
theory Inner_Product
-imports FrechetDeriv
+imports "~~/src/HOL/Complex_Main"
begin
subsection {* Real inner product spaces *}
@@ -177,7 +177,7 @@
lemmas isCont_inner [simp] =
bounded_bilinear.isCont [OF bounded_bilinear_inner]
-lemmas FDERIV_inner =
+lemmas FDERIV_inner [FDERIV_intros] =
bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
lemmas bounded_linear_inner_left =
@@ -186,6 +186,15 @@
lemmas bounded_linear_inner_right =
bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
+lemmas FDERIV_inner_right [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_inner_right]
+
+lemmas FDERIV_inner_left [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_inner_left]
+
+lemma differentiable_inner [simp]:
+ "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_inner)
subsection {* Class instances *}
@@ -260,9 +269,6 @@
where
"GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
-lemma deriv_fderiv: "DERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. h * D)"
- by (simp only: deriv_def field_fderiv_def)
-
lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
by (simp only: gderiv_def deriv_fderiv inner_real_def)
--- a/src/HOL/Library/Library.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Library/Library.thy Tue Apr 09 14:04:47 2013 +0200
@@ -23,7 +23,6 @@
Float
Formal_Power_Series
Fraction_Field
- FrechetDeriv
FuncSet
Function_Division
Function_Growth
--- a/src/HOL/Library/Product_Vector.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Library/Product_Vector.thy Tue Apr 09 14:04:47 2013 +0200
@@ -480,28 +480,31 @@
subsubsection {* Frechet derivatives involving pairs *}
-lemma FDERIV_Pair:
- assumes f: "FDERIV f x :> f'" and g: "FDERIV g x :> g'"
- shows "FDERIV (\<lambda>x. (f x, g x)) x :> (\<lambda>h. (f' h, g' h))"
-proof (rule FDERIV_I)
+lemma FDERIV_Pair [FDERIV_intros]:
+ assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
+ shows "FDERIV (\<lambda>x. (f x, g x)) x : s :> (\<lambda>h. (f' h, g' h))"
+proof (rule FDERIV_I_sandwich[of 1])
show "bounded_linear (\<lambda>h. (f' h, g' h))"
using f g by (intro bounded_linear_Pair FDERIV_bounded_linear)
- let ?Rf = "\<lambda>h. f (x + h) - f x - f' h"
- let ?Rg = "\<lambda>h. g (x + h) - g x - g' h"
- let ?R = "\<lambda>h. ((f (x + h), g (x + h)) - (f x, g x) - (f' h, g' h))"
- show "(\<lambda>h. norm (?R h) / norm h) -- 0 --> 0"
- proof (rule real_LIM_sandwich_zero)
- show "(\<lambda>h. norm (?Rf h) / norm h + norm (?Rg h) / norm h) -- 0 --> 0"
- using f g by (intro tendsto_add_zero FDERIV_D)
- fix h :: 'a assume "h \<noteq> 0"
- thus "0 \<le> norm (?R h) / norm h"
- by (simp add: divide_nonneg_pos)
- show "norm (?R h) / norm h \<le> norm (?Rf h) / norm h + norm (?Rg h) / norm h"
- unfolding add_divide_distrib [symmetric]
- by (simp add: norm_Pair divide_right_mono
- order_trans [OF sqrt_add_le_add_sqrt])
- qed
-qed
+ let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
+ let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
+ let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"
+
+ show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)"
+ using f g by (intro tendsto_add_zero) (auto simp: FDERIV_iff_norm)
+
+ fix y :: 'a assume "y \<noteq> x"
+ show "norm (?R y) / norm (y - x) \<le> norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)"
+ unfolding add_divide_distrib [symmetric]
+ by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
+qed simp
+
+lemmas FDERIV_fst [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_fst]
+lemmas FDERIV_snd [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_snd]
+
+lemma FDERIV_split [FDERIV_intros]:
+ "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
+ unfolding split_beta' .
subsection {* Product is an inner product space *}
--- a/src/HOL/Limits.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Limits.thy Tue Apr 09 14:04:47 2013 +0200
@@ -1532,6 +1532,11 @@
shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
by (drule_tac k="- a" in LIM_offset, simp)
+lemma LIM_offset_zero_iff:
+ fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
+ shows "f -- a --> L \<longleftrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+ using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
+
lemma LIM_zero:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Apr 09 14:04:47 2013 +0200
@@ -9,26 +9,15 @@
imports Brouwer_Fixpoint Operator_Norm
begin
-(* Because I do not want to type this all the time *)
-lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
-
-subsection {* Derivatives *}
-
-text {* The definition is slightly tricky since we make it work over
- nets of a particular form. This lets us prove theorems generally and use
- "at a" or "at a within s" for restriction to a set (1-sided on R etc.) *}
+lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
+proof -
+ assume "bounded_linear f"
+ then interpret f: bounded_linear f .
+ show "linear f"
+ by (simp add: f.add f.scaleR linear_def)
+qed
-definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a filter \<Rightarrow> bool)"
-(infixl "(has'_derivative)" 12) where
- "(f has_derivative f') net \<equiv> bounded_linear f' \<and> ((\<lambda>y. (1 / (norm (y - netlimit net))) *\<^sub>R
- (f y - (f (netlimit net) + f'(y - netlimit net)))) ---> 0) net"
-
-lemma derivative_linear[dest]:
- "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
- unfolding has_derivative_def by auto
-
-lemma netlimit_at_vector:
- (* TODO: move *)
+lemma netlimit_at_vector: (* TODO: move *)
fixes a :: "'a::real_normed_vector"
shows "netlimit (at a) = a"
proof (cases "\<exists>x. x \<noteq> a")
@@ -43,22 +32,63 @@
by (rule netlimit_within [of a UNIV])
qed simp
-lemma FDERIV_conv_has_derivative:
- shows "FDERIV f x :> f' = (f has_derivative f') (at x)"
- unfolding fderiv_def has_derivative_def netlimit_at_vector
- by (simp add: diff_diff_eq Lim_at_zero [where a=x]
- tendsto_norm_zero_iff [where 'b='b, symmetric])
+(* Because I do not want to type this all the time *)
+lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
+
+lemma derivative_linear[dest]:
+ "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
+ unfolding has_derivative_def by auto
+
+lemma derivative_is_linear:
+ "(f has_derivative f') net \<Longrightarrow> linear f'"
+ by (rule derivative_linear [THEN bounded_linear_imp_linear])
lemma DERIV_conv_has_derivative:
"(DERIV f x :> f') = (f has_derivative op * f') (at x)"
- unfolding deriv_fderiv FDERIV_conv_has_derivative
- by (subst mult_commute, rule refl)
+ using deriv_fderiv[of f x UNIV f'] by (subst (asm) mult_commute)
+
+subsection {* Derivatives *}
+
+subsubsection {* Combining theorems. *}
+
+lemmas has_derivative_id = FDERIV_ident
+lemmas has_derivative_const = FDERIV_const
+lemmas has_derivative_neg = FDERIV_minus
+lemmas has_derivative_add = FDERIV_add
+lemmas has_derivative_sub = FDERIV_diff
+lemmas has_derivative_setsum = FDERIV_setsum
+lemmas scaleR_right_has_derivative = FDERIV_scaleR_right
+lemmas scaleR_left_has_derivative = FDERIV_scaleR_left
+lemmas inner_right_has_derivative = FDERIV_inner_right
+lemmas inner_left_has_derivative = FDERIV_inner_left
+lemmas mult_right_has_derivative = FDERIV_mult_right
+lemmas mult_left_has_derivative = FDERIV_mult_left
+
+lemma has_derivative_add_const:
+ "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
+ by (intro FDERIV_eq_intros) auto
+
+subsection {* Derivative with composed bilinear function. *}
+
+lemma has_derivative_bilinear_within:
+ assumes "(f has_derivative f') (at x within s)"
+ assumes "(g has_derivative g') (at x within s)"
+ assumes "bounded_bilinear h"
+ shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
+ using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
+
+lemma has_derivative_bilinear_at:
+ assumes "(f has_derivative f') (at x)"
+ assumes "(g has_derivative g') (at x)"
+ assumes "bounded_bilinear h"
+ shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
+ using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
text {* These are the only cases we'll care about, probably. *}
lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
- unfolding has_derivative_def and Lim by(auto simp add:netlimit_within)
+ unfolding has_derivative_def Lim by (auto simp add: netlimit_within inverse_eq_divide field_simps)
lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
@@ -102,111 +132,6 @@
by (simp add: bounded_linear_mult_right has_derivative_within)
qed
-lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
-proof -
- assume "bounded_linear f"
- then interpret f: bounded_linear f .
- show "linear f"
- by (simp add: f.add f.scaleR linear_def)
-qed
-
-lemma derivative_is_linear:
- "(f has_derivative f') net \<Longrightarrow> linear f'"
- by (rule derivative_linear [THEN bounded_linear_imp_linear])
-
-subsubsection {* Combining theorems. *}
-
-lemma has_derivative_eq_rhs: "(f has_derivative x) F \<Longrightarrow> x = y \<Longrightarrow> (f has_derivative y) F"
- by simp
-
-ML {*
-
-structure Has_Derivative_Intros = Named_Thms
-(
- val name = @{binding has_derivative_intros}
- val description = "introduction rules for has_derivative"
-)
-
-*}
-
-setup {*
- Has_Derivative_Intros.setup #>
- Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros},
- map (fn thm => @{thm has_derivative_eq_rhs} OF [thm]) o Has_Derivative_Intros.get o Context.proof_of);
-*}
-
-lemma has_derivative_id[has_derivative_intros]: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net"
- unfolding has_derivative_def
- by (simp add: bounded_linear_ident tendsto_const)
-
-lemma has_derivative_const[has_derivative_intros]: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
- unfolding has_derivative_def
- by (simp add: bounded_linear_zero tendsto_const)
-
-lemma (in bounded_linear) has_derivative'[has_derivative_intros]: "(f has_derivative f) net"
- unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
- unfolding diff by (simp add: tendsto_const)
-
-lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
-
-lemma (in bounded_linear) has_derivative[has_derivative_intros]:
- assumes "((\<lambda>x. g x) has_derivative (\<lambda>h. g' h)) net"
- shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>h. f (g' h))) net"
- using assms unfolding has_derivative_def
- apply safe
- apply (erule bounded_linear_compose [OF local.bounded_linear])
- apply (drule local.tendsto)
- apply (simp add: local.scaleR local.diff local.add local.zero)
- done
-
-lemmas scaleR_right_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
-
-lemmas scaleR_left_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
-
-lemmas inner_right_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_inner_right]
-
-lemmas inner_left_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_inner_left]
-
-lemmas mult_right_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_mult_right]
-
-lemmas mult_left_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_mult_left]
-
-lemma has_derivative_neg[has_derivative_intros]:
- assumes "(f has_derivative f') net"
- shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
- using scaleR_right_has_derivative [where r="-1", OF assms] by auto
-
-lemma has_derivative_add[has_derivative_intros]:
- assumes "(f has_derivative f') net" and "(g has_derivative g') net"
- shows "((\<lambda>x. f(x) + g(x)) has_derivative (\<lambda>h. f'(h) + g'(h))) net"
-proof-
- note as = assms[unfolded has_derivative_def]
- show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
- using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
- by (auto simp add: algebra_simps)
-qed
-
-lemma has_derivative_add_const:
- "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
- by (intro has_derivative_eq_intros) auto
-
-lemma has_derivative_sub[has_derivative_intros]:
- assumes "(f has_derivative f') net" and "(g has_derivative g') net"
- shows "((\<lambda>x. f(x) - g(x)) has_derivative (\<lambda>h. f'(h) - g'(h))) net"
- unfolding diff_minus by (intro has_derivative_intros assms)
-
-lemma has_derivative_setsum[has_derivative_intros]:
- assumes "finite s" and "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net"
- shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net"
- using assms by (induct, simp_all add: has_derivative_const has_derivative_add)
-text {* Somewhat different results for derivative of scalar multiplier. *}
-
subsubsection {* Limit transformation for derivatives *}
lemma has_derivative_transform_within:
@@ -232,12 +157,14 @@
no_notation Deriv.differentiable (infixl "differentiable" 60)
-definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where
- "f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
+abbreviation differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where
+ "f differentiable net \<equiv> isDiff net f"
definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where
"f differentiable_on s \<equiv> (\<forall>x\<in>s. f differentiable (at x within s))"
+lemmas differentiable_def = isDiff_def
+
lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"
unfolding differentiable_def by auto
@@ -292,32 +219,8 @@
by(auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
lemma differentiable_imp_continuous_within:
- assumes "f differentiable (at x within s)"
- shows "continuous (at x within s) f"
-proof-
- from assms guess f' unfolding differentiable_def has_derivative_within ..
- note f'=this
- then interpret bounded_linear f' by auto
- have *:"\<And>xa. x\<noteq>xa \<Longrightarrow> (f' \<circ> (\<lambda>y. y - x)) xa + norm (xa - x) *\<^sub>R ((1 / norm (xa - x)) *\<^sub>R (f xa - (f x + f' (xa - x)))) - ((f' \<circ> (\<lambda>y. y - x)) x + 0) = f xa - f x"
- using zero by auto
- have **:"continuous (at x within s) (f' \<circ> (\<lambda>y. y - x))"
- apply(rule continuous_within_compose) apply(rule continuous_intros)+
- by(rule linear_continuous_within[OF f'[THEN conjunct1]])
- show ?thesis unfolding continuous_within
- using f'[THEN conjunct2, THEN Lim_mul_norm_within]
- apply- apply(drule tendsto_add)
- apply(rule **[unfolded continuous_within])
- unfolding Lim_within and dist_norm
- apply (rule, rule)
- apply (erule_tac x=e in allE)
- apply (erule impE | assumption)+
- apply (erule exE, rule_tac x=d in exI)
- by (auto simp add: zero *)
-qed
-
-lemma differentiable_imp_continuous_at:
- "f differentiable at x \<Longrightarrow> continuous (at x) f"
- by(rule differentiable_imp_continuous_within[of _ x UNIV])
+ "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
+ by (auto simp: differentiable_def intro: FDERIV_continuous)
lemma differentiable_imp_continuous_on:
"f differentiable_on s \<Longrightarrow> continuous_on s f"
@@ -390,132 +293,25 @@
subsection {* The chain rule. *}
-lemma diff_chain_within[has_derivative_intros]:
+lemma diff_chain_within[FDERIV_intros]:
assumes "(f has_derivative f') (at x within s)"
assumes "(g has_derivative g') (at (f x) within (f ` s))"
shows "((g o f) has_derivative (g' o f'))(at x within s)"
- unfolding has_derivative_within_alt
- apply(rule,rule bounded_linear_compose[unfolded o_def[THEN sym]])
- apply(rule assms(2)[unfolded has_derivative_def,THEN conjE],assumption)
- apply(rule assms(1)[unfolded has_derivative_def,THEN conjE],assumption)
-proof(rule,rule)
- note assms = assms[unfolded has_derivative_within_alt]
- fix e::real assume "0<e"
- guess B1 using bounded_linear.pos_bounded[OF assms(1)[THEN conjunct1, rule_format]] .. note B1 = this
- guess B2 using bounded_linear.pos_bounded[OF assms(2)[THEN conjunct1, rule_format]] .. note B2 = this
- have *:"e / 2 / B2 > 0" using `e>0` B2 apply-apply(rule divide_pos_pos) by auto
- guess d1 using assms(1)[THEN conjunct2, rule_format, OF *] .. note d1 = this
- have *:"e / 2 / (1 + B1) > 0" using `e>0` B1 apply-apply(rule divide_pos_pos) by auto
- guess de using assms(2)[THEN conjunct2, rule_format, OF *] .. note de = this
- guess d2 using assms(1)[THEN conjunct2, rule_format, OF zero_less_one] .. note d2 = this
-
- def d0 \<equiv> "(min d1 d2)/2" have d0:"d0>0" "d0 < d1" "d0 < d2" unfolding d0_def using d1 d2 by auto
- def d \<equiv> "(min d0 (de / (B1 + 1))) / 2" have "de * 2 / (B1 + 1) > de / (B1 + 1)" apply(rule divide_strict_right_mono) using B1 de by auto
- hence d:"d>0" "d < d1" "d < d2" "d < (de / (B1 + 1))" unfolding d_def using d0 d1 d2 de B1 by(auto intro!: divide_pos_pos simp add:min_less_iff_disj not_less)
-
- show "\<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm ((g \<circ> f) y - (g \<circ> f) x - (g' \<circ> f') (y - x)) \<le> e * norm (y - x)" apply(rule_tac x=d in exI)
- proof(rule,rule `d>0`,rule,rule)
- fix y assume as:"y \<in> s" "norm (y - x) < d"
- hence 1:"norm (f y - f x - f' (y - x)) \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x))" using d1 d2 d by auto
-
- have "norm (f y - f x) \<le> norm (f y - f x - f' (y - x)) + norm (f' (y - x))"
- using norm_triangle_sub[of "f y - f x" "f' (y - x)"]
- by(auto simp add:algebra_simps)
- also have "\<dots> \<le> norm (f y - f x - f' (y - x)) + B1 * norm (y - x)"
- apply(rule add_left_mono) using B1 by(auto simp add:algebra_simps)
- also have "\<dots> \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x)) + B1 * norm (y - x)"
- apply(rule add_right_mono) using d1 d2 d as by auto
- also have "\<dots> \<le> norm (y - x) + B1 * norm (y - x)" by auto
- also have "\<dots> = norm (y - x) * (1 + B1)" by(auto simp add:field_simps)
- finally have 3:"norm (f y - f x) \<le> norm (y - x) * (1 + B1)" by auto
+ using FDERIV_in_compose[OF assms] by (simp add: comp_def)
- hence "norm (f y - f x) \<le> d * (1 + B1)" apply-
- apply(rule order_trans,assumption,rule mult_right_mono)
- using as B1 by auto
- also have "\<dots> < de" using d B1 by(auto simp add:field_simps)
- finally have "norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 / (1 + B1) * norm (f y - f x)"
- apply-apply(rule de[THEN conjunct2,rule_format])
- using `y\<in>s` using d as by auto
- also have "\<dots> = (e / 2) * (1 / (1 + B1) * norm (f y - f x))" by auto
- also have "\<dots> \<le> e / 2 * norm (y - x)" apply(rule mult_left_mono)
- using `e>0` and 3 using B1 and `e>0` by(auto simp add:divide_le_eq)
- finally have 4:"norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
-
- interpret g': bounded_linear g' using assms(2) by auto
- interpret f': bounded_linear f' using assms(1) by auto
- have "norm (- g' (f' (y - x)) + g' (f y - f x)) = norm (g' (f y - f x - f' (y - x)))"
- by(auto simp add:algebra_simps f'.diff g'.diff g'.add)
- also have "\<dots> \<le> B2 * norm (f y - f x - f' (y - x))" using B2
- by (auto simp add: algebra_simps)
- also have "\<dots> \<le> B2 * (e / 2 / B2 * norm (y - x))"
- apply (rule mult_left_mono) using as d1 d2 d B2 by auto
- also have "\<dots> \<le> e / 2 * norm (y - x)" using B2 by auto
- finally have 5:"norm (- g' (f' (y - x)) + g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
-
- have "norm (g (f y) - g (f x) - g' (f y - f x)) + norm (g (f y) - g (f x) - g' (f' (y - x)) - (g (f y) - g (f x) - g' (f y - f x))) \<le> e * norm (y - x)"
- using 5 4 by auto
- thus "norm ((g \<circ> f) y - (g \<circ> f) x - (g' \<circ> f') (y - x)) \<le> e * norm (y - x)"
- unfolding o_def apply- apply(rule order_trans, rule norm_triangle_sub)
- by assumption
- qed
-qed
+lemma diff_chain_at[FDERIV_intros]:
+ "(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)"
+ using FDERIV_compose[of f f' x UNIV g g'] by (simp add: comp_def)
-lemma diff_chain_at[has_derivative_intros]:
- "(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)"
- using diff_chain_within[of f f' x UNIV g g']
- using has_derivative_within_subset[of g g' "f x" UNIV "range f"]
- by simp
subsection {* Composition rules stated just for differentiability. *}
-lemma differentiable_const [intro]:
- "(\<lambda>z. c) differentiable (net::'a::real_normed_vector filter)"
- unfolding differentiable_def using has_derivative_const by auto
-
-lemma differentiable_id [intro]:
- "(\<lambda>z. z) differentiable (net::'a::real_normed_vector filter)"
- unfolding differentiable_def using has_derivative_id by auto
-
-lemma differentiable_cmul [intro]:
- "f differentiable net \<Longrightarrow>
- (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
- unfolding differentiable_def
- apply(erule exE, drule scaleR_right_has_derivative) by auto
-
-lemma differentiable_neg [intro]:
- "f differentiable net \<Longrightarrow>
- (\<lambda>z. -(f z)) differentiable (net::'a::real_normed_vector filter)"
- unfolding differentiable_def
- apply(erule exE, drule has_derivative_neg) by auto
-
-lemma differentiable_add [intro]: "f differentiable net \<Longrightarrow> g differentiable net
- \<Longrightarrow> (\<lambda>z. f z + g z) differentiable net"
- by (auto intro: has_derivative_eq_intros simp: differentiable_def)
-
-lemma differentiable_sub [intro]: "f differentiable net \<Longrightarrow> g differentiable net
- \<Longrightarrow> (\<lambda>z. f z - g z) differentiable net"
- by (auto intro: has_derivative_eq_intros simp: differentiable_def)
-
-lemma differentiable_setsum [intro]:
- assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
- shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net"
-proof-
- guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] ..
- thus ?thesis unfolding differentiable_def apply-
- apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto
-qed
-
-lemma differentiable_setsum_numseg:
- shows "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> (f i) differentiable net \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) {m::nat..n}) differentiable net"
- apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto
-
lemma differentiable_chain_at:
- "f differentiable (at x) \<Longrightarrow> g differentiable (at(f x)) \<Longrightarrow> (g o f) differentiable (at x)"
+ "f differentiable (at x) \<Longrightarrow> g differentiable (at (f x)) \<Longrightarrow> (g o f) differentiable (at x)"
unfolding differentiable_def by(meson diff_chain_at)
lemma differentiable_chain_within:
- "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s))
- \<Longrightarrow> (g o f) differentiable (at x within s)"
+ "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g o f) differentiable (at x within s)"
unfolding differentiable_def by(meson diff_chain_within)
subsection {* Uniqueness of derivative *}
@@ -567,13 +363,12 @@
unfolding dist_norm
unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
- using i by auto
+ using i by (auto simp: inverse_eq_divide)
qed
qed
lemma frechet_derivative_unique_at:
shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
- unfolding FDERIV_conv_has_derivative [symmetric]
by (rule FDERIV_unique)
lemma frechet_derivative_unique_within_closed_interval:
@@ -735,7 +530,8 @@
show ?thesis by (simp add: fun_eq_iff)
qed
-lemma rolle: fixes f::"real\<Rightarrow>real"
+lemma rolle:
+ fixes f::"real\<Rightarrow>real"
assumes "a < b" and "f a = f b" and "continuous_on {a..b} f"
assumes "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
shows "\<exists>x\<in>{a<..<b}. f' x = (\<lambda>v. 0)"
@@ -782,8 +578,7 @@
proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
fix x assume x:"x \<in> {a<..<b}"
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
- by (intro has_derivative_intros assms(3)[rule_format,OF x]
- mult_right_has_derivative)
+ by (intro FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
then guess x ..
thus ?thesis apply(rule_tac x=x in bexI)
@@ -827,8 +622,9 @@
proof-
have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
apply(rule mvt) apply(rule assms(1))
- apply(rule continuous_on_inner continuous_on_intros assms(2))+
- unfolding o_def apply(rule,rule has_derivative_intros)
+ apply(rule continuous_on_inner continuous_on_intros assms(2) ballI)+
+ unfolding o_def
+ apply(rule FDERIV_inner_right)
using assms(3) by auto
then guess x .. note x=this
show ?thesis proof(cases "f a = f b")
@@ -873,7 +669,7 @@
case goal1
let ?u = "x + u *\<^sub>R (y - x)"
have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within {0<..<1})"
- apply(rule diff_chain_within) apply(rule has_derivative_intros)+
+ apply(rule diff_chain_within) apply(rule FDERIV_intros)+
apply(rule has_derivative_within_subset)
apply(rule assms(2)[rule_format]) using goal1 * by auto
thus ?case
@@ -1252,7 +1048,7 @@
apply(rule has_derivative_inverse_strong[where g'="g' x" and f=f])
apply(rule assms)+
unfolding continuous_on_eq_continuous_at[OF assms(1)]
- apply(rule,rule differentiable_imp_continuous_at)
+ apply(rule,rule differentiable_imp_continuous_within)
unfolding differentiable_def using assms by auto
text {* Invertible derivative continous at a point implies local
@@ -1306,13 +1102,15 @@
have *:"(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
unfolding o_def and diff using f'g' by auto
show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
- unfolding ph' * apply(rule diff_chain_within) defer
- apply(rule bounded_linear.has_derivative'[OF assms(3)])
- apply(rule has_derivative_intros) defer
+ unfolding ph' *
+ apply(simp add: comp_def)
+ apply(rule bounded_linear.FDERIV[OF assms(3)])
+ apply(rule FDERIV_intros) defer
apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
apply(rule has_derivative_at_within)
using assms(5) and `u\<in>s` `a\<in>s`
- by(auto intro!: has_derivative_intros bounded_linear.has_derivative' derivative_linear)
+ apply (auto intro!: FDERIV_intros bounded_linear.FDERIV[of _ "\<lambda>x. x"] derivative_linear)
+ done
have **:"bounded_linear (\<lambda>x. f' u x - f' a x)"
"bounded_linear (\<lambda>x. f' a x - f' u x)"
apply(rule_tac[!] bounded_linear_sub)
@@ -1354,7 +1152,7 @@
proof-
fix x assume "x\<in>s"
show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
- by(rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
+ by(rule FDERIV_intros assms(2)[rule_format] `x\<in>s`)+
{ fix h
have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
@@ -1587,88 +1385,12 @@
shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) sums_seq (g x)) k \<and> (g has_derivative g'(x)) (at x within s)"
unfolding sums_seq_def
apply(rule has_derivative_sequence[OF assms(1) _ assms(3)])
- apply(rule,rule)
- apply(rule has_derivative_setsum) defer
- apply(rule,rule assms(2)[rule_format],assumption)
+ apply(rule, rule)
+ apply(rule has_derivative_setsum)
+ apply(rule assms(2)[rule_format])
+ apply assumption
using assms(4-5) unfolding sums_seq_def by auto
-subsection {* Derivative with composed bilinear function. *}
-
-lemma has_derivative_bilinear_within:
- assumes "(f has_derivative f') (at x within s)"
- assumes "(g has_derivative g') (at x within s)"
- assumes "bounded_bilinear h"
- shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
-proof-
- have "(g ---> g x) (at x within s)"
- apply(rule differentiable_imp_continuous_within[unfolded continuous_within])
- using assms(2) unfolding differentiable_def by auto
- moreover
- interpret f':bounded_linear f'
- using assms unfolding has_derivative_def by auto
- interpret g':bounded_linear g'
- using assms unfolding has_derivative_def by auto
- interpret h:bounded_bilinear h
- using assms by auto
- have "((\<lambda>y. f' (y - x)) ---> 0) (at x within s)"
- unfolding f'.zero[THEN sym]
- using bounded_linear.tendsto [of f' "\<lambda>y. y - x" 0 "at x within s"]
- using tendsto_diff [OF Lim_within_id tendsto_const, of x x s]
- unfolding id_def using assms(1) unfolding has_derivative_def by auto
- hence "((\<lambda>y. f x + f' (y - x)) ---> f x) (at x within s)"
- using tendsto_add[OF tendsto_const, of "\<lambda>y. f' (y - x)" 0 "at x within s" "f x"]
- by auto
- ultimately
- have *:"((\<lambda>x'. h (f x + f' (x' - x)) ((1/(norm (x' - x))) *\<^sub>R (g x' - (g x + g' (x' - x))))
- + h ((1/ (norm (x' - x))) *\<^sub>R (f x' - (f x + f' (x' - x)))) (g x')) ---> h (f x) 0 + h 0 (g x)) (at x within s)"
- apply-apply(rule tendsto_add) apply(rule_tac[!] Lim_bilinear[OF _ _ assms(3)])
- using assms(1-2) unfolding has_derivative_within by auto
- guess B using bounded_bilinear.pos_bounded[OF assms(3)] .. note B=this
- guess C using f'.pos_bounded .. note C=this
- guess D using g'.pos_bounded .. note D=this
- have bcd:"B * C * D > 0" using B C D by (auto intro!: mult_pos_pos)
- have **:"((\<lambda>y. (1/(norm(y - x))) *\<^sub>R (h (f'(y - x)) (g'(y - x)))) ---> 0) (at x within s)"
- unfolding Lim_within
- proof(rule,rule) case goal1
- hence "e/(B*C*D)>0" using B C D by(auto intro!:divide_pos_pos mult_pos_pos)
- thus ?case apply(rule_tac x="e/(B*C*D)" in exI,rule)
- proof(rule,rule,erule conjE)
- fix y assume as:"y \<in> s" "0 < dist y x" "dist y x < e / (B * C * D)"
- have "norm (h (f' (y - x)) (g' (y - x))) \<le> norm (f' (y - x)) * norm (g' (y - x)) * B" using B by auto
- also have "\<dots> \<le> (norm (y - x) * C) * (D * norm (y - x)) * B"
- apply(rule mult_right_mono)
- apply(rule mult_mono) using B C D
- by (auto simp add: field_simps intro!:mult_nonneg_nonneg)
- also have "\<dots> = (B * C * D * norm (y - x)) * norm (y - x)"
- by (auto simp add: field_simps)
- also have "\<dots> < e * norm (y - x)"
- apply(rule mult_strict_right_mono)
- using as(3)[unfolded dist_norm] and as(2)
- unfolding pos_less_divide_eq[OF bcd] by (auto simp add: field_simps)
- finally show "dist ((1 / norm (y - x)) *\<^sub>R h (f' (y - x)) (g' (y - x))) 0 < e"
- unfolding dist_norm apply-apply(cases "y = x")
- by(auto simp add: field_simps)
- qed
- qed
- have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))"
- apply (rule bounded_linear_add)
- apply (rule bounded_linear_compose [OF h.bounded_linear_right `bounded_linear g'`])
- apply (rule bounded_linear_compose [OF h.bounded_linear_left `bounded_linear f'`])
- done
- thus ?thesis using tendsto_add[OF * **] unfolding has_derivative_within
- unfolding g'.add f'.scaleR f'.add g'.scaleR f'.diff g'.diff
- h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left
- scaleR_right_diff_distrib h.zero_right h.zero_left
- by(auto simp add:field_simps)
-qed
-
-lemma has_derivative_bilinear_at:
- assumes "(f has_derivative f') (at x)"
- assumes "(g has_derivative g') (at x)"
- assumes "bounded_bilinear h"
- shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
- using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
-
subsection {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> (real filter \<Rightarrow> bool)"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Apr 09 14:04:47 2013 +0200
@@ -4405,8 +4405,8 @@
have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
apply(rule diff_chain_within) apply(rule has_derivative_add)
unfolding scaleR_simps
- apply(intro has_derivative_intros)
- apply(intro has_derivative_intros)
+ apply(intro FDERIV_intros)
+ apply(intro FDERIV_intros)
apply(rule has_derivative_within_subset,rule assms(6)[rule_format])
apply(rule *) apply safe apply(rule conv[unfolded scaleR_simps]) using `x\<in>s` `c\<in>s` by auto
thus "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})" unfolding o_def .
--- a/src/HOL/Real_Vector_Spaces.thy Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Apr 09 14:04:47 2013 +0200
@@ -1048,6 +1048,73 @@
end
+lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)"
+ by default (auto intro!: exI[of _ 1])
+
+lemma bounded_linear_zero[simp]: "bounded_linear (\<lambda>x. 0)"
+ by default (auto intro!: exI[of _ 1])
+
+lemma bounded_linear_add:
+ assumes "bounded_linear f"
+ assumes "bounded_linear g"
+ shows "bounded_linear (\<lambda>x. f x + g x)"
+proof -
+ interpret f: bounded_linear f by fact
+ interpret g: bounded_linear g by fact
+ show ?thesis
+ proof
+ from f.bounded obtain Kf where Kf: "\<And>x. norm (f x) \<le> norm x * Kf" by blast
+ from g.bounded obtain Kg where Kg: "\<And>x. norm (g x) \<le> norm x * Kg" by blast
+ show "\<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K"
+ using add_mono[OF Kf Kg]
+ by (intro exI[of _ "Kf + Kg"]) (auto simp: field_simps intro: norm_triangle_ineq order_trans)
+ qed (simp_all add: f.add g.add f.scaleR g.scaleR scaleR_right_distrib)
+qed
+
+lemma bounded_linear_minus:
+ assumes "bounded_linear f"
+ shows "bounded_linear (\<lambda>x. - f x)"
+proof -
+ interpret f: bounded_linear f by fact
+ show ?thesis apply (unfold_locales)
+ apply (simp add: f.add)
+ apply (simp add: f.scaleR)
+ apply (simp add: f.bounded)
+ done
+qed
+
+lemma bounded_linear_compose:
+ assumes "bounded_linear f"
+ assumes "bounded_linear g"
+ shows "bounded_linear (\<lambda>x. f (g x))"
+proof -
+ interpret f: bounded_linear f by fact
+ interpret g: bounded_linear g by fact
+ show ?thesis proof (unfold_locales)
+ fix x y show "f (g (x + y)) = f (g x) + f (g y)"
+ by (simp only: f.add g.add)
+ next
+ fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
+ by (simp only: f.scaleR g.scaleR)
+ next
+ from f.pos_bounded
+ obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
+ from g.pos_bounded
+ obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
+ show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
+ proof (intro exI allI)
+ fix x
+ have "norm (f (g x)) \<le> norm (g x) * Kf"
+ using f .
+ also have "\<dots> \<le> (norm x * Kg) * Kf"
+ using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
+ also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
+ by (rule mult_assoc)
+ finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
+ qed
+ qed
+qed
+
lemma bounded_bilinear_mult:
"bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
apply (rule bounded_bilinear.intro)
@@ -1069,6 +1136,12 @@
using bounded_bilinear_mult
by (rule bounded_bilinear.bounded_linear_right)
+lemmas bounded_linear_mult_const =
+ bounded_linear_mult_left [THEN bounded_linear_compose]
+
+lemmas bounded_linear_const_mult =
+ bounded_linear_mult_right [THEN bounded_linear_compose]
+
lemma bounded_linear_divide:
"bounded_linear (\<lambda>x::'a::real_normed_field. x / y)"
unfolding divide_inverse by (rule bounded_linear_mult_left)
@@ -1093,6 +1166,18 @@
lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
unfolding of_real_def by (rule bounded_linear_scaleR_left)
+lemma real_bounded_linear:
+ fixes f :: "real \<Rightarrow> real"
+ shows "bounded_linear f \<longleftrightarrow> (\<exists>c::real. f = (\<lambda>x. x * c))"
+proof -
+ { fix x assume "bounded_linear f"
+ then interpret bounded_linear f .
+ from scaleR[of x 1] have "f x = x * f 1"
+ by simp }
+ then show ?thesis
+ by (auto intro: exI[of _ "f 1"] bounded_linear_mult_left)
+qed
+
instance real_normed_algebra_1 \<subseteq> perfect_space
proof
fix x::'a