--- a/NEWS Mon Oct 26 23:42:01 2015 +0000
+++ b/NEWS Tue Oct 27 15:17:02 2015 +0000
@@ -459,8 +459,8 @@
less_eq_multiset_def
INCOMPATIBILITY
-* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's
-integral theorem, ported from HOL Light
+* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's
+integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
* Multivariate_Analysis: Added topological concepts such as connected components
and the inside or outside of a set.
--- a/src/HOL/Algebra/UnivPoly.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Algebra/UnivPoly.thy Tue Oct 27 15:17:02 2015 +0000
@@ -860,7 +860,7 @@
next
show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)"
by (simp add: deg_belowI lcoeff_nonzero_deg
- inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
+ inj_on_eq_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
qed
text\<open>The following lemma is later \emph{overwritten} by the most
--- a/src/HOL/Fun.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Fun.thy Tue Oct 27 15:17:02 2015 +0000
@@ -171,7 +171,7 @@
lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
by (simp add: inj_on_def)
-lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
+lemma inj_on_eq_iff: "\<lbrakk>inj_on f A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y)"
by (force simp add: inj_on_def)
lemma inj_on_cong:
@@ -217,9 +217,6 @@
lemma inj_onD: "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"
by (unfold inj_on_def, blast)
-lemma inj_on_iff: "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"
- by (fact inj_on_eq_iff)
-
lemma comp_inj_on:
"[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A"
by (simp add: comp_def inj_on_def)
@@ -498,6 +495,10 @@
lemma inj_on_image_mem_iff: "\<lbrakk>inj_on f B; a \<in> B; A \<subseteq> B\<rbrakk> \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
by (auto simp: inj_on_def)
+(*FIXME DELETE*)
+lemma inj_on_image_mem_iff_alt: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f`A \<Longrightarrow> a \<in> B \<Longrightarrow> a \<in> A"
+ by (blast dest: inj_onD)
+
lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
by (blast dest: injD)
--- a/src/HOL/Induct/QuoDataType.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Induct/QuoDataType.thy Tue Oct 27 15:17:02 2015 +0000
@@ -168,7 +168,7 @@
done
text\<open>Reduces equality on abstractions to equality on representatives\<close>
-declare inj_on_Abs_Msg [THEN inj_on_iff, simp]
+declare inj_on_Abs_Msg [THEN inj_on_eq_iff, simp]
declare Abs_Msg_inverse [simp]
--- a/src/HOL/Induct/QuoNestedDataType.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Induct/QuoNestedDataType.thy Tue Oct 27 15:17:02 2015 +0000
@@ -185,7 +185,7 @@
done
text\<open>Reduces equality on abstractions to equality on representatives\<close>
-declare inj_on_Abs_Exp [THEN inj_on_iff, simp]
+declare inj_on_Abs_Exp [THEN inj_on_eq_iff, simp]
declare Abs_Exp_inverse [simp]
--- a/src/HOL/Library/Convex.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Library/Convex.thy Tue Oct 27 15:17:02 2015 +0000
@@ -48,6 +48,14 @@
shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
using assms unfolding convex_alt by auto
+lemma mem_convex_alt:
+ assumes "convex S" "x \<in> S" "y \<in> S" "u \<ge> 0" "v \<ge> 0" "u + v > 0"
+ shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) \<in> S"
+ apply (rule convexD)
+ using assms
+ apply (simp_all add: zero_le_divide_iff add_divide_distrib [symmetric])
+ done
+
lemma convex_empty[intro,simp]: "convex {}"
unfolding convex_def by simp
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Oct 27 15:17:02 2015 +0000
@@ -326,20 +326,20 @@
qed
lemma upd_inj: "i < n \<Longrightarrow> j < n \<Longrightarrow> upd i = upd j \<longleftrightarrow> i = j"
- using upd by (auto simp: bij_betw_def inj_on_iff)
+ using upd by (auto simp: bij_betw_def inj_on_eq_iff)
lemma upd_surj: "upd ` {..< n} = {..< n}"
using upd by (auto simp: bij_betw_def)
lemma in_upd_image: "A \<subseteq> {..< n} \<Longrightarrow> i < n \<Longrightarrow> upd i \<in> upd ` A \<longleftrightarrow> i \<in> A"
- using inj_on_image_mem_iff[of upd "{..< n}" A i ] upd
+ using inj_on_image_mem_iff[of upd "{..< n}"] upd
by (auto simp: bij_betw_def)
lemma enum_inj: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i = enum j \<longleftrightarrow> i = j"
- using inj_enum by (auto simp: inj_on_iff)
+ using inj_enum by (auto simp: inj_on_eq_iff)
lemma in_enum_image: "A \<subseteq> {.. n} \<Longrightarrow> i \<le> n \<Longrightarrow> enum i \<in> enum ` A \<longleftrightarrow> i \<in> A"
- using inj_on_image_mem_iff[OF inj_enum, of A i] by auto
+ using inj_on_image_mem_iff[OF inj_enum] by auto
lemma enum_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i \<le> enum j \<longleftrightarrow> i \<le> j"
by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Oct 27 15:17:02 2015 +0000
@@ -3167,4 +3167,1259 @@
by (force simp: L path_integral_integral)
qed
+subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
+
+text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
+
+lemma continuous_disconnected_range_constant:
+ assumes s: "connected s"
+ and conf: "continuous_on s f"
+ and fim: "f ` s \<subseteq> t"
+ and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
+ shows "\<exists>a. \<forall>x \<in> s. f x = a"
+proof (cases "s = {}")
+ case True then show ?thesis by force
+next
+ case False
+ { fix x assume "x \<in> s"
+ then have "f ` s \<subseteq> {f x}"
+ by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
+ }
+ with False show ?thesis
+ by blast
+qed
+
+lemma discrete_subset_disconnected:
+ fixes s :: "'a::topological_space set"
+ fixes t :: "'b::real_normed_vector set"
+ assumes conf: "continuous_on s f"
+ and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
+ shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
+proof -
+ { fix x assume x: "x \<in> s"
+ then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
+ using conf no [OF x] by auto
+ then have e2: "0 \<le> e / 2"
+ by simp
+ have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
+ apply (rule ccontr)
+ using connected_closed [of "connected_component_set (f ` s) (f x)"] `e>0`
+ apply (simp add: del: ex_simps)
+ apply (drule spec [where x="cball (f x) (e / 2)"])
+ apply (drule spec [where x="- ball(f x) e"])
+ apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
+ apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
+ using centre_in_cball connected_component_refl_eq e2 x apply blast
+ using ccs
+ apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF `y \<in> s`])
+ done
+ moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
+ by (auto simp: connected_component_in)
+ ultimately have "connected_component_set (f ` s) (f x) = {f x}"
+ by (auto simp: x)
+ }
+ with assms show ?thesis
+ by blast
+qed
+
+lemma finite_implies_discrete:
+ fixes s :: "'a::topological_space set"
+ assumes "finite (f ` s)"
+ shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
+proof -
+ have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
+ proof (cases "f ` s - {f x} = {}")
+ case True
+ with zero_less_numeral show ?thesis
+ by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
+ next
+ case False
+ then obtain z where z: "z \<in> s" "f z \<noteq> f x"
+ by blast
+ have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
+ using assms by simp
+ then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
+ apply (rule finite_imp_less_Inf)
+ using z apply force+
+ done
+ show ?thesis
+ by (force intro!: * cInf_le_finite [OF finn])
+ qed
+ with assms show ?thesis
+ by blast
+qed
+
+text\<open>This proof requires the existence of two separate values of the range type.\<close>
+lemma finite_range_constant_imp_connected:
+ assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+ \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
+ shows "connected s"
+proof -
+ { fix t u
+ assume clt: "closedin (subtopology euclidean s) t"
+ and clu: "closedin (subtopology euclidean s) u"
+ and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
+ have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
+ apply (subst tus [symmetric])
+ apply (rule continuous_on_cases_local)
+ using clt clu tue
+ apply (auto simp: tus continuous_on_const)
+ done
+ have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
+ by (rule finite_subset [of _ "{0,1}"]) auto
+ have "t = {} \<or> u = {}"
+ using assms [OF conif fi] tus [symmetric]
+ by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
+ }
+ then show ?thesis
+ by (simp add: connected_closed_in_eq)
+qed
+
+lemma continuous_disconnected_range_constant_eq:
+ "(connected s \<longleftrightarrow>
+ (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+ \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
+ \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
+ and continuous_discrete_range_constant_eq:
+ "(connected s \<longleftrightarrow>
+ (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+ continuous_on s f \<and>
+ (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
+ \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
+ and continuous_finite_range_constant_eq:
+ "(connected s \<longleftrightarrow>
+ (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+ continuous_on s f \<and> finite (f ` s)
+ \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
+proof -
+ have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
+ \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
+ by blast
+ have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
+ apply (rule *)
+ using continuous_disconnected_range_constant apply metis
+ apply clarify
+ apply (frule discrete_subset_disconnected; blast)
+ apply (blast dest: finite_implies_discrete)
+ apply (blast intro!: finite_range_constant_imp_connected)
+ done
+ then show ?thesis1 ?thesis2 ?thesis3
+ by blast+
+qed
+
+lemma continuous_discrete_range_constant:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
+ assumes s: "connected s"
+ and "continuous_on s f"
+ and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
+ shows "\<exists>a. \<forall>x \<in> s. f x = a"
+ using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
+ by blast
+
+lemma continuous_finite_range_constant:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
+ assumes "connected s"
+ and "continuous_on s f"
+ and "finite (f ` s)"
+ shows "\<exists>a. \<forall>x \<in> s. f x = a"
+ using assms continuous_finite_range_constant_eq
+ by blast
+
+
+text\<open>We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.\<close>
+
+subsection\<open>Winding Numbers\<close>
+
+text\<open>The result is an integer, but it doesn't have type @{typ int}!\<close>
+definition winding_number:: "[real \<Rightarrow> complex, complex] \<Rightarrow> complex" where
+ "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>
+ path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * 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>
+ path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * winding_number \<gamma> z"
+proof -
+ have "path_image \<gamma> \<subseteq> UNIV - {z}"
+ using assms by blast
+ then obtain d
+ where d: "d>0"
+ and pi_eq: "\<And>h1 h2. valid_path h1 \<and> valid_path h2 \<and>
+ (\<forall>t\<in>{0..1}. cmod (h1 t - \<gamma> t) < d \<and> cmod (h2 t - \<gamma> t) < d) \<and>
+ pathstart h2 = pathstart h1 \<and> pathfinish h2 = pathfinish h1 \<longrightarrow>
+ path_image h1 \<subseteq> UNIV - {z} \<and> path_image h2 \<subseteq> UNIV - {z} \<and>
+ (\<forall>f. f holomorphic_on UNIV - {z} \<longrightarrow> path_integral h2 f = path_integral h1 f)"
+ using path_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 `path \<gamma>`, of "d/2"] d by auto
+ def nn \<equiv> "1/(2* pi*ii) * path_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>
+ path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * 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>
+ pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and> (\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < min e (d / 2))"
+ using path_approx_polynomial_function [OF `path \<gamma>`, of "min e (d/2)"] d `0<e` by auto
+ have "(\<lambda>w. 1 / (w - z)) holomorphic_on UNIV - {z}"
+ by (auto simp: intro!: holomorphic_intros)
+ then show "?PP e nn"
+ apply (rule_tac x=p in exI)
+ using pi_eq [of h p] h p d
+ apply (auto simp: valid_path_polynomial_function norm_minus_commute nn_def)
+ done
+ qed
+ then show ?thesis
+ unfolding winding_number_def
+ apply (rule someI2_ex)
+ apply (blast intro: `0<e`)
+ done
+qed
+
+lemma winding_number_unique:
+ 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>
+ path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+ shows "winding_number \<gamma> z = n"
+proof -
+ have "path_image \<gamma> \<subseteq> UNIV - {z}"
+ using assms by blast
+ then obtain e
+ where e: "e>0"
+ and pi_eq: "\<And>h1 h2 f. \<lbrakk>valid_path h1; valid_path h2;
+ (\<forall>t\<in>{0..1}. cmod (h1 t - \<gamma> t) < e \<and> cmod (h2 t - \<gamma> t) < e);
+ pathstart h2 = pathstart h1; pathfinish h2 = pathfinish h1; f holomorphic_on UNIV - {z}\<rbrakk> \<Longrightarrow>
+ path_integral h2 f = path_integral h1 f"
+ using path_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>
+ path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * 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> path_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
+ using winding_number [OF \<gamma> e] by blast
+ have "2 * complex_of_real pi * \<i> * n = path_integral p (\<lambda>w. 1 / (w - z))"
+ using p by auto
+ also have "... = path_integral q (\<lambda>w. 1 / (w - z))"
+ apply (rule pi_eq)
+ using p q
+ by (auto simp: valid_path_polynomial_function norm_minus_commute intro!: holomorphic_intros)
+ also have "... = 2 * complex_of_real pi * \<i> * winding_number \<gamma> z"
+ using q by auto
+ finally have "2 * complex_of_real pi * \<i> * n = 2 * complex_of_real pi * \<i> * winding_number \<gamma> z" .
+ then show ?thesis
+ by simp
+qed
+
+lemma winding_number_unique_loop:
+ assumes \<gamma>: "path \<gamma>" "z \<notin> path_image \<gamma>"
+ 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>
+ path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+ shows "winding_number \<gamma> z = n"
+proof -
+ have "path_image \<gamma> \<subseteq> UNIV - {z}"
+ using assms by blast
+ then obtain e
+ where e: "e>0"
+ and pi_eq: "\<And>h1 h2 f. \<lbrakk>valid_path h1; valid_path h2;
+ (\<forall>t\<in>{0..1}. cmod (h1 t - \<gamma> t) < e \<and> cmod (h2 t - \<gamma> t) < e);
+ pathfinish h1 = pathstart h1; pathfinish h2 = pathstart h2; f holomorphic_on UNIV - {z}\<rbrakk> \<Longrightarrow>
+ path_integral h2 f = path_integral h1 f"
+ using path_integral_nearby_loop [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>
+ path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * 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> path_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
+ using winding_number [OF \<gamma> e] by blast
+ have "2 * complex_of_real pi * \<i> * n = path_integral p (\<lambda>w. 1 / (w - z))"
+ using p by auto
+ also have "... = path_integral q (\<lambda>w. 1 / (w - z))"
+ apply (rule pi_eq)
+ using p q loop
+ by (auto simp: valid_path_polynomial_function norm_minus_commute intro!: holomorphic_intros)
+ also have "... = 2 * complex_of_real pi * \<i> * winding_number \<gamma> z"
+ using q by auto
+ finally have "2 * complex_of_real pi * \<i> * n = 2 * complex_of_real pi * \<i> * winding_number \<gamma> z" .
+ then show ?thesis
+ 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) * path_integral \<gamma> (\<lambda>w. 1/(w - z))"
+ using assms by (auto simp: valid_path_imp_path intro!: winding_number_unique)
+
+lemma has_path_integral_winding_number:
+ assumes \<gamma>: "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
+ shows "((\<lambda>w. 1/(w - z)) has_path_integral (2*pi*ii*winding_number \<gamma> z)) \<gamma>"
+by (simp add: winding_number_valid_path has_path_integral_integral path_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)
+
+lemma winding_number_subpath_trivial [simp]: "z \<noteq> g x \<Longrightarrow> winding_number (subpath x x g) z = 0"
+ by (simp add: winding_number_valid_path)
+
+lemma winding_number_join:
+ assumes g1: "path g1" "z \<notin> path_image g1"
+ and g2: "path g2" "z \<notin> path_image g2"
+ and "pathfinish g1 = pathstart g2"
+ shows "winding_number(g1 +++ g2) z = winding_number g1 z + winding_number g2 z"
+ apply (rule winding_number_unique)
+ using assms apply (simp_all add: not_in_path_image_join)
+ apply (frule winding_number [OF g2])
+ apply (frule winding_number [OF g1], clarify)
+ apply (rename_tac p2 p1)
+ apply (rule_tac x="p1+++p2" in exI)
+ apply (simp add: not_in_path_image_join path_integrable_inversediff algebra_simps)
+ apply (auto simp: joinpaths_def)
+ done
+
+lemma winding_number_reversepath:
+ assumes "path \<gamma>" "z \<notin> path_image \<gamma>"
+ shows "winding_number(reversepath \<gamma>) z = - (winding_number \<gamma> z)"
+ apply (rule winding_number_unique)
+ using assms
+ apply simp_all
+ apply (frule winding_number [OF assms], clarify)
+ apply (rule_tac x="reversepath p" in exI)
+ apply (simp add: path_integral_reversepath path_integrable_inversediff valid_path_imp_reverse)
+ apply (auto simp: reversepath_def)
+ done
+
+lemma winding_number_shiftpath:
+ assumes \<gamma>: "path \<gamma>" "z \<notin> path_image \<gamma>"
+ and "pathfinish \<gamma> = pathstart \<gamma>" "a \<in> {0..1}"
+ shows "winding_number(shiftpath a \<gamma>) z = winding_number \<gamma> z"
+ apply (rule winding_number_unique_loop)
+ using assms
+ apply (simp_all add: path_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath)
+ apply (frule winding_number [OF \<gamma>], clarify)
+ apply (rule_tac x="shiftpath a p" in exI)
+ apply (simp add: path_integral_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath valid_path_shiftpath)
+ apply (auto simp: shiftpath_def)
+ done
+
+lemma winding_number_split_linepath:
+ assumes "c \<in> closed_segment a b" "z \<notin> closed_segment a b"
+ shows "winding_number(linepath a b) z = winding_number(linepath a c) z + winding_number(linepath c b) z"
+proof -
+ have "z \<notin> closed_segment a c" "z \<notin> closed_segment c b"
+ using assms apply (meson convex_contains_segment convex_segment ends_in_segment(1) subsetCE)
+ using assms by (meson convex_contains_segment convex_segment ends_in_segment(2) subsetCE)
+ then show ?thesis
+ using assms
+ by (simp add: winding_number_valid_path path_integral_split_linepath [symmetric] continuous_on_inversediff field_simps)
+qed
+
+lemma winding_number_cong:
+ "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p t = q t) \<Longrightarrow> winding_number p z = winding_number q z"
+ by (simp add: winding_number_def pathstart_def pathfinish_def)
+
+lemma winding_number_offset: "winding_number p z = winding_number (\<lambda>w. p w - z) 0"
+ apply (simp add: winding_number_def path_integral_integral path_image_def valid_path_def pathstart_def pathfinish_def)
+ apply (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe)
+ apply (rename_tac g)
+ apply (rule_tac x="\<lambda>t. g t - z" in exI)
+ apply (force simp: vector_derivative_def has_vector_derivative_diff_const piecewise_C1_differentiable_diff C1_differentiable_imp_piecewise)
+ apply (rename_tac g)
+ apply (rule_tac x="\<lambda>t. g t + z" in exI)
+ apply (simp add: piecewise_C1_differentiable_add vector_derivative_def has_vector_derivative_add_const C1_differentiable_imp_piecewise)
+ apply (force simp: algebra_simps)
+ done
+
+(* A combined theorem deducing several things piecewise.*)
+lemma winding_number_join_pos_combined:
+ "\<lbrakk>valid_path \<gamma>1; z \<notin> path_image \<gamma>1; 0 < Re(winding_number \<gamma>1 z);
+ valid_path \<gamma>2; z \<notin> path_image \<gamma>2; 0 < Re(winding_number \<gamma>2 z); pathfinish \<gamma>1 = pathstart \<gamma>2\<rbrakk>
+ \<Longrightarrow> valid_path(\<gamma>1 +++ \<gamma>2) \<and> z \<notin> path_image(\<gamma>1 +++ \<gamma>2) \<and> 0 < Re(winding_number(\<gamma>1 +++ \<gamma>2) z)"
+ by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path)
+
+
+(* Useful sufficient conditions for the winding number to be positive etc.*)
+
+lemma Re_winding_number:
+ "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>\<rbrakk>
+ \<Longrightarrow> Re(winding_number \<gamma> z) = Im(path_integral \<gamma> (\<lambda>w. 1/(w - z))) / (2*pi)"
+by (simp add: winding_number_valid_path field_simps Re_divide power2_eq_square)
+
+lemma winding_number_pos_le:
+ assumes \<gamma>: "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
+ and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> 0 \<le> Im (vector_derivative \<gamma> (at x) * cnj(\<gamma> x - z))"
+ shows "0 \<le> Re(winding_number \<gamma> z)"
+proof -
+ 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}
+ 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
+ apply (simp only: box_real)
+ apply (subst has_path_integral [symmetric])
+ using \<gamma>
+ apply (simp add: path_integrable_inversediff has_path_integral_integral)
+ done
+qed
+
+lemma winding_number_pos_lt_lemma:
+ assumes \<gamma>: "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
+ and e: "0 < e"
+ 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 (path_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"
+ "path_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])
+ apply simp
+ apply (subst has_path_integral [symmetric])
+ using \<gamma>
+ apply (simp_all add: path_integrable_inversediff has_path_integral_integral ge)
+ done
+ with e show ?thesis
+ by (simp add: Re_winding_number [OF \<gamma>] field_simps)
+qed
+
+lemma winding_number_pos_lt:
+ assumes \<gamma>: "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
+ and e: "0 < e"
+ and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> e \<le> Im (vector_derivative \<gamma> (at x) * cnj(\<gamma> x - z))"
+ shows "0 < Re (winding_number \<gamma> z)"
+proof -
+ have bm: "bounded ((\<lambda>w. w - z) ` (path_image \<gamma>))"
+ using bounded_translation [of _ "-z"] \<gamma> by (simp add: bounded_valid_path_image)
+ then obtain B where B: "B > 0" and Bno: "\<And>x. x \<in> (\<lambda>w. w - z) ` (path_image \<gamma>) \<Longrightarrow> norm x \<le> B"
+ using bounded_pos [THEN iffD1, OF bm] by blast
+ { fix x::real assume x: "0 < x" "x < 1"
+ then have B2: "cmod (\<gamma> x - z)^2 \<le> B^2" using Bno [of "\<gamma> x - z"]
+ by (simp add: path_image_def power2_eq_square mult_mono')
+ with x have "\<gamma> x \<noteq> z" using \<gamma>
+ using path_image_def by fastforce
+ then have "e / B\<^sup>2 \<le> Im (vector_derivative \<gamma> (at x) * cnj (\<gamma> x - z)) / (cmod (\<gamma> x - z))\<^sup>2"
+ using B ge [OF x] B2 e
+ apply (rule_tac y="e / (cmod (\<gamma> x - z))\<^sup>2" in order_trans)
+ apply (auto simp: divide_left_mono divide_right_mono)
+ done
+ then have "e / B\<^sup>2 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
+ by (simp add: Im_divide_Reals complex_div_cnj [of _ "\<gamma> x - z" for x] del: complex_cnj_diff times_complex.sel)
+ } note * = this
+ show ?thesis
+ using e B by (simp add: * winding_number_pos_lt_lemma [OF \<gamma>, of "e/B^2"])
+qed
+
+subsection\<open>The winding number is an integer\<close>
+
+text\<open>Proof from the book Complex Analysis by Lars V. Ahlfors, Chapter 4, section 2.1,
+ Also on page 134 of Serge Lang's book with the name title, etc.\<close>
+
+lemma exp_fg:
+ fixes z::complex
+ assumes g: "(g has_vector_derivative g') (at x within s)"
+ and f: "(f has_vector_derivative (g' / (g x - z))) (at x within s)"
+ and z: "g x \<noteq> z"
+ shows "((\<lambda>x. exp(-f x) * (g x - z)) has_vector_derivative 0) (at x within s)"
+proof -
+ have *: "(exp o (\<lambda>x. (- f x)) has_vector_derivative - (g' / (g x - z)) * exp (- f x)) (at x within s)"
+ using assms unfolding has_vector_derivative_def scaleR_conv_of_real
+ by (auto intro!: derivative_eq_intros)
+ show ?thesis
+ apply (rule has_vector_derivative_eq_rhs)
+ apply (rule bounded_bilinear.has_vector_derivative [OF bounded_bilinear_mult])
+ using z
+ apply (auto simp: intro!: derivative_eq_intros * [unfolded o_def] g)
+ done
+qed
+
+lemma winding_number_exp_integral:
+ fixes z::complex
+ assumes \<gamma>: "\<gamma> piecewise_C1_differentiable_on {a..b}"
+ and ab: "a \<le> b"
+ and z: "z \<notin> \<gamma> ` {a..b}"
+ shows "(\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)) integrable_on {a..b}"
+ (is "?thesis1")
+ "exp (- (integral {a..b} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))) * (\<gamma> b - z) = \<gamma> a - z"
+ (is "?thesis2")
+proof -
+ let ?D\<gamma> = "\<lambda>x. vector_derivative \<gamma> (at x)"
+ have [simp]: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<gamma> x \<noteq> z"
+ using z by force
+ have cong: "continuous_on {a..b} \<gamma>"
+ using \<gamma> by (simp add: piecewise_C1_differentiable_on_def)
+ obtain k where fink: "finite k" and g_C1_diff: "\<gamma> C1_differentiable_on ({a..b} - k)"
+ using \<gamma> by (force simp: piecewise_C1_differentiable_on_def)
+ have o: "open ({a<..<b} - k)"
+ using `finite k` by (simp add: finite_imp_closed open_Diff)
+ moreover have "{a<..<b} - k \<subseteq> {a..b} - k"
+ by force
+ ultimately have g_diff_at: "\<And>x. \<lbrakk>x \<notin> k; x \<in> {a<..<b}\<rbrakk> \<Longrightarrow> \<gamma> differentiable at x"
+ by (metis Diff_iff differentiable_on_subset C1_diff_imp_diff [OF g_C1_diff] differentiable_on_def differentiable_within_open)
+ { fix w
+ assume "w \<noteq> z"
+ have "continuous_on (ball w (cmod (w - z))) (\<lambda>w. 1 / (w - z))"
+ by (auto simp: dist_norm intro!: continuous_intros)
+ moreover have "\<And>x. cmod (w - x) < cmod (w - z) \<Longrightarrow> \<exists>f'. ((\<lambda>w. 1 / (w - z)) has_field_derivative f') (at x)"
+ by (auto simp: intro!: derivative_eq_intros)
+ ultimately have "\<exists>h. \<forall>y. norm(y - w) < norm(w - z) \<longrightarrow> (h has_field_derivative 1/(y - z)) (at y)"
+ using holomorphic_convex_primitive [of "ball w (norm(w - z))" "{}" "\<lambda>w. 1/(w - z)"]
+ by (simp add: complex_differentiable_def Ball_def dist_norm at_within_open_NO_MATCH norm_minus_commute)
+ }
+ then obtain h where h: "\<And>w y. w \<noteq> z \<Longrightarrow> norm(y - w) < norm(w - z) \<Longrightarrow> (h w has_field_derivative 1/(y - z)) (at y)"
+ by meson
+ have exy: "\<exists>y. ((\<lambda>x. inverse (\<gamma> x - z) * ?D\<gamma> x) has_integral y) {a..b}"
+ unfolding integrable_on_def [symmetric]
+ apply (rule path_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>], of "-{z}"])
+ apply (rename_tac w)
+ apply (rule_tac x="norm(w - z)" in exI)
+ apply (simp_all add: inverse_eq_divide)
+ apply (metis has_field_derivative_at_within h)
+ done
+ have vg_int: "(\<lambda>x. ?D\<gamma> x / (\<gamma> x - z)) integrable_on {a..b}"
+ unfolding box_real [symmetric] divide_inverse_commute
+ by (auto intro!: exy integrable_subinterval simp add: integrable_on_def ab)
+ with ab show ?thesis1
+ by (simp add: divide_inverse_commute integral_def integrable_on_def)
+ { fix t
+ assume t: "t \<in> {a..b}"
+ have cball: "continuous_on (ball (\<gamma> t) (dist (\<gamma> t) z)) (\<lambda>x. inverse (x - z))"
+ using z by (auto intro!: continuous_intros simp: dist_norm)
+ have icd: "\<And>x. cmod (\<gamma> t - x) < cmod (\<gamma> t - z) \<Longrightarrow> (\<lambda>w. inverse (w - z)) complex_differentiable at x"
+ unfolding complex_differentiable_def by (force simp: intro!: derivative_eq_intros)
+ obtain h where h: "\<And>x. cmod (\<gamma> t - x) < cmod (\<gamma> t - z) \<Longrightarrow>
+ (h has_field_derivative inverse (x - z)) (at x within {y. cmod (\<gamma> t - y) < cmod (\<gamma> t - z)})"
+ using holomorphic_convex_primitive [where f = "\<lambda>w. inverse(w - z)", OF convex_ball finite.emptyI cball icd]
+ by simp (auto simp: ball_def dist_norm that)
+ { fix x D
+ assume x: "x \<notin> k" "a < x" "x < b"
+ then have "x \<in> interior ({a..b} - k)"
+ using open_subset_interior [OF o] by fastforce
+ then have con: "isCont (\<lambda>x. ?D\<gamma> x) x"
+ using g_C1_diff x by (auto simp: C1_differentiable_on_eq intro: continuous_on_interior)
+ then have con_vd: "continuous (at x within {a..b}) (\<lambda>x. ?D\<gamma> x)"
+ by (rule continuous_at_imp_continuous_within)
+ have gdx: "\<gamma> differentiable at x"
+ using x by (simp add: g_diff_at)
+ have "((\<lambda>c. Exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
+ (at x within {a..b})"
+ using x gdx t
+ apply (clarsimp simp add: differentiable_iff_scaleR)
+ apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_within)
+ apply (simp_all add: has_vector_derivative_def [symmetric])
+ apply (rule has_vector_derivative_eq_rhs [OF integral_has_vector_derivative_continuous_at])
+ apply (rule con_vd continuous_intros cong vg_int | simp add: continuous_at_imp_continuous_within has_vector_derivative_continuous vector_derivative_at)+
+ done
+ } note * = this
+ have "exp (- (integral {a..t} (\<lambda>x. ?D\<gamma> x / (\<gamma> x - z)))) * (\<gamma> t - z) =\<gamma> a - z"
+ apply (rule has_derivative_zero_unique_strong_interval [of "{a,b} \<union> k" a b])
+ using t
+ apply (auto intro!: * continuous_intros fink cong indefinite_integral_continuous [OF vg_int] simp add: ab)+
+ done
+ }
+ with ab show ?thesis2
+ 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)"
+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 path_integral_integral exp_minus)
+
+
+subsection\<open>The version with complex integers and equality\<close>
+
+lemma integer_winding_number_eq:
+ assumes \<gamma>: "path \<gamma>" and z: "z \<notin> path_image \<gamma>"
+ shows "winding_number \<gamma> z \<in> \<int> \<longleftrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
+proof -
+ have *: "\<And>i::complex. \<And>g0 g1. \<lbrakk>i \<noteq> 0; g0 \<noteq> z; (g1 - z) / i = g0 - z\<rbrakk> \<Longrightarrow> (i = 1 \<longleftrightarrow> g1 = g0)"
+ by (simp add: field_simps) algebra
+ obtain p where p: "valid_path p" "z \<notin> path_image p"
+ "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>"
+ "path_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
+ using winding_number [OF assms, of 1] by auto
+ have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (Exp (path_integral p (\<lambda>w. 1 / (w - z))) = 1)"
+ using p by (simp add: exp_eq_1 complex_is_Int_iff)
+ have "winding_number p z \<in> \<int> \<longleftrightarrow> pathfinish p = pathstart p"
+ using p z
+ apply (simp add: winding_number_valid_path valid_path_def path_image_def pathstart_def pathfinish_def)
+ using winding_number_exp_integral(2) [of p 0 1 z]
+ apply (simp add: field_simps path_integral_integral exp_minus)
+ apply (rule *)
+ apply (auto simp: path_image_def field_simps)
+ done
+ then show ?thesis using p
+ by (auto simp: winding_number_valid_path)
+qed
+
+theorem integer_winding_number:
+ "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>\<rbrakk> \<Longrightarrow> winding_number \<gamma> z \<in> \<int>"
+by (metis integer_winding_number_eq)
+
+
+text\<open>If the winding number's magnitude is at least one, then the path must contain points in every direction.*)
+ We can thus bound the winding number of a path that doesn't intersect a given ray. \<close>
+
+lemma winding_number_pos_meets:
+ fixes z::complex
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and 1: "Re (winding_number \<gamma> z) \<ge> 1"
+ and w: "w \<noteq> z"
+ shows "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image \<gamma>"
+proof -
+ have [simp]: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<gamma> x \<noteq> z"
+ using z by (auto simp: path_image_def)
+ have [simp]: "z \<notin> \<gamma> ` {0..1}"
+ using path_image_def z by auto
+ have gpd: "\<gamma> piecewise_C1_differentiable_on {0..1}"
+ using \<gamma> valid_path_def by blast
+ def r \<equiv> "(w - z) / (\<gamma> 0 - z)"
+ have [simp]: "r \<noteq> 0"
+ using w z by (auto simp: r_def)
+ have "Arg r \<le> 2*pi"
+ by (simp add: Arg less_eq_real_def)
+ also have "... \<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] Cauchy_Integral_Thm.path_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"
+ apply (simp add:)
+ apply (rule Topological_Spaces.IVT')
+ apply (simp_all add: Complex_Transcendental.Arg_ge_0)
+ apply (intro continuous_intros indefinite_integral_continuous winding_number_exp_integral [OF gpd]; simp)
+ done
+ 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"
+ by blast
+ def i \<equiv> "integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
+ have iArg: "Arg 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)
+ have "Exp (- i) * (\<gamma> t - z) = \<gamma> 0 - z"
+ unfolding i_def
+ apply (rule winding_number_exp_integral [OF gpdt])
+ using t z unfolding path_image_def
+ apply force+
+ done
+ then have *: "\<gamma> t - z = exp i * (\<gamma> 0 - z)"
+ by (simp add: exp_minus field_simps)
+ then have "(w - z) = r * (\<gamma> 0 - z)"
+ by (simp add: r_def)
+ then have "z + complex_of_real (exp (Re i)) * (w - z) / complex_of_real (cmod r) = \<gamma> t"
+ apply (simp add:)
+ apply (subst Complex_Transcendental.Arg_eq [of r])
+ apply (simp add: iArg)
+ using *
+ apply (simp add: Exp_eq_polar field_simps)
+ done
+ with t show ?thesis
+ by (rule_tac x="exp(Re i) / norm r" in exI) (auto simp: path_image_def)
+qed
+
+lemma winding_number_big_meets:
+ fixes z::complex
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "abs (Re (winding_number \<gamma> z)) \<ge> 1"
+ and w: "w \<noteq> z"
+ shows "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image \<gamma>"
+proof -
+ { assume "Re (winding_number \<gamma> z) \<le> - 1"
+ then have "Re (winding_number (reversepath \<gamma>) z) \<ge> 1"
+ by (simp add: \<gamma> valid_path_imp_path winding_number_reversepath z)
+ moreover have "valid_path (reversepath \<gamma>)"
+ using \<gamma> valid_path_imp_reverse by auto
+ moreover have "z \<notin> path_image (reversepath \<gamma>)"
+ by (simp add: z)
+ ultimately have "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image (reversepath \<gamma>)"
+ using winding_number_pos_meets w by blast
+ then have ?thesis
+ by simp
+ }
+ then show ?thesis
+ using assms
+ by (simp add: Groups.abs_if_class.abs_if winding_number_pos_meets split: split_if_asm)
+qed
+
+lemma winding_number_less_1:
+ fixes z::complex
+ shows
+ "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
+ \<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
+ \<Longrightarrow> abs (Re(winding_number \<gamma> z)) < 1"
+ by (auto simp: not_less dest: winding_number_big_meets)
+
+text\<open>One way of proving that WN=1 for a loop.\<close>
+lemma winding_number_eq_1:
+ fixes z::complex
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+ and 0: "0 < Re(winding_number \<gamma> z)" and 2: "Re(winding_number \<gamma> z) < 2"
+ shows "winding_number \<gamma> z = 1"
+proof -
+ have "winding_number \<gamma> z \<in> Ints"
+ by (simp add: \<gamma> integer_winding_number loop valid_path_imp_path z)
+ then show ?thesis
+ using 0 2 by (auto simp: Ints_def)
+qed
+
+
+subsection\<open>Continuity of winding number and invariance on connected sets.\<close>
+
+lemma continuous_at_winding_number:
+ fixes z::complex
+ assumes \<gamma>: "path \<gamma>" and z: "z \<notin> path_image \<gamma>"
+ shows "continuous (at z) (winding_number \<gamma>)"
+proof -
+ obtain e where "e>0" and cbg: "cball z e \<subseteq> - path_image \<gamma>"
+ using open_contains_cball [of "- path_image \<gamma>"] z
+ by (force simp: closed_def [symmetric] closed_path_image [OF \<gamma>])
+ then have ppag: "path_image \<gamma> \<subseteq> - cball z (e/2)"
+ by (force simp: cball_def dist_norm)
+ have oc: "open (- cball z (e / 2))"
+ by (simp add: closed_def [symmetric])
+ obtain d where "d>0" and pi_eq:
+ "\<And>h1 h2. \<lbrakk>valid_path h1; valid_path h2;
+ (\<forall>t\<in>{0..1}. cmod (h1 t - \<gamma> t) < d \<and> cmod (h2 t - \<gamma> t) < d);
+ pathstart h2 = pathstart h1; pathfinish h2 = pathfinish h1\<rbrakk>
+ \<Longrightarrow>
+ path_image h1 \<subseteq> - cball z (e / 2) \<and>
+ path_image h2 \<subseteq> - cball z (e / 2) \<and>
+ (\<forall>f. f holomorphic_on - cball z (e / 2) \<longrightarrow> path_integral h2 f = path_integral h1 f)"
+ using path_integral_nearby_ends [OF oc \<gamma> ppag] by metis
+ obtain p where p: "valid_path p" "z \<notin> path_image p"
+ "pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma>"
+ and pg: "\<And>t. t\<in>{0..1} \<Longrightarrow> cmod (\<gamma> t - p t) < min d e / 2"
+ and pi: "path_integral p (\<lambda>x. 1 / (x - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
+ using winding_number [OF \<gamma> z, of "min d e / 2"] `d>0` `e>0` by auto
+ { fix w
+ assume d2: "cmod (w - z) < d/2" and e2: "cmod (w - z) < e/2"
+ then have wnotp: "w \<notin> path_image p"
+ using cbg `d>0` `e>0`
+ apply (simp add: path_image_def cball_def dist_norm, clarify)
+ apply (frule pg)
+ apply (drule_tac c="\<gamma> x" in subsetD)
+ apply (auto simp: less_eq_real_def norm_minus_commute norm_triangle_half_l)
+ done
+ have wnotg: "w \<notin> path_image \<gamma>"
+ using cbg e2 `e>0` by (force simp: dist_norm norm_minus_commute)
+ { fix k::real
+ assume k: "k>0"
+ then obtain q where q: "valid_path q" "w \<notin> path_image q"
+ "pathstart q = pathstart \<gamma> \<and> pathfinish q = pathfinish \<gamma>"
+ and qg: "\<And>t. t \<in> {0..1} \<Longrightarrow> cmod (\<gamma> t - q t) < min k (min d e) / 2"
+ and qi: "path_integral q (\<lambda>u. 1 / (u - w)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> w"
+ using winding_number [OF \<gamma> wnotg, of "min k (min d e) / 2"] `d>0` `e>0` k
+ by (force simp: min_divide_distrib_right)
+ have "path_integral p (\<lambda>u. 1 / (u - w)) = path_integral q (\<lambda>u. 1 / (u - w))"
+ apply (rule pi_eq [OF `valid_path q` `valid_path p`, THEN conjunct2, THEN conjunct2, rule_format])
+ apply (frule pg)
+ apply (frule qg)
+ using p q `d>0` e2
+ apply (auto simp: dist_norm norm_minus_commute intro!: holomorphic_intros)
+ done
+ then have "path_integral p (\<lambda>x. 1 / (x - w)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> w"
+ by (simp add: pi qi)
+ } note pip = this
+ have "path p"
+ using p by (simp add: valid_path_imp_path)
+ then have "winding_number p w = winding_number \<gamma> w"
+ apply (rule winding_number_unique [OF _ wnotp])
+ apply (rule_tac x=p in exI)
+ apply (simp add: p wnotp min_divide_distrib_right pip)
+ done
+ } note wnwn = this
+ obtain pe where "pe>0" and cbp: "cball z (3 / 4 * pe) \<subseteq> - path_image p"
+ using p open_contains_cball [of "- path_image p"]
+ by (force simp: closed_def [symmetric] closed_path_image [OF valid_path_imp_path])
+ obtain L
+ where "L>0"
+ and L: "\<And>f B. \<lbrakk>f holomorphic_on - cball z (3 / 4 * pe);
+ \<forall>z \<in> - cball z (3 / 4 * pe). cmod (f z) \<le> B\<rbrakk> \<Longrightarrow>
+ cmod (path_integral p f) \<le> L * B"
+ using path_integral_bound_exists [of "- cball z (3/4*pe)" p] cbp `valid_path p` by force
+ { fix e::real and w::complex
+ assume e: "0 < e" and w: "cmod (w - z) < pe/4" "cmod (w - z) < e * pe\<^sup>2 / (8 * L)"
+ then have [simp]: "w \<notin> path_image p"
+ using cbp p(2) `0 < pe`
+ by (force simp: dist_norm norm_minus_commute path_image_def cball_def)
+ have [simp]: "path_integral p (\<lambda>x. 1/(x - w)) - path_integral p (\<lambda>x. 1/(x - z)) =
+ path_integral p (\<lambda>x. 1/(x - w) - 1/(x - z))"
+ by (simp add: p path_integrable_inversediff path_integral_diff)
+ { fix x
+ assume pe: "3/4 * pe < cmod (z - x)"
+ have "cmod (w - x) < pe/4 + cmod (z - x)"
+ by (meson add_less_cancel_right norm_diff_triangle_le order_refl order_trans_rules(21) w(1))
+ then have wx: "cmod (w - x) < 4/3 * cmod (z - x)" using pe by simp
+ have "cmod (z - x) \<le> cmod (z - w) + cmod (w - x)"
+ using norm_diff_triangle_le by blast
+ also have "... < pe/4 + cmod (w - x)"
+ using w by (simp add: norm_minus_commute)
+ finally have "pe/2 < cmod (w - x)"
+ using pe by auto
+ then have "(pe/2)^2 < cmod (w - x) ^ 2"
+ apply (rule power_strict_mono)
+ using `pe>0` by auto
+ then have pe2: "pe^2 < 4 * cmod (w - x) ^ 2"
+ by auto
+ have "8 * L * cmod (w - z) < e * pe\<^sup>2"
+ using w `L>0` by (simp add: field_simps)
+ also have "... < e * 4 * cmod (w - x) * cmod (w - x)"
+ using pe2 `e>0` by (simp add: power2_eq_square)
+ also have "... < e * 4 * cmod (w - x) * (4/3 * cmod (z - x))"
+ using wx
+ apply (rule mult_strict_left_mono)
+ using pe2 e not_less_iff_gr_or_eq by fastforce
+ finally have "L * cmod (w - z) < 2/3 * e * cmod (w - x) * cmod (z - x)"
+ by simp
+ also have "... \<le> e * cmod (w - x) * cmod (z - x)"
+ using e by simp
+ finally have Lwz: "L * cmod (w - z) < e * cmod (w - x) * cmod (z - x)" .
+ have "L * cmod (1 / (x - w) - 1 / (x - z)) \<le> e"
+ apply (cases "x=z \<or> x=w")
+ using pe `pe>0` w `L>0`
+ apply (force simp: norm_minus_commute)
+ using wx w(2) `L>0` pe pe2 Lwz
+ apply (auto simp: divide_simps mult_less_0_iff norm_minus_commute norm_divide norm_mult power2_eq_square)
+ done
+ } note L_cmod_le = this
+ have *: "cmod (path_integral p (\<lambda>x. 1 / (x - w) - 1 / (x - z))) \<le> L * (e * pe\<^sup>2 / L / 4 * (inverse (pe / 2))\<^sup>2)"
+ apply (rule L)
+ using `pe>0` w
+ apply (force simp: dist_norm norm_minus_commute intro!: holomorphic_intros)
+ using `pe>0` w `L>0`
+ apply (auto simp: cball_def dist_norm field_simps L_cmod_le simp del: less_divide_eq_numeral1 le_divide_eq_numeral1)
+ done
+ have "cmod (path_integral p (\<lambda>x. 1 / (x - w)) - path_integral p (\<lambda>x. 1 / (x - z))) < 2*e"
+ apply (simp add:)
+ apply (rule le_less_trans [OF *])
+ using `L>0` e
+ apply (force simp: field_simps)
+ done
+ then have "cmod (winding_number p w - winding_number p z) < e"
+ using pi_ge_two e
+ by (force simp: winding_number_valid_path p field_simps norm_divide norm_mult intro: less_le_trans)
+ } note cmod_wn_diff = this
+ show ?thesis
+ apply (rule continuous_transform_at [of "min d e / 2" _ "winding_number p"])
+ apply (auto simp: `d>0` `e>0` dist_norm wnwn simp del: less_divide_eq_numeral1)
+ apply (simp add: continuous_at_eps_delta, clarify)
+ apply (rule_tac x="min (pe/4) (e/2*pe^2/L/4)" in exI)
+ using `pe>0` `L>0`
+ apply (simp add: dist_norm cmod_wn_diff)
+ done
+qed
+
+corollary continuous_on_winding_number:
+ "path \<gamma> \<Longrightarrow> continuous_on (- path_image \<gamma>) (\<lambda>w. winding_number \<gamma> w)"
+ by (simp add: continuous_at_imp_continuous_on continuous_at_winding_number)
+
+
+subsection{*The winding number is constant on a connected region*}
+
+lemma winding_number_constant:
+ assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and cs: "connected s" and sg: "s \<inter> path_image \<gamma> = {}"
+ shows "\<exists>k. \<forall>z \<in> s. winding_number \<gamma> z = k"
+proof -
+ { fix y z
+ assume ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z"
+ assume "y \<in> s" "z \<in> s"
+ then have "winding_number \<gamma> y \<in> \<int>" "winding_number \<gamma> z \<in> \<int>"
+ using integer_winding_number [OF \<gamma> loop] sg `y \<in> s` by auto
+ with ne have "1 \<le> cmod (winding_number \<gamma> y - winding_number \<gamma> z)"
+ by (auto simp: Ints_def of_int_diff [symmetric] simp del: of_int_diff)
+ } note * = this
+ show ?thesis
+ apply (rule continuous_discrete_range_constant [OF cs])
+ using continuous_on_winding_number [OF \<gamma>] sg
+ apply (metis Diff_Compl Diff_eq_empty_iff continuous_on_subset)
+ apply (rule_tac x=1 in exI)
+ apply (auto simp: *)
+ done
+qed
+
+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 fastforce
+
+lemma open_winding_number_levelsets:
+ assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+ shows "open {z. z \<notin> path_image \<gamma> \<and> winding_number \<gamma> z = k}"
+proof -
+ have op: "open (- path_image \<gamma>)"
+ by (simp add: closed_path_image \<gamma> open_Compl)
+ { fix z assume z: "z \<notin> path_image \<gamma>" and k: "k = winding_number \<gamma> z"
+ obtain e where e: "e>0" "ball z e \<subseteq> - path_image \<gamma>"
+ using open_contains_ball [of "- path_image \<gamma>"] op z
+ by blast
+ have "\<exists>e>0. \<forall>y. dist y z < e \<longrightarrow> y \<notin> path_image \<gamma> \<and> winding_number \<gamma> y = winding_number \<gamma> z"
+ apply (rule_tac x=e in exI)
+ using e apply (simp add: dist_norm ball_def norm_minus_commute)
+ apply (auto simp: dist_norm norm_minus_commute intro!: winding_number_eq [OF assms, where s = "ball z e"])
+ done
+ } then
+ show ?thesis
+ by (auto simp: Complex.open_complex_def)
+qed
+
+subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
+
+lemma winding_number_zero_in_outside:
+ assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)"
+ shows "winding_number \<gamma> z = 0"
+proof -
+ obtain B::real where "0 < B" and B: "path_image \<gamma> \<subseteq> ball 0 B"
+ using bounded_subset_ballD [OF bounded_path_image [OF \<gamma>]] by auto
+ obtain w::complex where w: "w \<notin> ball 0 (B + 1)"
+ by (metis abs_of_nonneg le_less less_irrefl mem_ball_0 norm_of_real)
+ have "- ball 0 (B + 1) \<subseteq> outside (path_image \<gamma>)"
+ apply (rule outside_subset_convex)
+ using B subset_ball by auto
+ then have wout: "w \<in> outside (path_image \<gamma>)"
+ using w by blast
+ moreover obtain k where "\<And>z. z \<in> outside (path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k"
+ using winding_number_constant [OF \<gamma> loop, of "outside(path_image \<gamma>)"] connected_outside
+ by (metis DIM_complex bounded_path_image dual_order.refl \<gamma> outside_no_overlap)
+ ultimately have "winding_number \<gamma> z = winding_number \<gamma> w"
+ using z by blast
+ also have "... = 0"
+ proof -
+ have wnot: "w \<notin> path_image \<gamma>" using wout by (simp add: outside_def)
+ { fix e::real assume "0<e"
+ obtain p where p: "polynomial_function p" "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>"
+ and pg1: "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> cmod (p t - \<gamma> t) < 1)"
+ and pge: "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> cmod (p t - \<gamma> t) < e)"
+ using path_approx_polynomial_function [OF \<gamma>, of "min 1 e"] `e>0` by force
+ have pip: "path_image p \<subseteq> ball 0 (B + 1)"
+ using B
+ apply (clarsimp simp add: path_image_def dist_norm ball_def)
+ apply (frule (1) pg1)
+ apply (fastforce dest: norm_add_less)
+ done
+ then have "w \<notin> path_image p" using w by blast
+ then have "\<exists>p. valid_path p \<and> w \<notin> path_image p \<and>
+ pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
+ (\<forall>t\<in>{0..1}. cmod (\<gamma> t - p t) < e) \<and> path_integral p (\<lambda>wa. 1 / (wa - w)) = 0"
+ apply (rule_tac x=p in exI)
+ apply (simp add: p valid_path_polynomial_function)
+ apply (intro conjI)
+ using pge apply (simp add: norm_minus_commute)
+ apply (rule path_integral_unique [OF Cauchy_theorem_convex_simple [OF _ convex_ball [of 0 "B+1"]]])
+ apply (rule holomorphic_intros | simp add: dist_norm)+
+ using mem_ball_0 w apply blast
+ using p apply (simp_all add: valid_path_polynomial_function loop pip)
+ done
+ }
+ then show ?thesis
+ by (auto intro: winding_number_unique [OF \<gamma>] simp add: wnot)
+ qed
+ finally show ?thesis .
+qed
+
+lemma winding_number_zero_outside:
+ "\<lbrakk>path \<gamma>; convex s; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> s; path_image \<gamma> \<subseteq> s\<rbrakk> \<Longrightarrow> winding_number \<gamma> z = 0"
+ by (meson convex_in_outside outside_mono subsetCE winding_number_zero_in_outside)
+
+lemma winding_number_zero_at_infinity:
+ assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+ shows "\<exists>B. \<forall>z. B \<le> norm z \<longrightarrow> winding_number \<gamma> z = 0"
+proof -
+ obtain B::real where "0 < B" and B: "path_image \<gamma> \<subseteq> ball 0 B"
+ using bounded_subset_ballD [OF bounded_path_image [OF \<gamma>]] by auto
+ then show ?thesis
+ apply (rule_tac x="B+1" in exI, clarify)
+ apply (rule winding_number_zero_outside [OF \<gamma> convex_cball [of 0 B] loop])
+ apply (meson less_add_one mem_cball_0 not_le order_trans)
+ using ball_subset_cball by blast
+qed
+
+lemma winding_number_zero_point:
+ "\<lbrakk>path \<gamma>; convex s; pathfinish \<gamma> = pathstart \<gamma>; open s; path_image \<gamma> \<subseteq> s\<rbrakk>
+ \<Longrightarrow> \<exists>z. z \<in> s \<and> winding_number \<gamma> z = 0"
+ using outside_compact_in_open [of "path_image \<gamma>" s] path_image_nonempty winding_number_zero_in_outside
+ by (fastforce simp add: compact_path_image)
+
+
+text\<open>If a path winds round a set, it winds rounds its inside.\<close>
+lemma winding_number_around_inside:
+ assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+ and cls: "closed s" and cos: "connected s" and s_disj: "s \<inter> path_image \<gamma> = {}"
+ and z: "z \<in> s" and wn_nz: "winding_number \<gamma> z \<noteq> 0" and w: "w \<in> s \<union> inside s"
+ shows "winding_number \<gamma> w = winding_number \<gamma> z"
+proof -
+ have ssb: "s \<subseteq> inside(path_image \<gamma>)"
+ proof
+ fix x :: complex
+ assume "x \<in> s"
+ hence "x \<notin> path_image \<gamma>"
+ by (meson disjoint_iff_not_equal s_disj)
+ thus "x \<in> inside (path_image \<gamma>)"
+ using `x \<in> s` by (metis (no_types) ComplI UnE cos \<gamma> loop s_disj union_with_outside winding_number_eq winding_number_zero_in_outside wn_nz z)
+qed
+ show ?thesis
+ apply (rule winding_number_eq [OF \<gamma> loop w])
+ using z apply blast
+ apply (simp add: cls connected_with_inside cos)
+ apply (simp add: Int_Un_distrib2 s_disj, safe)
+ by (meson ssb inside_inside_compact_connected [OF cls, of "path_image \<gamma>"] compact_path_image connected_path_image contra_subsetD disjoint_iff_not_equal \<gamma> inside_no_overlap)
+ qed
+
+
+text\<open>Bounding a WN by 1/2 for a path and point in opposite halfspaces.\<close>
+lemma winding_number_subpath_continuous:
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>"
+ shows "continuous_on {0..1} (\<lambda>x. winding_number(subpath 0 x \<gamma>) z)"
+proof -
+ 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) * path_integral (subpath 0 x \<gamma>) (\<lambda>w. 1/(w - z))"
+ using assms x
+ apply (simp add: path_integral_subpath_integral [OF path_integrable_inversediff])
+ done
+ also have "... = winding_number (subpath 0 x \<gamma>) z"
+ apply (subst winding_number_valid_path)
+ using assms x
+ apply (simp_all add: valid_path_subpath)
+ by (force simp: closed_segment_eq_real_ivl path_image_def)
+ finally show ?thesis .
+ qed
+ show ?thesis
+ apply (rule continuous_on_eq
+ [where f = "\<lambda>x. 1 / (2*pi*ii) *
+ 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 path_integrable_inversediff [OF assms, unfolded path_integrable_on])
+ using assms
+ apply (simp add: *)
+ done
+qed
+
+lemma winding_number_ivt_pos:
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "0 \<le> w" "w \<le> Re(winding_number \<gamma> z)"
+ shows "\<exists>t \<in> {0..1}. Re(winding_number(subpath 0 t \<gamma>) z) = w"
+ apply (rule ivt_increasing_component_on_1 [of 0 1, where ?k = "1::complex", simplified complex_inner_1_right])
+ apply (simp add:)
+ apply (rule winding_number_subpath_continuous [OF \<gamma> z])
+ using assms
+ apply (auto simp: path_image_def image_def)
+ done
+
+lemma winding_number_ivt_neg:
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "Re(winding_number \<gamma> z) \<le> w" "w \<le> 0"
+ shows "\<exists>t \<in> {0..1}. Re(winding_number(subpath 0 t \<gamma>) z) = w"
+ apply (rule ivt_decreasing_component_on_1 [of 0 1, where ?k = "1::complex", simplified complex_inner_1_right])
+ apply (simp add:)
+ apply (rule winding_number_subpath_continuous [OF \<gamma> z])
+ using assms
+ apply (auto simp: path_image_def image_def)
+ done
+
+lemma winding_number_ivt_abs:
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "0 \<le> w" "w \<le> \<bar>Re(winding_number \<gamma> z)\<bar>"
+ shows "\<exists>t \<in> {0..1}. \<bar>Re (winding_number (subpath 0 t \<gamma>) z)\<bar> = w"
+ using assms winding_number_ivt_pos [of \<gamma> z w] winding_number_ivt_neg [of \<gamma> z "-w"]
+ by force
+
+lemma winding_number_lt_half_lemma:
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and az: "a \<bullet> z \<le> b" and pag: "path_image \<gamma> \<subseteq> {w. a \<bullet> w > b}"
+ shows "Re(winding_number \<gamma> z) < 1/2"
+proof -
+ { assume "Re(winding_number \<gamma> z) \<ge> 1/2"
+ then obtain t::real where t: "0 \<le> t" "t \<le> 1" and sub12: "Re (winding_number (subpath 0 t \<gamma>) z) = 1/2"
+ using winding_number_ivt_pos [OF \<gamma> z, of "1/2"] by auto
+ have gt: "\<gamma> t - z = - (of_real (exp (- (2 * pi * Im (winding_number (subpath 0 t \<gamma>) z)))) * (\<gamma> 0 - z))"
+ using winding_number_exp_2pi [of "subpath 0 t \<gamma>" z]
+ apply (simp add: t \<gamma> valid_path_imp_path)
+ using closed_segment_eq_real_ivl path_image_def t z by (fastforce simp add: Euler sub12)
+ have "b < a \<bullet> \<gamma> 0"
+ proof -
+ have "\<gamma> 0 \<in> {c. b < a \<bullet> c}"
+ by (metis (no_types) pag atLeastAtMost_iff image_subset_iff order_refl path_image_def zero_le_one)
+ thus ?thesis
+ by blast
+ qed
+ moreover have "b < a \<bullet> \<gamma> t"
+ proof -
+ have "\<gamma> t \<in> {c. b < a \<bullet> c}"
+ by (metis (no_types) pag atLeastAtMost_iff image_subset_iff path_image_def t)
+ thus ?thesis
+ by blast
+ qed
+ ultimately have "0 < a \<bullet> (\<gamma> 0 - z)" "0 < a \<bullet> (\<gamma> t - z)" using az
+ by (simp add: inner_diff_right)+
+ then have False
+ by (simp add: gt inner_mult_right mult_less_0_iff)
+ }
+ then show ?thesis by force
+qed
+
+lemma winding_number_lt_half:
+ assumes "valid_path \<gamma>" "a \<bullet> z \<le> b" "path_image \<gamma> \<subseteq> {w. a \<bullet> w > b}"
+ shows "\<bar>Re (winding_number \<gamma> z)\<bar> < 1/2"
+proof -
+ have "z \<notin> path_image \<gamma>" using assms by auto
+ with assms show ?thesis
+ apply (simp add: winding_number_lt_half_lemma abs_if del: less_divide_eq_numeral1)
+ apply (metis complex_inner_1_right winding_number_lt_half_lemma [OF valid_path_imp_reverse, of \<gamma> z a b]
+ winding_number_reversepath valid_path_imp_path inner_minus_left path_image_reversepath)
+ done
+qed
+
+lemma winding_number_le_half:
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>"
+ and anz: "a \<noteq> 0" and azb: "a \<bullet> z \<le> b" and pag: "path_image \<gamma> \<subseteq> {w. a \<bullet> w \<ge> b}"
+ shows "\<bar>Re (winding_number \<gamma> z)\<bar> \<le> 1/2"
+proof -
+ { assume wnz_12: "\<bar>Re (winding_number \<gamma> z)\<bar> > 1/2"
+ have "isCont (winding_number \<gamma>) z"
+ by (metis continuous_at_winding_number valid_path_imp_path \<gamma> z)
+ then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < abs(Re(winding_number \<gamma> z)) - 1/2"
+ using continuous_at_eps_delta wnz_12 diff_less_iff(1) by blast
+ def z' \<equiv> "z - (d / (2 * cmod a)) *\<^sub>R a"
+ have *: "a \<bullet> z' \<le> b - d / 3 * cmod a"
+ unfolding z'_def inner_mult_right' divide_inverse
+ apply (simp add: divide_simps algebra_simps dot_square_norm power2_eq_square anz)
+ apply (metis `0 < d` add_increasing azb less_eq_real_def mult_nonneg_nonneg mult_right_mono norm_ge_zero norm_numeral)
+ done
+ have "cmod (winding_number \<gamma> z' - winding_number \<gamma> z) < \<bar>Re (winding_number \<gamma> z)\<bar> - 1/2"
+ using d [of z'] anz `d>0` by (simp add: dist_norm z'_def)
+ then have "1/2 < \<bar>Re (winding_number \<gamma> z)\<bar> - cmod (winding_number \<gamma> z' - winding_number \<gamma> z)"
+ by simp
+ then have "1/2 < \<bar>Re (winding_number \<gamma> z)\<bar> - \<bar>Re (winding_number \<gamma> z') - Re (winding_number \<gamma> z)\<bar>"
+ using abs_Re_le_cmod [of "winding_number \<gamma> z' - winding_number \<gamma> z"] by simp
+ then have wnz_12': "\<bar>Re (winding_number \<gamma> z')\<bar> > 1/2"
+ by linarith
+ moreover have "\<bar>Re (winding_number \<gamma> z')\<bar> < 1/2"
+ apply (rule winding_number_lt_half [OF \<gamma> *])
+ using azb `d>0` pag
+ apply (auto simp: add_strict_increasing anz divide_simps algebra_simps dest!: subsetD)
+ done
+ ultimately have False
+ by simp
+ }
+ then show ?thesis by force
+qed
+
+lemma winding_number_lt_half_linepath: "z \<notin> closed_segment a b \<Longrightarrow> \<bar>Re (winding_number (linepath a b) z)\<bar> < 1/2"
+ using separating_hyperplane_closed_point [of "closed_segment a b" z]
+ apply auto
+ apply (simp add: closed_segment_def)
+ apply (drule less_imp_le)
+ apply (frule winding_number_lt_half [OF valid_path_linepath [of a b]])
+ apply (auto simp: segment)
+ done
+
+
+text\<open> Positivity of WN for a linepath.\<close>
+lemma winding_number_linepath_pos_lt:
+ assumes "0 < Im ((b - a) * cnj (b - z))"
+ shows "0 < Re(winding_number(linepath a b) z)"
+proof -
+ have z: "z \<notin> path_image (linepath a b)"
+ using assms
+ by (simp add: closed_segment_def) (force simp: algebra_simps)
+ show ?thesis
+ apply (rule winding_number_pos_lt [OF valid_path_linepath z assms])
+ apply (simp add: linepath_def algebra_simps)
+ done
+qed
+
+
+subsection{* Cauchy's integral formula, again for a convex enclosing set.*}
+
+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 complex_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_path_integral (2*pi * ii * 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: complex_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
+ proof (cases "x = z")
+ case True then show ?thesis
+ apply (simp add: continuous_within)
+ apply (rule Lim_transform_away_within [of _ "z+1" _ "\<lambda>w::complex. (f w - f z)/(w - z)"])
+ using has_field_derivative_at_within DERIV_within_iff f'
+ apply (fastforce simp add:)+
+ done
+ next
+ case False
+ then have dxz: "dist x z > 0" using dist_nz by blast
+ have cf: "continuous (at x within s) f"
+ using conf continuous_on_eq_continuous_within that by blast
+ show ?thesis
+ apply (rule continuous_transform_within [OF dxz that, of "\<lambda>w::complex. (f w - f z)/(w - z)"])
+ apply (force simp: dist_commute)
+ apply (rule cf continuous_intros)+
+ using False by auto
+ qed
+ have fink': "finite (insert z k)" using \<open>finite k\<close> by blast
+ have *: "((\<lambda>w. if w = z then f' else (f w - f z) / (w - z)) has_path_integral 0) \<gamma>"
+ apply (rule Cauchy_theorem_convex [OF _ s fink' _ vpg pas loop])
+ using c apply (force simp: continuous_on_eq_continuous_within)
+ apply (rename_tac w)
+ apply (rule_tac d="dist w z" and f = "\<lambda>w. (f w - f z)/(w - z)" in complex_differentiable_transform_within)
+ apply (simp_all add: dist_pos_lt dist_commute)
+ apply (metis less_irrefl)
+ apply (rule derivative_intros fcd | simp)+
+ done
+ show ?thesis
+ apply (rule has_path_integral_eq)
+ using znotin has_path_integral_add [OF has_path_integral_lmul [OF has_path_integral_winding_number [OF vpg znotin], of "f z"] *]
+ apply (auto simp: mult_ac divide_simps)
+ done
+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_path_integral (2*pi * ii * 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)
+
end
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Oct 27 15:17:02 2015 +0000
@@ -88,22 +88,6 @@
lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
by auto
-lemma has_real_derivative:
- fixes f :: "real \<Rightarrow> real"
- assumes "(f has_derivative f') F"
- obtains c where "(f has_real_derivative c) F"
-proof -
- obtain c where "f' = (\<lambda>x. x * c)"
- by (metis assms has_derivative_bounded_linear real_bounded_linear)
- then show ?thesis
- by (metis assms that has_field_derivative_def mult_commute_abs)
-qed
-
-lemma has_real_derivative_iff:
- fixes f :: "real \<Rightarrow> real"
- shows "(\<exists>c. (f has_real_derivative c) F) = (\<exists>D. (f has_derivative D) F)"
- by (metis has_field_derivative_def has_real_derivative)
-
lemma continuous_mult_left:
fixes c::"'a::real_normed_algebra"
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)"
@@ -310,62 +294,62 @@
unfolding complex_differentiable_def
by (metis DERIV_subset top_greatest)
-lemma complex_differentiable_linear: "(op * c) complex_differentiable F"
+lemma complex_differentiable_linear [derivative_intros]: "(op * c) complex_differentiable F"
proof -
show ?thesis
unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs
by (force intro: has_derivative_mult_right)
qed
-lemma complex_differentiable_const: "(\<lambda>z. c) complex_differentiable F"
+lemma complex_differentiable_const [derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
unfolding complex_differentiable_def has_field_derivative_def
by (rule exI [where x=0])
(metis has_derivative_const lambda_zero)
-lemma complex_differentiable_ident: "(\<lambda>z. z) complex_differentiable F"
+lemma complex_differentiable_ident [derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
unfolding complex_differentiable_def has_field_derivative_def
by (rule exI [where x=1])
(simp add: lambda_one [symmetric])
-lemma complex_differentiable_id: "id complex_differentiable F"
+lemma complex_differentiable_id [derivative_intros]: "id complex_differentiable F"
unfolding id_def by (rule complex_differentiable_ident)
-lemma complex_differentiable_minus:
+lemma complex_differentiable_minus [derivative_intros]:
"f complex_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) complex_differentiable F"
using assms unfolding complex_differentiable_def
by (metis field_differentiable_minus)
-lemma complex_differentiable_add:
+lemma complex_differentiable_add [derivative_intros]:
assumes "f complex_differentiable F" "g complex_differentiable F"
shows "(\<lambda>z. f z + g z) complex_differentiable F"
using assms unfolding complex_differentiable_def
by (metis field_differentiable_add)
-lemma complex_differentiable_setsum:
+lemma complex_differentiable_setsum [derivative_intros]:
"(\<And>i. i \<in> I \<Longrightarrow> (f i) complex_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) complex_differentiable F"
by (induct I rule: infinite_finite_induct)
(auto intro: complex_differentiable_add complex_differentiable_const)
-lemma complex_differentiable_diff:
+lemma complex_differentiable_diff [derivative_intros]:
assumes "f complex_differentiable F" "g complex_differentiable F"
shows "(\<lambda>z. f z - g z) complex_differentiable F"
using assms unfolding complex_differentiable_def
by (metis field_differentiable_diff)
-lemma complex_differentiable_inverse:
+lemma complex_differentiable_inverse [derivative_intros]:
assumes "f complex_differentiable (at a within s)" "f a \<noteq> 0"
shows "(\<lambda>z. inverse (f z)) complex_differentiable (at a within s)"
using assms unfolding complex_differentiable_def
by (metis DERIV_inverse_fun)
-lemma complex_differentiable_mult:
+lemma complex_differentiable_mult [derivative_intros]:
assumes "f complex_differentiable (at a within s)"
"g complex_differentiable (at a within s)"
shows "(\<lambda>z. f z * g z) complex_differentiable (at a within s)"
using assms unfolding complex_differentiable_def
by (metis DERIV_mult [of f _ a s g])
-lemma complex_differentiable_divide:
+lemma complex_differentiable_divide [derivative_intros]:
assumes "f complex_differentiable (at a within s)"
"g complex_differentiable (at a within s)"
"g a \<noteq> 0"
@@ -373,7 +357,7 @@
using assms unfolding complex_differentiable_def
by (metis DERIV_divide [of f _ a s g])
-lemma complex_differentiable_power:
+lemma complex_differentiable_power [derivative_intros]:
assumes "f complex_differentiable (at a within s)"
shows "(\<lambda>z. f z ^ n) complex_differentiable (at a within s)"
using assms unfolding complex_differentiable_def
@@ -425,8 +409,10 @@
definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
(infixl "(holomorphic'_on)" 50)
where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f complex_differentiable (at x within s)"
-
-lemma holomorphic_on_empty: "f holomorphic_on {}"
+
+named_theorems holomorphic_intros "structural introduction rules for holomorphic_on"
+
+lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}"
by (simp add: holomorphic_on_def)
lemma holomorphic_on_open:
@@ -448,16 +434,16 @@
lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
by (metis holomorphic_transform)
-lemma holomorphic_on_linear: "(op * c) holomorphic_on s"
+lemma holomorphic_on_linear [holomorphic_intros]: "(op * c) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_linear)
-lemma holomorphic_on_const: "(\<lambda>z. c) holomorphic_on s"
+lemma holomorphic_on_const [holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_const)
-lemma holomorphic_on_ident: "(\<lambda>x. x) holomorphic_on s"
+lemma holomorphic_on_ident [holomorphic_intros]: "(\<lambda>x. x) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_ident)
-lemma holomorphic_on_id: "id holomorphic_on s"
+lemma holomorphic_on_id [holomorphic_intros]: "id holomorphic_on s"
unfolding id_def by (rule holomorphic_on_ident)
lemma holomorphic_on_compose:
@@ -469,54 +455,37 @@
"f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
by (metis holomorphic_on_compose holomorphic_on_subset)
-lemma holomorphic_on_minus: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
+lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
by (metis complex_differentiable_minus holomorphic_on_def)
-lemma holomorphic_on_add:
+lemma holomorphic_on_add [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_add)
-lemma holomorphic_on_diff:
+lemma holomorphic_on_diff [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_diff)
-lemma holomorphic_on_mult:
+lemma holomorphic_on_mult [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_mult)
-lemma holomorphic_on_inverse:
+lemma holomorphic_on_inverse [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. inverse (f z)) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_inverse)
-lemma holomorphic_on_divide:
+lemma holomorphic_on_divide [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. f z / g z) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_divide)
-lemma holomorphic_on_power:
+lemma holomorphic_on_power [holomorphic_intros]:
"f holomorphic_on s \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_power)
-lemma holomorphic_on_setsum:
+lemma holomorphic_on_setsum [holomorphic_intros]:
"(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
unfolding holomorphic_on_def by (metis complex_differentiable_setsum)
-definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
- "deriv f x \<equiv> SOME D. DERIV f x :> D"
-
-lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
- unfolding deriv_def by (metis some_equality DERIV_unique)
-
-lemma DERIV_deriv_iff_real_differentiable:
- fixes x :: real
- shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
- unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
-
-lemma real_derivative_chain:
- fixes x :: real
- shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
- \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
- by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv)
-
lemma DERIV_deriv_iff_complex_differentiable:
"DERIV f x :> deriv f x \<longleftrightarrow> f complex_differentiable at x"
unfolding complex_differentiable_def by (metis DERIV_imp_deriv)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Oct 27 15:17:02 2015 +0000
@@ -12,36 +12,6 @@
"~~/src/HOL/Library/Set_Algebras"
begin
-
-(* ------------------------------------------------------------------------- *)
-(* To be moved elsewhere *)
-(* ------------------------------------------------------------------------- *)
-
-lemma linear_scaleR [simp]: "linear (\<lambda>x. scaleR c x)"
- by (simp add: linear_iff scaleR_add_right)
-
-lemma linear_scaleR_left [simp]: "linear (\<lambda>r. scaleR r x)"
- by (simp add: linear_iff scaleR_add_left)
-
-lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
- by (simp add: inj_on_def)
-
-lemma linear_add_cmul:
- assumes "linear f"
- shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x + b *\<^sub>R f y"
- using linear_add[of f] linear_cmul[of f] assms by simp
-
-lemma mem_convex_alt:
- assumes "convex S" "x \<in> S" "y \<in> S" "u \<ge> 0" "v \<ge> 0" "u + v > 0"
- shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) \<in> S"
- apply (rule convexD)
- using assms
- apply (simp_all add: zero_le_divide_iff add_divide_distrib [symmetric])
- done
-
-lemma inj_on_image_mem_iff: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f`A \<Longrightarrow> a \<in> B \<Longrightarrow> a \<in> A"
- by (blast dest: inj_onD)
-
lemma independent_injective_on_span_image:
assumes iS: "independent S"
and lf: "linear f"
@@ -3699,8 +3669,8 @@
using y e2 h1 by auto
then have "y \<in> S"
using assms y hull_subset[of S] affine_hull_subset_span
- inj_on_image_mem_iff[of f "span S" S y]
- by auto
+ inj_on_image_mem_iff [OF \<open>inj_on f (span S)\<close>]
+ by (metis Int_iff span_inc subsetCE)
}
then have "z \<in> f ` (rel_interior S)"
using mem_rel_interior_cball[of x S] \<open>e > 0\<close> x by auto
@@ -6318,13 +6288,10 @@
definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
+definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
+
lemmas segment = open_segment_def closed_segment_def
-lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
- by (auto simp add: closed_segment_def open_segment_def)
-
-definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
-
lemma midpoint_refl: "midpoint x x = x"
unfolding midpoint_def
unfolding scaleR_right_distrib
@@ -6406,6 +6373,9 @@
by (safe; rule_tac x="1 - u" in exI; force)
qed
+lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
+ by (auto simp add: closed_segment_def open_segment_def)
+
lemma segment_open_subset_closed:
"open_segment a b \<subseteq> closed_segment a b"
by (auto simp: closed_segment_def open_segment_def)
@@ -6445,9 +6415,6 @@
using segment_furthest_le[OF assms, of b]
by (auto simp add:norm_minus_commute)
-lemma segment_refl [simp]: "closed_segment a a = {a}"
- unfolding segment by (auto simp add: algebra_simps)
-
lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
proof -
have "{a, b} = {b, a}" by auto
@@ -6455,6 +6422,19 @@
by (simp add: segment_convex_hull)
qed
+lemma open_segment_commute: "open_segment a b = open_segment b a"
+proof -
+ have "{a, b} = {b, a}" by auto
+ thus ?thesis
+ by (simp add: closed_segment_commute open_segment_def)
+qed
+
+lemma closed_segment_idem [simp]: "closed_segment a a = {a}"
+ unfolding segment by (auto simp add: algebra_simps)
+
+lemma open_segment_idem [simp]: "open_segment a a = {}"
+ by (simp add: open_segment_def)
+
lemma closed_segment_eq_real_ivl:
fixes a b::real
shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Oct 27 15:17:02 2015 +0000
@@ -2247,6 +2247,49 @@
by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
(auto simp: differentiable_def has_vector_derivative_def)
+lemma frechet_derivative_eq_vector_derivative:
+ assumes "f differentiable (at x)"
+ shows "(frechet_derivative f (at x)) = (\<lambda>r. r *\<^sub>R vector_derivative f (at x))"
+using assms
+by (auto simp: differentiable_iff_scaleR vector_derivative_def has_vector_derivative_def
+ intro: someI frechet_derivative_at [symmetric])
+
+lemma has_real_derivative:
+ fixes f :: "real \<Rightarrow> real"
+ assumes "(f has_derivative f') F"
+ obtains c where "(f has_real_derivative c) F"
+proof -
+ obtain c where "f' = (\<lambda>x. x * c)"
+ by (metis assms has_derivative_bounded_linear real_bounded_linear)
+ then show ?thesis
+ by (metis assms that has_field_derivative_def mult_commute_abs)
+qed
+
+lemma has_real_derivative_iff:
+ fixes f :: "real \<Rightarrow> real"
+ shows "(\<exists>c. (f has_real_derivative c) F) = (\<exists>D. (f has_derivative D) F)"
+ by (metis has_field_derivative_def has_real_derivative)
+
+definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "deriv f x \<equiv> SOME D. DERIV f x :> D"
+
+lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
+ unfolding deriv_def by (metis some_equality DERIV_unique)
+
+lemma DERIV_deriv_iff_real_differentiable:
+ fixes x :: real
+ shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
+ unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
+
+lemma real_derivative_chain:
+ fixes x :: real
+ shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
+ \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
+ by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv)
+lemma field_derivative_eq_vector_derivative:
+ "(deriv f x) = vector_derivative f (at x)"
+by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def)
+
lemma islimpt_closure_open:
fixes s :: "'a::perfect_space set"
assumes "open s" and t: "t = closure s" "x \<in> t"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Oct 27 15:17:02 2015 +0000
@@ -300,6 +300,20 @@
finally show ?thesis .
qed
+lemma linear_scaleR [simp]: "linear (\<lambda>x. scaleR c x)"
+ by (simp add: linear_iff scaleR_add_right)
+
+lemma linear_scaleR_left [simp]: "linear (\<lambda>r. scaleR r x)"
+ by (simp add: linear_iff scaleR_add_left)
+
+lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
+ by (simp add: inj_on_def)
+
+lemma linear_add_cmul:
+ assumes "linear f"
+ shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x + b *\<^sub>R f y"
+ using linear_add[of f] linear_cmul[of f] assms by simp
+
subsection \<open>Bilinear functions.\<close>
--- a/src/HOL/Probability/Projective_Limit.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Probability/Projective_Limit.thy Tue Oct 27 15:17:02 2015 +0000
@@ -204,8 +204,8 @@
then have fm_in: "fm n x \<in> fm n ` B n"
using K' by (force simp: K_def)
show "x \<in> B n"
- using `x \<in> K n` K_sets sets.sets_into_space J(1,2,3)[of n]
- by (intro inj_on_image_mem_iff[OF inj_on_fm _ fm_in, of "\<lambda>_. borel"]) auto
+ using `x \<in> K n` K_sets sets.sets_into_space J(1,2,3)[of n] inj_on_image_mem_iff[OF inj_on_fm]
+ by (metis (no_types) Int_iff K_def fm_in space_borel)
qed
def Z' \<equiv> "\<lambda>n. emb I (J n) (K n)"
have Z': "\<And>n. Z' n \<subseteq> Z n"
--- a/src/HOL/Topological_Spaces.thy Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Topological_Spaces.thy Tue Oct 27 15:17:02 2015 +0000
@@ -2187,7 +2187,7 @@
assumes inj: "inj_on f {a..b}"
shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
proof -
- note I = inj_on_iff[OF inj]
+ note I = inj_on_eq_iff[OF inj]
{ assume "f x < f a" "f x < f b"
then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x