14 lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z" |
14 lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z" |
15 by (simp add: complex_nonneg_Reals_iff cmod_eq_Re) |
15 by (simp add: complex_nonneg_Reals_iff cmod_eq_Re) |
16 |
16 |
17 lemma has_derivative_mult_right: |
17 lemma has_derivative_mult_right: |
18 fixes c:: "'a :: real_normed_algebra" |
18 fixes c:: "'a :: real_normed_algebra" |
19 shows "((( * ) c) has_derivative (( * ) c)) F" |
19 shows "(((*) c) has_derivative ((*) c)) F" |
20 by (rule has_derivative_mult_right [OF has_derivative_ident]) |
20 by (rule has_derivative_mult_right [OF has_derivative_ident]) |
21 |
21 |
22 lemma has_derivative_of_real[derivative_intros, simp]: |
22 lemma has_derivative_of_real[derivative_intros, simp]: |
23 "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F" |
23 "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F" |
24 using bounded_linear.has_derivative[OF bounded_linear_of_real] . |
24 using bounded_linear.has_derivative[OF bounded_linear_of_real] . |
25 |
25 |
26 lemma has_vector_derivative_real_field: |
26 lemma has_vector_derivative_real_field: |
27 "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)" |
27 "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)" |
28 using has_derivative_compose[of of_real of_real a _ f "( * ) f'"] |
28 using has_derivative_compose[of of_real of_real a _ f "(*) f'"] |
29 by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def) |
29 by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def) |
30 lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field |
30 lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field |
31 |
31 |
32 lemma fact_cancel: |
32 lemma fact_cancel: |
33 fixes c :: "'a::real_field" |
33 fixes c :: "'a::real_field" |
57 lemma vector_derivative_cnj: |
57 lemma vector_derivative_cnj: |
58 assumes "f differentiable at x" |
58 assumes "f differentiable at x" |
59 shows "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))" |
59 shows "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))" |
60 using assms by (intro vector_derivative_cnj_within) auto |
60 using assms by (intro vector_derivative_cnj_within) auto |
61 |
61 |
62 lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0" |
62 lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0" |
63 by auto |
63 by auto |
64 |
64 |
65 lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1" |
65 lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1" |
66 by auto |
66 by auto |
67 |
67 |
68 lemma uniformly_continuous_on_cmul_right [continuous_intros]: |
68 lemma uniformly_continuous_on_cmul_right [continuous_intros]: |
69 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
69 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
70 shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)" |
70 shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)" |
281 by (metis field_differentiable_transform_within linordered_field_no_ub holomorphic_on_def) |
281 by (metis field_differentiable_transform_within linordered_field_no_ub holomorphic_on_def) |
282 |
282 |
283 lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t" |
283 lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t" |
284 by (metis holomorphic_transform) |
284 by (metis holomorphic_transform) |
285 |
285 |
286 lemma holomorphic_on_linear [simp, holomorphic_intros]: "(( * ) c) holomorphic_on s" |
286 lemma holomorphic_on_linear [simp, holomorphic_intros]: "((*) c) holomorphic_on s" |
287 unfolding holomorphic_on_def by (metis field_differentiable_linear) |
287 unfolding holomorphic_on_def by (metis field_differentiable_linear) |
288 |
288 |
289 lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s" |
289 lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s" |
290 unfolding holomorphic_on_def by (metis field_differentiable_const) |
290 unfolding holomorphic_on_def by (metis field_differentiable_const) |
291 |
291 |
570 also have "... \<longleftrightarrow> ?rhs" |
570 also have "... \<longleftrightarrow> ?rhs" |
571 by (auto simp: analytic_on_open) |
571 by (auto simp: analytic_on_open) |
572 finally show ?thesis . |
572 finally show ?thesis . |
573 qed |
573 qed |
574 |
574 |
575 lemma analytic_on_linear [analytic_intros,simp]: "(( * ) c) analytic_on S" |
575 lemma analytic_on_linear [analytic_intros,simp]: "((*) c) analytic_on S" |
576 by (auto simp add: analytic_on_holomorphic) |
576 by (auto simp add: analytic_on_holomorphic) |
577 |
577 |
578 lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on S" |
578 lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on S" |
579 by (metis analytic_on_def holomorphic_on_const zero_less_one) |
579 by (metis analytic_on_def holomorphic_on_const zero_less_one) |
580 |
580 |
903 from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open) |
903 from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open) |
904 have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)" |
904 have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)" |
905 by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within) |
905 by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within) |
906 then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x" |
906 then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x" |
907 "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast |
907 "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast |
908 from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)" |
908 from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)" |
909 by (simp add: has_field_derivative_def S) |
909 by (simp add: has_field_derivative_def S) |
910 have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)" |
910 have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)" |
911 by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x]) |
911 by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x]) |
912 (insert g, auto simp: sums_iff) |
912 (insert g, auto simp: sums_iff) |
913 thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def |
913 thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def |
914 by (auto simp: summable_def field_differentiable_def has_field_derivative_def) |
914 by (auto simp: summable_def field_differentiable_def has_field_derivative_def) |
915 qed |
915 qed |