src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy

   "winding_number \<gamma> z \<equiv>
     @n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
                     pathstart p = pathstart \<gamma> \<and>
                     pathfinish p = pathfinish \<gamma> \<and>
                     (\<forall>t \<in> {0..1}. norm(\<gamma> t - p t) < e) \<and>
-                    contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+                    contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
 
 lemma winding_number:
   assumes "path \<gamma>" "z \<notin> path_image \<gamma>" "0 < e"
     shows "\<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
                pathstart p = pathstart \<gamma> \<and>
                pathfinish p = pathfinish \<gamma> \<and>
                (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
-               contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * winding_number \<gamma> z"
+               contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * winding_number \<gamma> z"
 proof -
   have "path_image \<gamma> \<subseteq> UNIV - {z}"
     using assms by blast
   then obtain d
     where d: "d>0"

                       (\<forall>f. f holomorphic_on UNIV - {z} \<longrightarrow> contour_integral h2 f = contour_integral h1 f)"
     using contour_integral_nearby_ends [of "UNIV - {z}" \<gamma>] assms by (auto simp: open_delete)
   then obtain h where h: "polynomial_function h \<and> pathstart h = pathstart \<gamma> \<and> pathfinish h = pathfinish \<gamma> \<and>
                           (\<forall>t \<in> {0..1}. norm(h t - \<gamma> t) < d/2)"
     using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "d/2"] d by auto
-  define nn where "nn = 1/(2* pi*ii) * contour_integral h (\<lambda>w. 1/(w - z))"
+  define nn where "nn = 1/(2* pi*\<i>) * contour_integral h (\<lambda>w. 1/(w - z))"
   have "\<exists>n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
                         pathstart p = pathstart \<gamma> \<and>  pathfinish p = pathfinish \<gamma> \<and>
                         (\<forall>t \<in> {0..1}. norm(\<gamma> t - p t) < e) \<and>
