author paulson Mon, 25 Jun 2018 14:06:50 +0100 changeset 68494 ebdd5508f386 parent 68492 c7e0a7bcacaf (current diff) parent 68493 143b4cc8fc74 (diff) child 68495 71483c0e0023 child 68496 7266fb64de69 child 68499 d4312962161a
merged
```--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 25 14:45:05 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 25 14:06:50 2018 +0100
@@ -84,7 +84,7 @@
shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
using arc_simple_path  inside_arc_empty by blast

-
+
subsection \<open>Piecewise differentiable functions\<close>

definition piecewise_differentiable_on
@@ -466,7 +466,7 @@
next
case False
have *: "\<And>x. finite (S \<inter> {y. m * y + c = x})"
-    using False not_finite_existsD by fastforce
+    using False not_finite_existsD by fastforce
show ?thesis
apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise])
apply (rule * assms derivative_intros | simp add: False vimage_def)+
@@ -601,7 +601,7 @@
have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
proof (rule differentiable_transform_within)
show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x"
-      using that g12D
+      using that g12D
apply (simp only: joinpaths_def)
by (rule differentiable_chain_at derivative_intros | force)+
show "\<And>x'. \<lbrakk>dist x' x < dist (x/2) (1/2)\<rbrakk>
@@ -740,7 +740,7 @@
by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - S\<close> that)
next
have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
-      then show "f differentiable at (g t)"
+      then show "f differentiable at (g t)"
using der[THEN field_differentiable_imp_differentiable] by auto
qed
moreover have "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
@@ -767,7 +767,7 @@
qed
ultimately have "f \<circ> g C1_differentiable_on {0..1} - S"
using C1_differentiable_on_eq by blast
-  moreover have "path (f \<circ> g)"
+  moreover have "path (f \<circ> g)"
apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
using der
@@ -898,7 +898,7 @@
{0..1}"
using has_integral_affinity01 [where m= "-1" and c=1, OF f [unfolded has_contour_integral_def]]
-  then show ?thesis
+  then show ?thesis
using S
apply (clarsimp simp: reversepath_def has_contour_integral_def)
apply (rule_tac S = "(\<lambda>x. 1 - x) ` S" in has_integral_spike_finite)
@@ -2155,7 +2155,7 @@
done
} note * = this
show ?thesis
-    using cd e
+    using cd e
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 * unfolding dist_norm
@@ -2508,7 +2508,7 @@
by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull])
have **: "\<And>f' x' f x::complex. f'*x' - f*x = f'*(x' - x) + x*(f' - f)"
-          have "norm (?pathint (shrink u) (shrink v) - ?pathint u v)
+          have "norm (?pathint (shrink u) (shrink v) - ?pathint u v)
\<le> (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))"
apply (rule has_integral_bound
[of _ "\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
@@ -2835,7 +2835,7 @@
qed

lemma contour_integral_convex_primitive:
-  assumes "convex S" "continuous_on S f"
+  assumes "convex S" "continuous_on S f"
"\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
obtains g where "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative f x) (at x within S)"
proof (cases "S={}")
@@ -2846,7 +2846,7 @@

lemma holomorphic_convex_primitive:
fixes f :: "complex \<Rightarrow> complex"
-  assumes "convex S" "finite K" and contf: "continuous_on S f"
+  assumes "convex S" "finite K" and contf: "continuous_on S f"
and fd: "\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x"
obtains g where "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative f x) (at x within S)"
proof (rule contour_integral_convex_primitive [OF \<open>convex S\<close> contf Cauchy_theorem_triangle_cofinite])
@@ -2871,7 +2871,7 @@
corollary Cauchy_theorem_convex:
"\<lbrakk>continuous_on S f; convex S; finite K;
\<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>
+      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)

@@ -3561,14 +3561,14 @@
assume "0 < e" and g: "winding_number_prop p z e g n"
then show "\<exists>r. winding_number_prop (\<lambda>w. p w - z) 0 e r n"
by (rule_tac x="\<lambda>t. g t - z" in exI)
-       (force simp: winding_number_prop_def contour_integral_integral valid_path_def path_defs
+       (force simp: winding_number_prop_def contour_integral_integral valid_path_def path_defs
vector_derivative_def has_vector_derivative_diff_const piecewise_C1_differentiable_diff C1_differentiable_imp_piecewise)
next
fix n e g
assume "0 < e" and g: "winding_number_prop (\<lambda>w. p w - z) 0 e g n"
then show "\<exists>r. winding_number_prop p z e r n"
apply (rule_tac x="\<lambda>t. g t + z" in exI)
-    apply (simp add: winding_number_prop_def contour_integral_integral valid_path_def path_defs
+    apply (simp add: winding_number_prop_def contour_integral_integral valid_path_def path_defs
apply (force simp: algebra_simps)
done
@@ -3665,7 +3665,7 @@
by (force simp: ge0)
show "((\<lambda>x. if 0 < x \<and> x < 1 then ?vd x else 0) has_integral ?int z) (cbox 0 1)"
by (rule has_integral_spike_interior [OF hi]) simp
-  qed
+  qed
then show ?thesis
by (simp add: Re_winding_number [OF \<gamma>] field_simps)
qed
@@ -3679,7 +3679,7 @@
let ?vd = "\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)"
let ?int = "\<lambda>z. contour_integral \<gamma> (\<lambda>w. 1 / (w - z))"
have hi: "(?vd has_integral ?int z) (cbox 0 1)"
-    unfolding box_real
+    unfolding box_real
apply (subst has_contour_integral [symmetric])
using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
@@ -3782,7 +3782,7 @@
unfolding integrable_on_def [symmetric]
proof (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>]])
show "\<exists>d h. 0 < d \<and>
-               (\<forall>y. cmod (y - w) < d \<longrightarrow> (h has_field_derivative inverse (y - z))(at y within - {z}))"
+               (\<forall>y. cmod (y - w) < d \<longrightarrow> (h has_field_derivative inverse (y - z))(at y within - {z}))"
if "w \<in> - {z}" for w
apply (rule_tac x="norm(w - z)" in exI)
using that inverse_eq_divide has_field_derivative_at_within h
@@ -3899,21 +3899,21 @@
have cont: "continuous_on {0..1}
(\<lambda>x. Im (integral {0..x} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))))"
by (intro continuous_intros indefinite_integral_continuous_1 winding_number_exp_integral [OF gpd]; simp)
-  have "Arg r \<le> 2*pi"
-    by (simp add: Arg less_eq_real_def)
+  have "Arg2pi r \<le> 2*pi"
+    by (simp add: Arg2pi less_eq_real_def)
also have "\<dots> \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))"
using 1
apply (simp add: winding_number_valid_path [OF \<gamma> z] contour_integral_integral)
apply (simp add: Complex.Re_divide field_simps power2_eq_square)
done
-  finally have "Arg r \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))" .
-  then have "\<exists>t. t \<in> {0..1} \<and> Im(integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg r"
-    by (simp add: Arg_ge_0 cont IVT')
+  finally have "Arg2pi r \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))" .
+  then have "\<exists>t. t \<in> {0..1} \<and> Im(integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg2pi r"
+    by (simp add: Arg2pi_ge_0 cont IVT')
then obtain t where t:     "t \<in> {0..1}"
-                  and eqArg: "Im (integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg r"
+                  and eqArg: "Im (integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg2pi r"
by blast
define i where "i = integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
-  have iArg: "Arg r = Im i"
+  have iArg: "Arg2pi r = Im i"
using eqArg by (simp add: i_def)
have gpdt: "\<gamma> piecewise_C1_differentiable_on {0..t}"
by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl piecewise_C1_differentiable_on_subset gpd t)
@@ -3927,7 +3927,7 @@
then have "z + complex_of_real (exp (Re i)) * (w - z) / complex_of_real (cmod r) = \<gamma> t"
apply simp
-    apply (subst Complex_Transcendental.Arg_eq [of r])
+    apply (subst Complex_Transcendental.Arg2pi_eq [of r])
using * apply (simp add: exp_eq_polar field_simps)
done
@@ -4158,7 +4158,7 @@
lemma winding_number_eq:
"\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> S; z \<in> S; connected S; S \<inter> path_image \<gamma> = {}\<rbrakk>
\<Longrightarrow> winding_number \<gamma> w = winding_number \<gamma> z"
-  using winding_number_constant by (metis constant_on_def)
+  using winding_number_constant by (metis constant_on_def)

lemma open_winding_number_levelsets:
assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
@@ -5329,7 +5329,7 @@
using \<open>0 \<le> B\<close>  \<open>0 < e\<close> by (simp add: divide_simps)
have "\<exists>h. (\<forall>x\<in>{0..1}. cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - h x) \<le> e) \<and> h integrable_on {0..1}"
proof (intro exI conjI ballI)
-      show "cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - f a (\<gamma> x) * vector_derivative \<gamma> (at x)) \<le> e"
+      show "cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - f a (\<gamma> x) * vector_derivative \<gamma> (at x)) \<le> e"
if "x \<in> {0..1}" for x
apply (rule order_trans [OF _ Ble])
using noleB [OF that] fga [OF that] \<open>0 \<le> B\<close> \<open>0 < e\<close>
@@ -5339,13 +5339,13 @@
qed (rule inta)
}
then show lintg: "l contour_integrable_on \<gamma>"
-    unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real)
+    unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real)
{ fix e::real
define B' where "B' = B + 1"
have B': "B' > 0" "B' > B" using  \<open>0 \<le> B\<close> by (auto simp: B'_def)
assume "0 < e"
then have ev_no': "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image \<gamma>. 2 * cmod (f n x - l x) < e / B'"
-      using ul_f [unfolded uniform_limit_iff dist_norm, rule_format, of "e / B' / 2"] B'
+      using ul_f [unfolded uniform_limit_iff dist_norm, rule_format, of "e / B' / 2"] B'
have ie: "integral {0..1::real} (\<lambda>x. e / 2) < e" using \<open>0 < e\<close> by simp
have *: "cmod (f x (\<gamma> t) * vector_derivative \<gamma> (at t) - l (\<gamma> t) * vector_derivative \<gamma> (at t)) \<le> e / 2"
@@ -6024,7 +6024,7 @@
\<Longrightarrow> f field_differentiable at x" for a b c x
by (metis cdf Diff_iff Int_iff ball_min_Int subsetD convex_ball e interior_mono interior_subset subset_hull)
obtain g where "\<And>w. w \<in> ball z (min d e) \<Longrightarrow> (g has_field_derivative f w) (at w within ball z (min d e))"
-        apply (rule contour_integral_convex_primitive
+        apply (rule contour_integral_convex_primitive
[OF convex_ball fde Cauchy_theorem_triangle_cofinite [OF _ K]])
using cont fd by auto
then have "f holomorphic_on ball z (min d e)"
@@ -6040,7 +6040,7 @@

lemma no_isolated_singularity':
fixes z::complex
-  assumes f: "\<And>z. z \<in> K \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within S)"
+  assumes f: "\<And>z. z \<in> K \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within S)"
and holf: "f holomorphic_on (S - K)" and S: "open S" and K: "finite K"
shows "f holomorphic_on S"
proof (rule no_isolated_singularity[OF _ assms(2-)])
@@ -6050,9 +6050,9 @@
show "(f \<longlongrightarrow> f z) (at z within S)"
proof (cases "z \<in> K")
case False
-      from holf have "continuous_on (S - K) f"
+      from holf have "continuous_on (S - K) f"
by (rule holomorphic_on_imp_continuous_on)
-      with z False have "(f \<longlongrightarrow> f z) (at z within (S - K))"
+      with z False have "(f \<longlongrightarrow> f z) (at z within (S - K))"
also from z K S False have "at z within (S - K) = at z within S"
by (subst (1 2) at_within_open) (auto intro: finite_imp_closed)
@@ -6071,7 +6071,7 @@
have *: "\<And>x. x \<in> interior S \<Longrightarrow> f field_differentiable at x"
unfolding holomorphic_on_open [symmetric] field_differentiable_def
using no_isolated_singularity [where S = "interior S"]
-    by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd
+    by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd
field_differentiable_at_within field_differentiable_def holomorphic_onI
holomorphic_on_imp_differentiable_at open_interior)
show ?thesis
@@ -6159,7 +6159,7 @@
proof -
\<comment> \<open>Replacing @{term r} and the original (weak) premises with stronger ones\<close>
obtain r where "r > 0" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
-  proof
+  proof
have "cball z ((r + dist w z) / 2) \<subseteq> ball z r"
using w by (simp add: dist_commute real_sum_of_halves subset_eq)
then show "f holomorphic_on cball z ((r + dist w z) / 2)"
@@ -6169,7 +6169,7 @@
then show "0 < (r + dist w z) / 2"
by simp (use zero_le_dist [of w z] in linarith)
qed (use w in \<open>auto simp: dist_commute\<close>)
-  then have holf: "f holomorphic_on ball z r"
+  then have holf: "f holomorphic_on ball z r"
using ball_subset_cball holomorphic_on_subset by blast
have contf: "continuous_on (cball z r) f"
@@ -6179,12 +6179,12 @@
by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> norm(u - w)"
-  proof
+  proof
show "\<And>u. cmod (u - z) = r \<Longrightarrow> r - dist z w \<le> cmod (u - w)"
qed (use w in \<open>auto simp: dist_norm norm_minus_commute\<close>)
have ul: "uniform_limit (sphere z r) (\<lambda>n x. (\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k))) (\<lambda>x. f x / (x - w)) sequentially"
-    unfolding uniform_limit_iff dist_norm
+    unfolding uniform_limit_iff dist_norm
proof clarify
fix e::real
assume "0 < e"
@@ -6378,7 +6378,7 @@
apply (auto intro: Cauchy_higher_derivative_integral_circlepath [where k=0, simplified])
done
have ul_less: "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - w)) (\<lambda>x. g x / (x - w)) F"
-      using greater \<open>0 < d\<close>
+      using greater \<open>0 < d\<close>
apply (clarsimp simp add: uniform_limit_iff dist_norm norm_divide diff_divide_distrib [symmetric] divide_simps)
apply (rule_tac e1="e * d" in eventually_mono [OF uniform_limitD [OF ulim]])
apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+
@@ -6389,7 +6389,7 @@
by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
have f_tends_cig: "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
proof (rule Lim_transform_eventually)
-      show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. f x u / (u - w))
+      show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. f x u / (u - w))
= 2 * of_real pi * \<i> * f x w"
apply (rule eventually_mono [OF cont contour_integral_unique [OF Cauchy_integral_circlepath]])
using w\<open>0 < d\<close> d_def by auto
@@ -6507,7 +6507,7 @@
proof -
obtain r where "0 < r" and r: "cball z r \<subseteq> S"
and ul: "uniform_limit (cball z r) f g sequentially"
-      using ulim_g [OF \<open>z \<in> S\<close>] by blast
+      using ulim_g [OF \<open>z \<in> S\<close>] by blast
have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and> f n holomorphic_on ball z r"
proof (intro eventuallyI conjI)
show "continuous_on (cball z r) (f x)" for x
@@ -6537,7 +6537,7 @@
proof -
obtain r where "0 < r" and r: "cball z r \<subseteq> S"
and ul: "uniform_limit (cball z r) f g sequentially"
-      using ulim_g [OF \<open>z \<in> S\<close>] by blast
+      using ulim_g [OF \<open>z \<in> S\<close>] by blast
have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and>
(\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))"
proof (intro eventuallyI conjI ballI)
@@ -6555,7 +6555,7 @@

