--- 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"
--- 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>
--- 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>
--- 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
--- 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)
--- 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);
--- 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"