-                        contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+                        contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
                     (is "\<exists>n. \<forall>e > 0. ?PP e n")
     proof (rule_tac x=nn in exI, clarify)
       fix e::real
       assume e: "e>0"
       obtain p where p: "polynomial_function p \<and>

   assumes \<gamma>: "path \<gamma>" "z \<notin> path_image \<gamma>"
       and pi:
         "\<And>e. e>0 \<Longrightarrow> \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
                           pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
                           (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
-                          contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+                          contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
    shows "winding_number \<gamma> z = n"
 proof -
   have "path_image \<gamma> \<subseteq> UNIV - {z}"
     using assms by blast
   then obtain e

     using contour_integral_nearby_ends [of "UNIV - {z}" \<gamma>] assms  by (auto simp: open_delete)
   obtain p where p:
      "valid_path p \<and> z \<notin> path_image p \<and>
       pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
       (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
-      contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+      contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
     using pi [OF e] by blast
   obtain q where q:
      "valid_path q \<and> z \<notin> path_image q \<and>
       pathstart q = pathstart \<gamma> \<and> pathfinish q = pathfinish \<gamma> \<and>
       (\<forall>t\<in>{0..1}. cmod (\<gamma> t - q t) < e) \<and> contour_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"

       and loop: "pathfinish \<gamma> = pathstart \<gamma>"
       and pi:
         "\<And>e. e>0 \<Longrightarrow> \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
                            pathfinish p = pathstart p \<and>
                            (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
-                           contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+                           contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
    shows "winding_number \<gamma> z = n"
 proof -
   have "path_image \<gamma> \<subseteq> UNIV - {z}"
     using assms by blast
   then obtain e

     using contour_integral_nearby_loops [of "UNIV - {z}" \<gamma>] assms  by (auto simp: open_delete)
   obtain p where p:
      "valid_path p \<and> z \<notin> path_image p \<and>
       pathfinish p = pathstart p \<and>
       (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
-      contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+      contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
     using pi [OF e] by blast
   obtain q where q:
      "valid_path q \<and> z \<notin> path_image q \<and>
       pathstart q = pathstart \<gamma> \<and> pathfinish q = pathfinish \<gamma> \<and>
       (\<forall>t\<in>{0..1}. cmod (\<gamma> t - q t) < e) \<and> contour_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"

     by simp
 qed
 
 lemma winding_number_valid_path:
   assumes "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
-    shows "winding_number \<gamma> z = 1/(2*pi*ii) * contour_integral \<gamma> (\<lambda>w. 1/(w - z))"
+    shows "winding_number \<gamma> z = 1/(2*pi*\<i>) * contour_integral \<gamma> (\<lambda>w. 1/(w - z))"
   using assms by (auto simp: valid_path_imp_path intro!: winding_number_unique)
 
 lemma has_contour_integral_winding_number:
   assumes \<gamma>: "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
-    shows "((\<lambda>w. 1/(w - z)) has_contour_integral (2*pi*ii*winding_number \<gamma> z)) \<gamma>"
+    shows "((\<lambda>w. 1/(w - z)) has_contour_integral (2*pi*\<i>*winding_number \<gamma> z)) \<gamma>"
 by (simp add: winding_number_valid_path has_contour_integral_integral contour_integrable_inversediff assms)
 
 lemma winding_number_trivial [simp]: "z \<noteq> a \<Longrightarrow> winding_number(linepath a a) z = 0"
   by (simp add: winding_number_valid_path)
 

   have *: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
     using ge by (simp add: Complex.Im_divide algebra_simps x)
   show ?thesis
     apply (simp add: Re_winding_number [OF \<gamma>] field_simps)
     apply (rule has_integral_component_nonneg
-             [of ii "\<lambda>x. if x \<in> {0<..<1}
+             [of \<i> "\<lambda>x. if x \<in> {0<..<1}
                          then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else 0", simplified])
       prefer 3 apply (force simp: *)
      apply (simp add: Basis_complex_def)
     apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)"])
     apply simp

       and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> e \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
     shows "0 < Re(winding_number \<gamma> z)"
 proof -
   have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
     apply (rule has_integral_component_le
-             [of ii "\<lambda>x. ii*e" "ii*e" "{0..1}"
-                    "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else ii*e"
+             [of \<i> "\<lambda>x. \<i>*e" "\<i>*e" "{0..1}"
+                    "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else \<i>*e"
                     "contour_integral \<gamma> (\<lambda>w. 1/(w - z))", simplified])
     using e
     apply (simp_all add: Basis_complex_def)
     using has_integral_const_real [of _ 0 1] apply force
     apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)", simplified box_real])

     by (simp add: divide_inverse_commute integral_def)
 qed
 
 corollary winding_number_exp_2pi:
     "\<lbrakk>path p; z \<notin> path_image p\<rbrakk>
-     \<Longrightarrow> pathfinish p - z = exp (2 * pi * ii * winding_number p z) * (pathstart p - z)"
+     \<Longrightarrow> pathfinish p - z = exp (2 * pi * \<i> * winding_number p z) * (pathstart p - z)"
 using winding_number [of p z 1] unfolding valid_path_def path_image_def pathstart_def pathfinish_def
   by (force dest: winding_number_exp_integral(2) [of _ 0 1 z] simp: field_simps contour_integral_integral exp_minus)
 
 
 subsection\<open>The version with complex integers and equality\<close>

   have *: "integral {0..x} (\<lambda>t. vector_derivative \<gamma> (at t) / (\<gamma> t - z)) / (2 * of_real pi * \<i>) =
          winding_number (subpath 0 x \<gamma>) z"
          if x: "0 \<le> x" "x \<le> 1" for x
   proof -
     have "integral {0..x} (\<lambda>t. vector_derivative \<gamma> (at t) / (\<gamma> t - z)) / (2 * of_real pi * \<i>) =
-          1 / (2*pi*ii) * contour_integral (subpath 0 x \<gamma>) (\<lambda>w. 1/(w - z))"
+          1 / (2*pi*\<i>) * contour_integral (subpath 0 x \<gamma>) (\<lambda>w. 1/(w - z))"
       using assms x
       apply (simp add: contour_integral_subcontour_integral [OF contour_integrable_inversediff])
       done
     also have "... = winding_number (subpath 0 x \<gamma>) z"
       apply (subst winding_number_valid_path)

       by (force simp: path_image_def)
     finally show ?thesis .
   qed
   show ?thesis
     apply (rule continuous_on_eq
-                 [where f = "\<lambda>x. 1 / (2*pi*ii) *
+                 [where f = "\<lambda>x. 1 / (2*pi*\<i>) *
                                  integral {0..x} (\<lambda>t. 1/(\<gamma> t - z) * vector_derivative \<gamma> (at t))"])
     apply (rule continuous_intros)+
     apply (rule indefinite_integral_continuous)
     apply (rule contour_integrable_inversediff [OF assms, unfolded contour_integrable_on])
       using assms

 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 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>"
+      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * 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: 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

 qed
 
 theorem Cauchy_integral_formula_convex_simple:
     "\<lbrakk>convex s; f holomorphic_on s; z \<in> interior s; valid_path \<gamma>; path_image \<gamma> \<subseteq> s - {z};
       pathfinish \<gamma> = pathstart \<gamma>\<rbrakk>
-     \<Longrightarrow> ((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+     \<Longrightarrow> ((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
   apply (rule Cauchy_integral_formula_weak [where k = "{}"])
   using holomorphic_on_imp_continuous_on
   by auto (metis at_within_interior holomorphic_on_def interiorE subsetCE)
 
 

 
 
 subsection\<open>Partial circle path\<close>
 
 definition part_circlepath :: "[complex, real, real, real, real] \<Rightarrow> complex"
-  where "part_circlepath z r s t \<equiv> \<lambda>x. z + of_real r * exp (ii * of_real (linepath s t x))"
+  where "part_circlepath z r s t \<equiv> \<lambda>x. z + of_real r * exp (\<i> * of_real (linepath s t x))"
 
 lemma pathstart_part_circlepath [simp]:
-     "pathstart(part_circlepath z r s t) = z + r*exp(ii * s)"
+     "pathstart(part_circlepath z r s t) = z + r*exp(\<i> * s)"
 by (metis part_circlepath_def pathstart_def pathstart_linepath)
 
 lemma pathfinish_part_circlepath [simp]:
-     "pathfinish(part_circlepath z r s t) = z + r*exp(ii*t)"
+     "pathfinish(part_circlepath z r s t) = z + r*exp(\<i>*t)"
 by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
 
 proposition has_vector_derivative_part_circlepath [derivative_intros]:
     "((part_circlepath z r s t) has_vector_derivative
-      (ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)))
+      (\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
      (at x within X)"
   apply (simp add: part_circlepath_def linepath_def scaleR_conv_of_real)
   apply (rule has_vector_derivative_real_complex)
   apply (rule derivative_eq_intros | simp)+
   done
 
 corollary vector_derivative_part_circlepath:
     "vector_derivative (part_circlepath z r s t) (at x) =
-       ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)"
+       \<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
   using has_vector_derivative_part_circlepath vector_derivative_at by blast
 
 corollary vector_derivative_part_circlepath01:
     "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
      \<Longrightarrow> vector_derivative (part_circlepath z r s t) (at x within {0..1}) =
-          ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)"
+          \<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
   using has_vector_derivative_part_circlepath
   by (auto simp: vector_derivative_at_within_ivl)
 
 lemma valid_path_part_circlepath [simp]: "valid_path (part_circlepath z r s t)"
   apply (simp add: valid_path_def)

 lemma path_part_circlepath [simp]: "path (part_circlepath z r s t)"
   by (simp add: valid_path_imp_path)
 
 proposition path_image_part_circlepath:
   assumes "s \<le> t"
-    shows "path_image (part_circlepath z r s t) = {z + r * exp(ii * of_real x) | x. s \<le> x \<and> x \<le> t}"
+    shows "path_image (part_circlepath z r s t) = {z + r * exp(\<i> * of_real x) | x. s \<le> x \<and> x \<le> t}"
 proof -
   { fix z::real
     assume "0 \<le> z" "z \<le> 1"
     with \<open>s \<le> t\<close> have "\<exists>x. (exp (\<i> * linepath s t z) = exp (\<i> * of_real x)) \<and> s \<le> x \<and> x \<le> t"
       apply (rule_tac x="(1 - z) * s + z * t" in exI)

     have [simp]: "\<bar>r\<bar> = r" using \<open>r > 0\<close> by linarith
     have [simp]: "cmod (complex_of_real t - complex_of_real s) = t-s"
       by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff)
     have "finite (part_circlepath z r s t -` {y} \<inter> {0..1})" if "y \<in> k" for y
     proof -
-      define w where "w = (y - z)/of_real r / exp(ii * of_real s)"
+      define w where "w = (y - z)/of_real r / exp(\<i> * of_real s)"
       have fin: "finite (of_real -` {z. cmod z \<le> 1 \<and> exp (\<i> * complex_of_real (t - s) * z) = w})"
         apply (rule finite_vimageI [OF finite_bounded_log2])
         using \<open>s < t\<close> apply (auto simp: inj_of_real)
         done
       show ?thesis

     apply (rule disjE)
     apply (force simp: part_circlepath_def simple_path_def intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+
     done
 next
   case False then have "r \<noteq> 0" "s \<noteq> t" by auto
-  have *: "\<And>x y z s t. ii*((1 - x) * s + x * t) = ii*(((1 - y) * s + y * t)) + z  \<longleftrightarrow> ii*(x - y) * (t - s) = z"
+  have *: "\<And>x y z s t. \<i>*((1 - x) * s + x * t) = \<i>*(((1 - y) * s + y * t)) + z  \<longleftrightarrow> \<i>*(x - y) * (t - s) = z"
     by (simp add: algebra_simps)
   have abs01: "\<And>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1
                       \<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> \<bar>x - y\<bar> \<in> {0,1})"
     by auto
   have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P \<bar>x - y\<bar>) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"

 subsection\<open>Special case of one complete circle\<close>
 
 definition circlepath :: "[complex, real, real] \<Rightarrow> complex"
   where "circlepath z r \<equiv> part_circlepath z r 0 (2*pi)"
 
-lemma circlepath: "circlepath z r = (\<lambda>x. z + r * exp(2 * of_real pi * ii * of_real x))"
+lemma circlepath: "circlepath z r = (\<lambda>x. z + r * exp(2 * of_real pi * \<i> * of_real x))"
   by (simp add: circlepath_def part_circlepath_def linepath_def algebra_simps)
 
 lemma pathstart_circlepath [simp]: "pathstart (circlepath z r) = z + r"
   by (simp add: circlepath_def)
 

 
 lemma path_image_circlepath_minus: "path_image (circlepath z (-r)) = path_image (circlepath z r)"
   using path_image_circlepath_minus_subset by fastforce
 
 proposition has_vector_derivative_circlepath [derivative_intros]:
- "((circlepath z r) has_vector_derivative (2 * pi * ii * r * exp (2 * of_real pi * ii * of_real x)))
+ "((circlepath z r) has_vector_derivative (2 * pi * \<i> * r * exp (2 * of_real pi * \<i> * of_real x)))
    (at x within X)"
   apply (simp add: circlepath_def scaleR_conv_of_real)
   apply (rule derivative_eq_intros)
   apply (simp add: algebra_simps)
   done
 
 corollary vector_derivative_circlepath:
    "vector_derivative (circlepath z r) (at x) =
-    2 * pi * ii * r * exp(2 * of_real pi * ii * x)"
+    2 * pi * \<i> * r * exp(2 * of_real pi * \<i> * x)"
 using has_vector_derivative_circlepath vector_derivative_at by blast
 
 corollary vector_derivative_circlepath01:
     "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
      \<Longrightarrow> vector_derivative (circlepath z r) (at x within {0..1}) =
-          2 * pi * ii * r * exp(2 * of_real pi * ii * x)"
+          2 * pi * \<i> * r * exp(2 * of_real pi * \<i> * x)"
   using has_vector_derivative_circlepath
   by (auto simp: vector_derivative_at_within_ivl)
 
 lemma valid_path_circlepath [simp]: "valid_path (circlepath z r)"
   by (simp add: circlepath_def)

 
 text\<open> Hence the Cauchy formula for points inside a circle.\<close>
 
 theorem Cauchy_integral_circlepath:
   assumes "continuous_on (cball z r) f" "f holomorphic_on (ball z r)" "norm(w - z) < r"
-  shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w))
+  shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * \<i> * f w))
          (circlepath z r)"
 proof -
   have "r > 0"
     using assms le_less_trans norm_ge_zero by blast
   have "((\<lambda>u. f u / (u - w)) has_contour_integral (2 * pi) * \<i> * winding_number (circlepath z r) w * f w)

     by (simp add: winding_number_circlepath assms)
 qed
 
 corollary Cauchy_integral_circlepath_simple:
   assumes "f holomorphic_on cball z r" "norm(w - z) < r"
-  shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w))
+  shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * \<i> * f w))
          (circlepath z r)"
 using assms by (force simp: holomorphic_on_imp_continuous_on holomorphic_on_subset Cauchy_integral_circlepath)
 
 
 lemma no_bounded_connected_component_imp_winding_number_zero:

   assumes contf: "continuous_on (cball z r) f"
       and holf: "f holomorphic_on ball z r"
       and w: "w \<in> ball z r"
     shows "(\<lambda>u. f u/(u - w)^2) contour_integrable_on (circlepath z r)"
            (is "?thes1")
-      and "(f has_field_derivative (1 / (2 * of_real pi * ii) * contour_integral(circlepath z r) (\<lambda>u. f u / (u - w)^2))) (at w)"
+      and "(f has_field_derivative (1 / (2 * of_real pi * \<i>) * contour_integral(circlepath z r) (\<lambda>u. f u / (u - w)^2))) (at w)"
            (is "?thes2")
 proof -
   have [simp]: "r \<ge> 0" using w
     using ball_eq_empty by fastforce
   have f: "continuous_on (path_image (circlepath z r)) f"
     by (rule continuous_on_subset [OF contf]) (force simp add: cball_def sphere_def)
   have int: "\<And>w. dist z w < r \<Longrightarrow>
-                 ((\<lambda>u. f u / (u - w)) has_contour_integral (\<lambda>x. 2 * of_real pi * ii * f x) w) (circlepath z r)"
+                 ((\<lambda>u. f u / (u - w)) has_contour_integral (\<lambda>x. 2 * of_real pi * \<i> * f x) w) (circlepath z r)"
     by (rule Cauchy_integral_circlepath [OF contf holf]) (simp add: dist_norm norm_minus_commute)
   show ?thes1
     apply (simp add: power2_eq_square)
     apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1, simplified])
     apply (blast intro: int)
     done
   have "((\<lambda>x. 2 * of_real pi * \<i> * f x) has_field_derivative contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)^2)) (at w)"
     apply (simp add: power2_eq_square)
