merged

--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Feb 01 09:14:40 2023 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Feb 01 12:43:39 2023 +0000
@@ -250,39 +250,56 @@
     by (auto simp: not_le)
 qed (insert assms, auto)
 
-lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
+lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on A \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on A"
   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"
+  "\<lbrakk>f holomorphic_on A; g holomorphic_on A\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) holomorphic_on A"
   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"
+  "\<lbrakk>f holomorphic_on A; g holomorphic_on A\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) holomorphic_on A"
   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"
+  "\<lbrakk>f holomorphic_on A; g holomorphic_on A\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) holomorphic_on A"
   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"
+  "\<lbrakk>f holomorphic_on A; \<And>z. z \<in> A \<Longrightarrow> f z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. inverse (f z)) holomorphic_on A"
   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"
+  "\<lbrakk>f holomorphic_on A; g holomorphic_on A; \<And>z. z \<in> A \<Longrightarrow> g z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. f z / g z) holomorphic_on A"
   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"
+  "f holomorphic_on A \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on A"
   unfolding holomorphic_on_def by (metis field_differentiable_power)
 
+lemma holomorphic_on_power_int [holomorphic_intros]:
+  assumes nz: "n \<ge> 0 \<or> (\<forall>x\<in>A. f x \<noteq> 0)" and f: "f holomorphic_on A"
+  shows   "(\<lambda>x. f x powi n) holomorphic_on A"
+proof (cases "n \<ge> 0")
+  case True
+  have "(\<lambda>x. f x ^ nat n) holomorphic_on A"
+    by (simp add: f holomorphic_on_power)
+  with True show ?thesis
+    by (simp add: power_int_def)
+next
+  case False
+  hence "(\<lambda>x. inverse (f x ^ nat (-n))) holomorphic_on A"
+    using nz by (auto intro!: holomorphic_intros f)
+  with False show ?thesis
+    by (simp add: power_int_def power_inverse)
+qed
+
 lemma holomorphic_on_sum [holomorphic_intros]:
-  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
+  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on A) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on A"
   unfolding holomorphic_on_def by (metis field_differentiable_sum)
 
 lemma holomorphic_on_prod [holomorphic_intros]:
-  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) holomorphic_on s"
+  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on A) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) holomorphic_on A"
   by (induction I rule: infinite_finite_induct) (auto intro: holomorphic_intros)
 
 lemma holomorphic_pochhammer [holomorphic_intros]:
@@ -327,6 +344,17 @@
   by (rule DERIV_imp_deriv)
      (metis DERIV_deriv_iff_field_differentiable has_field_derivative_transform_within_open at_within_open)
 
+lemma holomorphic_on_compose_cnj_cnj:
+  assumes "f holomorphic_on cnj ` A" "open A"
+  shows   "cnj \<circ> f \<circ> cnj holomorphic_on A"
+proof -
+  have [simp]: "open (cnj ` A)"
+    unfolding image_cnj_conv_vimage_cnj using assms by (intro open_vimage) auto
+  show ?thesis
+    using assms unfolding holomorphic_on_def
+    by (auto intro!: field_differentiable_cnj_cnj simp: at_within_open_NO_MATCH)
+qed
+  
 lemma holomorphic_nonconstant:
   assumes holf: "f holomorphic_on S" and "open S" "\<xi> \<in> S" "deriv f \<xi> \<noteq> 0"
     shows "\<not> f constant_on S"
@@ -528,6 +556,23 @@
   "f analytic_on S \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on S"
 by (induct n) (auto simp: analytic_on_mult)
 
+lemma analytic_on_power_int [analytic_intros]:
+  assumes nz: "n \<ge> 0 \<or> (\<forall>x\<in>A. f x \<noteq> 0)" and f: "f analytic_on A"
+  shows   "(\<lambda>x. f x powi n) analytic_on A"
+proof (cases "n \<ge> 0")
+  case True
+  have "(\<lambda>x. f x ^ nat n) analytic_on A"
+    using analytic_on_power f by blast
+  with True show ?thesis
+    by (simp add: power_int_def)
+next
+  case False
+  hence "(\<lambda>x. inverse (f x ^ nat (-n))) analytic_on A"
+    using nz by (auto intro!: analytic_intros f)
+  with False show ?thesis
+    by (simp add: power_int_def power_inverse)
+qed
+
 lemma analytic_on_sum [analytic_intros]:
   "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on S) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on S"
   by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_add)

--- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Feb 01 09:14:40 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Feb 01 12:43:39 2023 +0000
@@ -2296,7 +2296,17 @@
 lemma continuous_within_Arg: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Arg"
   using continuous_at_Arg continuous_at_imp_continuous_within by blast
 
-
+lemma Arg_Re_pos: "\<bar>Arg z\<bar> < pi / 2 \<longleftrightarrow> Re z > 0 \<or> z = 0"
+  using Arg_def Re_Ln_pos_lt by auto
+
+lemma Arg_Re_nonneg: "\<bar>Arg z\<bar> \<le> pi / 2 \<longleftrightarrow> Re z \<ge> 0"
+  using Re_Ln_pos_le[of z] by (cases "z = 0") (auto simp: Arg_eq_Im_Ln Arg_zero)
+
+lemma Arg_times:
+  assumes "Arg z + Arg w \<in> {-pi<..pi}" "z \<noteq> 0" "w \<noteq> 0"
+  shows   "Arg (z * w) = Arg z + Arg w"
+  using Arg_eq_Im_Ln Ln_times_simple assms by auto
+  
 subsection\<open>The Unwinding Number and the Ln product Formula\<close>
 
 text\<open>Note that in this special case the unwinding number is -1, 0 or 1. But it's always an integer.\<close>

--- a/src/HOL/Analysis/Derivative.thy	Wed Feb 01 09:14:40 2023 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Wed Feb 01 12:43:39 2023 +0000
@@ -2104,6 +2104,12 @@
   using assms unfolding field_differentiable_def
   by (metis DERIV_power)
 
+lemma field_differentiable_cnj_cnj:
+  assumes "f field_differentiable (at (cnj z))"
+  shows   "(cnj \<circ> f \<circ> cnj) field_differentiable (at z)"
+  using has_field_derivative_cnj_cnj assms
+  by (auto simp: field_differentiable_def)
+ 
 lemma field_differentiable_transform_within:
   "0 < d \<Longrightarrow>
         x \<in> S \<Longrightarrow>

--- a/src/HOL/Complex.thy	Wed Feb 01 09:14:40 2023 +0100
+++ b/src/HOL/Complex.thy	Wed Feb 01 12:43:39 2023 +0000
@@ -671,6 +671,22 @@
   shows   "((\<lambda>z. cnj (f z)) has_vector_derivative cnj f') (at z within A)"
   using assms by (auto simp: has_vector_derivative_complex_iff intro: derivative_intros)
 
+lemma has_field_derivative_cnj_cnj:
+  assumes "(f has_field_derivative F) (at (cnj z))"
+  shows   "((cnj \<circ> f \<circ> cnj) has_field_derivative cnj F) (at z)"
+proof -
+  have "cnj \<midarrow>0\<rightarrow> cnj 0"
+    by (subst lim_cnj) auto
+  also have "cnj 0 = 0"
+    by simp
+  finally have *: "filterlim cnj (at 0) (at 0)"
+    by (auto simp: filterlim_at eventually_at_filter)
+  have "(\<lambda>h. (f (cnj z + cnj h) - f (cnj z)) / cnj h) \<midarrow>0\<rightarrow> F"
+    by (rule filterlim_compose[OF _ *]) (use assms in \<open>auto simp: DERIV_def\<close>)
+  thus ?thesis
+    by (subst (asm) lim_cnj [symmetric]) (simp add: DERIV_def)
+qed
+
 
 subsection \<open>Basic Lemmas\<close>
 
@@ -1388,5 +1404,4 @@
   then show ?thesis using that by simp
 qed
 
-
 end