equal
deleted
inserted
replaced
87 |
87 |
88 lemma (in bounded_linear) bounded_linear: "bounded_linear f" .. |
88 lemma (in bounded_linear) bounded_linear: "bounded_linear f" .. |
89 |
89 |
90 lemma (in bounded_linear) has_derivative: |
90 lemma (in bounded_linear) has_derivative: |
91 "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F" |
91 "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F" |
92 using assms unfolding has_derivative_def |
92 unfolding has_derivative_def |
93 apply safe |
93 apply safe |
94 apply (erule bounded_linear_compose [OF bounded_linear]) |
94 apply (erule bounded_linear_compose [OF bounded_linear]) |
95 apply (drule tendsto) |
95 apply (drule tendsto) |
96 apply (simp add: scaleR diff add zero) |
96 apply (simp add: scaleR diff add zero) |
97 done |
97 done |
535 unfolding differentiable_def by (blast intro: has_derivative_inverse) |
535 unfolding differentiable_def by (blast intro: has_derivative_inverse) |
536 |
536 |
537 lemma differentiable_divide [simp, derivative_intros]: |
537 lemma differentiable_divide [simp, derivative_intros]: |
538 fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field" |
538 fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field" |
539 shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)" |
539 shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)" |
540 unfolding divide_inverse using assms by simp |
540 unfolding divide_inverse by simp |
541 |
541 |
542 lemma differentiable_power [simp, derivative_intros]: |
542 lemma differentiable_power [simp, derivative_intros]: |
543 fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field" |
543 fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field" |
544 shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)" |
544 shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)" |
545 unfolding differentiable_def by (blast intro: has_derivative_power) |
545 unfolding differentiable_def by (blast intro: has_derivative_power) |
740 corollary DERIV_minus: "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)" |
740 corollary DERIV_minus: "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)" |
741 by (rule field_differentiable_minus) |
741 by (rule field_differentiable_minus) |
742 |
742 |
743 lemma field_differentiable_diff[derivative_intros]: |
743 lemma field_differentiable_diff[derivative_intros]: |
744 "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> ((\<lambda>z. f z - g z) has_field_derivative f' - g') F" |
744 "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> ((\<lambda>z. f z - g z) has_field_derivative f' - g') F" |
745 by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus) |
745 by (simp only: diff_conv_add_uminus field_differentiable_add field_differentiable_minus) |
746 |
746 |
747 corollary DERIV_diff: |
747 corollary DERIV_diff: |
748 "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow> |
748 "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow> |
749 ((\<lambda>x. f x - g x) has_field_derivative D - E) (at x within s)" |
749 ((\<lambda>x. f x - g x) has_field_derivative D - E) (at x within s)" |
750 by (rule field_differentiable_diff) |
750 by (rule field_differentiable_diff) |