-    apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\<lambda>x. 2 * of_real pi * ii * f x", simplified])
+    apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\<lambda>x. 2 * of_real pi * \<i> * f x", simplified])
     apply (blast intro: int)
     done
   then have fder: "(f has_field_derivative contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)^2) / (2 * of_real pi * \<i>)) (at w)"
     by (rule DERIV_cdivide [where f = "\<lambda>x. 2 * of_real pi * \<i> * f x" and c = "2 * of_real pi * \<i>", simplified])
   show ?thes2

     then have holf_cball: "f holomorphic_on cball z r"
       apply (simp add: holomorphic_on_def)
       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)"
+    then have contfpi: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1/(2 * of_real pi*\<i>) * f x)"
       by (auto intro: continuous_intros)+
     have contf_cball: "continuous_on (cball z r) f" using holf_cball
       by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset)
     have holf_ball: "f holomorphic_on ball z r" using holf_cball
       using ball_subset_cball holomorphic_on_subset by blast

 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 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>"
+      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * 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] field_differentiable_def)
   using no_isolated_singularity [where s = "interior s"]
   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)

 
 proposition Cauchy_has_contour_integral_higher_derivative_circlepath:
   assumes contf: "continuous_on (cball z r) f"
       and holf: "f holomorphic_on ball z r"
       and w: "w \<in> ball z r"
