--- 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