subsection\<open>On analytic functions defined by a series\<close>
-
+
lemma series_and_derivative_comparison:
fixes S :: "complex set"
assumes S: "open S"
@@ -6878,7 +6878,7 @@
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
+      case True
then have "f field_differentiable at a"
using holfb \<open>0 < e\<close> holomorphic_on_imp_differentiable_at by auto
with True show ?thesis
@@ -6961,10 +6961,10 @@
\<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
shows "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on S" (is "?F analytic_on S")
unfolding analytic_on_def
-proof
+proof
fix x
assume "x \<in> S"
-  with g obtain e where "0 < e" and e: "g holomorphic_on ball x e"
+  with g obtain e where "0 < e" and e: "g holomorphic_on ball x e"
obtain d where "0 < d" and d: "\<And>w. w \<in> ball x d - {a} \<Longrightarrow> g w = (w - a) * f w"
using \<open>x \<in> S\<close> eq by blast
@@ -7279,7 +7279,7 @@
obtain k1 where "k1>0" and k1: "\<And>x'. norm (x' - x) \<le> k1 \<Longrightarrow> norm (deriv f x' - deriv f x) < e"
using \<open>0 < e\<close> continuous_within_E [OF con_derf [OF \<open>x \<in> U\<close>]]
by (metis UNIV_I dist_norm)
-      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> U"
+      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> U"
by (blast intro: openE [OF \<open>open U\<close>] \<open>x \<in> U\<close>)
have neq: "norm ((f z' - f x') / (z' - x') - deriv f x) \<le> e"
if "z' \<noteq> x'" and less_k1: "norm (x'-x, z'-x) < k1" and less_k2: "norm (x'-x, z'-x) < k2"
@@ -7518,7 +7518,7 @@
then have wn0: "\<And>w. w \<notin> S \<Longrightarrow> winding_number p w = 0"
show ?thesis
-    using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols
+    using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols
by (metis wn_eq cint_eq has_contour_integral_eqpath cint_fw cint_eq)
qed

