23 Usually the filter @{term F} is @{term "at x within s"}. @{term "(f has_derivative D) |
23 Usually the filter @{term F} is @{term "at x within s"}. @{term "(f has_derivative D) |
24 (at x within s)"} means: @{term D} is the derivative of function @{term f} at point @{term x} |
24 (at x within s)"} means: @{term D} is the derivative of function @{term f} at point @{term x} |
25 within the set @{term s}. Where @{term s} is used to express left or right sided derivatives. In |
25 within the set @{term s}. Where @{term s} is used to express left or right sided derivatives. In |
26 most cases @{term s} is either a variable or @{term UNIV}. |
26 most cases @{term s} is either a variable or @{term UNIV}. |
27 \<close> |
27 \<close> |
|
28 |
|
29 text \<open>These are the only cases we'll care about, probably.\<close> |
|
30 |
|
31 lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow> |
|
32 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)" |
|
33 unfolding has_derivative_def tendsto_iff |
|
34 by (subst eventually_Lim_ident_at) (auto simp add: field_simps) |
28 |
35 |
29 lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F" |
36 lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F" |
30 by simp |
37 by simp |
31 |
38 |
32 definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool" |
39 definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool" |
186 lemma has_derivative_subset: |
193 lemma has_derivative_subset: |
187 "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)" |
194 "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)" |
188 by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset) |
195 by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset) |
189 |
196 |
190 lemmas has_derivative_within_subset = has_derivative_subset |
197 lemmas has_derivative_within_subset = has_derivative_subset |
|
198 |
|
199 lemma has_derivative_within_singleton_iff: |
|
200 "(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g" |
|
201 by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear) |
|
202 |
|
203 |
|
204 subsubsection \<open>Limit transformation for derivatives\<close> |
|
205 |
|
206 lemma has_derivative_transform_within: |
|
207 assumes "(f has_derivative f') (at x within s)" |
|
208 and "0 < d" |
|
209 and "x \<in> s" |
|
210 and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'" |
|
211 shows "(g has_derivative f') (at x within s)" |
|
212 using assms |
|
213 unfolding has_derivative_within |
|
214 by (force simp add: intro: Lim_transform_within) |
|
215 |
|
216 lemma has_derivative_transform_within_open: |
|
217 assumes "(f has_derivative f') (at x within t)" |
|
218 and "open s" |
|
219 and "x \<in> s" |
|
220 and "\<And>x. x\<in>s \<Longrightarrow> f x = g x" |
|
221 shows "(g has_derivative f') (at x within t)" |
|
222 using assms unfolding has_derivative_within |
|
223 by (force simp add: intro: Lim_transform_within_open) |
|
224 |
|
225 lemma has_derivative_transform: |
|
226 assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x" |
|
227 assumes "(f has_derivative f') (at x within s)" |
|
228 shows "(g has_derivative f') (at x within s)" |
|
229 using assms |
|
230 by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto |
|
231 |
|
232 lemma has_derivative_transform_eventually: |
|
233 assumes "(f has_derivative f') (at x within s)" |
|
234 "(\<forall>\<^sub>F x' in at x within s. f x' = g x')" |
|
235 assumes "f x = g x" "x \<in> s" |
|
236 shows "(g has_derivative f') (at x within s)" |
|
237 using assms |
|
238 proof - |
|
239 from assms(2,3) obtain d where "d > 0" "\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'" |
|
240 by (force simp: eventually_at) |
|
241 from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)] |
|
242 show ?thesis . |
|
243 qed |
191 |
244 |
192 |
245 |
193 subsection \<open>Continuity\<close> |
246 subsection \<open>Continuity\<close> |
194 |
247 |
195 lemma has_derivative_continuous: |
248 lemma has_derivative_continuous: |
292 |
345 |
293 lemma has_derivative_compose: |
346 lemma has_derivative_compose: |
294 "(f has_derivative f') (at x within s) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> |
347 "(f has_derivative f') (at x within s) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> |
295 ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)" |
348 ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)" |
296 by (blast intro: has_derivative_in_compose has_derivative_subset) |
349 by (blast intro: has_derivative_in_compose has_derivative_subset) |
|
350 |
|
351 lemma has_derivative_in_compose2: |
|
352 assumes "\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)" |
|
353 assumes "f ` s \<subseteq> t" "x \<in> s" |
|
354 assumes "(f has_derivative f') (at x within s)" |
|
355 shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)" |
|
356 using assms |
|
357 by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g]) |
297 |
358 |
298 lemma (in bounded_bilinear) FDERIV: |
359 lemma (in bounded_bilinear) FDERIV: |
299 assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" |
360 assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" |
300 shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)" |
361 shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)" |
301 proof - |
362 proof - |
465 text \<open> |
526 text \<open> |
466 This can not generally shown for @{const has_derivative}, as we need to approach the point from |
527 This can not generally shown for @{const has_derivative}, as we need to approach the point from |
467 all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>. |
528 all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>. |
468 \<close> |
529 \<close> |
469 |
530 |
|
531 lemma has_derivative_at2: "(f has_derivative f') (at x) \<longleftrightarrow> |
|
532 bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)" |
|
533 using has_derivative_within [of f f' x UNIV] |
|
534 by simp |
470 lemma has_derivative_zero_unique: |
535 lemma has_derivative_zero_unique: |
471 assumes "((\<lambda>x. 0) has_derivative F) (at x)" |
536 assumes "((\<lambda>x. 0) has_derivative F) (at x)" |
472 shows "F = (\<lambda>h. 0)" |
537 shows "F = (\<lambda>h. 0)" |
473 proof - |
538 proof - |
474 interpret F: bounded_linear F |
539 interpret F: bounded_linear F |
540 lemma differentiable_compose: |
605 lemma differentiable_compose: |
541 "f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> |
606 "f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> |
542 (\<lambda>x. f (g x)) differentiable (at x within s)" |
607 (\<lambda>x. f (g x)) differentiable (at x within s)" |
543 by (blast intro: differentiable_in_compose differentiable_subset) |
608 by (blast intro: differentiable_in_compose differentiable_subset) |
544 |
609 |
545 lemma differentiable_sum [simp, derivative_intros]: |
610 lemma differentiable_add [simp, derivative_intros]: |
546 "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F" |
611 "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F" |
547 unfolding differentiable_def by (blast intro: has_derivative_add) |
612 unfolding differentiable_def by (blast intro: has_derivative_add) |
|
613 |
|
614 lemma differentiable_sum[simp, derivative_intros]: |
|
615 assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net" |
|
616 shows "(\<lambda>x. sum (\<lambda>a. f a x) s) differentiable net" |
|
617 proof - |
|
618 from bchoice[OF assms(2)[unfolded differentiable_def]] |
|
619 show ?thesis |
|
620 by (auto intro!: has_derivative_sum simp: differentiable_def) |
|
621 qed |
548 |
622 |
549 lemma differentiable_minus [simp, derivative_intros]: |
623 lemma differentiable_minus [simp, derivative_intros]: |
550 "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F" |
624 "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F" |
551 unfolding differentiable_def by (blast intro: has_derivative_minus) |
625 unfolding differentiable_def by (blast intro: has_derivative_minus) |
552 |
626 |
648 unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff .. |
722 unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff .. |
649 |
723 |
650 lemma mult_commute_abs: "(\<lambda>x. x * c) = ( * ) c" |
724 lemma mult_commute_abs: "(\<lambda>x. x * c) = ( * ) c" |
651 for c :: "'a::ab_semigroup_mult" |
725 for c :: "'a::ab_semigroup_mult" |
652 by (simp add: fun_eq_iff mult.commute) |
726 by (simp add: fun_eq_iff mult.commute) |
|
727 |
|
728 lemma DERIV_compose_FDERIV: |
|
729 fixes f::"real\<Rightarrow>real" |
|
730 assumes "DERIV f (g x) :> f'" |
|
731 assumes "(g has_derivative g') (at x within s)" |
|
732 shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)" |
|
733 using assms has_derivative_compose[of g g' x s f "( * ) f'"] |
|
734 by (auto simp: has_field_derivative_def ac_simps) |
653 |
735 |
654 |
736 |
655 subsection \<open>Vector derivative\<close> |
737 subsection \<open>Vector derivative\<close> |
656 |
738 |
657 lemma has_field_derivative_iff_has_vector_derivative: |
739 lemma has_field_derivative_iff_has_vector_derivative: |
996 then show "\<forall>\<^sub>F y in nhds x. real_of_int \<lfloor>f y\<rfloor> = real_of_int \<lfloor>f x\<rfloor>" |
1078 then show "\<forall>\<^sub>F y in nhds x. real_of_int \<lfloor>f y\<rfloor> = real_of_int \<lfloor>f x\<rfloor>" |
997 unfolding eventually_at_filter |
1079 unfolding eventually_at_filter |
998 by eventually_elim auto |
1080 by eventually_elim auto |
999 qed |
1081 qed |
1000 |
1082 |
|
1083 lemmas has_derivative_floor[derivative_intros] = |
|
1084 floor_has_real_derivative[THEN DERIV_compose_FDERIV] |
1001 |
1085 |
1002 text \<open>Caratheodory formulation of derivative at a point\<close> |
1086 text \<open>Caratheodory formulation of derivative at a point\<close> |
1003 |
1087 |
1004 lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*) |
1088 lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*) |
1005 "(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)" |
1089 "(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)" |