-    shows "((\<lambda>u. f u / (u - w) ^ (Suc k)) has_contour_integral ((2 * pi * ii) / (fact k) * (deriv ^^ k) f w))
+    shows "((\<lambda>u. f u / (u - w) ^ (Suc k)) has_contour_integral ((2 * pi * \<i>) / (fact k) * (deriv ^^ k) f w))
            (circlepath z r)"
 using w
 proof (induction k arbitrary: w)
   case 0 then show ?case
     using assms by (auto simp: Cauchy_integral_circlepath dist_commute dist_norm)

   assumes contf: "continuous_on (cball z r) f"
       and holf: "f holomorphic_on ball z r"
       and w: "w \<in> ball z r"
     shows "(\<lambda>u. f u / (u - w)^(Suc k)) contour_integrable_on (circlepath z r)"
            (is "?thes1")
-      and "(deriv ^^ k) f w = (fact k) / (2 * pi * ii) * contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k))"
+      and "(deriv ^^ k) f w = (fact k) / (2 * pi * \<i>) * contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k))"
            (is "?thes2")
 proof -
   have *: "((\<lambda>u. f u / (u - w) ^ Suc k) has_contour_integral (2 * pi) * \<i> / (fact k) * (deriv ^^ k) f w)
            (circlepath z r)"
     using Cauchy_has_contour_integral_higher_derivative_circlepath [OF assms]

     unfolding contour_integral_unique [OF *] by (simp add: divide_simps)
 qed
 
 corollary Cauchy_contour_integral_circlepath:
   assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \<in> ball z r"