@@ -7579,7 +7579,7 @@
using valid_path_imp_path by blast

proposition holomorphic_logarithm_exists:
-  assumes A: "convex A" "open A"
+  assumes A: "convex A" "open A"
and f: "f holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
and z0: "z0 \<in> A"
obtains g where "g holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> exp (g x) = f x"```
```--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jun 25 14:45:05 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jun 25 14:06:50 2018 +0100
@@ -60,7 +60,7 @@
shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
proof (cases "Im z = 0 \<or> Re z = 0")
case True
-  with assms abs_square_less_1 show ?thesis
+  with assms abs_square_less_1 show ?thesis
by (force simp add: Re_power2 Im_power2 cmod_def)
next
case False
@@ -210,7 +210,7 @@

lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
(is "?lhs = ?rhs")
-proof
+proof
assume "exp z = 1"
then have "Re z = 0"
by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
@@ -770,15 +770,15 @@

subsection\<open>The argument of a complex number\<close>

-definition Arg :: "complex \<Rightarrow> real" where
- "Arg z \<equiv> if z = 0 then 0
+definition Arg2pi :: "complex \<Rightarrow> real" where
+ "Arg2pi z \<equiv> if z = 0 then 0
else THE t. 0 \<le> t \<and> t < 2*pi \<and>
z = of_real(norm z) * exp(\<i> * of_real t)"

-lemma Arg_0 [simp]: "Arg(0) = 0"
-
-lemma Arg_unique_lemma:
+lemma Arg2pi_0 [simp]: "Arg2pi(0) = 0"
+
+lemma Arg2pi_unique_lemma:
assumes z:  "z = of_real(norm z) * exp(\<i> * of_real t)"
and z': "z = of_real(norm z) * exp(\<i> * of_real t')"
and t:  "0 \<le> t"  "t < 2*pi"
@@ -803,10 +803,10 @@
qed

-lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
+lemma Arg2pi: "0 \<le> Arg2pi z & Arg2pi z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
proof (cases "z=0")
case True then show ?thesis
next
case False
obtain t where t: "0 \<le> t" "t < 2*pi"
@@ -819,70 +819,70 @@
apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
done
show ?thesis
-    apply (simp add: Arg_def False)
+    apply (simp add: Arg2pi_def False)
apply (rule theI [where a=t])
using t z False
-    apply (auto intro: Arg_unique_lemma)
+    apply (auto intro: Arg2pi_unique_lemma)
done
qed

