# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1711632777 0
# Node ID 35b2143aeec6234a36fc7d871a16dc88215a77ea
# Parent  19cc354ba62533a01b8d60549da984d716592544
An assortment of new material, mostly due to Manuel

diff -r 19cc354ba625 -r 35b2143aeec6 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Mar 28 13:32:57 2024 +0000
@@ -763,6 +763,10 @@
      (simp_all add: integral_linear[OF _ bounded_linear_cnj, symmetric]
                     o_def integrable_on_cnj_iff not_integrable_integral)
 
+lemma has_integral_cnj: "(cnj \<circ> f has_integral (cnj I)) A  = (f has_integral I) A"
+  unfolding has_integral_iff comp_def
+  by (metis integral_cnj complex_cnj_cancel_iff integrable_on_cnj_iff)
+
 lemma integral_component_eq[simp]:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes "f integrable_on S"
@@ -2395,6 +2399,12 @@
   shows "g integrable_on T"
   using assms has_integral_spike_finite by blast
 
+lemma integrable_spike_finite_eq:
+  assumes "finite S"
+    and "\<And>x. x \<in> T - S \<Longrightarrow> f x = g x"
+  shows "f integrable_on T \<longleftrightarrow> g integrable_on T"
+  by (metis assms integrable_spike_finite)
+
 lemma has_integral_bound_spike_finite:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "0 \<le> B" "finite S"
diff -r 19cc354ba625 -r 35b2143aeec6 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Thu Mar 28 13:32:57 2024 +0000
@@ -623,6 +623,15 @@
   by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
         pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
 
+lemma homotopic_paths_rid':
+  assumes "path p" "path_image p \<subseteq> s" "x = pathfinish p"
+  shows "homotopic_paths s (p +++ linepath x x) p"
+  using homotopic_paths_rid[of p s] assms by simp
+
+lemma homotopic_paths_lid':
+   "\<lbrakk>path p; path_image p \<subseteq> s; x = pathstart p\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath x x +++ p) p"
+  using homotopic_paths_lid[of p s] by simp
+
 proposition homotopic_paths_assoc:
    "\<lbrakk>path p; path_image p \<subseteq> S; path q; path_image q \<subseteq> S; path r; path_image r \<subseteq> S; pathfinish p = pathstart q;
      pathfinish q = pathstart r\<rbrakk>
diff -r 19cc354ba625 -r 35b2143aeec6 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Mar 28 13:32:57 2024 +0000
@@ -121,6 +121,20 @@
   using assms
   by (simp add: loop_free_linear_image_eq path_linear_image_eq simple_path_def)
 
+lemma simple_pathI [intro?]:
+  assumes "path p"
+  assumes "\<And>x y. 0 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> p x = p y \<Longrightarrow> x = 0 \<and> y = 1"
+  shows   "simple_path p"
+  unfolding simple_path_def loop_free_def
+proof (intro ballI conjI impI)
+  fix x y assume "x \<in> {0..1}" "y \<in> {0..1}" "p x = p y"
+  thus "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
+    by (metis assms(2) atLeastAtMost_iff linorder_less_linear)
+qed fact+
+
+lemma arcD: "arc p \<Longrightarrow> p x = p y \<Longrightarrow> x \<in> {0..1} \<Longrightarrow> y \<in> {0..1} \<Longrightarrow> x = y"
+  by (auto simp: arc_def inj_on_def)
+
 lemma arc_translation_eq:
   fixes g :: "real \<Rightarrow> 'a::euclidean_space"
   shows "arc((\<lambda>x. a + x) \<circ> g) \<longleftrightarrow> arc g"
@@ -670,6 +684,38 @@
   using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
 
 
+subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Symmetry and loops\<close>
+
+lemma path_sym:
+  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
+  by auto
+
+lemma simple_path_sym:
+  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
+     \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
+  by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)
+
+lemma path_image_sym:
+  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
+     \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
+  by (simp add: path_image_join sup_commute)
+
+lemma simple_path_joinI:
+  assumes "arc p1" "arc p2" "pathfinish p1 = pathstart p2"
+  assumes "path_image p1 \<inter> path_image p2 
+        \<subseteq> insert (pathstart p2) (if pathstart p1 = pathfinish p2 then {pathstart p1} else {})"
+  shows   "simple_path (p1 +++ p2)"
+  by (smt (verit, best) Int_commute arc_imp_simple_path arc_join assms insert_commute simple_path_join_loop simple_path_sym)
+
+lemma simple_path_join3I:
+  assumes "arc p1" "arc p2" "arc p3"
+  assumes "path_image p1 \<inter> path_image p2 \<subseteq> {pathstart p2}"
+  assumes "path_image p2 \<inter> path_image p3 \<subseteq> {pathstart p3}"
+  assumes "path_image p1 \<inter> path_image p3 \<subseteq> {pathstart p1} \<inter> {pathfinish p3}"
+  assumes "pathfinish p1 = pathstart p2" "pathfinish p2 = pathstart p3"
+  shows   "simple_path (p1 +++ p2 +++ p3)"
+  using assms by (intro simple_path_joinI arc_join) (auto simp: path_image_join)
+
 subsection\<^marker>\<open>tag unimportant\<close>\<open>The joining of paths is associative\<close>
 
 lemma path_assoc:
