--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Aug 28 00:08:14 2019 +0200
@@ -19,6 +19,7 @@
Path_Connected
Homeomorphism
Continuous_Extension
+ Derivative
begin
subsection \<open>Retractions\<close>
@@ -4936,4 +4937,249 @@
shows "connected(-S)"
using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast
+subsubsection \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
+
+lemma brouwer_surjective:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+ assumes "compact T"
+ and "convex T"
+ and "T \<noteq> {}"
+ and "continuous_on T f"
+ and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
+ and "x \<in> S"
+ shows "\<exists>y\<in>T. f y = x"
+proof -
+ have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
+ by (auto simp add: algebra_simps)
+ show ?thesis
+ unfolding *
+ apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
+ apply (intro continuous_intros)
+ using assms
+ apply auto
+ done
+qed
+
+lemma brouwer_surjective_cball:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+ assumes "continuous_on (cball a e) f"
+ and "e > 0"
+ and "x \<in> S"
+ and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
+ shows "\<exists>y\<in>cball a e. f y = x"
+ apply (rule brouwer_surjective)
+ apply (rule compact_cball convex_cball)+
+ unfolding cball_eq_empty
+ using assms
+ apply auto
+ done
+
+subsubsection \<open>Inverse function theorem\<close>
+
+text \<open>See Sussmann: "Multidifferential calculus", Theorem 2.1.1\<close>
+
+lemma sussmann_open_mapping:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+ assumes "open S"
+ and contf: "continuous_on S f"
+ and "x \<in> S"
+ and derf: "(f has_derivative f') (at x)"
+ and "bounded_linear g'" "f' \<circ> g' = id"
+ and "T \<subseteq> S"
+ and x: "x \<in> interior T"
+ shows "f x \<in> interior (f ` T)"
+proof -
+ interpret f': bounded_linear f'
+ using assms unfolding has_derivative_def by auto
+ interpret g': bounded_linear g'
+ using assms by auto
+ obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
+ using bounded_linear.pos_bounded[OF assms(5)] by blast
+ hence *: "1 / (2 * B) > 0" by auto
+ obtain e0 where e0:
+ "0 < e0"
+ "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
+ using derf unfolding has_derivative_at_alt
+ using * by blast
+ obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
+ using mem_interior_cball x by blast
+ have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
+ obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
+ using field_lbound_gt_zero[OF *] by blast
+ have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
+ proof (rule brouwer_surjective_cball)
+ have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
+ proof-
+ have "dist x z = norm (g' (f x) - g' y)"
+ unfolding as(2) and dist_norm by auto
+ also have "\<dots> \<le> norm (f x - y) * B"
+ by (metis B(2) g'.diff)
+ also have "\<dots> \<le> e * B"
+ by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
+ also have "\<dots> \<le> e1"
+ using B(1) e(3) pos_less_divide_eq by fastforce
+ finally have "z \<in> cball x e1"
+ by force
+ then show "z \<in> S"
+ using e1 assms(7) by auto
+ qed
+ show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
+ unfolding g'.diff
+ proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
+ show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
+ by (rule continuous_on_subset[OF contf]) (use z in blast)
+ show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
+ by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
+ qed
+ next
+ fix y z
+ assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
+ have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
+ using B by auto
+ also have "\<dots> \<le> e * B"
+ by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
+ also have "\<dots> < e0"
+ using B(1) e(2) pos_less_divide_eq by blast
+ finally have *: "norm (x + g' (z - f x) - x) < e0"
+ by auto
+ have **: "f x + f' (x + g' (z - f x) - x) = z"
+ using assms(6)[unfolded o_def id_def,THEN cong]
+ by auto
+ have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
+ norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
+ using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
+ by (auto simp add: algebra_simps)
+ also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
+ using e0(2)[rule_format, OF *]
+ by (simp only: algebra_simps **) auto
+ also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
+ using y by (auto simp: dist_norm)
+ also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
+ using * B by (auto simp add: field_simps)
+ also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
+ by auto
+ also have "\<dots> \<le> e/2 + e/2"
+ using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
+ finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
+ by (auto simp: dist_norm)
+ qed (use e that in auto)
+ show ?thesis
+ unfolding mem_interior
+ proof (intro exI conjI subsetI)
+ fix y
+ assume "y \<in> ball (f x) (e / 2)"
+ then have *: "y \<in> cball (f x) (e / 2)"
+ by auto
+ obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
+ using lem * by blast
+ then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
+ using B
+ by (auto simp add: field_simps)
+ also have "\<dots> \<le> e * B"
+ by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
+ also have "\<dots> \<le> e1"
+ using e B unfolding less_divide_eq by auto
+ finally have "x + g'(z - f x) \<in> T"
+ by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
+ then show "y \<in> f ` T"
+ using z by auto
+ qed (use e in auto)
+qed
+
+text \<open>Hence the following eccentric variant of the inverse function theorem.
+ This has no continuity assumptions, but we do need the inverse function.
+ We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
+ algebra theory I've set up so far.\<close>
+
+lemma has_derivative_inverse_strong:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+ assumes "open S"
+ and "x \<in> S"
+ and contf: "continuous_on S f"
+ and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+ and derf: "(f has_derivative f') (at x)"
+ and id: "f' \<circ> g' = id"
+ shows "(g has_derivative g') (at (f x))"
+proof -
+ have linf: "bounded_linear f'"
+ using derf unfolding has_derivative_def by auto
+ then have ling: "bounded_linear g'"
+ unfolding linear_conv_bounded_linear[symmetric]
+ using id right_inverse_linear by blast
+ moreover have "g' \<circ> f' = id"
+ using id linf ling
+ unfolding linear_conv_bounded_linear[symmetric]
+ using linear_inverse_left
+ by auto
+ moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
+ apply (rule sussmann_open_mapping)
+ apply (rule assms ling)+
+ apply auto
+ done
+ have "continuous (at (f x)) g"
+ unfolding continuous_at Lim_at
+ proof (rule, rule)
+ fix e :: real
+ assume "e > 0"
+ then have "f x \<in> interior (f ` (ball x e \<inter> S))"
+ using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
+ by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
+ then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
+ unfolding mem_interior by blast
+ show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
+ proof (intro exI allI impI conjI)
+ fix y
+ assume "0 < dist y (f x) \<and> dist y (f x) < d"
+ then have "g y \<in> g ` f ` (ball x e \<inter> S)"
+ by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
+ then show "dist (g y) (g (f x)) < e"
+ using gf[OF \<open>x \<in> S\<close>]
+ by (simp add: assms(4) dist_commute image_iff)
+ qed (use d in auto)
+ qed
+ moreover have "f x \<in> interior (f ` S)"
+ apply (rule sussmann_open_mapping)
+ apply (rule assms ling)+
+ using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
+ apply auto
+ done
+ moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
+ by (metis gf imageE interiorE subsetD that)
+ ultimately show ?thesis using assms
+ by (metis has_derivative_inverse_basic_x open_interior)
+qed
+
+text \<open>A rewrite based on the other domain.\<close>
+
+lemma has_derivative_inverse_strong_x:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+ assumes "open S"
+ and "g y \<in> S"
+ and "continuous_on S f"
+ and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+ and "(f has_derivative f') (at (g y))"
+ and "f' \<circ> g' = id"
+ and "f (g y) = y"
+ shows "(g has_derivative g') (at y)"
+ using has_derivative_inverse_strong[OF assms(1-6)]
+ unfolding assms(7)
+ by simp
+
+text \<open>On a region.\<close>
+
+theorem has_derivative_inverse_on:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+ assumes "open S"
+ and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
+ and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+ and "f' x \<circ> g' x = id"
+ and "x \<in> S"
+ shows "(g has_derivative g'(x)) (at (f x))"
+proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
+ show "continuous_on S f"
+ unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
+ using derf has_derivative_continuous by blast
+qed (use assms in auto)
+
+
end
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed Aug 28 00:08:14 2019 +0200
@@ -5,7 +5,7 @@
section \<open>Complex Analysis Basics\<close>
theory Complex_Analysis_Basics
- imports Derivative "HOL-Library.Nonpos_Ints"
+ imports Brouwer_Fixpoint "HOL-Library.Nonpos_Ints"
begin
(* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
--- a/src/HOL/Analysis/Derivative.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy Wed Aug 28 00:08:14 2019 +0200
@@ -6,7 +6,11 @@
section \<open>Derivative\<close>
theory Derivative
-imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
+ imports
+ Path_Connected
+ Operator_Norm
+ Uniform_Limit
+ Bounded_Linear_Function
begin
declare bounded_linear_inner_left [intro]
@@ -1203,251 +1207,6 @@
qed
-subsection \<open>Inverse function theorem\<close>
-
-text \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
-
-lemma brouwer_surjective:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
- assumes "compact T"
- and "convex T"
- and "T \<noteq> {}"
- and "continuous_on T f"
- and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
- and "x \<in> S"
- shows "\<exists>y\<in>T. f y = x"
-proof -
- have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
- by (auto simp add: algebra_simps)
- show ?thesis
- unfolding *
- apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
- apply (intro continuous_intros)
- using assms
- apply auto
- done
-qed
-
-lemma brouwer_surjective_cball:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
- assumes "continuous_on (cball a e) f"
- and "e > 0"
- and "x \<in> S"
- and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
- shows "\<exists>y\<in>cball a e. f y = x"
- apply (rule brouwer_surjective)
- apply (rule compact_cball convex_cball)+
- unfolding cball_eq_empty
- using assms
- apply auto
- done
-
-text \<open>See Sussmann: "Multidifferential calculus", Theorem 2.1.1\<close>
-
-lemma sussmann_open_mapping:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
- assumes "open S"
- and contf: "continuous_on S f"
- and "x \<in> S"
- and derf: "(f has_derivative f') (at x)"
- and "bounded_linear g'" "f' \<circ> g' = id"
- and "T \<subseteq> S"
- and x: "x \<in> interior T"
- shows "f x \<in> interior (f ` T)"
-proof -
- interpret f': bounded_linear f'
- using assms unfolding has_derivative_def by auto
- interpret g': bounded_linear g'
- using assms by auto
- obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
- using bounded_linear.pos_bounded[OF assms(5)] by blast
- hence *: "1 / (2 * B) > 0" by auto
- obtain e0 where e0:
- "0 < e0"
- "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
- using derf unfolding has_derivative_at_alt
- using * by blast
- obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
- using mem_interior_cball x by blast
- have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
- obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
- using field_lbound_gt_zero[OF *] by blast
- have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
- proof (rule brouwer_surjective_cball)
- have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
- proof-
- have "dist x z = norm (g' (f x) - g' y)"
- unfolding as(2) and dist_norm by auto
- also have "\<dots> \<le> norm (f x - y) * B"
- by (metis B(2) g'.diff)
- also have "\<dots> \<le> e * B"
- by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
- also have "\<dots> \<le> e1"
- using B(1) e(3) pos_less_divide_eq by fastforce
- finally have "z \<in> cball x e1"
- by force
- then show "z \<in> S"
- using e1 assms(7) by auto
- qed
- show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
- unfolding g'.diff
- proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
- show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
- by (rule continuous_on_subset[OF contf]) (use z in blast)
- show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
- by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
- qed
- next
- fix y z
- assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
- have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
- using B by auto
- also have "\<dots> \<le> e * B"
- by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
- also have "\<dots> < e0"
- using B(1) e(2) pos_less_divide_eq by blast
- finally have *: "norm (x + g' (z - f x) - x) < e0"
- by auto
- have **: "f x + f' (x + g' (z - f x) - x) = z"
- using assms(6)[unfolded o_def id_def,THEN cong]
- by auto
- have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
- norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
- using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
- by (auto simp add: algebra_simps)
- also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
- using e0(2)[rule_format, OF *]
- by (simp only: algebra_simps **) auto
- also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
- using y by (auto simp: dist_norm)
- also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
- using * B by (auto simp add: field_simps)
- also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
- by auto
- also have "\<dots> \<le> e/2 + e/2"
- using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
- finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
- by (auto simp: dist_norm)
- qed (use e that in auto)
- show ?thesis
- unfolding mem_interior
- proof (intro exI conjI subsetI)
- fix y
- assume "y \<in> ball (f x) (e / 2)"
- then have *: "y \<in> cball (f x) (e / 2)"
- by auto
- obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
- using lem * by blast
- then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
- using B
- by (auto simp add: field_simps)
- also have "\<dots> \<le> e * B"
- by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
- also have "\<dots> \<le> e1"
- using e B unfolding less_divide_eq by auto
- finally have "x + g'(z - f x) \<in> T"
- by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
- then show "y \<in> f ` T"
- using z by auto
- qed (use e in auto)
-qed
-
-text \<open>Hence the following eccentric variant of the inverse function theorem.
- This has no continuity assumptions, but we do need the inverse function.
- We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
- algebra theory I've set up so far.\<close>
-
-lemma has_derivative_inverse_strong:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
- assumes "open S"
- and "x \<in> S"
- and contf: "continuous_on S f"
- and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
- and derf: "(f has_derivative f') (at x)"
- and id: "f' \<circ> g' = id"
- shows "(g has_derivative g') (at (f x))"
-proof -
- have linf: "bounded_linear f'"
- using derf unfolding has_derivative_def by auto
- then have ling: "bounded_linear g'"
- unfolding linear_conv_bounded_linear[symmetric]
- using id right_inverse_linear by blast
- moreover have "g' \<circ> f' = id"
- using id linf ling
- unfolding linear_conv_bounded_linear[symmetric]
- using linear_inverse_left
- by auto
- moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
- apply (rule sussmann_open_mapping)
- apply (rule assms ling)+
- apply auto
- done
- have "continuous (at (f x)) g"
- unfolding continuous_at Lim_at
- proof (rule, rule)
- fix e :: real
- assume "e > 0"
- then have "f x \<in> interior (f ` (ball x e \<inter> S))"
- using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
- by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
- then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
- unfolding mem_interior by blast
- show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
- proof (intro exI allI impI conjI)
- fix y
- assume "0 < dist y (f x) \<and> dist y (f x) < d"
- then have "g y \<in> g ` f ` (ball x e \<inter> S)"
- by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
- then show "dist (g y) (g (f x)) < e"
- using gf[OF \<open>x \<in> S\<close>]
- by (simp add: assms(4) dist_commute image_iff)
- qed (use d in auto)
- qed
- moreover have "f x \<in> interior (f ` S)"
- apply (rule sussmann_open_mapping)
- apply (rule assms ling)+
- using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
- apply auto
- done
- moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
- by (metis gf imageE interiorE subsetD that)
- ultimately show ?thesis using assms
- by (metis has_derivative_inverse_basic_x open_interior)
-qed
-
-text \<open>A rewrite based on the other domain.\<close>
-
-lemma has_derivative_inverse_strong_x:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
- assumes "open S"
- and "g y \<in> S"
- and "continuous_on S f"
- and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
- and "(f has_derivative f') (at (g y))"
- and "f' \<circ> g' = id"
- and "f (g y) = y"
- shows "(g has_derivative g') (at y)"
- using has_derivative_inverse_strong[OF assms(1-6)]
- unfolding assms(7)
- by simp
-
-text \<open>On a region.\<close>
-
-theorem has_derivative_inverse_on:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
- assumes "open S"
- and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
- and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
- and "f' x \<circ> g' x = id"
- and "x \<in> S"
- shows "(g has_derivative g'(x)) (at (f x))"
-proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
- show "continuous_on S f"
- unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
- using derf has_derivative_continuous by blast
-qed (use assms in auto)
-
-
text \<open>Invertible derivative continuous at a point implies local
injectivity. It's only for this we need continuity of the derivative,
except of course if we want the fact that the inverse derivative is
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Aug 28 00:08:14 2019 +0200
@@ -5,7 +5,7 @@
*)
theory Equivalence_Lebesgue_Henstock_Integration
- imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
+ imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral Homeomorphism
begin
lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
--- a/src/HOL/Analysis/Further_Topology.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Wed Aug 28 00:08:14 2019 +0200
@@ -6,6 +6,18 @@
imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration
begin
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Retracts and intervals in ordered euclidean space\<close>
+
+lemma ANR_interval [iff]:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "ANR{a..b}"
+ by (simp add: interval_cbox)
+
+lemma ENR_interval [iff]:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "ENR{a..b}"
+ by (auto simp: interval_cbox)
+
subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
lemma spheremap_lemma1:
--- a/src/HOL/Analysis/Homeomorphism.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Wed Aug 28 00:08:14 2019 +0200
@@ -38,246 +38,6 @@
subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
-proposition ray_to_rel_frontier:
- fixes a :: "'a::real_inner"
- assumes "bounded S"
- and a: "a \<in> rel_interior S"
- and aff: "(a + l) \<in> affine hull S"
- and "l \<noteq> 0"
- obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
- "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
-proof -
- have aaff: "a \<in> affine hull S"
- by (meson a hull_subset rel_interior_subset rev_subsetD)
- let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
- obtain B where "B > 0" and B: "S \<subseteq> ball a B"
- using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast
- have "a + (B / norm l) *\<^sub>R l \<notin> ball a B"
- by (simp add: dist_norm \<open>l \<noteq> 0\<close>)
- with B have "a + (B / norm l) *\<^sub>R l \<notin> rel_interior S"
- using rel_interior_subset subsetCE by blast
- with \<open>B > 0\<close> \<open>l \<noteq> 0\<close> have nonMT: "?D \<noteq> {}"
- using divide_pos_pos zero_less_norm_iff by fastforce
- have bdd: "bdd_below ?D"
- by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq)
- have relin_Ex: "\<And>x. x \<in> rel_interior S \<Longrightarrow>
- \<exists>e>0. \<forall>x'\<in>affine hull S. dist x' x < e \<longrightarrow> x' \<in> rel_interior S"
- using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff)
- define d where "d = Inf ?D"
- obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "\<And>\<eta>. \<lbrakk>0 \<le> \<eta>; \<eta> < \<epsilon>\<rbrakk> \<Longrightarrow> (a + \<eta> *\<^sub>R l) \<in> rel_interior S"
- proof -
- obtain e where "e>0"
- and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' a < e \<Longrightarrow> x' \<in> rel_interior S"
- using relin_Ex a by blast
- show thesis
- proof (rule_tac \<epsilon> = "e / norm l" in that)
- show "0 < e / norm l" by (simp add: \<open>0 < e\<close> \<open>l \<noteq> 0\<close>)
- next
- show "a + \<eta> *\<^sub>R l \<in> rel_interior S" if "0 \<le> \<eta>" "\<eta> < e / norm l" for \<eta>
- proof (rule e)
- show "a + \<eta> *\<^sub>R l \<in> affine hull S"
- by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
- show "dist (a + \<eta> *\<^sub>R l) a < e"
- using that by (simp add: \<open>l \<noteq> 0\<close> dist_norm pos_less_divide_eq)
- qed
- qed
- qed
- have inint: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> a + e *\<^sub>R l \<in> rel_interior S"
- unfolding d_def using cInf_lower [OF _ bdd]
- by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left)
- have "\<epsilon> \<le> d"
- unfolding d_def
- apply (rule cInf_greatest [OF nonMT])
- using \<epsilon> dual_order.strict_implies_order le_less_linear by blast
- with \<open>0 < \<epsilon>\<close> have "0 < d" by simp
- have "a + d *\<^sub>R l \<notin> rel_interior S"
- proof
- assume adl: "a + d *\<^sub>R l \<in> rel_interior S"
- obtain e where "e > 0"
- and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S"
- using relin_Ex adl by blast
- have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
- proof (rule cInf_greatest [OF nonMT], clarsimp)
- fix x::real
- assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S"
- show "d + e / norm l \<le> x"
- proof (cases "x < d")
- case True with inint nonrel \<open>0 < x\<close>
- show ?thesis by auto
- next
- case False
- then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e"
- by (simp add: field_simps \<open>l \<noteq> 0\<close>)
- have ain: "a + x *\<^sub>R l \<in> affine hull S"
- by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
- show ?thesis
- using e [OF ain] nonrel dle by force
- qed
- qed
- then show False
- using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps)
- qed
- moreover have "a + d *\<^sub>R l \<in> closure S"
- proof (clarsimp simp: closure_approachable)
- fix \<eta>::real assume "0 < \<eta>"
- have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S"
- apply (rule subsetD [OF rel_interior_subset inint])
- using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto
- have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))"
- by (metis min_def mult_left_mono norm_ge_zero order_refl)
- also have "... < \<eta>"
- using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps)
- finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" .
- show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>"
- apply (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI)
- using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps)
- done
- qed
- ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S"
- by (simp add: rel_frontier_def)
- show ?thesis
- by (rule that [OF \<open>0 < d\<close> infront inint])
-qed
-
-corollary ray_to_frontier:
- fixes a :: "'a::euclidean_space"
- assumes "bounded S"
- and a: "a \<in> interior S"
- and "l \<noteq> 0"
- obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
- "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
-proof -
- have "interior S = rel_interior S"
- using a rel_interior_nonempty_interior by auto
- then have "a \<in> rel_interior S"
- using a by simp
- then show ?thesis
- apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>])
- using a affine_hull_nonempty_interior apply blast
- by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
-qed
-
-
-lemma segment_to_rel_frontier_aux:
- fixes x :: "'a::euclidean_space"
- assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
- obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
- "open_segment x z \<subseteq> rel_interior S"
-proof -
- have "x + (y - x) \<in> affine hull S"
- using hull_inc [OF y] by auto
- then obtain d where "0 < d" and df: "(x + d *\<^sub>R (y-x)) \<in> rel_frontier S"
- and di: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (x + e *\<^sub>R (y-x)) \<in> rel_interior S"
- by (rule ray_to_rel_frontier [OF \<open>bounded S\<close> x]) (use xy in auto)
- show ?thesis
- proof
- show "x + d *\<^sub>R (y - x) \<in> rel_frontier S"
- by (simp add: df)
- next
- have "open_segment x y \<subseteq> rel_interior S"
- using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast
- moreover have "x + d *\<^sub>R (y - x) \<in> open_segment x y" if "d < 1"
- using xy
- apply (auto simp: in_segment)
- apply (rule_tac x="d" in exI)
- using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps)
- done
- ultimately have "1 \<le> d"
- using df rel_frontier_def by fastforce
- moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x"
- by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
- ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y - x))"
- apply (auto simp: in_segment)
- apply (rule_tac x="1/d" in exI)
- apply (auto simp: divide_simps algebra_simps)
- done
- next
- show "open_segment x (x + d *\<^sub>R (y - x)) \<subseteq> rel_interior S"
- apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x])
- using df rel_frontier_def by auto
- qed
-qed
-
-lemma segment_to_rel_frontier:
- fixes x :: "'a::euclidean_space"
- assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
- and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
- obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
- "open_segment x z \<subseteq> rel_interior S"
-proof (cases "x=y")
- case True
- with xy have "S \<noteq> {x}"
- by blast
- with True show ?thesis
- by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y)
-next
- case False
- then show ?thesis
- using segment_to_rel_frontier_aux [OF S x y] that by blast
-qed
-
-proposition rel_frontier_not_sing:
- fixes a :: "'a::euclidean_space"
- assumes "bounded S"
- shows "rel_frontier S \<noteq> {a}"
-proof (cases "S = {}")
- case True then show ?thesis by simp
-next
- case False
- then obtain z where "z \<in> S"
- by blast
- then show ?thesis
- proof (cases "S = {z}")
- case True then show ?thesis by simp
- next
- case False
- then obtain w where "w \<in> S" "w \<noteq> z"
- using \<open>z \<in> S\<close> by blast
- show ?thesis
- proof
- assume "rel_frontier S = {a}"
- then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S"
- using \<open>w \<noteq> z\<close> by auto
- then show False
- proof cases
- case 1
- then have w: "w \<in> rel_interior S"
- using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce
- have "w + (w - z) \<in> affine hull S"
- by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
- then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S"
- using \<open>w \<noteq> z\<close> \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w)
- moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S"
- using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z - w)"] \<open>w \<noteq> z\<close> \<open>z \<in> S\<close>
- by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
- ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)"
- using \<open>rel_frontier S = {a}\<close> by force
- moreover have "e \<noteq> -d "
- using \<open>0 < e\<close> \<open>0 < d\<close> by force
- ultimately show False
- by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
- next
- case 2
- then have z: "z \<in> rel_interior S"
- using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce
- have "z + (z - w) \<in> affine hull S"
- by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
- then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S"
- using \<open>w \<noteq> z\<close> \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z)
- moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S"
- using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w - z)"] \<open>w \<noteq> z\<close> \<open>w \<in> S\<close>
- by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
- ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)"
- using \<open>rel_frontier S = {a}\<close> by force
- moreover have "e \<noteq> -d "
- using \<open>0 < e\<close> \<open>0 < d\<close> by force
- ultimately show False
- by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
- qed
- qed
- qed
-qed
-
proposition
fixes S :: "'a::euclidean_space set"
assumes "compact S" and 0: "0 \<in> rel_interior S"
@@ -1268,6 +1028,20 @@
using assms
by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
+lemma homeomorphic_closed_intervals:
+ fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
+ assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
+ shows "(cbox a b) homeomorphic (cbox c d)"
+apply (rule homeomorphic_convex_compact)
+using assms apply auto
+done
+
+lemma homeomorphic_closed_intervals_real:
+ fixes a::real and b and c::real and d
+ assumes "a<b" and "c<d"
+ shows "{a..b} homeomorphic {c..d}"
+ using assms by (auto intro: homeomorphic_convex_compact)
+
subsection\<open>Covering spaces and lifting results for them\<close>
definition\<^marker>\<open>tag important\<close> covering_space
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Aug 28 00:08:14 2019 +0200
@@ -300,20 +300,6 @@
shows "compact {a .. b}"
by (metis compact_cbox interval_cbox)
-lemma homeomorphic_closed_intervals:
- fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
- assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
- shows "(cbox a b) homeomorphic (cbox c d)"
-apply (rule homeomorphic_convex_compact)
-using assms apply auto
-done
-
-lemma homeomorphic_closed_intervals_real:
- fixes a::real and b and c::real and d
- assumes "a<b" and "c<d"
- shows "{a..b} homeomorphic {c..d}"
- using assms by (auto intro: homeomorphic_convex_compact)
-
no_notation
eucl_less (infix "<e" 50)
@@ -349,15 +335,5 @@
end
-lemma ANR_interval [iff]:
- fixes a :: "'a::ordered_euclidean_space"
- shows "ANR{a..b}"
-by (simp add: interval_cbox)
-
-lemma ENR_interval [iff]:
- fixes a :: "'a::ordered_euclidean_space"
- shows "ENR{a..b}"
- by (auto simp: interval_cbox)
-
end
--- a/src/HOL/Analysis/Starlike.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Starlike.thy Wed Aug 28 00:08:14 2019 +0200
@@ -3357,6 +3357,246 @@
then show "?lhs \<supseteq> ?rhs" by blast
qed
+proposition ray_to_rel_frontier:
+ fixes a :: "'a::real_inner"
+ assumes "bounded S"
+ and a: "a \<in> rel_interior S"
+ and aff: "(a + l) \<in> affine hull S"
+ and "l \<noteq> 0"
+ obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
+ "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
+proof -
+ have aaff: "a \<in> affine hull S"
+ by (meson a hull_subset rel_interior_subset rev_subsetD)
+ let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
+ obtain B where "B > 0" and B: "S \<subseteq> ball a B"
+ using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast
+ have "a + (B / norm l) *\<^sub>R l \<notin> ball a B"
+ by (simp add: dist_norm \<open>l \<noteq> 0\<close>)
+ with B have "a + (B / norm l) *\<^sub>R l \<notin> rel_interior S"
+ using rel_interior_subset subsetCE by blast
+ with \<open>B > 0\<close> \<open>l \<noteq> 0\<close> have nonMT: "?D \<noteq> {}"
+ using divide_pos_pos zero_less_norm_iff by fastforce
+ have bdd: "bdd_below ?D"
+ by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq)
+ have relin_Ex: "\<And>x. x \<in> rel_interior S \<Longrightarrow>
+ \<exists>e>0. \<forall>x'\<in>affine hull S. dist x' x < e \<longrightarrow> x' \<in> rel_interior S"
+ using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff)
+ define d where "d = Inf ?D"
+ obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "\<And>\<eta>. \<lbrakk>0 \<le> \<eta>; \<eta> < \<epsilon>\<rbrakk> \<Longrightarrow> (a + \<eta> *\<^sub>R l) \<in> rel_interior S"
+ proof -
+ obtain e where "e>0"
+ and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' a < e \<Longrightarrow> x' \<in> rel_interior S"
+ using relin_Ex a by blast
+ show thesis
+ proof (rule_tac \<epsilon> = "e / norm l" in that)
+ show "0 < e / norm l" by (simp add: \<open>0 < e\<close> \<open>l \<noteq> 0\<close>)
+ next
+ show "a + \<eta> *\<^sub>R l \<in> rel_interior S" if "0 \<le> \<eta>" "\<eta> < e / norm l" for \<eta>
+ proof (rule e)
+ show "a + \<eta> *\<^sub>R l \<in> affine hull S"
+ by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
+ show "dist (a + \<eta> *\<^sub>R l) a < e"
+ using that by (simp add: \<open>l \<noteq> 0\<close> dist_norm pos_less_divide_eq)
+ qed
+ qed
+ qed
+ have inint: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> a + e *\<^sub>R l \<in> rel_interior S"
+ unfolding d_def using cInf_lower [OF _ bdd]
+ by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left)
+ have "\<epsilon> \<le> d"
+ unfolding d_def
+ apply (rule cInf_greatest [OF nonMT])
+ using \<epsilon> dual_order.strict_implies_order le_less_linear by blast
+ with \<open>0 < \<epsilon>\<close> have "0 < d" by simp
+ have "a + d *\<^sub>R l \<notin> rel_interior S"
+ proof
+ assume adl: "a + d *\<^sub>R l \<in> rel_interior S"
+ obtain e where "e > 0"
+ and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S"
+ using relin_Ex adl by blast
+ have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
+ proof (rule cInf_greatest [OF nonMT], clarsimp)
+ fix x::real
+ assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S"
+ show "d + e / norm l \<le> x"
+ proof (cases "x < d")
+ case True with inint nonrel \<open>0 < x\<close>
+ show ?thesis by auto
+ next
+ case False
+ then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e"
+ by (simp add: field_simps \<open>l \<noteq> 0\<close>)
+ have ain: "a + x *\<^sub>R l \<in> affine hull S"
+ by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
+ show ?thesis
+ using e [OF ain] nonrel dle by force
+ qed
+ qed
+ then show False
+ using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps)
+ qed
+ moreover have "a + d *\<^sub>R l \<in> closure S"
+ proof (clarsimp simp: closure_approachable)
+ fix \<eta>::real assume "0 < \<eta>"
+ have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S"
+ apply (rule subsetD [OF rel_interior_subset inint])
+ using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto
+ have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))"
+ by (metis min_def mult_left_mono norm_ge_zero order_refl)
+ also have "... < \<eta>"
+ using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps)
+ finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" .
+ show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>"
+ apply (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI)
+ using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps)
+ done
+ qed
+ ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S"
+ by (simp add: rel_frontier_def)
+ show ?thesis
+ by (rule that [OF \<open>0 < d\<close> infront inint])
+qed
+
+corollary ray_to_frontier:
+ fixes a :: "'a::euclidean_space"
+ assumes "bounded S"
+ and a: "a \<in> interior S"
+ and "l \<noteq> 0"
+ obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
+ "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
+proof -
+ have "interior S = rel_interior S"
+ using a rel_interior_nonempty_interior by auto
+ then have "a \<in> rel_interior S"
+ using a by simp
+ then show ?thesis
+ apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>])
+ using a affine_hull_nonempty_interior apply blast
+ by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
+qed
+
+
+lemma segment_to_rel_frontier_aux:
+ fixes x :: "'a::euclidean_space"
+ assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
+ obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
+ "open_segment x z \<subseteq> rel_interior S"
+proof -
+ have "x + (y - x) \<in> affine hull S"
+ using hull_inc [OF y] by auto
+ then obtain d where "0 < d" and df: "(x + d *\<^sub>R (y-x)) \<in> rel_frontier S"
+ and di: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (x + e *\<^sub>R (y-x)) \<in> rel_interior S"
+ by (rule ray_to_rel_frontier [OF \<open>bounded S\<close> x]) (use xy in auto)
+ show ?thesis
+ proof
+ show "x + d *\<^sub>R (y - x) \<in> rel_frontier S"
+ by (simp add: df)
+ next
+ have "open_segment x y \<subseteq> rel_interior S"
+ using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast
+ moreover have "x + d *\<^sub>R (y - x) \<in> open_segment x y" if "d < 1"
+ using xy
+ apply (auto simp: in_segment)
+ apply (rule_tac x="d" in exI)
+ using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps)
+ done
+ ultimately have "1 \<le> d"
+ using df rel_frontier_def by fastforce
+ moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x"
+ by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
+ ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y - x))"
+ apply (auto simp: in_segment)
+ apply (rule_tac x="1/d" in exI)
+ apply (auto simp: divide_simps algebra_simps)
+ done
+ next
+ show "open_segment x (x + d *\<^sub>R (y - x)) \<subseteq> rel_interior S"
+ apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x])
+ using df rel_frontier_def by auto
+ qed
+qed
+
+lemma segment_to_rel_frontier:
+ fixes x :: "'a::euclidean_space"
+ assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
+ and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
+ obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
+ "open_segment x z \<subseteq> rel_interior S"
+proof (cases "x=y")
+ case True
+ with xy have "S \<noteq> {x}"
+ by blast
+ with True show ?thesis
+ by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y)
+next
+ case False
+ then show ?thesis
+ using segment_to_rel_frontier_aux [OF S x y] that by blast
+qed
+
+proposition rel_frontier_not_sing:
+ fixes a :: "'a::euclidean_space"
+ assumes "bounded S"
+ shows "rel_frontier S \<noteq> {a}"
+proof (cases "S = {}")
+ case True then show ?thesis by simp
+next
+ case False
+ then obtain z where "z \<in> S"
+ by blast
+ then show ?thesis
+ proof (cases "S = {z}")
+ case True then show ?thesis by simp
+ next
+ case False
+ then obtain w where "w \<in> S" "w \<noteq> z"
+ using \<open>z \<in> S\<close> by blast
+ show ?thesis
+ proof
+ assume "rel_frontier S = {a}"
+ then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S"
+ using \<open>w \<noteq> z\<close> by auto
+ then show False
+ proof cases
+ case 1
+ then have w: "w \<in> rel_interior S"
+ using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce
+ have "w + (w - z) \<in> affine hull S"
+ by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
+ then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S"
+ using \<open>w \<noteq> z\<close> \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w)
+ moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S"
+ using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z - w)"] \<open>w \<noteq> z\<close> \<open>z \<in> S\<close>
+ by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
+ ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)"
+ using \<open>rel_frontier S = {a}\<close> by force
+ moreover have "e \<noteq> -d "
+ using \<open>0 < e\<close> \<open>0 < d\<close> by force
+ ultimately show False
+ by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
+ next
+ case 2
+ then have z: "z \<in> rel_interior S"
+ using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce
+ have "z + (z - w) \<in> affine hull S"
+ by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
+ then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S"
+ using \<open>w \<noteq> z\<close> \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z)
+ moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S"
+ using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w - z)"] \<open>w \<noteq> z\<close> \<open>w \<in> S\<close>
+ by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
+ ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)"
+ using \<open>rel_frontier S = {a}\<close> by force
+ moreover have "e \<noteq> -d "
+ using \<open>0 < e\<close> \<open>0 < d\<close> by force
+ ultimately show False
+ by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
+ qed
+ qed
+ qed
+qed
+
subsection\<^marker>\<open>tag unimportant\<close> \<open>Convexity on direct sums\<close>