diff -r 19cc354ba625 -r 35b2143aeec6 src/HOL/Complex_Analysis/Contour_Integration.thy
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy	Thu Mar 28 13:32:57 2024 +0000
@@ -1278,6 +1278,80 @@
 lemma part_circlepath_cnj: "cnj (part_circlepath c r a b x) = part_circlepath (cnj c) r (-a) (-b) x"
   by (simp add: part_circlepath_def exp_cnj linepath_def algebra_simps)
 
+lemma contour_integrable_on_compose_cnj_iff:
+  assumes "valid_path \<gamma>"
+  shows   "f contour_integrable_on (cnj \<circ> \<gamma>) \<longleftrightarrow> (cnj \<circ> f \<circ> cnj) contour_integrable_on \<gamma>"
+proof -
+  from assms obtain S where S: "finite S" "\<gamma> C1_differentiable_on {0..1} - S"
+    unfolding valid_path_def piecewise_C1_differentiable_on_def by blast
+  have "f contour_integrable_on (cnj \<circ> \<gamma>) \<longleftrightarrow>
+        ((\<lambda>t. cnj (cnj (f (cnj (\<gamma> t))) * vector_derivative \<gamma> (at t))) integrable_on {0..1})"
+    unfolding contour_integrable_on o_def
+  proof (intro integrable_spike_finite_eq [OF S(1)])
+    fix t :: real assume "t \<in> {0..1} - S"
+    hence "\<gamma> differentiable at t"
+      using S(2) by (meson C1_differentiable_on_eq)
+    hence "vector_derivative (\<lambda>x. cnj (\<gamma> x)) (at t) = cnj (vector_derivative \<gamma> (at t))"
+      by (rule vector_derivative_cnj)
+    thus "f (cnj (\<gamma> t)) * vector_derivative (\<lambda>x. cnj (\<gamma> x)) (at t) =
+          cnj (cnj (f (cnj (\<gamma> t))) * vector_derivative \<gamma> (at t))"
+      by simp
+  qed
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. cnj (f (cnj (\<gamma> t))) * vector_derivative \<gamma> (at t)) integrable_on {0..1})"
+    by (rule integrable_on_cnj_iff)
+  also have "\<dots> \<longleftrightarrow> (cnj \<circ> f \<circ> cnj) contour_integrable_on \<gamma>"
+    by (simp add: contour_integrable_on o_def)
+  finally show ?thesis .
+qed
+
+lemma contour_integral_cnj:
+  assumes "valid_path \<gamma>"
+  shows   "contour_integral (cnj \<circ> \<gamma>) f = cnj (contour_integral \<gamma> (cnj \<circ> f \<circ> cnj))"
+proof -
+  from assms obtain S where S: "finite S" "\<gamma> C1_differentiable_on {0..1} - S"
+    unfolding valid_path_def piecewise_C1_differentiable_on_def by blast
+  have "contour_integral (cnj \<circ> \<gamma>) f =
+          integral {0..1} (\<lambda>t. cnj (cnj (f (cnj (\<gamma> t))) * vector_derivative \<gamma> (at t)))"
+    unfolding contour_integral_integral
+  proof (intro integral_spike)
+    fix t assume "t \<in> {0..1} - S"
+    hence "\<gamma> differentiable at t"
+      using S(2) by (meson C1_differentiable_on_eq)
+    hence "vector_derivative (\<lambda>x. cnj (\<gamma> x)) (at t) = cnj (vector_derivative \<gamma> (at t))"
+      by (rule vector_derivative_cnj)
+    thus "cnj (cnj (f (cnj (\<gamma> t))) * vector_derivative \<gamma> (at t)) =
+            f ((cnj \<circ> \<gamma>) t) * vector_derivative (cnj \<circ> \<gamma>) (at t)"
+      by (simp add: o_def)
+  qed (use S(1) in auto)
+  also have "\<dots> = cnj (integral {0..1} (\<lambda>t. cnj (f (cnj (\<gamma> t))) * vector_derivative \<gamma> (at t)))"
+    by (subst integral_cnj [symmetric]) auto
+  also have "\<dots> = cnj (contour_integral \<gamma> (cnj \<circ> f \<circ> cnj))"
+    by (simp add: contour_integral_integral)
+  finally show ?thesis .
+qed
+
+lemma contour_integral_negatepath:
+  assumes "valid_path \<gamma>"
+  shows   "contour_integral (uminus \<circ> \<gamma>) f = -(contour_integral \<gamma> (\<lambda>x. f (-x)))" (is "?lhs = ?rhs")
+proof (cases "f contour_integrable_on (uminus \<circ> \<gamma>)")
+  case True
+  hence *: "(f has_contour_integral ?lhs) (uminus \<circ> \<gamma>)"
+    using has_contour_integral_integral by blast
+  have "((\<lambda>z. f (-z)) has_contour_integral - contour_integral (uminus \<circ> \<gamma>) f)
+            (uminus \<circ> (uminus \<circ> \<gamma>))"
+    by (rule has_contour_integral_negatepath) (use * assms in auto)
+  hence "((\<lambda>x. f (-x)) has_contour_integral -?lhs) \<gamma>"
+    by (simp add: o_def)
+  thus ?thesis
+    by (simp add: contour_integral_unique)
+next
+  case False
+  hence "\<not>(\<lambda>z. f (- z)) contour_integrable_on \<gamma>"
+    using contour_integrable_negatepath[of \<gamma> f] assms by auto
+  with False show ?thesis
+    by (simp add: not_integrable_contour_integral)
+qed
+
 lemma contour_integral_bound_part_circlepath:
   assumes "f contour_integrable_on part_circlepath c r a b"
   assumes "B \<ge> 0" "r \<ge> 0" "\<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> norm (f x) \<le> B"
@@ -1687,12 +1761,11 @@
   { fix e::real
     assume "0 < e"
     then have "0 < e / (\<bar>B\<bar> + 1)" by simp
-    then have "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image \<gamma>. cmod (f n x - l x) < e / (\<bar>B\<bar> + 1)"
+    then have \<section>: "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image \<gamma>. cmod (f n x - l x) < e / (\<bar>B\<bar> + 1)"
       using ul_f [unfolded uniform_limit_iff dist_norm] by auto
-    with ev_fint
     obtain a where fga: "\<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f a (\<gamma> x) - l (\<gamma> x)) < e / (\<bar>B\<bar> + 1)"
                and inta: "(\<lambda>t. f a (\<gamma> t) * vector_derivative \<gamma> (at t)) integrable_on {0..1}"
-      using eventually_happens [OF eventually_conj]
+      using eventually_happens [OF eventually_conj [OF ev_fint \<section>]]
       by (fastforce simp: contour_integrable_on path_image_def)
     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)