complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 07 15:57:02 2016 +0000
@@ -208,7 +208,7 @@
the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
can integrate all derivatives.''
-"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec.
+"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec.
Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151-165.
And indeed he does not assume that his derivatives are continuous, but the penalty is unreasonably
@@ -645,7 +645,7 @@
where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g \<or> ~ f contour_integrable_on g \<and> i=0"
lemma not_integrable_contour_integral: "~ f contour_integrable_on g \<Longrightarrow> contour_integral g f = 0"
- unfolding contour_integrable_on_def contour_integral_def by blast
+ unfolding contour_integrable_on_def contour_integral_def by blast
lemma contour_integral_unique: "(f has_contour_integral i) g \<Longrightarrow> contour_integral g f = i"
apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def)
@@ -1113,7 +1113,7 @@
lemma contour_integral_shiftpath:
assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
shows "contour_integral (shiftpath a g) f = contour_integral g f"
- using assms
+ using assms
by (simp add: contour_integral_def contour_integrable_on_def has_contour_integral_shiftpath_eq)
@@ -1398,7 +1398,7 @@
have cfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
apply (rule continuous_on_compose [OF cg, unfolded o_def])
using assms
- apply (metis complex_differentiable_def complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
+ apply (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
done
{ fix x::real
assume a: "a < x" and b: "x < b" and xk: "x \<notin> k"
@@ -2034,7 +2034,7 @@
lemma holomorphic_point_small_triangle:
assumes x: "x \<in> s"
and f: "continuous_on s f"
- and cd: "f complex_differentiable (at x within s)"
+ and cd: "f field_differentiable (at x within s)"
and e: "0 < e"
shows "\<exists>k>0. \<forall>a b c. dist a b \<le> k \<and> dist b c \<le> k \<and> dist c a \<le> k \<and>
x \<in> convex hull {a,b,c} \<and> convex hull {a,b,c} \<subseteq> s
@@ -2089,7 +2089,7 @@
} note * = this
show ?thesis
using cd e
- apply (simp add: complex_differentiable_def has_field_derivative_def has_derivative_within_alt approachable_lt_le2 Ball_def)
+ apply (simp add: field_differentiable_def has_field_derivative_def has_derivative_within_alt approachable_lt_le2 Ball_def)
apply (clarify dest!: spec mp)
using *
apply (simp add: dist_norm, blast)
@@ -2204,7 +2204,7 @@
then obtain x where x: "\<And>n. x \<in> convex hull {fa n, fb n, fc n}" by auto
then have xin: "x \<in> convex hull {a,b,c}"
using assms f0 by blast
- then have fx: "f complex_differentiable at x within (convex hull {a,b,c})"
+ then have fx: "f field_differentiable at x within (convex hull {a,b,c})"
using assms holomorphic_on_def by blast
{ fix k n
assume k: "0 < k"
@@ -2506,7 +2506,7 @@
lemma Cauchy_theorem_triangle_cofinite:
assumes "continuous_on (convex hull {a,b,c}) f"
and "finite s"
- and "(\<And>x. x \<in> interior(convex hull {a,b,c}) - s \<Longrightarrow> f complex_differentiable (at x))"
+ and "(\<And>x. x \<in> interior(convex hull {a,b,c}) - s \<Longrightarrow> f field_differentiable (at x))"
shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
using assms
proof (induction "card s" arbitrary: a b c s rule: less_induct)
@@ -2514,7 +2514,7 @@
show ?case
proof (cases "s={}")
case True with less show ?thesis
- by (fastforce simp: holomorphic_on_def complex_differentiable_at_within
+ by (fastforce simp: holomorphic_on_def field_differentiable_at_within
Cauchy_theorem_triangle_interior)
next
case False
@@ -2682,7 +2682,7 @@
assumes contf: "continuous_on s f"
and s: "starlike s" and os: "open s"
and k: "finite k"
- and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x"
+ and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f field_differentiable at x"
shows "\<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x)"
proof -
obtain a where a: "a\<in>s" and a_cs: "\<And>x. x\<in>s \<Longrightarrow> closed_segment a x \<subseteq> s"
@@ -2709,7 +2709,7 @@
lemma Cauchy_theorem_starlike:
"\<lbrakk>open s; starlike s; finite k; continuous_on s f;
- \<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x;
+ \<And>x. x \<in> s - k \<Longrightarrow> f field_differentiable at x;
valid_path g; path_image g \<subseteq> s; pathfinish g = pathstart g\<rbrakk>
\<Longrightarrow> (f has_contour_integral 0) g"
by (metis holomorphic_starlike_primitive Cauchy_theorem_primitive at_within_open)
@@ -2800,7 +2800,7 @@
fixes f :: "complex \<Rightarrow> complex"
shows
"\<lbrakk>convex s; finite k; continuous_on s f;
- \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x\<rbrakk>
+ \<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x\<rbrakk>
\<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
apply (rule contour_integral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
prefer 3
@@ -2810,7 +2810,7 @@
lemma Cauchy_theorem_convex:
"\<lbrakk>continuous_on s f; convex s; finite k;
- \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x;
+ \<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x;
valid_path g; path_image g \<subseteq> s;
pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
by (metis holomorphic_convex_primitive Cauchy_theorem_primitive)
@@ -2828,7 +2828,7 @@
text\<open>In particular for a disc\<close>
lemma Cauchy_theorem_disc:
"\<lbrakk>finite k; continuous_on (cball a e) f;
- \<And>x. x \<in> ball a e - k \<Longrightarrow> f complex_differentiable at x;
+ \<And>x. x \<in> ball a e - k \<Longrightarrow> f field_differentiable at x;
valid_path g; path_image g \<subseteq> cball a e;
pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
apply (rule Cauchy_theorem_convex)
@@ -2914,7 +2914,7 @@
and os: "open s"
and k: "finite k"
and g: "valid_path g" "path_image g \<subseteq> s"
- and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x"
+ and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f field_differentiable at x"
shows "f contour_integrable_on g"
proof -
{ fix z
@@ -2944,7 +2944,7 @@
shows "f contour_integrable_on g"
apply (rule contour_integrable_holomorphic [OF _ os Finite_Set.finite.emptyI g])
apply (simp add: fh holomorphic_on_imp_continuous_on)
- using fh by (simp add: complex_differentiable_def holomorphic_on_open os)
+ using fh by (simp add: field_differentiable_def holomorphic_on_open os)
lemma continuous_on_inversediff:
fixes z:: "'a::real_normed_field" shows "z \<notin> s \<Longrightarrow> continuous_on s (\<lambda>w. 1 / (w - z))"
@@ -3819,7 +3819,7 @@
by (auto simp: intro!: derivative_eq_intros)
ultimately have "\<exists>h. \<forall>y. norm(y - w) < norm(w - z) \<longrightarrow> (h has_field_derivative 1/(y - z)) (at y)"
using holomorphic_convex_primitive [of "ball w (norm(w - z))" "{}" "\<lambda>w. 1/(w - z)"]
- by (simp add: complex_differentiable_def Ball_def dist_norm at_within_open_NO_MATCH norm_minus_commute)
+ by (simp add: field_differentiable_def Ball_def dist_norm at_within_open_NO_MATCH norm_minus_commute)
}
then obtain h where h: "\<And>w y. w \<noteq> z \<Longrightarrow> norm(y - w) < norm(w - z) \<Longrightarrow> (h w has_field_derivative 1/(y - z)) (at y)"
by meson
@@ -3840,8 +3840,8 @@
assume t: "t \<in> {a..b}"
have cball: "continuous_on (ball (\<gamma> t) (dist (\<gamma> t) z)) (\<lambda>x. inverse (x - z))"
using z by (auto intro!: continuous_intros simp: dist_norm)
- have icd: "\<And>x. cmod (\<gamma> t - x) < cmod (\<gamma> t - z) \<Longrightarrow> (\<lambda>w. inverse (w - z)) complex_differentiable at x"
- unfolding complex_differentiable_def by (force simp: intro!: derivative_eq_intros)
+ have icd: "\<And>x. cmod (\<gamma> t - x) < cmod (\<gamma> t - z) \<Longrightarrow> (\<lambda>w. inverse (w - z)) field_differentiable at x"
+ unfolding field_differentiable_def by (force simp: intro!: derivative_eq_intros)
obtain h where h: "\<And>x. cmod (\<gamma> t - x) < cmod (\<gamma> t - z) \<Longrightarrow>
(h has_field_derivative inverse (x - z)) (at x within {y. cmod (\<gamma> t - y) < cmod (\<gamma> t - z)})"
using holomorphic_convex_primitive [where f = "\<lambda>w. inverse(w - z)", OF convex_ball finite.emptyI cball icd]
@@ -4492,13 +4492,13 @@
lemma Cauchy_integral_formula_weak:
assumes s: "convex s" and "finite k" and conf: "continuous_on s f"
- and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x)"
+ and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
and z: "z \<in> interior s - k" and vpg: "valid_path \<gamma>"
and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
proof -
obtain f' where f': "(f has_field_derivative f') (at z)"
- using fcd [OF z] by (auto simp: complex_differentiable_def)
+ using fcd [OF z] by (auto simp: field_differentiable_def)
have pas: "path_image \<gamma> \<subseteq> s" and znotin: "z \<notin> path_image \<gamma>" using pasz by blast+
have c: "continuous (at x within s) (\<lambda>w. if w = z then f' else (f w - f z) / (w - z))" if "x \<in> s" for x
proof (cases "x = z")
@@ -4525,7 +4525,7 @@
apply (rule Cauchy_theorem_convex [OF _ s fink' _ vpg pas loop])
using c apply (force simp: continuous_on_eq_continuous_within)
apply (rename_tac w)
- apply (rule_tac d="dist w z" and f = "\<lambda>w. (f w - f z)/(w - z)" in complex_differentiable_transform_within)
+ apply (rule_tac d="dist w z" and f = "\<lambda>w. (f w - f z)/(w - z)" in field_differentiable_transform_within)
apply (simp_all add: dist_pos_lt dist_commute)
apply (metis less_irrefl)
apply (rule derivative_intros fcd | simp)+
@@ -5675,7 +5675,7 @@
using open_contains_cball \<open>z \<in> s\<close> \<open>open s\<close> by blast
then have holf_cball: "f holomorphic_on cball z r"
apply (simp add: holomorphic_on_def)
- using complex_differentiable_at_within complex_differentiable_def fder by blast
+ using field_differentiable_at_within field_differentiable_def fder by blast
then have "continuous_on (path_image (circlepath z r)) f"
using \<open>r > 0\<close> by (force elim: holomorphic_on_subset [THEN holomorphic_on_imp_continuous_on])
then have contfpi: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1/(2 * of_real pi*ii) * f x)"
@@ -5715,7 +5715,7 @@
lemma holomorphic_deriv [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
-by (metis DERIV_deriv_iff_complex_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
+by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
lemma analytic_deriv: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
using analytic_on_holomorphic holomorphic_deriv by auto
@@ -5729,7 +5729,7 @@
lemma has_field_derivative_higher_deriv:
"\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
\<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
-by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply
+by (metis (no_types, hide_lams) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
@@ -5968,7 +5968,7 @@
apply (simp add: Suc.IH)
done
also have "... = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z)) z"
- apply (rule complex_derivative_cmult)
+ apply (rule deriv_cmult)
apply (rule analytic_on_imp_differentiable_at [OF _ Suc.prems])
apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and t=t, unfolded o_def])
apply (simp add: analytic_on_linear)
@@ -5978,7 +5978,7 @@
also have "... = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "op*u", unfolded o_def])
apply (rule derivative_intros)
- using Suc.prems complex_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
+ using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
apply (simp add: deriv_linear)
done
finally show ?case
@@ -6030,8 +6030,8 @@
shows "f holomorphic_on s"
proof -
{ fix z
- assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f complex_differentiable at x"
- have "f complex_differentiable at z"
+ assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f field_differentiable at x"
+ have "f field_differentiable at z"
proof (cases "z \<in> k")
case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
next
@@ -6059,19 +6059,19 @@
qed
}
with holf s k show ?thesis
- by (simp add: holomorphic_on_open open_Diff finite_imp_closed complex_differentiable_def [symmetric])
+ by (simp add: holomorphic_on_open open_Diff finite_imp_closed field_differentiable_def [symmetric])
qed
proposition Cauchy_integral_formula_convex:
assumes s: "convex s" and k: "finite k" and contf: "continuous_on s f"
- and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x)"
+ and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
and z: "z \<in> interior s" and vpg: "valid_path \<gamma>"
and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
- apply (simp add: holomorphic_on_open [symmetric] complex_differentiable_def)
+ apply (simp add: holomorphic_on_open [symmetric] field_differentiable_def)
using no_isolated_singularity [where s = "interior s"]
- apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset
+ apply (metis k contf fcd holomorphic_on_open field_differentiable_def continuous_on_subset
has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
using assms
apply auto
@@ -6103,8 +6103,8 @@
by (rule contour_integral_unique)
have "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) w) (at w)"
using Suc.prems assms has_field_derivative_higher_deriv by auto
- then have dnf_diff: "\<And>n. (deriv ^^ n) f complex_differentiable (at w)"
- by (force simp add: complex_differentiable_def)
+ then have dnf_diff: "\<And>n. (deriv ^^ n) f field_differentiable (at w)"
+ by (force simp add: field_differentiable_def)
have "deriv (\<lambda>w. complex_of_real (2 * pi) * \<i> / (fact k) * (deriv ^^ k) f w) w =
of_nat (Suc k) * contour_integral (circlepath z r) (\<lambda>u. f u / (u - w) ^ Suc (Suc k))"
by (force intro!: DERIV_imp_deriv Cauchy_next_derivative_circlepath [OF f Suc.IH _ Suc.prems])
@@ -6112,7 +6112,7 @@
by (simp only: con)
finally have "deriv (\<lambda>w. ((2 * pi) * \<i> / (fact k)) * (deriv ^^ k) f w) w = of_nat (Suc k) * X" .
then have "((2 * pi) * \<i> / (fact k)) * deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X"
- by (metis complex_derivative_cmult dnf_diff)
+ by (metis deriv_cmult dnf_diff)
then have "deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X / ((2 * pi) * \<i> / (fact k))"
by (simp add: field_simps)
then show ?case
@@ -6432,7 +6432,7 @@
let ?conint = "contour_integral (circlepath z r)"
have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r"
by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F];
- auto simp: holomorphic_on_open complex_differentiable_def)+
+ auto simp: holomorphic_on_open field_differentiable_def)+
then obtain g' where g': "\<And>x. x \<in> ball z r \<Longrightarrow> (g has_field_derivative g' x) (at x)"
using DERIV_deriv_iff_has_field_derivative
by (fastforce simp add: holomorphic_on_open)
@@ -6845,54 +6845,54 @@
shows "(\<lambda>z. if z = a then deriv f a
else (f z - f a) / (z - a)) holomorphic_on s" (is "?F holomorphic_on s")
proof -
- have F1: "?F complex_differentiable (at u within s)" if "u \<in> s" "u \<noteq> a" for u
+ have F1: "?F field_differentiable (at u within s)" if "u \<in> s" "u \<noteq> a" for u
proof -
- have fcd: "f complex_differentiable at u within s"
+ have fcd: "f field_differentiable at u within s"
using holf holomorphic_on_def by (simp add: \<open>u \<in> s\<close>)
- have cd: "(\<lambda>z. (f z - f a) / (z - a)) complex_differentiable at u within s"
+ have cd: "(\<lambda>z. (f z - f a) / (z - a)) field_differentiable at u within s"
by (rule fcd derivative_intros | simp add: that)+
have "0 < dist a u" using that dist_nz by blast
then show ?thesis
- by (rule complex_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> s\<close>)
+ by (rule field_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> s\<close>)
qed
- have F2: "?F complex_differentiable at a" if "0 < e" "ball a e \<subseteq> s" for e
+ have F2: "?F field_differentiable at a" if "0 < e" "ball a e \<subseteq> s" for e
proof -
have holfb: "f holomorphic_on ball a e"
by (rule holomorphic_on_subset [OF holf \<open>ball a e \<subseteq> s\<close>])
have 2: "?F holomorphic_on ball a e - {a}"
apply (rule holomorphic_on_subset [where s = "s - {a}"])
- apply (simp add: holomorphic_on_def complex_differentiable_def [symmetric])
+ apply (simp add: holomorphic_on_def field_differentiable_def [symmetric])
using mem_ball that
- apply (auto intro: F1 complex_differentiable_within_subset)
+ apply (auto intro: F1 field_differentiable_within_subset)
done
have "isCont (\<lambda>z. if z = a then deriv f a else (f z - f a) / (z - a)) x"
if "dist a x < e" for x
proof (cases "x=a")
case True then show ?thesis
using holfb \<open>0 < e\<close>
- apply (simp add: holomorphic_on_open complex_differentiable_def [symmetric])
+ apply (simp add: holomorphic_on_open field_differentiable_def [symmetric])
apply (drule_tac x=a in bspec)
- apply (auto simp: DERIV_deriv_iff_complex_differentiable [symmetric] continuous_at DERIV_iff2
+ apply (auto simp: DERIV_deriv_iff_field_differentiable [symmetric] continuous_at DERIV_iff2
elim: rev_iffD1 [OF _ LIM_equal])
done
next
case False with 2 that show ?thesis
- by (force simp: holomorphic_on_open open_Diff complex_differentiable_def [symmetric] complex_differentiable_imp_continuous_at)
+ by (force simp: holomorphic_on_open open_Diff field_differentiable_def [symmetric] field_differentiable_imp_continuous_at)
qed
then have 1: "continuous_on (ball a e) ?F"
by (clarsimp simp: continuous_on_eq_continuous_at)
have "?F holomorphic_on ball a e"
by (auto intro: no_isolated_singularity [OF 1 2])
with that show ?thesis
- by (simp add: holomorphic_on_open complex_differentiable_def [symmetric]
- complex_differentiable_at_within)
+ by (simp add: holomorphic_on_open field_differentiable_def [symmetric]
+ field_differentiable_at_within)
qed
show ?thesis
proof
- fix x assume "x \<in> s" show "?F complex_differentiable at x within s"
+ fix x assume "x \<in> s" show "?F field_differentiable at x within s"
proof (cases "x=a")
case True then show ?thesis
- using a by (auto simp: mem_interior intro: complex_differentiable_at_within F2)
+ using a by (auto simp: mem_interior intro: field_differentiable_at_within F2)
next
case False with F1 \<open>x \<in> s\<close>
show ?thesis by blast
@@ -6916,8 +6916,8 @@
show ?thesis by fastforce
next
case False with assms show ?thesis
- apply (simp add: holomorphic_on_def complex_differentiable_def [symmetric], clarify)
- apply (rule complex_differentiable_transform_within [where f = "\<lambda>z. (f z - f a)/(z - a)" and d = 1])
+ apply (simp add: holomorphic_on_def field_differentiable_def [symmetric], clarify)
+ apply (rule field_differentiable_transform_within [where f = "\<lambda>z. (f z - f a)/(z - a)" and d = 1])
apply (rule derivative_intros | force)+
done
qed
@@ -7082,16 +7082,16 @@
have *: "(\<lambda>c. if c = y then deriv f y else (f c - f y) / (c - y)) holomorphic_on u"
by (simp add: holf pole_lemma_open u)
then have "isCont (\<lambda>x. if x = y then deriv f y else (f x - f y) / (x - y)) y"
- using at_within_open complex_differentiable_imp_continuous_at holomorphic_on_def that u by fastforce
+ using at_within_open field_differentiable_imp_continuous_at holomorphic_on_def that u by fastforce
then have "continuous_on u (d y)"
apply (simp add: d_def continuous_on_eq_continuous_at u, clarify)
using * holomorphic_on_def
- by (meson complex_differentiable_within_open complex_differentiable_imp_continuous_at u)
+ by (meson field_differentiable_within_open field_differentiable_imp_continuous_at u)
moreover have "d y holomorphic_on u - {y}"
- apply (simp add: d_def holomorphic_on_open u open_delete complex_differentiable_def [symmetric])
+ apply (simp add: d_def holomorphic_on_open u open_delete field_differentiable_def [symmetric])
apply (intro ballI)
apply (rename_tac w)
- apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in complex_differentiable_transform_within)
+ apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in field_differentiable_transform_within)
apply (auto simp: dist_pos_lt dist_commute intro!: derivative_intros)
using analytic_on_imp_differentiable_at analytic_on_open holf u apply blast
done
@@ -7262,7 +7262,7 @@
have derf_le: "w \<in> closed_segment x' z' \<Longrightarrow> z' \<noteq> x' \<Longrightarrow> cmod (deriv f w - deriv f x) \<le> e" for w
by (blast intro: cs_less less_k1 k1 [unfolded divide_const_simps dist_norm] less_imp_le le_less_trans)
have f_has_der: "\<And>x. x \<in> u \<Longrightarrow> (f has_field_derivative deriv f x) (at x within u)"
- by (metis DERIV_deriv_iff_complex_differentiable at_within_open holf holomorphic_on_def u)
+ by (metis DERIV_deriv_iff_field_differentiable at_within_open holf holomorphic_on_def u)
have "closed_segment x' z' \<subseteq> u"
by (rule order_trans [OF _ k2]) (simp add: cs_less le_less_trans [OF _ less_k2] dist_complex_def norm_minus_commute subset_iff)
then have cint_derf: "(deriv f has_contour_integral f z' - f x') (linepath x' z')"
@@ -7306,14 +7306,14 @@
by (rule continuous_on_compose continuous_intros continuous_on_subset [OF cond_uu] | force intro: that)+
then have *: "continuous_on u (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
by (rule rev_iffD1 [OF _ continuous_on_cong [OF refl]]) (simp add: d_def field_simps)
- have **: "\<And>x. \<lbrakk>x \<in> u; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) complex_differentiable at x"
- apply (rule_tac f = "\<lambda>x. (f w - f x)/(w - x)" and d = "dist x w" in complex_differentiable_transform_within)
+ have **: "\<And>x. \<lbrakk>x \<in> u; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) field_differentiable at x"
+ apply (rule_tac f = "\<lambda>x. (f w - f x)/(w - x)" and d = "dist x w" in field_differentiable_transform_within)
apply (rule u derivative_intros holomorphic_on_imp_differentiable_at [OF holf] | force simp add: dist_commute)+
done
show ?thesis
unfolding d_def
apply (rule no_isolated_singularity [OF * _ u, where k = "{w}"])
- apply (auto simp: complex_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
+ apply (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
done
qed
{ fix a b
@@ -7388,14 +7388,14 @@
by (simp add: h_def x au o_def)
qed
show ?thesis
- proof (simp add: holomorphic_on_open complex_differentiable_def [symmetric], clarify)
+ proof (simp add: holomorphic_on_open field_differentiable_def [symmetric], clarify)
fix z0
consider "z0 \<in> v" | "z0 \<in> u" using uv_Un by blast
- then show "h complex_differentiable at z0"
+ then show "h field_differentiable at z0"
proof cases
assume "z0 \<in> v" then show ?thesis
using Cauchy_next_derivative [OF con_pa_f le_B f_has_cint _ ov] V f_has_cint \<open>valid_path \<gamma>\<close>
- by (auto simp: complex_differentiable_def v_def)
+ by (auto simp: field_differentiable_def v_def)
next
assume "z0 \<in> u" then
obtain e where "e>0" and e: "ball z0 e \<subseteq> u" by (blast intro: openE [OF u])
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 07 15:57:02 2016 +0000
@@ -277,159 +277,159 @@
subsection\<open>Holomorphic functions\<close>
-definition complex_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
- (infixr "(complex'_differentiable)" 50)
- where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
+definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
+ (infixr "(field'_differentiable)" 50)
+ where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
-lemma complex_differentiable_derivI:
- "f complex_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
-by (simp add: complex_differentiable_def DERIV_deriv_iff_has_field_derivative)
+lemma field_differentiable_derivI:
+ "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
+by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
-lemma complex_differentiable_imp_continuous_at:
- "f complex_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
- by (metis DERIV_continuous complex_differentiable_def)
+lemma field_differentiable_imp_continuous_at:
+ "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
+ by (metis DERIV_continuous field_differentiable_def)
-lemma complex_differentiable_within_subset:
- "\<lbrakk>f complex_differentiable (at x within s); t \<subseteq> s\<rbrakk>
- \<Longrightarrow> f complex_differentiable (at x within t)"
- by (metis DERIV_subset complex_differentiable_def)
+lemma field_differentiable_within_subset:
+ "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
+ \<Longrightarrow> f field_differentiable (at x within t)"
+ by (metis DERIV_subset field_differentiable_def)
-lemma complex_differentiable_at_within:
- "\<lbrakk>f complex_differentiable (at x)\<rbrakk>
- \<Longrightarrow> f complex_differentiable (at x within s)"
- unfolding complex_differentiable_def
+lemma field_differentiable_at_within:
+ "\<lbrakk>f field_differentiable (at x)\<rbrakk>
+ \<Longrightarrow> f field_differentiable (at x within s)"
+ unfolding field_differentiable_def
by (metis DERIV_subset top_greatest)
-lemma complex_differentiable_linear [simp,derivative_intros]: "(op * c) complex_differentiable F"
+lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
proof -
show ?thesis
- unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs
+ unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
by (force intro: has_derivative_mult_right)
qed
-lemma complex_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
- unfolding complex_differentiable_def has_field_derivative_def
+lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
+ unfolding field_differentiable_def has_field_derivative_def
by (rule exI [where x=0])
(metis has_derivative_const lambda_zero)
-lemma complex_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
- unfolding complex_differentiable_def has_field_derivative_def
+lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
+ unfolding field_differentiable_def has_field_derivative_def
by (rule exI [where x=1])
(simp add: lambda_one [symmetric])
-lemma complex_differentiable_id [simp,derivative_intros]: "id complex_differentiable F"
- unfolding id_def by (rule complex_differentiable_ident)
+lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
+ unfolding id_def by (rule field_differentiable_ident)
-lemma complex_differentiable_minus [derivative_intros]:
- "f complex_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) complex_differentiable F"
- using assms unfolding complex_differentiable_def
+lemma field_differentiable_minus [derivative_intros]:
+ "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
+ using assms unfolding field_differentiable_def
by (metis field_differentiable_minus)
-lemma complex_differentiable_add [derivative_intros]:
- assumes "f complex_differentiable F" "g complex_differentiable F"
- shows "(\<lambda>z. f z + g z) complex_differentiable F"
- using assms unfolding complex_differentiable_def
+lemma field_differentiable_add [derivative_intros]:
+ assumes "f field_differentiable F" "g field_differentiable F"
+ shows "(\<lambda>z. f z + g z) field_differentiable F"
+ using assms unfolding field_differentiable_def
by (metis field_differentiable_add)
-lemma complex_differentiable_add_const [simp,derivative_intros]:
- "op + c complex_differentiable F"
- by (simp add: complex_differentiable_add)
+lemma field_differentiable_add_const [simp,derivative_intros]:
+ "op + c field_differentiable F"
+ by (simp add: field_differentiable_add)
-lemma complex_differentiable_setsum [derivative_intros]:
- "(\<And>i. i \<in> I \<Longrightarrow> (f i) complex_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) complex_differentiable F"
+lemma field_differentiable_setsum [derivative_intros]:
+ "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
by (induct I rule: infinite_finite_induct)
- (auto intro: complex_differentiable_add complex_differentiable_const)
+ (auto intro: field_differentiable_add field_differentiable_const)
-lemma complex_differentiable_diff [derivative_intros]:
- assumes "f complex_differentiable F" "g complex_differentiable F"
- shows "(\<lambda>z. f z - g z) complex_differentiable F"
- using assms unfolding complex_differentiable_def
+lemma field_differentiable_diff [derivative_intros]:
+ assumes "f field_differentiable F" "g field_differentiable F"
+ shows "(\<lambda>z. f z - g z) field_differentiable F"
+ using assms unfolding field_differentiable_def
by (metis field_differentiable_diff)
-lemma complex_differentiable_inverse [derivative_intros]:
- assumes "f complex_differentiable (at a within s)" "f a \<noteq> 0"
- shows "(\<lambda>z. inverse (f z)) complex_differentiable (at a within s)"
- using assms unfolding complex_differentiable_def
+lemma field_differentiable_inverse [derivative_intros]:
+ assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
+ shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
by (metis DERIV_inverse_fun)
-lemma complex_differentiable_mult [derivative_intros]:
- assumes "f complex_differentiable (at a within s)"
- "g complex_differentiable (at a within s)"
- shows "(\<lambda>z. f z * g z) complex_differentiable (at a within s)"
- using assms unfolding complex_differentiable_def
+lemma field_differentiable_mult [derivative_intros]:
+ assumes "f field_differentiable (at a within s)"
+ "g field_differentiable (at a within s)"
+ shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
by (metis DERIV_mult [of f _ a s g])
-lemma complex_differentiable_divide [derivative_intros]:
- assumes "f complex_differentiable (at a within s)"
- "g complex_differentiable (at a within s)"
+lemma field_differentiable_divide [derivative_intros]:
+ assumes "f field_differentiable (at a within s)"
+ "g field_differentiable (at a within s)"
"g a \<noteq> 0"
- shows "(\<lambda>z. f z / g z) complex_differentiable (at a within s)"
- using assms unfolding complex_differentiable_def
+ shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
by (metis DERIV_divide [of f _ a s g])
-lemma complex_differentiable_power [derivative_intros]:
- assumes "f complex_differentiable (at a within s)"
- shows "(\<lambda>z. f z ^ n) complex_differentiable (at a within s)"
- using assms unfolding complex_differentiable_def
+lemma field_differentiable_power [derivative_intros]:
+ assumes "f field_differentiable (at a within s)"
+ shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
by (metis DERIV_power)
-lemma complex_differentiable_transform_within:
+lemma field_differentiable_transform_within:
"0 < d \<Longrightarrow>
x \<in> s \<Longrightarrow>
(\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
- f complex_differentiable (at x within s)
- \<Longrightarrow> g complex_differentiable (at x within s)"
- unfolding complex_differentiable_def has_field_derivative_def
+ f field_differentiable (at x within s)
+ \<Longrightarrow> g field_differentiable (at x within s)"
+ unfolding field_differentiable_def has_field_derivative_def
by (blast intro: has_derivative_transform_within)
-lemma complex_differentiable_compose_within:
- assumes "f complex_differentiable (at a within s)"
- "g complex_differentiable (at (f a) within f`s)"
- shows "(g o f) complex_differentiable (at a within s)"
- using assms unfolding complex_differentiable_def
+lemma field_differentiable_compose_within:
+ assumes "f field_differentiable (at a within s)"
+ "g field_differentiable (at (f a) within f`s)"
+ shows "(g o f) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
by (metis DERIV_image_chain)
-lemma complex_differentiable_compose:
- "f complex_differentiable at z \<Longrightarrow> g complex_differentiable at (f z)
- \<Longrightarrow> (g o f) complex_differentiable at z"
-by (metis complex_differentiable_at_within complex_differentiable_compose_within)
+lemma field_differentiable_compose:
+ "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
+ \<Longrightarrow> (g o f) field_differentiable at z"
+by (metis field_differentiable_at_within field_differentiable_compose_within)
-lemma complex_differentiable_within_open:
- "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f complex_differentiable at a within s \<longleftrightarrow>
- f complex_differentiable at a"
- unfolding complex_differentiable_def
+lemma field_differentiable_within_open:
+ "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
+ f field_differentiable at a"
+ unfolding field_differentiable_def
by (metis at_within_open)
subsection\<open>Caratheodory characterization\<close>
-lemma complex_differentiable_caratheodory_at:
- "f complex_differentiable (at z) \<longleftrightarrow>
+lemma field_differentiable_caratheodory_at:
+ "f field_differentiable (at z) \<longleftrightarrow>
(\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
using CARAT_DERIV [of f]
- by (simp add: complex_differentiable_def has_field_derivative_def)
+ by (simp add: field_differentiable_def has_field_derivative_def)
-lemma complex_differentiable_caratheodory_within:
- "f complex_differentiable (at z within s) \<longleftrightarrow>
+lemma field_differentiable_caratheodory_within:
+ "f field_differentiable (at z within s) \<longleftrightarrow>
(\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
using DERIV_caratheodory_within [of f]
- by (simp add: complex_differentiable_def has_field_derivative_def)
+ by (simp add: field_differentiable_def has_field_derivative_def)
subsection\<open>Holomorphic\<close>
definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
(infixl "(holomorphic'_on)" 50)
- where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f complex_differentiable (at x within s)"
+ where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f field_differentiable (at x within s)"
named_theorems holomorphic_intros "structural introduction rules for holomorphic_on"
-lemma holomorphic_onI [intro?]: "(\<And>x. x \<in> s \<Longrightarrow> f complex_differentiable (at x within s)) \<Longrightarrow> f holomorphic_on s"
+lemma holomorphic_onI [intro?]: "(\<And>x. x \<in> s \<Longrightarrow> f field_differentiable (at x within s)) \<Longrightarrow> f holomorphic_on s"
by (simp add: holomorphic_on_def)
-lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f complex_differentiable (at x within s)"
+lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x within s)"
by (simp add: holomorphic_on_def)
lemma holomorphic_on_imp_differentiable_at:
- "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f complex_differentiable (at x)"
+ "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x)"
using at_within_open holomorphic_on_def by fastforce
lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}"
@@ -437,38 +437,38 @@
lemma holomorphic_on_open:
"open s \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>f'. DERIV f x :> f')"
- by (auto simp: holomorphic_on_def complex_differentiable_def has_field_derivative_def at_within_open [of _ s])
+ by (auto simp: holomorphic_on_def field_differentiable_def has_field_derivative_def at_within_open [of _ s])
lemma holomorphic_on_imp_continuous_on:
"f holomorphic_on s \<Longrightarrow> continuous_on s f"
- by (metis complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
+ by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
lemma holomorphic_on_subset:
"f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
unfolding holomorphic_on_def
- by (metis complex_differentiable_within_subset subsetD)
+ by (metis field_differentiable_within_subset subsetD)
lemma holomorphic_transform: "\<lbrakk>f holomorphic_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g holomorphic_on s"
- by (metis complex_differentiable_transform_within linordered_field_no_ub holomorphic_on_def)
+ by (metis field_differentiable_transform_within linordered_field_no_ub holomorphic_on_def)
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"
by (metis holomorphic_transform)
lemma holomorphic_on_linear [simp, holomorphic_intros]: "(op * c) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_linear)
+ unfolding holomorphic_on_def by (metis field_differentiable_linear)
lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_const)
+ unfolding holomorphic_on_def by (metis field_differentiable_const)
lemma holomorphic_on_ident [simp, holomorphic_intros]: "(\<lambda>x. x) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_ident)
+ unfolding holomorphic_on_def by (metis field_differentiable_ident)
lemma holomorphic_on_id [simp, holomorphic_intros]: "id holomorphic_on s"
unfolding id_def by (rule holomorphic_on_ident)
lemma holomorphic_on_compose:
"f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g o f) holomorphic_on s"
- using complex_differentiable_compose_within[of f _ s g]
+ using field_differentiable_compose_within[of f _ s g]
by (auto simp: holomorphic_on_def)
lemma holomorphic_on_compose_gen:
@@ -476,49 +476,49 @@
by (metis holomorphic_on_compose holomorphic_on_subset)
lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
- by (metis complex_differentiable_minus holomorphic_on_def)
+ by (metis field_differentiable_minus holomorphic_on_def)
lemma holomorphic_on_add [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_add)
+ unfolding holomorphic_on_def by (metis field_differentiable_add)
lemma holomorphic_on_diff [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_diff)
+ unfolding holomorphic_on_def by (metis field_differentiable_diff)
lemma holomorphic_on_mult [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_mult)
+ unfolding holomorphic_on_def by (metis field_differentiable_mult)
lemma holomorphic_on_inverse [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. inverse (f z)) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_inverse)
+ unfolding holomorphic_on_def by (metis field_differentiable_inverse)
lemma holomorphic_on_divide [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. f z / g z) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_divide)
+ unfolding holomorphic_on_def by (metis field_differentiable_divide)
lemma holomorphic_on_power [holomorphic_intros]:
"f holomorphic_on s \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_power)
+ unfolding holomorphic_on_def by (metis field_differentiable_power)
lemma holomorphic_on_setsum [holomorphic_intros]:
"(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
- unfolding holomorphic_on_def by (metis complex_differentiable_setsum)
+ unfolding holomorphic_on_def by (metis field_differentiable_setsum)
-lemma DERIV_deriv_iff_complex_differentiable:
- "DERIV f x :> deriv f x \<longleftrightarrow> f complex_differentiable at x"
- unfolding complex_differentiable_def by (metis DERIV_imp_deriv)
+lemma DERIV_deriv_iff_field_differentiable:
+ "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
+ unfolding field_differentiable_def by (metis DERIV_imp_deriv)
lemma holomorphic_derivI:
"\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
\<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
-by (metis DERIV_deriv_iff_complex_differentiable at_within_open holomorphic_on_def has_field_derivative_at_within)
+by (metis DERIV_deriv_iff_field_differentiable at_within_open holomorphic_on_def has_field_derivative_at_within)
lemma complex_derivative_chain:
- "f complex_differentiable at x \<Longrightarrow> g complex_differentiable at (f x)
+ "f field_differentiable at x \<Longrightarrow> g field_differentiable at (f x)
\<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
- by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv)
+ by (metis DERIV_deriv_iff_field_differentiable DERIV_chain DERIV_imp_deriv)
lemma deriv_linear [simp]: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
by (metis DERIV_imp_deriv DERIV_cmult_Id)
@@ -532,50 +532,50 @@
lemma deriv_const [simp]: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
by (metis DERIV_imp_deriv DERIV_const)
-lemma complex_derivative_add [simp]:
- "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+lemma deriv_add [simp]:
+ "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
- unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+ unfolding DERIV_deriv_iff_field_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_intros)
-lemma complex_derivative_diff [simp]:
- "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+lemma deriv_diff [simp]:
+ "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
- unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+ unfolding DERIV_deriv_iff_field_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_intros)
-lemma complex_derivative_mult [simp]:
- "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+lemma deriv_mult [simp]:
+ "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
- unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+ unfolding DERIV_deriv_iff_field_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
-lemma complex_derivative_cmult [simp]:
- "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
- unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+lemma deriv_cmult [simp]:
+ "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
+ unfolding DERIV_deriv_iff_field_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
-lemma complex_derivative_cmult_right [simp]:
- "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
- unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+lemma deriv_cmult_right [simp]:
+ "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
+ unfolding DERIV_deriv_iff_field_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
-lemma complex_derivative_cdivide_right [simp]:
- "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c"
+lemma deriv_cdivide_right [simp]:
+ "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c"
unfolding Fields.field_class.field_divide_inverse
- by (blast intro: complex_derivative_cmult_right)
+ by (blast intro: deriv_cmult_right)
lemma complex_derivative_transform_within_open:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
\<Longrightarrow> deriv f z = deriv g z"
unfolding holomorphic_on_def
by (rule DERIV_imp_deriv)
- (metis DERIV_deriv_iff_complex_differentiable DERIV_transform_within_open at_within_open)
+ (metis DERIV_deriv_iff_field_differentiable DERIV_transform_within_open at_within_open)
-lemma complex_derivative_compose_linear:
- "f complex_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
+lemma deriv_compose_linear:
+ "f field_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
apply (rule DERIV_imp_deriv)
-apply (simp add: DERIV_deriv_iff_complex_differentiable [symmetric])
+apply (simp add: DERIV_deriv_iff_field_differentiable [symmetric])
apply (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id])
apply (simp add: algebra_simps)
done
@@ -602,7 +602,7 @@
lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
- (metis centre_in_ball complex_differentiable_at_within)
+ (metis centre_in_ball field_differentiable_at_within)
lemma analytic_on_open: "open s \<Longrightarrow> f analytic_on s \<longleftrightarrow> f holomorphic_on s"
apply (auto simp: analytic_imp_holomorphic)
@@ -610,9 +610,9 @@
by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball)
lemma analytic_on_imp_differentiable_at:
- "f analytic_on s \<Longrightarrow> x \<in> s \<Longrightarrow> f complex_differentiable (at x)"
+ "f analytic_on s \<Longrightarrow> x \<in> s \<Longrightarrow> f field_differentiable (at x)"
apply (auto simp: analytic_on_def holomorphic_on_def)
-by (metis Topology_Euclidean_Space.open_ball centre_in_ball complex_differentiable_within_open)
+by (metis Topology_Euclidean_Space.open_ball centre_in_ball field_differentiable_within_open)
lemma analytic_on_subset: "f analytic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f analytic_on t"
by (auto simp: analytic_on_def)
@@ -674,7 +674,7 @@
obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball (f x) e'" using g
by (metis analytic_on_def g image_eqI x)
have "isCont f x"
- by (metis analytic_on_imp_differentiable_at complex_differentiable_imp_continuous_at f x)
+ by (metis analytic_on_imp_differentiable_at field_differentiable_imp_continuous_at f x)
with e' obtain d where d: "0 < d" and fd: "f ` ball x d \<subseteq> ball (f x) e'"
by (auto simp: continuous_at_ball)
have "g \<circ> f holomorphic_on ball x (min d e)"
@@ -864,25 +864,25 @@
show "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
apply (rule DERIV_imp_deriv [OF DERIV_add])
using s
- apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
+ apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
done
show "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
apply (rule DERIV_imp_deriv [OF DERIV_diff])
using s
- apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
+ apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
done
show "deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
apply (rule DERIV_imp_deriv [OF DERIV_mult'])
using s
- apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
+ apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
done
qed
-lemma complex_derivative_cmult_at:
+lemma deriv_cmult_at:
"f analytic_on {z} \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
-lemma complex_derivative_cmult_right_at:
+lemma deriv_cmult_right_at:
"f analytic_on {z} \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
@@ -927,7 +927,6 @@
qed
qed
-
lemma has_complex_derivative_series:
fixes s :: "complex set"
assumes cvs: "convex s"
@@ -970,13 +969,13 @@
qed
-lemma complex_differentiable_series:
+lemma field_differentiable_series:
fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
assumes "convex s" "open s"
assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
- shows "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)"
+ shows "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
proof -
from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
unfolding uniformly_convergent_on_def by blast
@@ -991,22 +990,22 @@
have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
(insert g, auto simp: sums_iff)
- thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
- by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
+ thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
+ by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
qed
-lemma complex_differentiable_series':
+lemma field_differentiable_series':
fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
assumes "convex s" "open s"
assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
- shows "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x0)"
- using complex_differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
+ shows "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x0)"
+ using field_differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
subsection\<open>Bound theorem\<close>
-lemma complex_differentiable_bound:
+lemma field_differentiable_bound:
fixes s :: "complex set"
assumes cvs: "convex s"
and df: "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z within s)"
@@ -1155,7 +1154,7 @@
(\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
by (simp add: norm_minus_commute)
also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
- apply (rule complex_differentiable_bound
+ apply (rule field_differentiable_bound
[where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
and s = "closed_segment w z", OF convex_closed_segment])
apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs]
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Mar 07 15:57:02 2016 +0000
@@ -3,7 +3,7 @@
text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close>
theory Complex_Transcendental
-imports
+imports
Complex_Analysis_Basics
Summation
begin
@@ -11,7 +11,7 @@
(* TODO: Figure out what to do with Möbius transformations *)
definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
-lemma moebius_inverse:
+lemma moebius_inverse:
assumes "a * d \<noteq> b * c" "c * z + d \<noteq> 0"
shows "moebius d (-b) (-c) a (moebius a b c d z) = z"
proof -
@@ -21,7 +21,7 @@
unfolding moebius_def by (simp add: moebius_def divide_simps) (simp add: algebra_simps)?
qed
-lemma moebius_inverse':
+lemma moebius_inverse':
assumes "a * d \<noteq> b * c" "c * z - a \<noteq> 0"
shows "moebius a b c d (moebius d (-b) (-c) a z) = z"
using assms moebius_inverse[of d a "-b" "-c" z]
@@ -61,21 +61,16 @@
subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
-lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
- using DERIV_exp complex_differentiable_at_within complex_differentiable_def by blast
+lemma field_differentiable_within_exp: "exp field_differentiable (at z within s)"
+ using DERIV_exp field_differentiable_at_within field_differentiable_def by blast
lemma continuous_within_exp:
fixes z::"'a::{real_normed_field,banach}"
shows "continuous (at z within s) exp"
by (simp add: continuous_at_imp_continuous_within)
-lemma continuous_on_exp:
- fixes s::"'a::{real_normed_field,banach} set"
- shows "continuous_on s exp"
-by (simp add: continuous_on_exp continuous_on_id)
-
lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
- by (simp add: complex_differentiable_within_exp holomorphic_on_def)
+ by (simp add: field_differentiable_within_exp holomorphic_on_def)
subsection\<open>Euler and de Moivre formulas.\<close>
@@ -158,23 +153,23 @@
lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
by (simp add: cos_exp_eq exp_cnj field_simps)
-lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
- using DERIV_sin complex_differentiable_def by blast
-
-lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
- by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)
-
-lemma complex_differentiable_at_cos: "cos complex_differentiable at z"
- using DERIV_cos complex_differentiable_def by blast
-
-lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)"
- by (simp add: complex_differentiable_at_cos complex_differentiable_at_within)
+lemma field_differentiable_at_sin: "sin field_differentiable at z"
+ using DERIV_sin field_differentiable_def by blast
+
+lemma field_differentiable_within_sin: "sin field_differentiable (at z within s)"
+ by (simp add: field_differentiable_at_sin field_differentiable_at_within)
+
+lemma field_differentiable_at_cos: "cos field_differentiable at z"
+ using DERIV_cos field_differentiable_def by blast
+
+lemma field_differentiable_within_cos: "cos field_differentiable (at z within s)"
+ by (simp add: field_differentiable_at_cos field_differentiable_at_within)
lemma holomorphic_on_sin: "sin holomorphic_on s"
- by (simp add: complex_differentiable_within_sin holomorphic_on_def)
+ by (simp add: field_differentiable_within_sin holomorphic_on_def)
lemma holomorphic_on_cos: "cos holomorphic_on s"
- by (simp add: complex_differentiable_within_cos holomorphic_on_def)
+ by (simp add: field_differentiable_within_cos holomorphic_on_def)
subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
@@ -887,13 +882,13 @@
lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
by (simp add: cnj_cos cnj_sin tan_def)
-lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
- unfolding complex_differentiable_def
+lemma field_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan field_differentiable at z"
+ unfolding field_differentiable_def
using DERIV_tan by blast
-lemma complex_differentiable_within_tan: "~(cos z = 0)
- \<Longrightarrow> tan complex_differentiable (at z within s)"
- using complex_differentiable_at_tan complex_differentiable_at_within by blast
+lemma field_differentiable_within_tan: "~(cos z = 0)
+ \<Longrightarrow> tan field_differentiable (at z within s)"
+ using field_differentiable_at_tan field_differentiable_at_within by blast
lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
using continuous_at_imp_continuous_within isCont_tan by blast
@@ -902,7 +897,7 @@
by (simp add: continuous_at_imp_continuous_on)
lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
- by (simp add: complex_differentiable_within_tan holomorphic_on_def)
+ by (simp add: field_differentiable_within_tan holomorphic_on_def)
subsection\<open>Complex logarithms (the conventional principal value)\<close>
@@ -1033,28 +1028,28 @@
by (metis (no_types) Im_exp Ln_in_Reals assms complex_nonpos_Reals_iff complex_is_Real_iff exp_Ln mult_zero_right not_less pi_neq_zero sin_pi znz)
then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi
by (simp add: le_neq_trans znz)
- show "(Ln has_field_derivative inverse(z)) (at z)"
+ have "(exp has_field_derivative z) (at (Ln z))"
+ by (metis znz DERIV_exp exp_Ln)
+ then show "(Ln has_field_derivative inverse(z)) (at z)"
apply (rule has_complex_derivative_inverse_strong_x
- [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
+ [where s = "{w. -pi < Im(w) \<and> Im(w) < pi}"])
using znz *
- apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
- apply (metis DERIV_exp exp_Ln)
- apply (metis mpi_less_Im_Ln)
+ apply (auto simp: Transcendental.continuous_on_exp [OF continuous_on_id] open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt mpi_less_Im_Ln)
done
qed
declare has_field_derivative_Ln [derivative_intros]
declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
-lemma complex_differentiable_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln complex_differentiable at z"
- using complex_differentiable_def has_field_derivative_Ln by blast
-
-lemma complex_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
- \<Longrightarrow> Ln complex_differentiable (at z within s)"
- using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
+lemma field_differentiable_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln field_differentiable at z"
+ using field_differentiable_def has_field_derivative_Ln by blast
+
+lemma field_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
+ \<Longrightarrow> Ln field_differentiable (at z within s)"
+ using field_differentiable_at_Ln field_differentiable_within_subset by blast
lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
- by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
+ by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Ln)
lemma isCont_Ln' [simp]:
"\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
@@ -1067,7 +1062,7 @@
by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
- by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
+ by (simp add: field_differentiable_within_Ln holomorphic_on_def)
subsection\<open>Quadrant-type results for Ln\<close>
@@ -1163,11 +1158,11 @@
text\<open>A reference to the set of positive real numbers\<close>
lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
-by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp
+by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp
Re_complex_of_real complex_is_Real_iff exp_Ln exp_of_real pi_gt_zero)
lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
-by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def
+by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def
mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)
@@ -1178,7 +1173,7 @@
apply (rule exp_complex_eqI)
apply (auto simp: abs_if split: if_split_asm)
using Im_Ln_less_pi Im_Ln_le_pi apply force
- apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff
+ apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff
mpi_less_Im_Ln mult.commute mult_2_right)
by (metis exp_Ln exp_cnj)
@@ -1267,7 +1262,7 @@
done
also have "... = - Ln (- z) + \<i> * complex_of_real pi"
apply (subst Ln_inverse)
- using z by (auto simp add: complex_nonneg_Reals_iff)
+ using z by (auto simp add: complex_nonneg_Reals_iff)
also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
apply (subst Ln_minus [OF assms])
using assms z
@@ -1340,7 +1335,7 @@
have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
using Arg_Ln Arg_gt_0 complex_is_Real_iff by auto
consider "Re z < 0" | "Im z \<noteq> 0" using assms
- using complex_nonneg_Reals_iff not_le by blast
+ using complex_nonneg_Reals_iff not_le by blast
then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg z"
using "*" by (simp add: isCont_def) (metis Arg_Ln Arg_gt_0 complex_is_Real_iff)
show ?thesis
@@ -1375,7 +1370,7 @@
by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
- ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
+ ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
(at z within ball 0 1)"
by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
@@ -1412,13 +1407,13 @@
also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
(auto simp: assms field_simps intro!: always_eventually)
- hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
+ hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
by (intro summable_norm)
(auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i
by (intro mult_left_mono) (simp_all add: divide_simps)
- hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i)) \<le>
+ hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i)) \<le>
(\<Sum>i. norm (-(z^2) * (-z)^i))" using A assms
apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)
apply (intro suminf_le summable_mult summable_geometric)
@@ -1632,16 +1627,16 @@
apply (intro derivative_eq_intros | simp add: assms)+
done
-lemma complex_differentiable_powr_right:
+lemma field_differentiable_powr_right:
fixes w::complex
shows
- "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
-using complex_differentiable_def has_field_derivative_powr_right by blast
+ "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
+using field_differentiable_def has_field_derivative_powr_right by blast
lemma holomorphic_on_powr_right:
"f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
- unfolding holomorphic_on_def complex_differentiable_def
-by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
+ unfolding holomorphic_on_def field_differentiable_def
+by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
lemma norm_powr_real_powr:
"w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
@@ -1814,7 +1809,7 @@
proof (cases "z=0", simp)
assume "z \<noteq> 0"
then show ?thesis
- by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj)
+ by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj)
qed
lemma has_field_derivative_csqrt:
@@ -1839,17 +1834,17 @@
done
qed
-lemma complex_differentiable_at_csqrt:
- "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt complex_differentiable at z"
- using complex_differentiable_def has_field_derivative_csqrt by blast
-
-lemma complex_differentiable_within_csqrt:
- "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt complex_differentiable (at z within s)"
- using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
+lemma field_differentiable_at_csqrt:
+ "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable at z"
+ using field_differentiable_def has_field_derivative_csqrt by blast
+
+lemma field_differentiable_within_csqrt:
+ "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable (at z within s)"
+ using field_differentiable_at_csqrt field_differentiable_within_subset by blast
lemma continuous_at_csqrt:
"z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) csqrt"
- by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
+ by (simp add: field_differentiable_within_csqrt field_differentiable_imp_continuous_at)
corollary isCont_csqrt' [simp]:
"\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
@@ -1857,7 +1852,7 @@
lemma continuous_within_csqrt:
"z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) csqrt"
- by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
+ by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_csqrt)
lemma continuous_on_csqrt [continuous_intros]:
"(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s csqrt"
@@ -1865,7 +1860,7 @@
lemma holomorphic_on_csqrt:
"(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> csqrt holomorphic_on s"
- by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
+ by (simp add: field_differentiable_within_csqrt holomorphic_on_def)
lemma continuous_within_closed_nontrivial:
"closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
@@ -1875,7 +1870,7 @@
lemma continuous_within_csqrt_posreal:
"continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
- case True
+ case True
then have "Im z = 0" "Re z < 0 \<or> z = 0"
using cnj.code complex_cnj_zero_iff by (auto simp: complex_nonpos_Reals_iff) fastforce
then show ?thesis
@@ -2013,20 +2008,20 @@
done
qed
-lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan complex_differentiable at z"
+lemma field_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan field_differentiable at z"
using has_field_derivative_Arctan
- by (auto simp: complex_differentiable_def)
-
-lemma complex_differentiable_within_Arctan:
- "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
- using complex_differentiable_at_Arctan complex_differentiable_at_within by blast
+ by (auto simp: field_differentiable_def)
+
+lemma field_differentiable_within_Arctan:
+ "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan field_differentiable (at z within s)"
+ using field_differentiable_at_Arctan field_differentiable_at_within by blast
declare has_field_derivative_Arctan [derivative_intros]
declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros]
lemma continuous_at_Arctan:
"(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z) Arctan"
- by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan)
+ by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Arctan)
lemma continuous_within_Arctan:
"(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arctan"
@@ -2038,7 +2033,7 @@
lemma holomorphic_on_Arctan:
"(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
- by (simp add: complex_differentiable_within_Arctan holomorphic_on_def)
+ by (simp add: field_differentiable_within_Arctan holomorphic_on_def)
lemma Arctan_series:
assumes z: "norm (z :: complex) < 1"
@@ -2051,20 +2046,20 @@
have summable: "summable (\<lambda>n. g n * u^n)" if "norm u < 1" for u
proof (cases "u = 0")
assume u: "u \<noteq> 0"
- have "(\<lambda>n. ereal (norm (h u n) / norm (h u (Suc n)))) = (\<lambda>n. ereal (inverse (norm u)^2) *
+ have "(\<lambda>n. ereal (norm (h u n) / norm (h u (Suc n)))) = (\<lambda>n. ereal (inverse (norm u)^2) *
ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n)))))"
proof
fix n
- have "ereal (norm (h u n) / norm (h u (Suc n))) =
- ereal (inverse (norm u)^2) * ereal ((of_nat (2*Suc n+1) / of_nat (Suc n)) /
+ have "ereal (norm (h u n) / norm (h u (Suc n))) =
+ ereal (inverse (norm u)^2) * ereal ((of_nat (2*Suc n+1) / of_nat (Suc n)) /
(of_nat (2*Suc n-1) / of_nat (Suc n)))"
- by (simp add: h_def norm_mult norm_power norm_divide divide_simps
+ by (simp add: h_def norm_mult norm_power norm_divide divide_simps
power2_eq_square eval_nat_numeral del: of_nat_add of_nat_Suc)
also have "of_nat (2*Suc n+1) / of_nat (Suc n) = (2::real) + inverse (real (Suc n))"
by (auto simp: divide_simps simp del: of_nat_Suc) simp_all?
also have "of_nat (2*Suc n-1) / of_nat (Suc n) = (2::real) - inverse (real (Suc n))"
- by (auto simp: divide_simps simp del: of_nat_Suc) simp_all?
- finally show "ereal (norm (h u n) / norm (h u (Suc n))) = ereal (inverse (norm u)^2) *
+ by (auto simp: divide_simps simp del: of_nat_Suc) simp_all?
+ finally show "ereal (norm (h u n) / norm (h u (Suc n))) = ereal (inverse (norm u)^2) *
ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n))))" .
qed
also have "\<dots> \<longlonglongrightarrow> ereal (inverse (norm u)^2) * ereal ((2 + 0) / (2 - 0))"
@@ -2076,7 +2071,7 @@
ultimately have A: "liminf (\<lambda>n. ereal (cmod (h u n) / cmod (h u (Suc n)))) > 1" by simp
from u have "summable (h u)"
by (intro summable_norm_cancel[OF ratio_test_convergence[OF _ A]])
- (auto simp: h_def norm_divide norm_mult norm_power simp del: of_nat_Suc
+ (auto simp: h_def norm_divide norm_mult norm_power simp del: of_nat_Suc
intro!: mult_pos_pos divide_pos_pos always_eventually)
thus "summable (\<lambda>n. g n * u^n)"
by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
@@ -2095,10 +2090,10 @@
also have "(\<lambda>n. diffs g n * u^n) = (\<lambda>n. if even n then (\<i>*u)^n else 0)"
by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib)
also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)"
- by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
+ by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
(auto elim!: evenE simp: subseq_def power_mult power_mult_distrib)
also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all
- hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
+ hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide)
finally have "(G has_field_derivative inverse (1 + u\<^sup>2)) (at u)" .
from DERIV_diff[OF has_field_derivative_Arctan this] Im_u u
@@ -2126,12 +2121,12 @@
hence "norm (\<i> * y) < 1" unfolding y_def by (subst norm_mult) simp
hence "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) sums ((-2*\<i>) * Arctan (\<i>*y))"
by (intro Arctan_series sums_mult) simp_all
- also have "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) =
+ also have "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) =
(\<lambda>n. (-2*\<i>) * ((-1)^n * (\<i>*y*(-y\<^sup>2)^n)/of_nat (2*n+1)))"
by (intro ext) (simp_all add: power_mult power_mult_distrib)
also have "\<dots> = (\<lambda>n. 2*y* ((-1) * (-y\<^sup>2))^n/of_nat (2*n+1))"
by (intro ext, subst power_mult_distrib) (simp add: algebra_simps power_mult)
- also have "\<dots> = (\<lambda>n. 2*y^(2*n+1) / of_nat (2*n+1))"
+ also have "\<dots> = (\<lambda>n. 2*y^(2*n+1) / of_nat (2*n+1))"
by (subst power_add, subst power_mult) (simp add: mult_ac)
also have "\<dots> = (\<lambda>n. of_real (2*((x-1)/(x+1))^(2*n+1) / of_nat (2*n+1)))"
by (intro ext) (simp add: y_def)
@@ -2261,7 +2256,7 @@
{ fix w::complex and z::complex
assume *: "w \<in> \<real>" "z \<in> \<real>"
have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)"
- apply (rule complex_differentiable_bound [OF convex_Reals, of Arctan _ 1])
+ apply (rule field_differentiable_bound [OF convex_Reals, of Arctan _ 1])
apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
apply (force simp add: Reals_def)
apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
@@ -2303,7 +2298,7 @@
lemma one_minus_z2_notin_nonpos_Reals:
assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
shows "1 - z\<^sup>2 \<notin> \<real>\<^sub>\<le>\<^sub>0"
- using assms
+ using assms
apply (auto simp: complex_nonpos_Reals_iff Re_power2 Im_power2)
using power2_less_0 [of "Im z"] apply force
using abs_square_less_1 not_le by blast
@@ -2441,13 +2436,13 @@
declare has_field_derivative_Arcsin [derivative_intros]
declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
-lemma complex_differentiable_at_Arcsin:
- "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable at z"
- using complex_differentiable_def has_field_derivative_Arcsin by blast
-
-lemma complex_differentiable_within_Arcsin:
- "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable (at z within s)"
- using complex_differentiable_at_Arcsin complex_differentiable_within_subset by blast
+lemma field_differentiable_at_Arcsin:
+ "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin field_differentiable at z"
+ using field_differentiable_def has_field_derivative_Arcsin by blast
+
+lemma field_differentiable_within_Arcsin:
+ "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin field_differentiable (at z within s)"
+ using field_differentiable_at_Arcsin field_differentiable_within_subset by blast
lemma continuous_within_Arcsin:
"(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arcsin"
@@ -2458,7 +2453,7 @@
by (simp add: continuous_at_imp_continuous_on)
lemma holomorphic_on_Arcsin: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin holomorphic_on s"
- by (simp add: complex_differentiable_within_Arcsin holomorphic_on_def)
+ by (simp add: field_differentiable_within_Arcsin holomorphic_on_def)
subsection\<open>Inverse Cosine\<close>
@@ -2483,7 +2478,7 @@
text\<open>A very tricky argument to find!\<close>
lemma isCont_Arccos_lemma:
- assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+ assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
shows False
proof (cases "Im z = 0")
case True
@@ -2608,13 +2603,13 @@
declare has_field_derivative_Arcsin [derivative_intros]
declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
-lemma complex_differentiable_at_Arccos:
- "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable at z"
- using complex_differentiable_def has_field_derivative_Arccos by blast
-
-lemma complex_differentiable_within_Arccos:
- "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable (at z within s)"
- using complex_differentiable_at_Arccos complex_differentiable_within_subset by blast
+lemma field_differentiable_at_Arccos:
+ "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos field_differentiable at z"
+ using field_differentiable_def has_field_derivative_Arccos by blast
+
+lemma field_differentiable_within_Arccos:
+ "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos field_differentiable (at z within s)"
+ using field_differentiable_at_Arccos field_differentiable_within_subset by blast
lemma continuous_within_Arccos:
"(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arccos"
@@ -2625,7 +2620,7 @@
by (simp add: continuous_at_imp_continuous_on)
lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
- by (simp add: complex_differentiable_within_Arccos holomorphic_on_def)
+ by (simp add: field_differentiable_within_Arccos holomorphic_on_def)
subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Mon Mar 07 15:57:02 2016 +0000
@@ -671,7 +671,7 @@
by (auto intro: holomorphic_factor_order_of_zero [OF assms])
have con: "continuous_on (ball \<xi> r) (\<lambda>z. deriv g z / g z)"
by (rule continuous_intros) (auto simp: gne holg holomorphic_deriv holomorphic_on_imp_continuous_on)
- have cd: "\<And>x. dist \<xi> x < r \<Longrightarrow> (\<lambda>z. deriv g z / g z) complex_differentiable at x"
+ have cd: "\<And>x. dist \<xi> x < r \<Longrightarrow> (\<lambda>z. deriv g z / g z) field_differentiable at x"
apply (rule derivative_intros)+
using holg mem_ball apply (blast intro: holomorphic_deriv holomorphic_on_imp_differentiable_at)
apply (metis Topology_Euclidean_Space.open_ball at_within_open holg holomorphic_on_def mem_ball)
@@ -687,7 +687,7 @@
by (auto intro!: continuous_intros simp add: holg holomorphic_on_imp_continuous_on gne)
have 0: "dist \<xi> x < r \<Longrightarrow> ((\<lambda>x. exp (h x) / g x) has_field_derivative 0) (at x)" for x
apply (rule h derivative_eq_intros | simp)+
- apply (rule DERIV_deriv_iff_complex_differentiable [THEN iffD2])
+ apply (rule DERIV_deriv_iff_field_differentiable [THEN iffD2])
using holg apply (auto simp: holomorphic_on_imp_differentiable_at gne h)
done
obtain c where c: "\<And>x. x \<in> ball \<xi> r \<Longrightarrow> exp (h x) / g x = c"
@@ -852,15 +852,15 @@
have holh: "h holomorphic_on S"
proof (simp add: holomorphic_on_def, clarify)
fix z assume "z \<in> S"
- show "h complex_differentiable at z within S"
+ show "h field_differentiable at z within S"
proof (cases "z = \<xi>")
case True then show ?thesis
- using complex_differentiable_at_within complex_differentiable_def h0 by blast
+ using field_differentiable_at_within field_differentiable_def h0 by blast
next
case False
- then have "f complex_differentiable at z within S"
+ then have "f field_differentiable at z within S"
using holomorphic_onD [OF holf, of z] \<open>z \<in> S\<close>
- unfolding complex_differentiable_def DERIV_within_iff
+ unfolding field_differentiable_def DERIV_within_iff
by (force intro: exI [where x="dist \<xi> z"] elim: Lim_transform_within_set [unfolded eventually_at])
then show ?thesis
by (simp add: h_def power2_eq_square derivative_intros)
@@ -1131,7 +1131,7 @@
apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g'])
using g' *
apply (simp_all add: linear_conv_bounded_linear that)
- using DERIV_deriv_iff_complex_differentiable has_field_derivative_imp_has_derivative holf
+ using DERIV_deriv_iff_field_differentiable has_field_derivative_imp_has_derivative holf
holomorphic_on_imp_differentiable_at \<open>open S\<close> apply blast
done
qed
@@ -1204,7 +1204,7 @@
using holg by (simp add: holomorphic_on_subset subset_ball)
have gd: "\<And>w. dist \<xi> w < \<delta> \<Longrightarrow> (g has_field_derivative deriv g w) (at w)"
using holg
- by (simp add: DERIV_deriv_iff_complex_differentiable holomorphic_on_def at_within_open_NO_MATCH)
+ by (simp add: DERIV_deriv_iff_field_differentiable holomorphic_on_def at_within_open_NO_MATCH)
have *: "\<And>w. w \<in> ball \<xi> (min r \<delta>)
\<Longrightarrow> ((\<lambda>w. (w - \<xi>) * g w) has_field_derivative ((w - \<xi>) * deriv g w + g w))
(at w)"
@@ -1266,7 +1266,7 @@
have *: "(the_inv_into S f has_field_derivative inverse (deriv f z)) (at (f z))" if "z \<in> S" for z
proof -
have 1: "(f has_field_derivative deriv f z) (at z)"
- using DERIV_deriv_iff_complex_differentiable \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_on_imp_differentiable_at
+ using DERIV_deriv_iff_field_differentiable \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_on_imp_differentiable_at
by blast
have 2: "deriv f z \<noteq> 0"
using \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_injective_imp_regular injf by blast
@@ -1524,7 +1524,7 @@
have 3: "contour_integral (reversepath (linepath b' a')) f =
- contour_integral (linepath b' a') f"
by (rule contour_integral_reversepath [OF valid_path_linepath])
- have fcd_le: "f complex_differentiable at x"
+ have fcd_le: "f field_differentiable at x"
if "x \<in> interior S \<and> x \<in> interior {x. d \<bullet> x \<le> k}" for x
proof -
have "f holomorphic_on S \<inter> {c. d \<bullet> c < k}"
@@ -1532,7 +1532,7 @@
then have "\<exists>C D. x \<in> interior C \<inter> interior D \<and> f holomorphic_on interior C \<inter> interior D"
using that
by (metis Collect_mem_eq Int_Collect \<open>d \<noteq> 0\<close> interior_halfspace_le interior_open \<open>open S\<close>)
- then show "f complex_differentiable at x"
+ then show "f field_differentiable at x"
by (metis at_within_interior holomorphic_on_def interior_Int interior_interior)
qed
have ab_le: "\<And>x. x \<in> closed_segment a b \<Longrightarrow> d \<bullet> x \<le> k"
@@ -1557,7 +1557,7 @@
contour_integral (linepath a' b') f +
contour_integral (linepath b' a) f = 0"
by (rule has_chain_integral_chain_integral4)
- have fcd_ge: "f complex_differentiable at x"
+ have fcd_ge: "f field_differentiable at x"
if "x \<in> interior S \<and> x \<in> interior {x. k \<le> d \<bullet> x}" for x
proof -
have f2: "f holomorphic_on S \<inter> {c. k < d \<bullet> c}"
@@ -1566,7 +1566,7 @@
by (simp add: interior_open \<open>open S\<close>)
then have "x \<in> S \<inter> interior {c. k \<le> d \<bullet> c}"
using that by simp
- then show "f complex_differentiable at x"
+ then show "f field_differentiable at x"
using f3 f2 unfolding holomorphic_on_def
by (metis (no_types) \<open>d \<noteq> 0\<close> at_within_interior interior_Int interior_halfspace_ge interior_interior)
qed
@@ -1688,10 +1688,10 @@
apply (intro continuous_intros continuous_on_compose continuous_on_subset [OF contf])
using cnjs apply auto
done
- have "cnj \<circ> f \<circ> cnj complex_differentiable at x within S \<inter> {z. Im z < 0}"
- if "x \<in> S" "Im x < 0" "f complex_differentiable at (cnj x) within S \<inter> {z. 0 < Im z}" for x
+ have "cnj \<circ> f \<circ> cnj field_differentiable at x within S \<inter> {z. Im z < 0}"
+ if "x \<in> S" "Im x < 0" "f field_differentiable at (cnj x) within S \<inter> {z. 0 < Im z}" for x
using that
- apply (simp add: complex_differentiable_def Derivative.DERIV_within_iff Lim_within dist_norm, clarify)
+ apply (simp add: field_differentiable_def Derivative.DERIV_within_iff Lim_within dist_norm, clarify)
apply (rule_tac x="cnj f'" in exI)
apply (elim all_forward ex_forward conj_forward imp_forward asm_rl, clarify)
apply (drule_tac x="cnj xa" in bspec)
@@ -1902,11 +1902,11 @@
by (simp add: o_def)
have hol0: "(\<lambda>z. f (a + z)) holomorphic_on cball 0 r"
unfolding fz by (intro holomorphic_intros holf holomorphic_on_compose | simp)+
- then have [simp]: "\<And>x. norm x < r \<Longrightarrow> (\<lambda>z. f (a + z)) complex_differentiable at x"
+ then have [simp]: "\<And>x. norm x < r \<Longrightarrow> (\<lambda>z. f (a + z)) field_differentiable at x"
by (metis Topology_Euclidean_Space.open_ball at_within_open ball_subset_cball diff_0 dist_norm holomorphic_on_def holomorphic_on_subset mem_ball norm_minus_cancel)
- have [simp]: "\<And>z. norm z < r \<Longrightarrow> f complex_differentiable at (a + z)"
+ have [simp]: "\<And>z. norm z < r \<Longrightarrow> f field_differentiable at (a + z)"
by (metis holf open_ball add_diff_cancel_left' dist_complex_def holomorphic_on_imp_differentiable_at holomorphic_on_subset interior_cball interior_subset mem_ball norm_minus_commute)
- then have [simp]: "f complex_differentiable at a"
+ then have [simp]: "f field_differentiable at a"
by (metis add.comm_neutral \<open>0 < r\<close> norm_eq_zero)
have hol1: "(\<lambda>z. f (a + z) - f a) holomorphic_on cball 0 r"
by (intro holomorphic_intros hol0)
@@ -1920,7 +1920,7 @@
then show ?thesis
apply clarify
apply (drule_tac c="x - f a" in subsetD)
- apply (force simp: fz \<open>0 < r\<close> dist_norm complex_derivative_chain complex_differentiable_compose)+
+ apply (force simp: fz \<open>0 < r\<close> dist_norm complex_derivative_chain field_differentiable_compose)+
done
qed
@@ -2026,7 +2026,7 @@
case False
def C \<equiv> "deriv f a"
have "0 < norm C" using False by (simp add: C_def)
- have dfa: "f complex_differentiable at a"
+ have dfa: "f field_differentiable at a"
apply (rule holomorphic_on_imp_differentiable_at [OF holf])
using \<open>0 < r\<close> by auto
have fo: "(\<lambda>z. f (a + of_real r * z)) = f o (\<lambda>z. (a + of_real r * z))"
@@ -2045,7 +2045,7 @@
have *: "((\<lambda>x. f (a + of_real r * x)) has_field_derivative
(deriv f (a + of_real r * z) * of_real r)) (at z)"
apply (simp add: fo)
- apply (rule DERIV_chain [OF complex_differentiable_derivI])
+ apply (rule DERIV_chain [OF field_differentiable_derivI])
apply (rule holomorphic_on_imp_differentiable_at [OF holf], simp)
using \<open>0 < r\<close> apply (simp add: dist_norm norm_mult that)
apply (rule derivative_eq_intros | simp)+
@@ -2055,10 +2055,10 @@
using \<open>0 < r\<close> by (auto simp: C_def False)
qed
have 2: "deriv (\<lambda>z. f (a + of_real r * z) / (C * of_real r)) 0 = 1"
- apply (subst complex_derivative_cdivide_right)
- apply (simp add: complex_differentiable_def fo)
+ apply (subst deriv_cdivide_right)
+ apply (simp add: field_differentiable_def fo)
apply (rule exI)
- apply (rule DERIV_chain [OF complex_differentiable_derivI])
+ apply (rule DERIV_chain [OF field_differentiable_derivI])
apply (simp add: dfa)
apply (rule derivative_eq_intros | simp add: C_def False fo)+
using \<open>0 < r\<close>
--- a/src/HOL/Multivariate_Analysis/Gamma.thy Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy Mon Mar 07 15:57:02 2016 +0000
@@ -1355,21 +1355,21 @@
"z \<in> \<real> \<Longrightarrow> Gamma z \<in> (\<real> :: complex set)" and rGamma_complex_real: "z \<in> \<real> \<Longrightarrow> rGamma z \<in> \<real>"
by (simp_all add: Reals_cnj_iff cnj_Gamma cnj_rGamma)
-lemma complex_differentiable_rGamma: "rGamma complex_differentiable (at z within A)"
- using has_field_derivative_rGamma[of z] unfolding complex_differentiable_def by blast
+lemma field_differentiable_rGamma: "rGamma field_differentiable (at z within A)"
+ using has_field_derivative_rGamma[of z] unfolding field_differentiable_def by blast
lemma holomorphic_on_rGamma: "rGamma holomorphic_on A"
- unfolding holomorphic_on_def by (auto intro!: complex_differentiable_rGamma)
+ unfolding holomorphic_on_def by (auto intro!: field_differentiable_rGamma)
lemma analytic_on_rGamma: "rGamma analytic_on A"
unfolding analytic_on_def by (auto intro!: exI[of _ 1] holomorphic_on_rGamma)
-lemma complex_differentiable_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma complex_differentiable (at z within A)"
- using has_field_derivative_Gamma[of z] unfolding complex_differentiable_def by auto
+lemma field_differentiable_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma field_differentiable (at z within A)"
+ using has_field_derivative_Gamma[of z] unfolding field_differentiable_def by auto
lemma holomorphic_on_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma holomorphic_on A"
- unfolding holomorphic_on_def by (auto intro!: complex_differentiable_Gamma)
+ unfolding holomorphic_on_def by (auto intro!: field_differentiable_Gamma)
lemma analytic_on_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
@@ -1383,14 +1383,14 @@
declare has_field_derivative_rGamma_complex'[THEN DERIV_chain2, derivative_intros]
-lemma complex_differentiable_Polygamma:
+lemma field_differentiable_Polygamma:
fixes z::complex
shows
- "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n complex_differentiable (at z within A)"
- using has_field_derivative_Polygamma[of z n] unfolding complex_differentiable_def by auto
+ "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n field_differentiable (at z within A)"
+ using has_field_derivative_Polygamma[of z n] unfolding field_differentiable_def by auto
lemma holomorphic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n holomorphic_on A"
- unfolding holomorphic_on_def by (auto intro!: complex_differentiable_Polygamma)
+ unfolding holomorphic_on_def by (auto intro!: field_differentiable_Polygamma)
lemma analytic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n analytic_on A"
by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)