corollary
-  shows Arg_ge_0: "0 \<le> Arg z"
-    and Arg_lt_2pi: "Arg z < 2*pi"
-    and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
-  using Arg by auto
-
-lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg z)) = z"
-  by (metis Arg_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
-
-lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
-  by (rule Arg_unique_lemma [OF _ Arg_eq])
-  (use Arg [of z] in \<open>auto simp: norm_mult\<close>)
-
-lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
-  apply (rule Arg_unique [of "norm z"])
+  shows Arg2pi_ge_0: "0 \<le> Arg2pi z"
+    and Arg2pi_lt_2pi: "Arg2pi z < 2*pi"
+    and Arg2pi_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
+  using Arg2pi by auto
+
+lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg2pi z)) = z"
+  by (metis Arg2pi_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
+
+lemma Arg2pi_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg2pi z = a"
+  by (rule Arg2pi_unique_lemma [OF _ Arg2pi_eq])
+  (use Arg2pi [of z] in \<open>auto simp: norm_mult\<close>)
+
+lemma Arg2pi_minus: "z \<noteq> 0 \<Longrightarrow> Arg2pi (-z) = (if Arg2pi z < pi then Arg2pi z + pi else Arg2pi z - pi)"
+  apply (rule Arg2pi_unique [of "norm z"])
apply (rule complex_eqI)
-  using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z]
+  using Arg2pi_ge_0 [of z] Arg2pi_eq [of z] Arg2pi_lt_2pi [of z]
apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
apply (metis Re_rcis Im_rcis rcis_def)+
done

-lemma Arg_times_of_real [simp]:
-  assumes "0 < r" shows "Arg (of_real r * z) = Arg z"
+lemma Arg2pi_times_of_real [simp]:
+  assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z"
proof (cases "z=0")
case False
show ?thesis
-    by (rule Arg_unique [of "r * norm z"]) (use Arg False assms in auto)
+    by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms in auto)
qed auto

-lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
-  by (metis Arg_times_of_real mult.commute)
-
-lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
-  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
-
-lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
+lemma Arg2pi_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg2pi (z * of_real r) = Arg2pi z"
+  by (metis Arg2pi_times_of_real mult.commute)
+
+lemma Arg2pi_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg2pi (z / of_real r) = Arg2pi z"
+  by (metis Arg2pi_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
+
+lemma Arg2pi_le_pi: "Arg2pi z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
proof (cases "z=0")
case False
-  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
-    by (metis Arg_eq)
-  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
+  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+    by (metis Arg2pi_eq)
+  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg2pi z))))"
using False  by (simp add: zero_le_mult_iff)
-  also have "... \<longleftrightarrow> Arg z \<le> pi"
-    by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
+  also have "... \<longleftrightarrow> Arg2pi z \<le> pi"
+    by (simp add: Im_exp) (metis Arg2pi_ge_0 Arg2pi_lt_2pi sin_lt_zero sin_ge_zero not_le)
finally show ?thesis
by blast
qed auto

-lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
+lemma Arg2pi_lt_pi: "0 < Arg2pi z \<and> Arg2pi z < pi \<longleftrightarrow> 0 < Im z"
proof (cases "z=0")
case False
-  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
-    by (metis Arg_eq)
-  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
+  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+    by (metis Arg2pi_eq)
+  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg2pi z))))"
using False by (simp add: zero_less_mult_iff)
-  also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
-    using Arg_ge_0 Arg_lt_2pi sin_le_zero sin_gt_zero
+  also have "... \<longleftrightarrow> 0 < Arg2pi z \<and> Arg2pi z < pi"
+    using Arg2pi_ge_0 Arg2pi_lt_2pi sin_le_zero sin_gt_zero
apply (auto simp: Im_exp)
using le_less apply fastforce
using not_le by blast
@@ -890,19 +890,19 @@
by blast
qed auto

-lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
+lemma Arg2pi_eq_0: "Arg2pi z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
proof (cases "z=0")
case False
-  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
-    by (metis Arg_eq)
-  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
+  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+    by (metis Arg2pi_eq)
+  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg2pi z)))"
using False  by (simp add: zero_le_mult_iff)
-  also have "... \<longleftrightarrow> Arg z = 0"
+  also have "... \<longleftrightarrow> Arg2pi z = 0"
proof -
-    have [simp]: "Arg z = 0 \<Longrightarrow> z \<in> \<real>"
-      using Arg_eq [of z] by (auto simp: Reals_def)
-    moreover have "\<lbrakk>z \<in> \<real>; 0 \<le> cos (Arg z)\<rbrakk> \<Longrightarrow> Arg z = 0"
-      by (metis Arg_lt_pi Arg_ge_0 Arg_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
+    have [simp]: "Arg2pi z = 0 \<Longrightarrow> z \<in> \<real>"
+      using Arg2pi_eq [of z] by (auto simp: Reals_def)
+    moreover have "\<lbrakk>z \<in> \<real>; 0 \<le> cos (Arg2pi z)\<rbrakk> \<Longrightarrow> Arg2pi z = 0"
+      by (metis Arg2pi_lt_pi Arg2pi_ge_0 Arg2pi_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
ultimately show ?thesis
by (auto simp: Re_exp)
qed
@@ -910,104 +910,104 @@
by blast
qed auto

-corollary Arg_gt_0:
+corollary Arg2pi_gt_0:
assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
-    shows "Arg z > 0"
-  using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce
-
-lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
-
-lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
-  using Arg_eq_0 [of "-z"]
-  by (metis Arg_eq_0 Arg_gt_0 Arg_le_pi Arg_lt_pi complex_is_Real_iff dual_order.order_iff_strict not_less pi_neq_zero)
-
-lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
-  using Arg_eq_0 Arg_eq_pi not_le by auto
-
-lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
+    shows "Arg2pi z > 0"
+  using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order by fastforce
+
+lemma Arg2pi_of_real: "Arg2pi(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
+
+lemma Arg2pi_eq_pi: "Arg2pi z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
+  using Arg2pi_eq_0 [of "-z"]
+  by (metis Arg2pi_eq_0 Arg2pi_gt_0 Arg2pi_le_pi Arg2pi_lt_pi complex_is_Real_iff dual_order.order_iff_strict not_less pi_neq_zero)
+
+lemma Arg2pi_eq_0_pi: "Arg2pi z = 0 \<or> Arg2pi z = pi \<longleftrightarrow> z \<in> \<real>"
+  using Arg2pi_eq_0 Arg2pi_eq_pi not_le by auto
+
+lemma Arg2pi_inverse: "Arg2pi(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg2pi z else 2*pi - Arg2pi z)"
proof (cases "z=0")
case False
show ?thesis
-    apply (rule Arg_unique [of "inverse (norm z)"])
-    using False Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z]
+    apply (rule Arg2pi_unique [of "inverse (norm z)"])
+    using False Arg2pi_ge_0 [of z] Arg2pi_lt_2pi [of z] Arg2pi_eq [of z] Arg2pi_eq_0 [of z]
apply (auto simp: exp_diff field_simps)
done
qed auto

-lemma Arg_eq_iff:
+lemma Arg2pi_eq_iff:
assumes "w \<noteq> 0" "z \<noteq> 0"
-     shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
-  using assms Arg_eq [of z] Arg_eq [of w]
+     shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
+  using assms Arg2pi_eq [of z] Arg2pi_eq [of w]
apply auto
apply (rule_tac x="norm w / norm z" in exI)
by (metis mult.commute mult.left_commute)

-lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
-  by (metis Arg_eq_0 Arg_inverse inverse_inverse_eq)
-
-lemma Arg_divide:
-  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
-    shows "Arg(z / w) = Arg z - Arg w"
-  apply (rule Arg_unique [of "norm(z / w)"])
-  using assms Arg_eq Arg_ge_0 [of w] Arg_lt_2pi [of z]
+lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \<longleftrightarrow> Arg2pi z = 0"
+  by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq)
+
+lemma Arg2pi_divide:
+  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg2pi w \<le> Arg2pi z"
+    shows "Arg2pi(z / w) = Arg2pi z - Arg2pi w"
+  apply (rule Arg2pi_unique [of "norm(z / w)"])
+  using assms Arg2pi_eq Arg2pi_ge_0 [of w] Arg2pi_lt_2pi [of z]
apply (auto simp: exp_diff norm_divide field_simps)
done

