1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Jul 04 09:25:17 2010 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sun Jul 04 09:26:30 2010 -0700
1.3 @@ -39,7 +39,24 @@
1.4 unfolding dist_norm diff_0_right norm_scaleR
1.5 unfolding dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed
1.6
1.7 -lemma FDERIV_conv_has_derivative:"FDERIV f (x::'a::{real_normed_vector,perfect_space}) :> f' = (f has_derivative f') (at x)" (is "?l = ?r") proof
1.8 +lemma netlimit_at_vector:
1.9 + fixes a :: "'a::real_normed_vector"
1.10 + shows "netlimit (at a) = a"
1.11 +proof (cases "\<exists>x. x \<noteq> a")
1.12 + case True then obtain x where x: "x \<noteq> a" ..
1.13 + have "\<not> trivial_limit (at a)"
1.14 + unfolding trivial_limit_def eventually_at dist_norm
1.15 + apply clarsimp
1.16 + apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI)
1.17 + apply (simp add: norm_sgn sgn_zero_iff x)
1.18 + done
1.19 + thus ?thesis
1.20 + by (rule netlimit_within [of a UNIV, unfolded within_UNIV])
1.21 +qed simp
1.22 +
1.23 +lemma FDERIV_conv_has_derivative:
1.24 + shows "FDERIV f x :> f' = (f has_derivative f') (at x)" (is "?l = ?r")
1.25 +proof
1.26 assume ?l note as = this[unfolded fderiv_def]
1.27 show ?r unfolding has_derivative_def Lim_at apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule)
1.28 fix e::real assume "e>0"
1.29 @@ -47,14 +64,14 @@
1.30 thus "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
1.31 dist ((1 / norm (xa - netlimit (at x))) *\<^sub>R (f xa - (f (netlimit (at x)) + f' (xa - netlimit (at x))))) (0) < e"
1.32 apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa - x" in allE)
1.33 - unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next
1.34 + unfolding dist_norm netlimit_at_vector[of x] by (auto simp add: diff_diff_eq) qed next
1.35 assume ?r note as = this[unfolded has_derivative_def]
1.36 show ?l unfolding fderiv_def LIM_def apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule)
1.37 fix e::real assume "e>0"
1.38 guess d using as[THEN conjunct2,unfolded Lim_at,rule_format,OF`e>0`] ..
1.39 thus "\<exists>s>0. \<forall>xa. xa \<noteq> 0 \<and> dist xa 0 < s \<longrightarrow> dist (norm (f (x + xa) - f x - f' xa) / norm xa) 0 < e" apply-
1.40 apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE)
1.41 - unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed
1.42 + unfolding dist_norm netlimit_at_vector[of x] by (auto simp add: diff_diff_eq add.commute) qed qed
1.43
1.44 subsection {* These are the only cases we'll care about, probably. *}
1.45
1.46 @@ -86,7 +103,7 @@
1.47
1.48 lemma has_derivative_within_open:
1.49 "a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
1.50 - unfolding has_derivative_within has_derivative_at using Lim_within_open by auto
1.51 + by (simp only: at_within_interior interior_open)
1.52
1.53 lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
1.54 proof -
1.55 @@ -272,7 +289,7 @@
1.56
1.57 lemma differentiable_within_open: assumes "a \<in> s" "open s" shows
1.58 "f differentiable (at a within s) \<longleftrightarrow> (f differentiable (at a))"
1.59 - unfolding differentiable_def has_derivative_within_open[OF assms] by auto
1.60 + using assms by (simp only: at_within_interior interior_open)
1.61
1.62 lemma differentiable_on_eq_differentiable_at: "open s \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))"
1.63 unfolding differentiable_on_def by(auto simp add: differentiable_within_open)
1.64 @@ -477,10 +494,12 @@
1.65 \<Longrightarrow> (g o f) differentiable (at x within s)"
1.66 unfolding differentiable_def by(meson diff_chain_within)
1.67
1.68 -subsection {* Uniqueness of derivative. *)
1.69 -(* *)
1.70 -(* The general result is a bit messy because we need approachability of the *)
1.71 -(* limit point from any direction. But OK for nontrivial intervals etc. *}
1.72 +subsection {* Uniqueness of derivative *}
1.73 +
1.74 +text {*
1.75 + The general result is a bit messy because we need approachability of the
1.76 + limit point from any direction. But OK for nontrivial intervals etc.
1.77 +*}
1.78
1.79 lemma frechet_derivative_unique_within: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1.80 assumes "(f has_derivative f') (at x within s)" "(f has_derivative f'') (at x within s)"
1.81 @@ -507,10 +526,10 @@
1.82 unfolding dist_norm unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
1.83 scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib using i by auto qed qed
1.84
1.85 -lemma frechet_derivative_unique_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1.86 +lemma frechet_derivative_unique_at:
1.87 shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
1.88 - apply(rule frechet_derivative_unique_within[of f f' x UNIV f'']) unfolding within_UNIV apply(assumption)+
1.89 - apply(rule,rule,rule,rule) apply(rule_tac x="e/2" in exI) by auto
1.90 + unfolding FDERIV_conv_has_derivative [symmetric]
1.91 + by (rule FDERIV_unique)
1.92
1.93 lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
1.94 unfolding continuous_at Lim_at unfolding dist_nz by auto
1.95 @@ -547,7 +566,7 @@
1.96 by (rule frechet_derivative_unique_at)
1.97 qed
1.98
1.99 -lemma frechet_derivative_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1.100 +lemma frechet_derivative_at:
1.101 shows "(f has_derivative f') (at x) \<Longrightarrow> (f' = frechet_derivative f (at x))"
1.102 apply(rule frechet_derivative_unique_at[of f],assumption)
1.103 unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto
1.104 @@ -1241,13 +1260,16 @@
1.105 using f' unfolding scaleR[THEN sym] by auto
1.106 next assume ?r thus ?l unfolding vector_derivative_def has_vector_derivative_def differentiable_def by auto qed
1.107
1.108 -lemma vector_derivative_unique_at: fixes f::"real\<Rightarrow> 'n::euclidean_space"
1.109 - assumes "(f has_vector_derivative f') (at x)" "(f has_vector_derivative f'') (at x)" shows "f' = f''" proof-
1.110 - have *:"(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')" apply(rule frechet_derivative_unique_at)
1.111 - using assms[unfolded has_vector_derivative_def] by auto
1.112 - show ?thesis proof(rule ccontr) assume "f' \<noteq> f''" moreover
1.113 - hence "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')" using * by auto
1.114 - ultimately show False unfolding expand_fun_eq by auto qed qed
1.115 +lemma vector_derivative_unique_at:
1.116 + assumes "(f has_vector_derivative f') (at x)"
1.117 + assumes "(f has_vector_derivative f'') (at x)"
1.118 + shows "f' = f''"
1.119 +proof-
1.120 + have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
1.121 + using assms [unfolded has_vector_derivative_def]
1.122 + by (rule frechet_derivative_unique_at)
1.123 + thus ?thesis unfolding expand_fun_eq by auto
1.124 +qed
1.125
1.126 lemma vector_derivative_unique_within_closed_interval: fixes f::"real \<Rightarrow> 'n::ordered_euclidean_space"
1.127 assumes "a < b" "x \<in> {a..b}"
1.128 @@ -1260,8 +1282,8 @@
1.129 hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" using * by (auto simp: expand_fun_eq)
1.130 ultimately show False unfolding o_def by auto qed qed
1.131
1.132 -lemma vector_derivative_at: fixes f::"real \<Rightarrow> 'a::euclidean_space" shows
1.133 - "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
1.134 +lemma vector_derivative_at:
1.135 + shows "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
1.136 apply(rule vector_derivative_unique_at) defer apply assumption
1.137 unfolding vector_derivative_works[THEN sym] differentiable_def
1.138 unfolding has_vector_derivative_def by auto