-    shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k)) = (2 * pi * ii) * (deriv ^^ k) f w / (fact k)"
+    shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k)) = (2 * pi * \<i>) * (deriv ^^ k) f w / (fact k)"
 by (simp add: Cauchy_higher_derivative_integral_circlepath [OF assms])
 
 corollary Cauchy_contour_integral_circlepath_2:
   assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \<in> ball z r"
-    shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^2) = (2 * pi * ii) * deriv f w"
+    shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^2) = (2 * pi * \<i>) * deriv f w"
   using Cauchy_contour_integral_circlepath [OF assms, of 1]
   by (simp add: power2_eq_square)
 
 
 subsection\<open>A holomorphic function is analytic, i.e. has local power series.\<close>

     apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf])
     using \<open>0 < r\<close>
     apply auto
     done
   then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
-             sums (2 * of_real pi * ii * f w)"
+             sums (2 * of_real pi * \<i> * f w)"
     using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]])
   then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2)))
-            sums ((2 * of_real pi * ii * f w) / (\<i> * (complex_of_real pi * 2)))"
+            sums ((2 * of_real pi * \<i> * f w) / (\<i> * (complex_of_real pi * 2)))"
     by (rule sums_divide)
   then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2)))
             sums f w"
     by (simp add: field_simps)
   then show ?thesis

       done
     have g_cint: "(\<lambda>u. g u/(u - w)) contour_integrable_on circlepath z r"
       by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
     have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) \<longlongrightarrow> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
       by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