-lemma Arg_le_div_sum:
-  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
-    shows "Arg z = Arg w + Arg(z / w)"
-  by (simp add: Arg_divide assms)
-
-lemma Arg_le_div_sum_eq:
+lemma Arg2pi_le_div_sum:
+  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg2pi w \<le> Arg2pi z"
+    shows "Arg2pi z = Arg2pi w + Arg2pi(z / w)"
+  by (simp add: Arg2pi_divide assms)
+
+lemma Arg2pi_le_div_sum_eq:
assumes "w \<noteq> 0" "z \<noteq> 0"
-    shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
-  using assms by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
-
-lemma Arg_diff:
+    shows "Arg2pi w \<le> Arg2pi z \<longleftrightarrow> Arg2pi z = Arg2pi w + Arg2pi(z / w)"
+  using assms by (auto simp: Arg2pi_ge_0 intro: Arg2pi_le_div_sum)
+
+lemma Arg2pi_diff:
assumes "w \<noteq> 0" "z \<noteq> 0"
-    shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
-  using assms Arg_divide Arg_inverse [of "w/z"]
-  apply (clarsimp simp add: Arg_ge_0 Arg_divide not_le)
-  by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
-
+    shows "Arg2pi w - Arg2pi z = (if Arg2pi z \<le> Arg2pi w then Arg2pi(w / z) else Arg2pi(w/z) - 2*pi)"
+  using assms Arg2pi_divide Arg2pi_inverse [of "w/z"]
+  apply (clarsimp simp add: Arg2pi_ge_0 Arg2pi_divide not_le)
+  by (metis Arg2pi_eq_0 less_irrefl minus_diff_eq right_minus_eq)
+
assumes "w \<noteq> 0" "z \<noteq> 0"
-    shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
-  using assms Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
-  apply (auto simp: Arg_ge_0 Arg_divide not_le)
+    shows "Arg2pi w + Arg2pi z = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi(w * z) else Arg2pi(w * z) + 2*pi)"
+  using assms Arg2pi_diff [of "w*z" z] Arg2pi_le_div_sum_eq [of z "w*z"]
+  apply (auto simp: Arg2pi_ge_0 Arg2pi_divide not_le)
done

-lemma Arg_times:
+lemma Arg2pi_times:
assumes "w \<noteq> 0" "z \<noteq> 0"
-    shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
-                            else (Arg w + Arg z) - 2*pi)"
+    shows "Arg2pi (w * z) = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi w + Arg2pi z
+                            else (Arg2pi w + Arg2pi z) - 2*pi)"
by auto

-lemma Arg_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg (cnj z) = Arg (inverse z)"
-  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
+lemma Arg2pi_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg2pi (cnj z) = Arg2pi (inverse z)"
+  apply (simp add: Arg2pi_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
by (metis of_real_power zero_less_norm_iff zero_less_power)

-lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
+lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg2pi z else 2*pi - Arg2pi z)"
proof (cases "z=0")
case False
then show ?thesis
-    by (simp add: Arg_cnj_eq_inverse Arg_inverse)
+    by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse)
qed auto

-lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
-  using Arg_eq_0 Arg_eq_0_pi by auto
-
-lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
-  by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
+lemma Arg2pi_real: "z \<in> \<real> \<Longrightarrow> Arg2pi z = (if 0 \<le> Re z then 0 else pi)"
+  using Arg2pi_eq_0 Arg2pi_eq_0_pi by auto
+
+lemma Arg2pi_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg2pi(exp z) = Im z"
+  by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)

lemma complex_split_polar:
obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
-  using Arg cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
+  using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq by fastforce

lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
proof (cases w rule: complex_split_polar)
@@ -1108,10 +1108,10 @@
have "ln (exp 0) = (0::complex)"
then show ?thesis
-    by simp
+    by simp
qed

-
+
lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex
by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)

@@ -1214,7 +1214,7 @@
lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S Ln"

-lemma continuous_on_Ln' [continuous_intros]:
+lemma continuous_on_Ln' [continuous_intros]:
"continuous_on S f \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S (\<lambda>x. Ln (f x))"
by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto

@@ -1254,7 +1254,7 @@
using exp_le \<open>3 \<le> x\<close> x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)
qed
qed
-
+

@@ -1367,7 +1367,7 @@
have "\<bar>Im (cnj (Ln z))\<bar> < pi"
by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
moreover have "\<bar>Im (Ln (cnj z))\<bar> \<le> pi"
-        by (meson abs_le_iff complex_cnj_zero_iff less_eq_real_def minus_less_iff  False Im_Ln_le_pi mpi_less_Im_Ln)
+        by (meson abs_le_iff complex_cnj_zero_iff less_eq_real_def minus_less_iff  False Im_Ln_le_pi mpi_less_Im_Ln)
ultimately show ?thesis
by simp
qed
@@ -1375,7 +1375,7 @@
by simp
show "exp (cnj (Ln z)) = exp (Ln (cnj z))"
by (metis False complex_cnj_zero_iff exp_Ln exp_cnj)
-  qed
+  qed
qed (use assms in auto)

@@ -1395,11 +1395,11 @@
ultimately show ?thesis
by simp
qed
-    finally show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi"
+    finally show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi"
by simp
show "exp (Ln (inverse z)) = exp (- Ln z)"
-  qed
+  qed
qed (use assms in auto)

