src/HOL/Deriv.thy

   Usually the filter @{term F} is @{term "at x within s"}.  @{term "(f has_derivative D)
   (at x within s)"} means: @{term D} is the derivative of function @{term f} at point @{term x}
   within the set @{term s}. Where @{term s} is used to express left or right sided derivatives. In
   most cases @{term s} is either a variable or @{term UNIV}.
 \<close>
+
+text \<open>These are the only cases we'll care about, probably.\<close>
+
+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)))) \<longlongrightarrow> 0) (at x within s)"
+  unfolding has_derivative_def tendsto_iff
+  by (subst eventually_Lim_ident_at) (auto simp add: field_simps)
 
 lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
   by simp
 
 definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"

 lemma has_derivative_subset:
   "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
   by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset)
 
 lemmas has_derivative_within_subset = has_derivative_subset
+
+lemma has_derivative_within_singleton_iff:
+  "(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g"
+  by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear)
+
+
+subsubsection \<open>Limit transformation for derivatives\<close>
+
+lemma has_derivative_transform_within:
+  assumes "(f has_derivative f') (at x within s)"
+    and "0 < d"
+    and "x \<in> s"
+    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+  unfolding has_derivative_within
+  by (force simp add: intro: Lim_transform_within)
+
+lemma has_derivative_transform_within_open:
+  assumes "(f has_derivative f') (at x within t)"
+    and "open s"
+    and "x \<in> s"
+    and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
+  shows "(g has_derivative f') (at x within t)"
+  using assms unfolding has_derivative_within
+  by (force simp add: intro: Lim_transform_within_open)
+
+lemma has_derivative_transform:
+  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+  assumes "(f has_derivative f') (at x within s)"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+  by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto
+
+lemma has_derivative_transform_eventually:
+  assumes "(f has_derivative f') (at x within s)"
+    "(\<forall>\<^sub>F x' in at x within s. f x' = g x')"
+  assumes "f x = g x" "x \<in> s"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+proof -
+  from assms(2,3) obtain d where "d > 0" "\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'"
+    by (force simp: eventually_at)
+  from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)]
+  show ?thesis .
+qed
 
 
 subsection \<open>Continuity\<close>
 
 lemma has_derivative_continuous:

 
 lemma has_derivative_compose:
   "(f has_derivative f') (at x within s) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow>
   ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
   by (blast intro: has_derivative_in_compose has_derivative_subset)
+
+lemma has_derivative_in_compose2:
+  assumes "\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)"
+  assumes "f ` s \<subseteq> t" "x \<in> s"
+  assumes "(f has_derivative f') (at x within s)"
+  shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)"
+  using assms
+  by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g])
 
 lemma (in bounded_bilinear) FDERIV:
   assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)"
 proof -

 text \<open>
 This can not generally shown for @{const has_derivative}, as we need to approach the point from
 all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>.
 \<close>
 
+lemma has_derivative_at2: "(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)))) \<longlongrightarrow> 0) (at x)"
+  using has_derivative_within [of f f' x UNIV]
+  by simp
 lemma has_derivative_zero_unique:
   assumes "((\<lambda>x. 0) has_derivative F) (at x)"
   shows "F = (\<lambda>h. 0)"
 proof -
   interpret F: bounded_linear F

 lemma differentiable_compose:
   "f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow>
     (\<lambda>x. f (g x)) differentiable (at x within s)"
   by (blast intro: differentiable_in_compose differentiable_subset)
 
-lemma differentiable_sum [simp, derivative_intros]:
+lemma differentiable_add [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_add)
+
+lemma differentiable_sum[simp, derivative_intros]:
+  assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
+  shows "(\<lambda>x. sum (\<lambda>a. f a x) s) differentiable net"
+proof -
+  from bchoice[OF assms(2)[unfolded differentiable_def]]
+  show ?thesis
+    by (auto intro!: has_derivative_sum simp: differentiable_def)
+qed
 
 lemma differentiable_minus [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_minus)
 

   unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
 
 lemma mult_commute_abs: "(\<lambda>x. x * c) = ( * ) c"
   for c :: "'a::ab_semigroup_mult"
   by (simp add: fun_eq_iff mult.commute)
+
+lemma DERIV_compose_FDERIV:
+  fixes f::"real\<Rightarrow>real"
+  assumes "DERIV f (g x) :> f'"
+  assumes "(g has_derivative g') (at x within s)"
+  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
+  using assms has_derivative_compose[of g g' x s f "( * ) f'"]
+  by (auto simp: has_field_derivative_def ac_simps)
 
 
 subsection \<open>Vector derivative\<close>
 
 lemma has_field_derivative_iff_has_vector_derivative:

   then show "\<forall>\<^sub>F y in nhds x. real_of_int \<lfloor>f y\<rfloor> = real_of_int \<lfloor>f x\<rfloor>"
     unfolding eventually_at_filter
     by eventually_elim auto
 qed
 
+lemmas has_derivative_floor[derivative_intros] =
+  floor_has_real_derivative[THEN DERIV_compose_FDERIV]
 
 text \<open>Caratheodory formulation of derivative at a point\<close>
 
 lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
   "(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)"