-    have f_tends_cig: "((\<lambda>n. 2 * of_real pi * ii * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
+    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"
       apply (rule Lim_transform_eventually [where f = "\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. f n u/(u - w))"])
       apply (rule eventually_mono [OF cont])
       apply (rule contour_integral_unique [OF Cauchy_integral_circlepath])
       using w
       apply (auto simp: norm_minus_commute dist_norm cif_tends_cig)

 lemma Cauchy_integral_formula_global_weak:
     assumes u: "open u" and holf: "f holomorphic_on u"
         and z: "z \<in> u" and \<gamma>: "polynomial_function \<gamma>"
         and pasz: "path_image \<gamma> \<subseteq> u - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
         and zero: "\<And>w. w \<notin> u \<Longrightarrow> winding_number \<gamma> w = 0"
-      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
 proof -
   obtain \<gamma>' where pf\<gamma>': "polynomial_function \<gamma>'" and \<gamma>': "\<And>x. (\<gamma> has_vector_derivative (\<gamma>' x)) (at x)"
     using has_vector_derivative_polynomial_function [OF \<gamma>] by blast
   then have "bounded(path_image \<gamma>')"
     by (simp add: path_image_def compact_imp_bounded compact_continuous_image continuous_on_polymonial_function)

 theorem Cauchy_integral_formula_global:
     assumes s: "open s" and holf: "f holomorphic_on s"
         and z: "z \<in> s" and vpg: "valid_path \<gamma>"
         and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
         and zero: "\<And>w. w \<notin> s \<Longrightarrow> winding_number \<gamma> w = 0"
-      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
 proof -
   have "path \<gamma>" using vpg by (blast intro: valid_path_imp_path)
   have hols: "(\<lambda>w. f w / (w - z)) holomorphic_on s - {z}" "(\<lambda>w. 1 / (w - z)) holomorphic_on s - {z}"
     by (rule holomorphic_intros holomorphic_on_subset [OF holf] | force)+
   then have cint_fw: "(\<lambda>w. f w / (w - z)) contour_integrable_on \<gamma>"