lemma Ln_minus1 [simp]: "Ln(-1) = \<i> * pi"
@@ -1529,28 +1529,28 @@
using assms by (simp add: powr_def)

-subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
-
-lemma Arg_Ln:
-  assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
+subsection\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
+
+lemma Arg2pi_Ln:
+  assumes "0 < Arg2pi z" shows "Arg2pi z = Im(Ln(-z)) + pi"
proof (cases "z = 0")
case True
with assms show ?thesis
by simp
next
case False
-  then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
-    using Arg [of z]
+  then have "z / of_real(norm z) = exp(\<i> * of_real(Arg2pi z))"
+    using Arg2pi [of z]
by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
-  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
+  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg2pi z) - pi))"
using cis_conv_exp cis_pi
by (auto simp: exp_diff algebra_simps)
-  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
+  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg2pi z) - pi)))"
by simp
-  also have "... = \<i> * (of_real(Arg z) - pi)"
-    using Arg [of z] assms pi_not_less_zero
+  also have "... = \<i> * (of_real(Arg2pi z) - pi)"
+    using Arg2pi [of z] assms pi_not_less_zero
by auto
-  finally have "Arg z =  Im (Ln (- z / of_real (cmod z))) + pi"
+  finally have "Arg2pi z =  Im (Ln (- z / of_real (cmod z))) + pi"
by simp
also have "... = Im (Ln (-z) - ln (cmod z)) + pi"
by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
@@ -1559,23 +1559,23 @@
finally show ?thesis .
qed

-lemma continuous_at_Arg:
+lemma continuous_at_Arg2pi:
assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
-    shows "continuous (at z) Arg"
+    shows "continuous (at z) Arg2pi"
proof -
have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
-  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
+  have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
+    using Arg2pi_Ln Arg2pi_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
-  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)
+  then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
+    using "*"  by (simp add: isCont_def) (metis Arg2pi_Ln Arg2pi_gt_0 complex_is_Real_iff)
show ?thesis
unfolding continuous_at
proof (rule Lim_transform_within_open)
-    show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
-      by (auto simp add: Arg_Ln [OF Arg_gt_0] complex_nonneg_Reals_iff)
+    show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
+      by (auto simp add: Arg2pi_Ln [OF Arg2pi_gt_0] complex_nonneg_Reals_iff)
qed (use assms in auto)
qed

@@ -1662,8 +1662,8 @@
(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> (\<Sum>i. norm (-(z^2) * (-z)^i))"
+  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)
@@ -1678,14 +1678,14 @@
qed

-text\<open>Relation between Arg and arctangent in upper halfplane\<close>
-lemma Arg_arctan_upperhalf:
+text\<open>Relation between Arg2pi and arctangent in upper halfplane\<close>
+lemma Arg2pi_arctan_upperhalf:
assumes "0 < Im z"
-    shows "Arg z = pi/2 - arctan(Re z / Im z)"
+    shows "Arg2pi z = pi/2 - arctan(Re z / Im z)"
proof (cases "z = 0")
case False
show ?thesis
-  proof (rule Arg_unique [of "norm z"])
+  proof (rule Arg2pi_unique [of "norm z"])
show "(cmod z) * exp (\<i> * (pi / 2 - arctan (Re z / Im z))) = z"
apply (auto simp: exp_Euler cos_diff sin_diff)
using assms norm_complex_def [of z, symmetric]
@@ -1695,34 +1695,34 @@
qed (use False arctan [of "Re z / Im z"] in auto)
qed (use assms in auto)

-lemma Arg_eq_Im_Ln:
+lemma Arg2pi_eq_Im_Ln:
assumes "0 \<le> Im z" "0 < Re z"
-    shows "Arg z = Im (Ln z)"
+    shows "Arg2pi z = Im (Ln z)"
proof (cases "Im z = 0")
case True then show ?thesis
-    using Arg_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto
+    using Arg2pi_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto
next
case False
-  then have *: "Arg z > 0"
-    using Arg_gt_0 complex_is_Real_iff by blast
+  then have *: "Arg2pi z > 0"
+    using Arg2pi_gt_0 complex_is_Real_iff by blast
then have "z \<noteq> 0"
by auto
with * assms False show ?thesis
-    by (subst Arg_Ln) (auto simp: Ln_minus)
+    by (subst Arg2pi_Ln) (auto simp: Ln_minus)
qed

-lemma continuous_within_upperhalf_Arg:
+lemma continuous_within_upperhalf_Arg2pi:
assumes "z \<noteq> 0"
-    shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
+    shows "continuous (at z within {z. 0 \<le> Im z}) Arg2pi"
proof (cases "z \<in> \<real>\<^sub>\<ge>\<^sub>0")
case False then show ?thesis
-    using continuous_at_Arg continuous_at_imp_continuous_within by auto
+    using continuous_at_Arg2pi continuous_at_imp_continuous_within by auto
next
case True
then have z: "z \<in> \<real>" "0 < Re z"
using assms  by (auto simp: complex_nonneg_Reals_iff complex_is_Real_iff complex_neq_0)
-  then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
-    by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
+  then have [simp]: "Arg2pi z = 0" "Im (Ln z) = 0"
+    by (auto simp: Arg2pi_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
show ?thesis
proof (clarsimp simp add: continuous_within Lim_within dist_norm)
fix e::real
@@ -1739,50 +1739,50 @@
then have "0 < Re x"
using z by linarith
}
-    then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg x\<bar> < e"
+    then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg2pi x\<bar> < e"
apply (rule_tac x="min d (Re z / 2)" in exI)
using z d
-      apply (auto simp: Arg_eq_Im_Ln)
+      apply (auto simp: Arg2pi_eq_Im_Ln)
done
qed
qed

-lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg"
+lemma continuous_on_upperhalf_Arg2pi: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg2pi"
unfolding continuous_on_eq_continuous_within
-  by (metis DiffE Diff_subset continuous_within_subset continuous_within_upperhalf_Arg insertCI)
-
-lemma open_Arg_less_Int:
+  by (metis DiffE Diff_subset continuous_within_subset continuous_within_upperhalf_Arg2pi insertCI)
+
+lemma open_Arg2pi2pi_less_Int:
assumes "0 \<le> s" "t \<le> 2*pi"
-    shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
+    shows "open ({y. s < Arg2pi y} \<inter> {y. Arg2pi y < t})"
proof -
-  have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg"
-    using continuous_at_Arg continuous_at_imp_continuous_within
+  have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg2pi"
+    using continuous_at_Arg2pi continuous_at_imp_continuous_within
by (auto simp: continuous_on_eq_continuous_within)
have 2: "open (UNIV - \<real>\<^sub>\<ge>\<^sub>0 :: complex set)"  by (simp add: open_Diff)
have "open ({z. s < z} \<inter> {z. z < t})"
using open_lessThan [of t] open_greaterThan [of s]
by (metis greaterThan_def lessThan_def open_Int)
-  moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
-    using assms by (auto simp: Arg_real complex_nonneg_Reals_iff complex_is_Real_iff)
+  moreover have "{y. s < Arg2pi y} \<inter> {y. Arg2pi y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
+    using assms by (auto simp: Arg2pi_real complex_nonneg_Reals_iff complex_is_Real_iff)
ultimately show ?thesis
using continuous_imp_open_vimage [OF 1 2, of  "{z. Re z > s} \<inter> {z. Re z < t}"]
by auto
qed

