# HG changeset patch # User paulson # Date 1507559663 -3600 # Node ID deabce3ccf1f8c4de092893ff90d59c271585883 # Parent 6b76a5d1b7a569b6fc7578afbe6250cabf9e3d61 new material about connectedness, etc. diff -r 6b76a5d1b7a5 -r deabce3ccf1f src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Oct 08 16:50:37 2017 +0200 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Oct 09 15:34:23 2017 +0100 @@ -180,7 +180,7 @@ have "f differentiable at x within ({a<..finite s\ finite_imp_closed) ultimately show "f differentiable at x within {a..b}" @@ -192,7 +192,7 @@ have "g differentiable at x within ({c<..finite t\ finite_imp_closed) ultimately show "g differentiable at x within {a..b}" @@ -1446,7 +1446,7 @@ show ?thesis apply (rule fundamental_theorem_of_calculus_interior_strong) using k assms cfg * - apply (auto simp: at_within_closed_interval) + apply (auto simp: at_within_Icc_at) done qed @@ -4158,7 +4158,7 @@ subsection\Winding number is zero "outside" a curve, in various senses\ -lemma winding_number_zero_in_outside: +proposition winding_number_zero_in_outside: assumes \: "path \" and loop: "pathfinish \ = pathstart \" and z: "z \ outside (path_image \)" shows "winding_number \ z = 0" proof - @@ -4210,7 +4210,11 @@ finally show ?thesis . qed -lemma winding_number_zero_outside: +corollary winding_number_zero_const: "a \ z \ winding_number (\t. a) z = 0" + by (rule winding_number_zero_in_outside) + (auto simp: pathfinish_def pathstart_def path_polynomial_function) + +corollary winding_number_zero_outside: "\path \; convex s; pathfinish \ = pathstart \; z \ s; path_image \ \ s\ \ winding_number \ z = 0" by (meson convex_in_outside outside_mono subsetCE winding_number_zero_in_outside) diff -r 6b76a5d1b7a5 -r deabce3ccf1f src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Oct 08 16:50:37 2017 +0200 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Oct 09 15:34:23 2017 +0100 @@ -1233,7 +1233,7 @@ lemma continuous_on_Ln [continuous_intros]: "(\z. z \ s \ z \ \\<^sub>\\<^sub>0) \ continuous_on s Ln" by (simp add: continuous_at_imp_continuous_on continuous_within_Ln) -lemma holomorphic_on_Ln: "(\z. z \ s \ z \ \\<^sub>\\<^sub>0) \ Ln holomorphic_on s" +lemma holomorphic_on_Ln [holomorphic_intros]: "(\z. z \ s \ z \ \\<^sub>\\<^sub>0) \ Ln holomorphic_on s" by (simp add: field_differentiable_within_Ln holomorphic_on_def) lemma divide_ln_mono: diff -r 6b76a5d1b7a5 -r deabce3ccf1f src/HOL/Analysis/Conformal_Mappings.thy --- a/src/HOL/Analysis/Conformal_Mappings.thy Sun Oct 08 16:50:37 2017 +0200 +++ b/src/HOL/Analysis/Conformal_Mappings.thy Mon Oct 09 15:34:23 2017 +0100 @@ -1454,6 +1454,15 @@ qed qed +corollary Schwarz_Lemma': + assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0" + and no: "\z. norm z < 1 \ norm (f z) < 1" + shows "((\\. norm \ < 1 \ norm (f \) \ norm \) \ norm(deriv f 0) \ 1) \ + (((\z. norm z < 1 \ z \ 0 \ norm(f z) = norm z) \ norm(deriv f 0) = 1) + \ (\\. (\z. norm z < 1 \ f z = \ * z) \ norm \ = 1))" + using Schwarz_Lemma [OF assms] + by (metis (no_types) norm_eq_zero zero_less_one) + subsection\The Schwarz reflection principle\ lemma hol_pal_lem0: diff -r 6b76a5d1b7a5 -r deabce3ccf1f src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Oct 08 16:50:37 2017 +0200 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Oct 09 15:34:23 2017 +0100 @@ -4696,6 +4696,15 @@ finally show ?thesis . qed +lemma interior_atLeastLessThan [simp]: + fixes a::real shows "interior {a..R f (g x)) (at x)" if "x \ {a..b} - (s \ {a,b})" for x - using deriv[of x] that by (simp add: at_within_closed_interval o_def) + using deriv[of x] that by (simp add: at_within_Icc_at o_def) have "((\x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}" using le cont_int s deriv cont_int by (intro fundamental_theorem_of_calculus_interior_strong[of "s \ {a,b}"]) simp_all diff -r 6b76a5d1b7a5 -r deabce3ccf1f src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Sun Oct 08 16:50:37 2017 +0200 +++ b/src/HOL/Analysis/Path_Connected.thy Mon Oct 09 15:34:23 2017 +0100 @@ -166,6 +166,9 @@ lemma simple_path_eq_arc: "pathfinish g \ pathstart g \ (simple_path g = arc g)" by (simp add: arc_simple_path) +lemma path_image_const [simp]: "path_image (\t. a) = {a}" + by (force simp: path_image_def) + lemma path_image_nonempty [simp]: "path_image g \ {}" unfolding path_image_def image_is_empty box_eq_empty by auto @@ -1511,13 +1514,7 @@ assumes "convex s" shows "path_connected s" unfolding path_connected_def - apply rule - apply rule - apply (rule_tac x = "linepath x y" in exI) - unfolding path_image_linepath - using assms [unfolded convex_contains_segment] - apply auto - done + using assms convex_contains_segment by fastforce lemma path_connected_UNIV [iff]: "path_connected (UNIV :: 'a::real_normed_vector set)" by (simp add: convex_imp_path_connected) @@ -1528,13 +1525,7 @@ lemma path_connected_imp_connected: assumes "path_connected S" shows "connected S" - unfolding connected_def not_ex - apply rule - apply rule - apply (rule ccontr) - unfolding not_not - apply (elim conjE) -proof - +proof (rule connectedI) fix e1 e2 assume as: "open e1" "open e2" "S \ e1 \ e2" "e1 \ e2 \ S = {}" "e1 \ S \ {}" "e2 \ S \ {}" then obtain x1 x2 where obt:"x1 \ e1 \ S" "x2 \ e2 \ S" @@ -1570,31 +1561,14 @@ fix y assume as: "y \ path_component_set S x" then have "y \ S" - apply - - apply (rule path_component_mem(2)) - unfolding mem_Collect_eq - apply auto - done + by (simp add: path_component_mem(2)) then obtain e where e: "e > 0" "ball y e \ S" using assms[unfolded open_contains_ball] by auto - show "\e > 0. ball y e \ path_component_set S x" - apply (rule_tac x=e in exI) - apply (rule,rule \e>0\) - apply rule - unfolding mem_ball mem_Collect_eq - proof - - fix z - assume "dist y z < e" - then show "path_component S x z" - apply (rule_tac path_component_trans[of _ _ y]) - defer - apply (rule path_component_of_subset[OF e(2)]) - apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) - using \e > 0\ as - apply auto - done - qed +have "\u. dist y u < e \ path_component S x u" + by (metis (full_types) as centre_in_ball convex_ball convex_imp_path_connected e mem_Collect_eq mem_ball path_component_eq path_component_of_subset path_connected_component) + then show "\e > 0. ball y e \ path_component_set S x" + using \e>0\ by auto qed lemma open_non_path_component: @@ -1904,6 +1878,8 @@ using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast +subsection\Path components\ + lemma Union_path_component [simp]: "Union {path_component_set S x |x. x \ S} = S" apply (rule subset_antisym) @@ -2151,7 +2127,6 @@ by (auto simp: path_connected_component) qed - lemma connected_complement_bounded_convex: fixes s :: "'a :: euclidean_space set" assumes "bounded s" "convex s" "2 \ DIM('a)" @@ -2300,6 +2275,65 @@ qed +subsection\Every annulus is a connected set\ + +lemma path_connected_2DIM_I: + fixes a :: "'N::euclidean_space" + assumes 2: "2 \ DIM('N)" and pc: "path_connected {r. 0 \ r \ P r}" + shows "path_connected {x. P(norm(x - a))}" +proof - + have "{x. P(norm(x - a))} = op+a ` {x. P(norm x)}" + by force + moreover have "path_connected {x::'N. P(norm x)}" + proof - + let ?D = "{x. 0 \ x \ P x} \ sphere (0::'N) 1" + have "x \ (\z. fst z *\<^sub>R snd z) ` ?D" + if "P (norm x)" for x::'N + proof (cases "x=0") + case True + with that show ?thesis + apply (simp add: image_iff) + apply (rule_tac x=0 in exI, simp) + using vector_choose_size zero_le_one by blast + next + case False + with that show ?thesis + by (rule_tac x="(norm x, x /\<^sub>R norm x)" in image_eqI) auto + qed + then have *: "{x::'N. P(norm x)} = (\z. fst z *\<^sub>R snd z) ` ?D" + by auto + have "continuous_on ?D (\z:: real\'N. fst z *\<^sub>R snd z)" + by (intro continuous_intros) + moreover have "path_connected ?D" + by (metis path_connected_Times [OF pc] path_connected_sphere 2) + ultimately show ?thesis + apply (subst *) + apply (rule path_connected_continuous_image, auto) + done + qed + ultimately show ?thesis + using path_connected_translation by metis +qed + +lemma path_connected_annulus: + fixes a :: "'N::euclidean_space" + assumes "2 \ DIM('N)" + shows "path_connected {x. r1 < norm(x - a) \ norm(x - a) < r2}" + "path_connected {x. r1 < norm(x - a) \ norm(x - a) \ r2}" + "path_connected {x. r1 \ norm(x - a) \ norm(x - a) < r2}" + "path_connected {x. r1 \ norm(x - a) \ norm(x - a) \ r2}" + by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms]) + +lemma connected_annulus: + fixes a :: "'N::euclidean_space" + assumes "2 \ DIM('N::euclidean_space)" + shows "connected {x. r1 < norm(x - a) \ norm(x - a) < r2}" + "connected {x. r1 < norm(x - a) \ norm(x - a) \ r2}" + "connected {x. r1 \ norm(x - a) \ norm(x - a) < r2}" + "connected {x. r1 \ norm(x - a) \ norm(x - a) \ r2}" + by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected) + + subsection\Relations between components and path components\ lemma open_connected_component: @@ -2894,11 +2928,21 @@ shows "outside s = - s" by (metis ComplD assms convex_in_outside equalityI inside_Un_outside subsetI sup.cobounded2) +lemma outside_singleton [simp]: + fixes x :: "'a :: {real_normed_vector, perfect_space}" + shows "outside {x} = -{x}" + by (auto simp: outside_convex) + lemma inside_convex: fixes s :: "'a :: {real_normed_vector, perfect_space} set" shows "convex s \ inside s = {}" by (simp add: inside_outside outside_convex) +lemma inside_singleton [simp]: + fixes x :: "'a :: {real_normed_vector, perfect_space}" + shows "inside {x} = {}" + by (auto simp: inside_convex) + lemma outside_subset_convex: fixes s :: "'a :: {real_normed_vector, perfect_space} set" shows "\convex t; s \ t\ \ - t \ outside s" @@ -4119,6 +4163,39 @@ by (blast intro: homotopic_loops_trans) qed +lemma homotopic_paths_loop_parts: + assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)" and "path q" + shows "homotopic_paths S p q" +proof - + have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))" + using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp + then have "path p" + using \path q\ homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast + show ?thesis + proof (cases "pathfinish p = pathfinish q") + case True + have pipq: "path_image p \ S" "path_image q \ S" + by (metis Un_subset_iff paths \path p\ \path q\ homotopic_loops_imp_subset homotopic_paths_imp_path loops + path_image_join path_image_reversepath path_imp_reversepath path_join_eq)+ + have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))" + using \path p\ \path_image p \ S\ homotopic_paths_rid homotopic_paths_sym by blast + moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))" + by (simp add: True \path p\ \path q\ pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym) + moreover have "homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)" + by (simp add: True \path p\ \path q\ homotopic_paths_assoc pipq) + moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)" + by (simp add: \path q\ homotopic_paths_join paths pipq) + moreover then have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ q) q" + by (metis \path q\ homotopic_paths_imp_path homotopic_paths_lid linepath_trivial path_join_path_ends pathfinish_def pipq(2)) + ultimately show ?thesis + using homotopic_paths_trans by metis + next + case False + then show ?thesis + using \path q\ homotopic_loops_imp_path loops path_join_path_ends by fastforce + qed +qed + subsection\ Homotopy of "nearby" function, paths and loops.\ diff -r 6b76a5d1b7a5 -r deabce3ccf1f src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Sun Oct 08 16:50:37 2017 +0200 +++ b/src/HOL/Analysis/Starlike.thy Mon Oct 09 15:34:23 2017 +0100 @@ -3776,24 +3776,6 @@ subsection\Explicit formulas for interior and relative interior of convex hull\ -lemma interior_atLeastAtMost [simp]: - fixes a::real shows "interior {a..b} = {a<.. x < b \ (at x within {a..b}) = at x" - by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost) - lemma at_within_cbox_finite: assumes "x \ box a b" "x \ S" "finite S" shows "(at x within cbox a b - S) = at x" @@ -5087,7 +5069,6 @@ using separation_closures [of S T] by (metis assms closure_closed disjnt_def inf_commute) - lemma separation_normal_local: fixes S :: "'a::euclidean_space set" assumes US: "closedin (subtopology euclidean U) S" @@ -5147,6 +5128,139 @@ by auto (meson bounded_ball bounded_subset compl_le_swap2 disjoint_eq_subset_Compl) qed +subsection\Connectedness of the intersection of a chain\ + +proposition connected_chain: + fixes \ :: "'a :: euclidean_space set set" + assumes cc: "\S. S \ \ \ compact S \ connected S" + and linear: "\S T. S \ \ \ T \ \ \ S \ T \ T \ S" + shows "connected(\\)" +proof (cases "\ = {}") + case True then show ?thesis + by auto +next + case False + then have cf: "compact(\\)" + by (simp add: cc compact_Inter) + have False if AB: "closed A" "closed B" "A \ B = {}" + and ABeq: "A \ B = \\" and "A \ {}" "B \ {}" for A B + proof - + obtain U V where "open U" "open V" "A \ U" "B \ V" "U \ V = {}" + using separation_normal [OF AB] by metis + obtain K where "K \ \" "compact K" + using cc False by blast + then obtain N where "open N" and "K \ N" + by blast + let ?\ = "insert (U \ V) ((\S. N - S) ` \)" + obtain \ where "\ \ ?\" "finite \" "K \ \\" + proof (rule compactE [OF \compact K\]) + show "K \ \insert (U \ V) (op - N ` \)" + using \K \ N\ ABeq \A \ U\ \B \ V\ by auto + show "\B. B \ insert (U \ V) (op - N ` \) \ open B" + by (auto simp: \open U\ \open V\ open_Un \open N\ cc compact_imp_closed open_Diff) + qed + then have "finite(\ - {U \ V})" + by blast + moreover have "\ - {U \ V} \ (\S. N - S) ` \" + using \\ \ ?\\ by blast + ultimately obtain \ where "\ \ \" "finite \" and Deq: "\ - {U \ V} = (\S. N-S) ` \" + using finite_subset_image by metis + obtain J where "J \ \" and J: "(\S\\. N - S) \ N - J" + proof (cases "\ = {}") + case True + with \\ \ {}\ that show ?thesis + by auto + next + case False + have "\S T. \S \ \; T \ \\ \ S \ T \ T \ S" + by (meson \\ \ \\ in_mono local.linear) + with \finite \\ \\ \ {}\ + have "\J \ \. (\S\\. N - S) \ N - J" + proof induction + case (insert X \) + show ?case + proof (cases "\ = {}") + case True then show ?thesis by auto + next + case False + then have "\S T. \S \ \; T \ \\ \ S \ T \ T \ S" + by (simp add: insert.prems) + with insert.IH False obtain J where "J \ \" and J: "(\Y\\. N - Y) \ N - J" + by metis + have "N - J \ N - X \ N - X \ N - J" + by (meson Diff_mono \J \ \\ insert.prems(2) insert_iff order_refl) + then show ?thesis + proof + assume "N - J \ N - X" with J show ?thesis + by auto + next + assume "N - X \ N - J" + with J have "N - X \ UNION \ (op - N) \ N - J" + by auto + with \J \ \\ show ?thesis + by blast + qed + qed + qed simp + with \\ \ \\ show ?thesis by (blast intro: that) + qed + have "K \ \(insert (U \ V) (\ - {U \ V}))" + using \K \ \\\ by auto + also have "... \ (U \ V) \ (N - J)" + by (metis (no_types, hide_lams) Deq Un_subset_iff Un_upper2 J Union_insert order_trans sup_ge1) + finally have "J \ K \ U \ V" + by blast + moreover have "connected(J \ K)" + by (metis Int_absorb1 \J \ \\ \K \ \\ cc inf.orderE local.linear) + moreover have "U \ (J \ K) \ {}" + using ABeq \J \ \\ \K \ \\ \