equal
deleted
inserted
replaced
385 "norm (f y - f x - f' (y - x)) \<le> e / 2 * norm (y - x)" |
385 "norm (f y - f x - f' (y - x)) \<le> e / 2 * norm (y - x)" |
386 thus "\<bar>1 / norm (y - x)\<bar> * norm (f y - (f x + f' (y - x))) < e" |
386 thus "\<bar>1 / norm (y - x)\<bar> * norm (f y - (f x + f' (y - x))) < e" |
387 apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:group_simps) qed auto qed |
387 apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:group_simps) qed auto qed |
388 |
388 |
389 lemma has_derivative_at_alt: |
389 lemma has_derivative_at_alt: |
390 "(f has_derivative f') (at (x::real^'n)) \<longleftrightarrow> bounded_linear f' \<and> |
390 "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and> |
391 (\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm(f y - f x - f'(y - x)) \<le> e * norm(y - x))" |
391 (\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm(f y - f x - f'(y - x)) \<le> e * norm(y - x))" |
392 using has_derivative_within_alt[where s=UNIV] unfolding within_UNIV by auto |
392 using has_derivative_within_alt[where s=UNIV] unfolding within_UNIV by auto |
393 |
393 |
394 subsection {* The chain rule. *} |
394 subsection {* The chain rule. *} |
395 |
395 |