-lemma open_Arg_gt: "open {z. t < Arg z}"
+lemma open_Arg2pi2pi_gt: "open {z. t < Arg2pi z}"
proof (cases "t < 0")
-  case True then have "{z. t < Arg z} = UNIV"
-    using Arg_ge_0 less_le_trans by auto
+  case True then have "{z. t < Arg2pi z} = UNIV"
+    using Arg2pi_ge_0 less_le_trans by auto
then show ?thesis
by simp
next
case False then show ?thesis
-    using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi
+    using open_Arg2pi2pi_less_Int [of t "2*pi"] Arg2pi_lt_2pi
by auto
qed

-lemma closed_Arg_le: "closed {z. Arg z \<le> t}"
-  using open_Arg_gt [of t]
+lemma closed_Arg2pi2pi_le: "closed {z. Arg2pi z \<le> t}"
+  using open_Arg2pi2pi_gt [of t]
by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)

subsection\<open>Complex Powers\<close>
@@ -1890,7 +1890,7 @@
declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]

lemma has_field_derivative_powr_of_int:
-  fixes z :: complex
+  fixes z :: complex
assumes gderiv:"(g has_field_derivative gd) (at z within s)" and "g z\<noteq>0"
shows "((\<lambda>z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within s)"
proof -
@@ -1905,7 +1905,7 @@
case False
then have "n-1 \<ge>0" using \<open>n\<ge>0\<close> by auto
then have "g z powr (of_int (n - 1)) = g z ^ (nat n - 1)"
-        using powr_of_int[OF \<open>g z\<noteq>0\<close>,of "n-1"] by (simp add: nat_diff_distrib')
+        using powr_of_int[OF \<open>g z\<noteq>0\<close>,of "n-1"] by (simp add: nat_diff_distrib')
then show ?thesis unfolding dd_def dd'_def by simp
then have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within s)
@@ -1958,7 +1958,7 @@
qed

lemma field_differentiable_powr_of_int:
-  fixes z :: complex
+  fixes z :: complex
assumes gderiv:"g field_differentiable (at z within s)" and "g z\<noteq>0"
shows "(\<lambda>z. g z powr of_int n) field_differentiable (at z within s)"
using has_field_derivative_powr_of_int assms(2) field_differentiable_def gderiv by blast
@@ -1972,7 +1972,7 @@
apply (rule_tac holomorphic_cong)
using assms(2) by (auto simp add:powr_of_int)
moreover have "(\<lambda>z. (f z) ^ nat n) holomorphic_on s"
-    using assms(1) by (auto intro:holomorphic_intros)
+    using assms(1) by (auto intro:holomorphic_intros)
ultimately show ?thesis by auto
next
case False
@@ -1980,7 +1980,7 @@
apply (rule_tac holomorphic_cong)
using assms(2) by (auto simp add:powr_of_int power_inverse)
moreover have "(\<lambda>z. inverse (f z) ^ nat (-n)) holomorphic_on s"
-    using assms by (auto intro!:holomorphic_intros)
+    using assms by (auto intro!:holomorphic_intros)
ultimately show ?thesis by auto
qed

@@ -2194,7 +2194,7 @@
apply (auto simp: norm_divide norm_powr_real divide_simps)
apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff)
done
-  then show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
+  then show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
by blast
qed

@@ -2504,7 +2504,7 @@
proof -
have nz0: "1 + \<i>*z \<noteq> 0"
using assms
-    by (metis abs_one add_diff_cancel_left' complex_i_mult_minus diff_0 i_squared imaginary_unit.simps
+    by (metis abs_one add_diff_cancel_left' complex_i_mult_minus diff_0 i_squared imaginary_unit.simps
less_asym neg_equal_iff_equal)
have "z \<noteq> -\<i>" using assms
by auto
@@ -2847,7 +2847,7 @@
using arctan_bounds[of "1/5"   4]
arctan_bounds[of "1/239" 4]
-
+
corollary pi_gt3: "pi > 3"
using pi_approx by simp

@@ -2987,7 +2987,7 @@
lemma has_field_derivative_Arcsin:
assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
-proof -
+proof -
have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
using assms one_minus_z2_notin_nonpos_Reals by force
then have "cos (Arcsin z) \<noteq> 0"
@@ -3682,8 +3682,8 @@
lemma homotopic_loops_imp_homotopic_circlemaps:
assumes "homotopic_loops S p q"
shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
-                          (p \<circ> (\<lambda>z. (Arg z / (2 * pi))))
-                          (q \<circ> (\<lambda>z. (Arg z / (2 * pi))))"
+                          (p \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))
+                          (q \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))"
proof -
obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
@@ -3693,41 +3693,41 @@
using assms
by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
define j where "j \<equiv> \<lambda>z. if 0 \<le> Im (snd z)
-                          then h (fst z, Arg (snd z) / (2 * pi))
-                          else h (fst z, 1 - Arg (cnj (snd z)) / (2 * pi))"
-  have Arg_eq: "1 - Arg (cnj y) / (2 * pi) = Arg y / (2 * pi) \<or> Arg y = 0 \<and> Arg (cnj y) = 0" if "cmod y = 1" for y
-    using that Arg_eq_0_pi Arg_eq_pi by (force simp: Arg_cnj divide_simps)
+                          then h (fst z, Arg2pi (snd z) / (2 * pi))
+                          else h (fst z, 1 - Arg2pi (cnj (snd z)) / (2 * pi))"
+  have Arg2pi_eq: "1 - Arg2pi (cnj y) / (2 * pi) = Arg2pi y / (2 * pi) \<or> Arg2pi y = 0 \<and> Arg2pi (cnj y) = 0" if "cmod y = 1" for y
+    using that Arg2pi_eq_0_pi Arg2pi_eq_pi by (force simp: Arg2pi_cnj divide_simps)
show ?thesis
proof (simp add: homotopic_with; intro conjI ballI exI)
-    show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg (snd w) / (2 * pi)))"
+    show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi)))"
proof (rule continuous_on_eq)
-      show j: "j x = h (fst x, Arg (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
-        using Arg_eq that h01 by (force simp: j_def)
+      show j: "j x = h (fst x, Arg2pi (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
+        using Arg2pi_eq that h01 by (force simp: j_def)
have eq:  "S = S \<inter> (UNIV \<times> {z. 0 \<le> Im z}) \<union> S \<inter> (UNIV \<times> {z. Im z \<le> 0})" for S :: "(real*complex)set"
by auto
-      have c1: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. 0 \<le> Im z}) (\<lambda>x. h (fst x, Arg (snd x) / (2 * pi)))"
-        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
-            apply (auto simp: Arg)
-        apply (meson Arg_lt_2pi linear not_le)
+      have c1: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. 0 \<le> Im z}) (\<lambda>x. h (fst x, Arg2pi (snd x) / (2 * pi)))"
+        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi])
+            apply (auto simp: Arg2pi)
+        apply (meson Arg2pi_lt_2pi linear not_le)
done
-      have c2: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. Im z \<le> 0}) (\<lambda>x. h (fst x, 1 - Arg (cnj (snd x)) / (2 * pi)))"
-        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
-            apply (auto simp: Arg)
-        apply (meson Arg_lt_2pi linear not_le)
+      have c2: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. Im z \<le> 0}) (\<lambda>x. h (fst x, 1 - Arg2pi (cnj (snd x)) / (2 * pi)))"
+        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi])
+            apply (auto simp: Arg2pi)
+        apply (meson Arg2pi_lt_2pi linear not_le)
done
show "continuous_on ({0..1} \<times> sphere 0 1) j"
apply (subst eq)
apply (rule continuous_on_cases_local)
apply (simp_all add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)
-        using Arg_eq h01
+        using Arg2pi_eq h01
by force
qed
-    have "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
-      by (auto simp: Arg_ge_0 Arg_lt_2pi less_imp_le)
+    have "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
+      by (auto simp: Arg2pi_ge_0 Arg2pi_lt_2pi less_imp_le)
also have "... \<subseteq> S"
using him by blast
-    finally show "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
+    finally show "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
qed (auto simp: h0 h1)
qed

