merged
authornipkow
Fri Jul 13 15:00:38 2018 +0200 (2 months ago)
changeset 686220987ae51a3be
parent 68620 707437105595
parent 68621 27432da24236
child 68623 b942da0962c2
merged
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Jul 13 12:14:26 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Jul 13 15:00:38 2018 +0200
     1.3 @@ -18,40 +18,6 @@
     1.4  imports Path_Connected Homeomorphism
     1.5  begin
     1.6  
     1.7 -subsection \<open>Unit cubes\<close>
     1.8 -
     1.9 -(* FIXME mv euclidean topological space *)
    1.10 -definition unit_cube :: "'a::euclidean_space set"
    1.11 -  where "unit_cube = {x. \<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1}"
    1.12 -
    1.13 -lemma mem_unit_cube: "x \<in> unit_cube \<longleftrightarrow> (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
    1.14 -  unfolding unit_cube_def by simp
    1.15 -
    1.16 -lemma bounded_unit_cube: "bounded unit_cube"
    1.17 -  unfolding bounded_def
    1.18 -proof (intro exI ballI)
    1.19 -  fix y :: 'a assume y: "y \<in> unit_cube"
    1.20 -  have "dist 0 y = norm y" by (rule dist_0_norm)
    1.21 -  also have "\<dots> = norm (\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R i)" unfolding euclidean_representation ..
    1.22 -  also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_sum)
    1.23 -  also have "\<dots> \<le> (\<Sum>i::'a\<in>Basis. 1)"
    1.24 -    by (rule sum_mono, simp add: y [unfolded mem_unit_cube])
    1.25 -  finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
    1.26 -qed
    1.27 -
    1.28 -lemma closed_unit_cube: "closed unit_cube"
    1.29 -  unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
    1.30 -  by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
    1.31 -
    1.32 -lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
    1.33 -  unfolding compact_eq_seq_compact_metric
    1.34 -  using bounded_unit_cube closed_unit_cube
    1.35 -  by (rule bounded_closed_imp_seq_compact)
    1.36 -
    1.37 -lemma convex_unit_cube: "convex unit_cube"
    1.38 -  by (rule is_interval_convex) (fastforce simp add: is_interval_def mem_unit_cube)
    1.39 -
    1.40 -
    1.41  (* FIXME mv topology euclidean space *)
    1.42  subsection \<open>Retractions\<close>
    1.43  
    1.44 @@ -3126,44 +3092,44 @@
    1.45  
    1.46  subsection \<open>Brouwer's fixed point theorem\<close>
    1.47  
    1.48 -text \<open>We start proving Brouwer's fixed point theorem for unit cubes.\<close>
    1.49 +text \<open>We start proving Brouwer's fixed point theorem for the unit cube = \<open>cbox 0 One\<close>.\<close>
    1.50  
    1.51  lemma brouwer_cube:
    1.52    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
    1.53 -  assumes "continuous_on unit_cube f"
    1.54 -    and "f ` unit_cube \<subseteq> unit_cube"
    1.55 -  shows "\<exists>x\<in>unit_cube. f x = x"
    1.56 +  assumes "continuous_on (cbox 0 One) f"
    1.57 +    and "f ` cbox 0 One \<subseteq> cbox 0 One"
    1.58 +  shows "\<exists>x\<in>cbox 0 One. f x = x"
    1.59  proof (rule ccontr)
    1.60    define n where "n = DIM('a)"
    1.61    have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
    1.62      unfolding n_def by (auto simp: Suc_le_eq DIM_positive)
    1.63    assume "\<not> ?thesis"
    1.64 -  then have *: "\<not> (\<exists>x\<in>unit_cube. f x - x = 0)"
    1.65 +  then have *: "\<not> (\<exists>x\<in>cbox 0 One. f x - x = 0)"
    1.66      by auto
    1.67    obtain d where
    1.68 -      d: "d > 0" "\<And>x. x \<in> unit_cube \<Longrightarrow> d \<le> norm (f x - x)"
    1.69 -    apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
    1.70 +      d: "d > 0" "\<And>x. x \<in> cbox 0 One \<Longrightarrow> d \<le> norm (f x - x)"
    1.71 +    apply (rule brouwer_compactness_lemma[OF compact_cbox _ *])
    1.72      apply (rule continuous_intros assms)+
    1.73      apply blast
    1.74      done
    1.75 -  have *: "\<forall>x. x \<in> unit_cube \<longrightarrow> f x \<in> unit_cube"
    1.76 -    "\<forall>x. x \<in> (unit_cube::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
    1.77 +  have *: "\<forall>x. x \<in> cbox 0 One \<longrightarrow> f x \<in> cbox 0 One"
    1.78 +    "\<forall>x. x \<in> (cbox 0 One::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
    1.79      using assms(2)[unfolded image_subset_iff Ball_def]
    1.80 -    unfolding mem_unit_cube
    1.81 +    unfolding cbox_def
    1.82      by auto
    1.83    obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where label [rule_format]:
    1.84      "\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
    1.85 -    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
    1.86 -    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
    1.87 -    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
    1.88 -    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
    1.89 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
    1.90 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
    1.91 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
    1.92 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
    1.93      using kuhn_labelling_lemma[OF *] by auto
    1.94    note label = this [rule_format]
    1.95 -  have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
    1.96 +  have lem1: "\<forall>x\<in>cbox 0 One. \<forall>y\<in>cbox 0 One. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
    1.97      \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
    1.98    proof safe
    1.99      fix x y :: 'a
   1.100 -    assume x: "x \<in> unit_cube" and y: "y \<in> unit_cube"
   1.101 +    assume x: "x \<in> cbox 0 One" and y: "y \<in> cbox 0 One"
   1.102      fix i
   1.103      assume i: "label x i \<noteq> label y i" "i \<in> Basis"
   1.104      have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
   1.105 @@ -3188,18 +3154,18 @@
   1.106      finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
   1.107        unfolding inner_simps .
   1.108    qed
   1.109 -  have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
   1.110 +  have "\<exists>e>0. \<forall>x\<in>cbox 0 One. \<forall>y\<in>cbox 0 One. \<forall>z\<in>cbox 0 One. \<forall>i\<in>Basis.
   1.111      norm (x - z) < e \<longrightarrow> norm (y - z) < e \<longrightarrow> label x i \<noteq> label y i \<longrightarrow>
   1.112        \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
   1.113    proof -
   1.114      have d': "d / real n / 8 > 0"
   1.115        using d(1) by (simp add: n_def DIM_positive)
   1.116 -    have *: "uniformly_continuous_on unit_cube f"
   1.117 -      by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])
   1.118 +    have *: "uniformly_continuous_on (cbox 0 One) f"
   1.119 +      by (rule compact_uniformly_continuous[OF assms(1) compact_cbox])
   1.120      obtain e where e:
   1.121          "e > 0"
   1.122 -        "\<And>x x'. x \<in> unit_cube \<Longrightarrow>
   1.123 -          x' \<in> unit_cube \<Longrightarrow>
   1.124 +        "\<And>x x'. x \<in> cbox 0 One \<Longrightarrow>
   1.125 +          x' \<in> cbox 0 One \<Longrightarrow>
   1.126            norm (x' - x) < e \<Longrightarrow>
   1.127            norm (f x' - f x) < d / real n / 8"
   1.128        using *[unfolded uniformly_continuous_on_def,rule_format,OF d']
   1.129 @@ -3211,7 +3177,7 @@
   1.130          using d' e by auto
   1.131        fix x y z i
   1.132        assume as:
   1.133 -        "x \<in> unit_cube" "y \<in> unit_cube" "z \<in> unit_cube"
   1.134 +        "x \<in> cbox 0 One" "y \<in> cbox 0 One" "z \<in> cbox 0 One"
   1.135          "norm (x - z) < min (e / 2) (d / real n / 8)"
   1.136          "norm (y - z) < min (e / 2) (d / real n / 8)"
   1.137          "label x i \<noteq> label y i"
   1.138 @@ -3249,9 +3215,9 @@
   1.139    then
   1.140    obtain e where e:
   1.141      "e > 0"
   1.142 -    "\<And>x y z i. x \<in> unit_cube \<Longrightarrow>
   1.143 -      y \<in> unit_cube \<Longrightarrow>
   1.144 -      z \<in> unit_cube \<Longrightarrow>
   1.145 +    "\<And>x y z i. x \<in> cbox 0 One \<Longrightarrow>
   1.146 +      y \<in> cbox 0 One \<Longrightarrow>
   1.147 +      z \<in> cbox 0 One \<Longrightarrow>
   1.148        i \<in> Basis \<Longrightarrow>
   1.149        norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<Longrightarrow>
   1.150        \<bar>(f z - z) \<bullet> i\<bar> < d / real n"
   1.151 @@ -3290,9 +3256,9 @@
   1.152      using label(1)[OF b'']
   1.153      by auto
   1.154    { fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
   1.155 -    then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
   1.156 +    then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (cbox 0 One::'a set)"
   1.157        using b'_Basis
   1.158 -      by (auto simp: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
   1.159 +      by (auto simp: cbox_def inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
   1.160    note cube = this
   1.161    have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
   1.162        (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
   1.163 @@ -3314,8 +3280,8 @@
   1.164      have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
   1.165        using q(1) b'
   1.166        by (auto intro: less_imp_le simp: bij_betw_def)
   1.167 -    then have "z \<in> unit_cube"
   1.168 -      unfolding z_def mem_unit_cube
   1.169 +    then have "z \<in> cbox 0 One"
   1.170 +      unfolding z_def cbox_def
   1.171        using b'_Basis
   1.172        by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.173      then have d_fz_z: "d \<le> norm (f z - z)"
   1.174 @@ -3353,18 +3319,18 @@
   1.175      using q(1)[rule_format,OF b'_im]
   1.176      apply (auto simp: Suc_le_eq)
   1.177      done
   1.178 -  then have "r' \<in> unit_cube"
   1.179 -    unfolding r'_def mem_unit_cube
   1.180 +  then have "r' \<in> cbox 0 One"
   1.181 +    unfolding r'_def cbox_def
   1.182      using b'_Basis
   1.183      by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.184    define s' :: 'a where "s' = (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)"
   1.185    have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
   1.186      using b'_im q(1) rs(2) by fastforce
   1.187 -  then have "s' \<in> unit_cube"
   1.188 -    unfolding s'_def mem_unit_cube
   1.189 +  then have "s' \<in> cbox 0 One"
   1.190 +    unfolding s'_def cbox_def
   1.191      using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.192 -  have "z \<in> unit_cube"
   1.193 -    unfolding z_def mem_unit_cube
   1.194 +  have "z \<in> cbox 0 One"
   1.195 +    unfolding z_def cbox_def
   1.196      using b'_Basis q(1)[rule_format,OF b'_im] \<open>p > 0\<close>
   1.197      by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
   1.198    {
   1.199 @@ -3394,7 +3360,7 @@
   1.200    then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
   1.201      using rs(3) i
   1.202      unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
   1.203 -    by (intro e(2)[OF \<open>r'\<in>unit_cube\<close> \<open>s'\<in>unit_cube\<close> \<open>z\<in>unit_cube\<close>]) auto
   1.204 +    by (intro e(2)[OF \<open>r'\<in>cbox 0 One\<close> \<open>s'\<in>cbox 0 One\<close> \<open>z\<in>cbox 0 One\<close>]) auto
   1.205    then show False
   1.206      using i by auto
   1.207  qed
   1.208 @@ -3410,7 +3376,7 @@
   1.209      and "f ` S \<subseteq> S"
   1.210    obtains x where "x \<in> S" and "f x = x"
   1.211  proof -
   1.212 -  let ?U = "unit_cube :: 'a set"
   1.213 +  let ?U = "cbox 0 One :: 'a set"
   1.214    have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
   1.215    proof (rule interiorI)
   1.216      let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> i < 1})"
   1.217 @@ -3418,12 +3384,12 @@
   1.218        by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id)
   1.219      show "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
   1.220        by simp
   1.221 -    show "?I \<subseteq> unit_cube"
   1.222 -      unfolding unit_cube_def by force
   1.223 +    show "?I \<subseteq> cbox 0 One"
   1.224 +      unfolding cbox_def by force
   1.225    qed
   1.226    then have *: "interior ?U \<noteq> {}" by fast
   1.227    have *: "?U homeomorphic S"
   1.228 -    using homeomorphic_convex_compact[OF convex_unit_cube compact_unit_cube * assms(2,1,3)] .
   1.229 +    using homeomorphic_convex_compact[OF convex_box(1) compact_cbox * assms(2,1,3)] .
   1.230    have "\<forall>f. continuous_on ?U f \<and> f ` ?U \<subseteq> ?U \<longrightarrow>
   1.231      (\<exists>x\<in>?U. f x = x)"
   1.232      using brouwer_cube by auto