@@ -720,22 +766,6 @@
       \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
 by (simp add: arc_simple_path simple_path_assoc)
 
-subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Symmetry and loops\<close>
-
-lemma path_sym:
-  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
-  by auto
-
-lemma simple_path_sym:
-  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
-     \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
-  by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)
-
-lemma path_image_sym:
-  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
-     \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
-  by (simp add: path_image_join sup_commute)
-
 
 subsection\<open>Subpath\<close>
 
diff -r 19cc354ba625 -r 35b2143aeec6 src/HOL/Analysis/Smooth_Paths.thy
--- a/src/HOL/Analysis/Smooth_Paths.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Analysis/Smooth_Paths.thy	Thu Mar 28 13:32:57 2024 +0000
@@ -3,8 +3,7 @@
 *)
 section\<^marker>\<open>tag unimportant\<close> \<open>Smooth paths\<close>
 theory Smooth_Paths
-  imports
-  Retracts
+  imports Retracts
 begin
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close>
@@ -439,4 +438,97 @@
 lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)"
   by (simp add: Let_def rectpath_def)
 
+lemma linear_image_valid_path:
+  fixes p :: "real \<Rightarrow> 'a :: euclidean_space"
+  assumes  "valid_path p" "linear f"
+  shows    "valid_path (f \<circ> p)"
+  unfolding valid_path_def piecewise_C1_differentiable_on_def
+proof (intro conjI)
+  from assms have "path p"
+    by (simp add: valid_path_imp_path)
+  thus "continuous_on {0..1} (f \<circ> p)"
+    unfolding o_def path_def by (intro linear_continuous_on_compose[OF _ assms(2)])
+  from assms(1) obtain S where S: "finite S" "p C1_differentiable_on {0..1} - S"
+    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
+  from S(2) obtain p' :: "real \<Rightarrow> 'a"
+    where p': "\<And>x. x \<in> {0..1} - S \<Longrightarrow> (p has_vector_derivative p' x) (at x)"
+              "continuous_on ({0..1} - S) p'"
+    by (fastforce simp: C1_differentiable_on_def)
+
+  have "(f \<circ> p has_vector_derivative f (p' x)) (at x)" if "x \<in> {0..1} - S" for x
+    by (rule vector_derivative_diff_chain_within [OF p'(1)[OF that]]
+             linear_imp_has_derivative assms)+
+  moreover have "continuous_on ({0..1} - S) (\<lambda>x. f (p' x))"
+    by (rule linear_continuous_on_compose [OF p'(2) assms(2)])
+  ultimately have "f \<circ> p C1_differentiable_on {0..1} - S"
+    unfolding C1_differentiable_on_def by (intro exI[of _ "\<lambda>x. f (p' x)"]) fast
+  thus "\<exists>S. finite S \<and> f \<circ> p C1_differentiable_on {0..1} - S"
+    using \<open>finite S\<close> by blast
+qed
+
+lemma valid_path_times:
+  fixes \<gamma>::"real \<Rightarrow> 'a ::real_normed_field"
+  assumes "c\<noteq>0"
+  shows "valid_path ((*) c \<circ> \<gamma>) = valid_path \<gamma>"
+proof 
+  assume "valid_path ((*) c \<circ> \<gamma>)"
+  then have "valid_path ((*) (1/c) \<circ> ((*) c \<circ> \<gamma>))"
+    by (simp add: valid_path_compose)
+  then show "valid_path \<gamma>" 
+    unfolding comp_def using \<open>c\<noteq>0\<close> by auto
+next
+  assume "valid_path \<gamma>"
+  then show "valid_path ((*) c \<circ> \<gamma>)"
+    by (simp add: valid_path_compose)
+qed
+
+lemma path_compose_cnj_iff [simp]: "path (cnj \<circ> p) \<longleftrightarrow> path p"
+proof -
+  have "path (cnj \<circ> p)" if "path p" for p
+    by (intro path_continuous_image continuous_intros that)
+  from this[of p] and this[of "cnj \<circ> p"] show ?thesis
+    by (auto simp: o_def)
+qed
+
+lemma valid_path_cnj:
+  fixes g::"real \<Rightarrow> complex"
+    shows "valid_path (cnj \<circ> g) = valid_path g"
+proof
+  show valid:"valid_path (cnj \<circ> g)" if "valid_path g" for g
+  proof -
+    obtain S where "finite S" and g_diff: "g C1_differentiable_on {0..1} - S"
+      using \<open>valid_path g\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
+  
+    have g_diff':"g differentiable at t" when "t\<in>{0..1} - S" for t
+      by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - S\<close> that)
+    then have "(cnj \<circ> g) differentiable at t" when "t\<in>{0..1} - S" for t
+      using bounded_linear_cnj bounded_linear_imp_differentiable differentiable_chain_at that by blast
+    moreover have "continuous_on ({0..1} - S)
+        (\<lambda>x. vector_derivative (cnj \<circ> g) (at x))"
+    proof -
+      have "continuous_on ({0..1} - S)
+          (\<lambda>x. vector_derivative (cnj \<circ> g) (at x))
+        = continuous_on ({0..1} - S)
+          (\<lambda>x. cnj (vector_derivative g (at x)))"
+        apply (rule continuous_on_cong[OF refl])
+        unfolding comp_def using g_diff'
+        using has_vector_derivative_cnj vector_derivative_at vector_derivative_works by blast
+      also have "\<dots>"
+        apply (intro continuous_intros)
+        using C1_differentiable_on_eq g_diff by blast
+      finally show ?thesis .
+    qed
+    ultimately have "cnj \<circ> g C1_differentiable_on {0..1} - S"
+      using C1_differentiable_on_eq by blast
+    moreover have "path (cnj \<circ> g)"
+      apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
+      by (intro continuous_intros)
+    ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
+      using \<open>finite S\<close> by auto
+  qed
+  from this[of "cnj o g"]
+  show "valid_path (cnj \<circ> g) \<Longrightarrow> valid_path g"
+    unfolding comp_def by simp
+qed
+
 end
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)
diff -r 19cc354ba625 -r 35b2143aeec6 src/HOL/Complex_Analysis/Winding_Numbers.thy
--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy	Thu Mar 28 13:32:57 2024 +0000
@@ -87,6 +87,30 @@
     by simp
 qed
 
+lemma winding_number_prop_reversepath:
+  assumes "winding_number_prop \<gamma> z e p n"
+  shows   "winding_number_prop (reversepath \<gamma>) z e (reversepath p) (-n)"
+proof -
+  have p: "valid_path p" "z \<notin> path_image p" "pathstart p = pathstart \<gamma>"
+          "pathfinish p = pathfinish \<gamma>" "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (\<gamma> t - p t) < e"
+          "contour_integral p (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i> * n"
+    using assms by (auto simp: winding_number_prop_def)
+  show ?thesis
+    unfolding winding_number_prop_def
+  proof (intro conjI strip)
+    show "norm (reversepath \<gamma> t - reversepath p t) < e" if "t \<in> {0..1}" for t
+      unfolding reversepath_def using p(5)[of "1 - t"] that by auto
+    show "contour_integral (reversepath p) (\<lambda>w. 1 / (w - z)) =
+             complex_of_real (2 * pi) * \<i> * - n"
+      using p by (subst contour_integral_reversepath) auto
+  qed (use p in auto)
+qed
+
+lemma winding_number_prop_reversepath_iff:
+  "winding_number_prop (reversepath \<gamma>) z e p n \<longleftrightarrow> winding_number_prop \<gamma> z e (reversepath p) (-n)"
+  using winding_number_prop_reversepath[of "reversepath \<gamma>" z e p n]
+        winding_number_prop_reversepath[of \<gamma> z e "reversepath p" "-n"] by auto
+
 (*NB not winding_number_prop here due to the loop in p*)
 lemma winding_number_unique_loop:
   assumes \<gamma>: "path \<gamma>" "z \<notin> path_image \<gamma>"
@@ -274,6 +298,63 @@
     using assms by (simp add: winding_number_valid_path valid_path_negatepath image_def path_defs)
 qed
 
+lemma winding_number_cnj:
+  assumes "path \<gamma>" "z \<notin> path_image \<gamma>"
+  shows   "winding_number (cnj \<circ> \<gamma>) (cnj z) = -cnj (winding_number \<gamma> z)"
+proof (rule winding_number_unique)
+  show "\<exists>p. winding_number_prop (cnj \<circ> \<gamma>) (cnj z) e p (-cnj (winding_number \<gamma> z))"
+    if "e > 0" for e
+  proof -
+    from winding_number[OF assms(1,2) \<open>e > 0\<close>]
+    obtain p where "winding_number_prop \<gamma> z e p (winding_number \<gamma> z)"
+      by blast
+    then have p: "valid_path p" "z \<notin> path_image p"
+        "pathstart p = pathstart \<gamma>"
+        "pathfinish p = pathfinish \<gamma>"
+        "\<And>t. t \<in> {0..1} \<Longrightarrow> cmod (\<gamma> t - p t) < e" and
+        p_cont:"contour_integral p (\<lambda>w. 1 / (w - z)) =
+          complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z" 
+      unfolding winding_number_prop_def by auto
+    
+    have "valid_path (cnj \<circ> p)"
+      using p(1) by (subst valid_path_cnj) auto
+    moreover have "cnj z \<notin> path_image (cnj \<circ> p)"
+      using p(2) by (auto simp: path_image_def)
+    moreover have "pathstart (cnj \<circ> p) = pathstart (cnj \<circ> \<gamma>)" 
+      using p(3) by (simp add: pathstart_compose)
+    moreover have "pathfinish (cnj \<circ> p) = pathfinish (cnj \<circ> \<gamma>)" 
+      using p(4) by (simp add: pathfinish_compose)
+    moreover have "cmod ((cnj \<circ> \<gamma>) t - (cnj \<circ> p) t) < e"
+      if t: "t \<in> {0..1}" for t
+    proof -
+      have "(cnj \<circ> \<gamma>) t - (cnj \<circ> p) t = cnj (\<gamma> t - p t)"
+        by simp
+      also have "norm \<dots> = norm (\<gamma> t - p t)"
+        by (subst complex_mod_cnj) auto
+      also have "\<dots> < e"
+        using p(5)[OF t] by simp
+      finally show ?thesis .
+    qed
+    moreover have "contour_integral (cnj \<circ> p) (\<lambda>w. 1 / (w - cnj z)) =
+          cnj (complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z)" (is "?L=?R")
+    proof -
+      have "?L = contour_integral (cnj \<circ> p) (cnj \<circ> (\<lambda>w. 1 / (cnj w - z)))"
+        by (simp add: o_def)
+      also have "\<dots> = cnj (contour_integral p (\<lambda>x. 1 / (x - z)))"
+        using p(1) by (subst contour_integral_cnj) (auto simp: o_def)
+      also have "\<dots> = ?R"
+        using p_cont by simp
+      finally show ?thesis .
+    qed
+    ultimately show ?thesis
+      by (intro exI[of _ "cnj \<circ> p"]) (auto simp: winding_number_prop_def)
+  qed
+  show "path (cnj \<circ> \<gamma>)"
+    by (intro path_continuous_image continuous_intros) (use assms in auto)
+  show "cnj z \<notin> path_image (cnj \<circ> \<gamma>)"
+    using \<open>z \<notin> path_image \<gamma>\<close> unfolding path_image_def by auto
+qed
+
 text \<open>A combined theorem deducing several things piecewise.\<close>
 lemma winding_number_join_pos_combined:
      "\<lbrakk>valid_path \<gamma>1; z \<notin> path_image \<gamma>1; 0 < Re(winding_number \<gamma>1 z);
diff -r 19cc354ba625 -r 35b2143aeec6 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Transcendental.thy	Thu Mar 28 13:32:57 2024 +0000
@@ -2994,14 +2994,20 @@
     by (auto simp: powr_minus field_simps)
 qed
 
+lemma powr_mono': "a \<le> (b::real) \<Longrightarrow> x \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr b \<le> x powr a"
+  using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps)
+
 lemma powr_mono_both:
   fixes x :: real
   assumes "0 \<le> a" "a \<le> b" "1 \<le> x" "x \<le> y"
     shows "x powr a \<le> y powr b"
   by (meson assms order.trans powr_mono powr_mono2 zero_le_one)
 
-lemma powr_mono': "a \<le> (b::real) \<Longrightarrow> x \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr b \<le> x powr a"
-  using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps)
+lemma powr_mono_both':
+  fixes x :: real
+  assumes "a \<ge> b" "b\<ge>0" "0 < x" "x \<le> y" "y \<le> 1"
+    shows "x powr a \<le> y powr b"
+  by (meson assms nless_le order.trans powr_mono' powr_mono2)
 
 lemma powr_less_mono':
   assumes "(x::real) > 0" "x < 1" "a < b"