@@ -3794,7 +3794,7 @@
assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
then have "homotopic_loops S p p"
-  then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg z / (2 * pi))) (\<lambda>x. a)"
+  then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi))) (\<lambda>x. a)"
by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
proof (intro exI conjI)
@@ -3802,11 +3802,11 @@
using homotopic_with_imp_subset2 [OF homp]
by (metis dist_0_norm image_subset_iff mem_sphere norm_one)
have teq: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk>
-               \<Longrightarrow> t = Arg (exp (2 * of_real pi * of_real t * \<i>)) / (2 * pi) \<or> t=1 \<and> Arg (exp (2 * of_real pi * of_real t * \<i>)) = 0"
+               \<Longrightarrow> t = Arg2pi (exp (2 * of_real pi * of_real t * \<i>)) / (2 * pi) \<or> t=1 \<and> Arg2pi (exp (2 * of_real pi * of_real t * \<i>)) = 0"
apply (rule disjCI)
-      using Arg_of_real [of 1] apply (auto simp: Arg_exp)
+      using Arg2pi_of_real [of 1] apply (auto simp: Arg2pi_exp)
done
-    have "homotopic_loops S p (p \<circ> (\<lambda>z. Arg z / (2 * pi)) \<circ> exp \<circ> (\<lambda>t. 2 * complex_of_real pi * complex_of_real t * \<i>))"
+    have "homotopic_loops S p (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi)) \<circ> exp \<circ> (\<lambda>t. 2 * complex_of_real pi * complex_of_real t * \<i>))"
apply (rule homotopic_loops_eq [OF p])
using p teq apply (fastforce simp: pathfinish_def pathstart_def)
done
@@ -3855,45 +3855,45 @@
have "homotopic_loops (path_image \<gamma>) \<gamma> \<gamma>"
by (simp add: assms homotopic_loops_refl simple_path_imp_path)
then have hom: "homotopic_with (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
-               (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
+               (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi)))"
by (rule homotopic_loops_imp_homotopic_circlemaps)
-  have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) g"
+  have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) g"
proof (rule homeomorphism_compact)
-    show "continuous_on (sphere 0 1) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
+    show "continuous_on (sphere 0 1) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi)))"
using hom homotopic_with_imp_continuous by blast
-    show "inj_on (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (sphere 0 1)"
+    show "inj_on (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) (sphere 0 1)"
proof
fix x y
assume xy: "x \<in> sphere 0 1" "y \<in> sphere 0 1"
-         and eq: "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) x = (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) y"
-      then have "(Arg x / (2*pi)) = (Arg y / (2*pi))"
+         and eq: "(\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) x = (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) y"
+      then have "(Arg2pi x / (2*pi)) = (Arg2pi y / (2*pi))"
proof -
-        have "(Arg x / (2*pi)) \<in> {0..1}" "(Arg y / (2*pi)) \<in> {0..1}"
-          using Arg_ge_0 Arg_lt_2pi dual_order.strict_iff_order by fastforce+
+        have "(Arg2pi x / (2*pi)) \<in> {0..1}" "(Arg2pi y / (2*pi)) \<in> {0..1}"
+          using Arg2pi_ge_0 Arg2pi_lt_2pi dual_order.strict_iff_order by fastforce+
with eq show ?thesis
-          using \<open>simple_path \<gamma>\<close> Arg_lt_2pi unfolding simple_path_def o_def
+          using \<open>simple_path \<gamma>\<close> Arg2pi_lt_2pi unfolding simple_path_def o_def
by (metis eq_divide_eq_1 not_less_iff_gr_or_eq)
qed
with xy show "x = y"
-        by (metis Arg Arg_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
+        by (metis Arg2pi Arg2pi_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
qed
-    have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg z / (2*pi)) = \<gamma> x"
-       by (metis Arg_ge_0 Arg_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
-     moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
+    have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg2pi z / (2*pi)) = \<gamma> x"
+       by (metis Arg2pi_ge_0 Arg2pi_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
+     moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg2pi z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
proof (cases "x=1")
case True
then show ?thesis
apply (rule_tac x=1 in bexI)
-         apply (metis loop Arg_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
+         apply (metis loop Arg2pi_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
done
next
case False
-       then have *: "(Arg (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
-         using that by (auto simp: Arg_exp divide_simps)
+       then have *: "(Arg2pi (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
+         using that by (auto simp: Arg2pi_exp divide_simps)
show ?thesis
by (rule_tac x="exp(\<i> * of_real(2*pi*x))" in bexI) (auto simp: *)
qed
-    ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
+    ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
by (auto simp: path_image_def image_iff)
qed auto
then have "path_image \<gamma> homeomorphic sphere (0::complex) 1"```