src/HOL/Analysis/Topology_Euclidean_Space.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69516 09bb8f470959
child 69544 5aa5a8d6e5b5
permissions -rw-r--r--
capitalize proper names in lemma names
lp15@63938
     1
(*  Author:     L C Paulson, University of Cambridge
himmelma@33175
     2
    Author:     Amine Chaieb, University of Cambridge
himmelma@33175
     3
    Author:     Robert Himmelmann, TU Muenchen
huffman@44075
     4
    Author:     Brian Huffman, Portland State University
himmelma@33175
     5
*)
himmelma@33175
     6
immler@69516
     7
section \<open>Elementary Topology in Euclidean Space\<close>
himmelma@33175
     8
himmelma@33175
     9
theory Topology_Euclidean_Space
immler@69516
    10
  imports
immler@69516
    11
    Elementary_Topology
immler@69516
    12
    Linear_Algebra
immler@69516
    13
    Norm_Arith
hoelzl@51343
    14
begin
hoelzl@51343
    15
hoelzl@50526
    16
lemma euclidean_dist_l2:
hoelzl@50526
    17
  fixes x y :: "'a :: euclidean_space"
nipkow@67155
    18
  shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
nipkow@67155
    19
  unfolding dist_norm norm_eq_sqrt_inner L2_set_def
hoelzl@50526
    20
  by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
hoelzl@50526
    21
immler@67685
    22
lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
immler@67685
    23
proof -
immler@67685
    24
  have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
immler@67685
    25
    by simp
immler@67685
    26
  also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
immler@67685
    27
    by (intro sum_mono2) (auto simp: that)
immler@67685
    28
  finally show ?thesis
immler@67685
    29
    unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
immler@67685
    30
    by (auto intro!: real_le_rsqrt)
immler@67685
    31
qed
immler@67685
    32
immler@67685
    33
wenzelm@60420
    34
subsection \<open>Boxes\<close>
immler@56189
    35
hoelzl@57447
    36
abbreviation One :: "'a::euclidean_space"
hoelzl@57447
    37
  where "One \<equiv> \<Sum>Basis"
hoelzl@57447
    38
lp15@63114
    39
lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
lp15@63114
    40
proof -
lp15@63114
    41
  have "dependent (Basis :: 'a set)"
lp15@63114
    42
    apply (simp add: dependent_finite)
lp15@63114
    43
    apply (rule_tac x="\<lambda>i. 1" in exI)
lp15@63114
    44
    using SOME_Basis apply (auto simp: assms)
lp15@63114
    45
    done
lp15@63114
    46
  with independent_Basis show False by force
lp15@63114
    47
qed
lp15@63114
    48
lp15@63114
    49
corollary One_neq_0[iff]: "One \<noteq> 0"
lp15@63114
    50
  by (metis One_non_0)
lp15@63114
    51
lp15@63114
    52
corollary Zero_neq_One[iff]: "0 \<noteq> One"
lp15@63114
    53
  by (metis One_non_0)
lp15@63114
    54
immler@67962
    55
definition%important (in euclidean_space) eucl_less (infix "<e" 50)
immler@54775
    56
  where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
immler@54775
    57
immler@67962
    58
definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
immler@67962
    59
definition%important "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
immler@54775
    60
immler@54775
    61
lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
immler@54775
    62
  and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
immler@56188
    63
  and mem_box: "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i)"
immler@56188
    64
    "x \<in> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
immler@56188
    65
  by (auto simp: box_eucl_less eucl_less_def cbox_def)
immler@56188
    66
lp15@60615
    67
lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \<times> cbox c d"
lp15@60615
    68
  by (force simp: cbox_def Basis_prod_def)
lp15@60615
    69
lp15@60615
    70
lemma cbox_Pair_iff [iff]: "(x, y) \<in> cbox (a, c) (b, d) \<longleftrightarrow> x \<in> cbox a b \<and> y \<in> cbox c d"
lp15@60615
    71
  by (force simp: cbox_Pair_eq)
lp15@60615
    72
lp15@65587
    73
lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)"
lp15@65587
    74
  apply (auto simp: cbox_def Basis_complex_def)
lp15@65587
    75
  apply (rule_tac x = "(Re x, Im x)" in image_eqI)
lp15@65587
    76
  using complex_eq by auto
lp15@65587
    77
lp15@60615
    78
lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
lp15@60615
    79
  by (force simp: cbox_Pair_eq)
lp15@60615
    80
lp15@60615
    81
lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
lp15@60615
    82
  by auto
lp15@60615
    83
immler@56188
    84
lemma mem_box_real[simp]:
immler@56188
    85
  "(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b"
immler@56188
    86
  "(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b"
immler@56188
    87
  by (auto simp: mem_box)
immler@56188
    88
immler@56188
    89
lemma box_real[simp]:
immler@56188
    90
  fixes a b:: real
immler@56188
    91
  shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
immler@56188
    92
  by auto
hoelzl@50526
    93
hoelzl@57447
    94
lemma box_Int_box:
hoelzl@57447
    95
  fixes a :: "'a::euclidean_space"
hoelzl@57447
    96
  shows "box a b \<inter> box c d =
hoelzl@57447
    97
    box (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
hoelzl@57447
    98
  unfolding set_eq_iff and Int_iff and mem_box by auto
hoelzl@57447
    99
immler@50087
   100
lemma rational_boxes:
wenzelm@61076
   101
  fixes x :: "'a::euclidean_space"
wenzelm@53291
   102
  assumes "e > 0"
lp15@66643
   103
  shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat>) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e"
immler@50087
   104
proof -
wenzelm@63040
   105
  define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
wenzelm@53291
   106
  then have e: "e' > 0"
nipkow@56541
   107
    using assms by (auto simp: DIM_positive)
hoelzl@50526
   108
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
immler@50087
   109
  proof
wenzelm@53255
   110
    fix i
wenzelm@53255
   111
    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
wenzelm@53255
   112
    show "?th i" by auto
immler@50087
   113
  qed
wenzelm@55522
   114
  from choice[OF this] obtain a where
wenzelm@55522
   115
    a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
hoelzl@50526
   116
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
immler@50087
   117
  proof
wenzelm@53255
   118
    fix i
wenzelm@53255
   119
    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
wenzelm@53255
   120
    show "?th i" by auto
immler@50087
   121
  qed
wenzelm@55522
   122
  from choice[OF this] obtain b where
wenzelm@55522
   123
    b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
hoelzl@50526
   124
  let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
hoelzl@50526
   125
  show ?thesis
hoelzl@50526
   126
  proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
wenzelm@53255
   127
    fix y :: 'a
wenzelm@53255
   128
    assume *: "y \<in> box ?a ?b"
wenzelm@53015
   129
    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
nipkow@67155
   130
      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
hoelzl@50526
   131
    also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
nipkow@64267
   132
    proof (rule real_sqrt_less_mono, rule sum_strict_mono)
wenzelm@53255
   133
      fix i :: "'a"
wenzelm@53255
   134
      assume i: "i \<in> Basis"
wenzelm@53255
   135
      have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
wenzelm@53255
   136
        using * i by (auto simp: box_def)
wenzelm@53255
   137
      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
wenzelm@53255
   138
        using a by auto
wenzelm@53255
   139
      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
wenzelm@53255
   140
        using b by auto
wenzelm@53255
   141
      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
wenzelm@53255
   142
        by auto
hoelzl@50526
   143
      then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
immler@50087
   144
        unfolding e'_def by (auto simp: dist_real_def)
wenzelm@53015
   145
      then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
immler@50087
   146
        by (rule power_strict_mono) auto
wenzelm@53015
   147
      then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
immler@50087
   148
        by (simp add: power_divide)
immler@50087
   149
    qed auto
wenzelm@53255
   150
    also have "\<dots> = e"
lp15@61609
   151
      using \<open>0 < e\<close> by simp
wenzelm@53255
   152
    finally show "y \<in> ball x e"
wenzelm@53255
   153
      by (auto simp: ball_def)
hoelzl@50526
   154
  qed (insert a b, auto simp: box_def)
hoelzl@50526
   155
qed
immler@51103
   156
hoelzl@50526
   157
lemma open_UNION_box:
wenzelm@61076
   158
  fixes M :: "'a::euclidean_space set"
wenzelm@53282
   159
  assumes "open M"
hoelzl@50526
   160
  defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
hoelzl@50526
   161
  defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
wenzelm@53015
   162
  defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
hoelzl@50526
   163
  shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
wenzelm@52624
   164
proof -
wenzelm@60462
   165
  have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" if "x \<in> M" for x
wenzelm@60462
   166
  proof -
wenzelm@52624
   167
    obtain e where e: "e > 0" "ball x e \<subseteq> M"
wenzelm@60420
   168
      using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
wenzelm@53282
   169
    moreover obtain a b where ab:
wenzelm@53282
   170
      "x \<in> box a b"
wenzelm@53282
   171
      "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
wenzelm@53282
   172
      "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>"
wenzelm@53282
   173
      "box a b \<subseteq> ball x e"
wenzelm@52624
   174
      using rational_boxes[OF e(1)] by metis
wenzelm@60462
   175
    ultimately show ?thesis
wenzelm@52624
   176
       by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
wenzelm@52624
   177
          (auto simp: euclidean_representation I_def a'_def b'_def)
wenzelm@60462
   178
  qed
wenzelm@52624
   179
  then show ?thesis by (auto simp: I_def)
wenzelm@52624
   180
qed
wenzelm@52624
   181
lp15@66154
   182
corollary open_countable_Union_open_box:
lp15@66154
   183
  fixes S :: "'a :: euclidean_space set"
lp15@66154
   184
  assumes "open S"
lp15@66154
   185
  obtains \<D> where "countable \<D>" "\<D> \<subseteq> Pow S" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = S"
lp15@66154
   186
proof -
lp15@66154
   187
  let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
lp15@66154
   188
  let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
lp15@66154
   189
  let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (?a f) (?b f) \<subseteq> S}"
lp15@66154
   190
  let ?\<D> = "(\<lambda>f. box (?a f) (?b f)) ` ?I"
lp15@66154
   191
  show ?thesis
lp15@66154
   192
  proof
lp15@66154
   193
    have "countable ?I"
lp15@66154
   194
      by (simp add: countable_PiE countable_rat)
lp15@66154
   195
    then show "countable ?\<D>"
lp15@66154
   196
      by blast
lp15@66154
   197
    show "\<Union>?\<D> = S"
lp15@66154
   198
      using open_UNION_box [OF assms] by metis
lp15@66154
   199
  qed auto
lp15@66154
   200
qed
lp15@66154
   201
lp15@66154
   202
lemma rational_cboxes:
lp15@66154
   203
  fixes x :: "'a::euclidean_space"
lp15@66154
   204
  assumes "e > 0"
lp15@66154
   205
  shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat>) \<and> x \<in> cbox a b \<and> cbox a b \<subseteq> ball x e"
lp15@66154
   206
proof -
lp15@66154
   207
  define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
lp15@66154
   208
  then have e: "e' > 0"
lp15@66154
   209
    using assms by auto
lp15@66154
   210
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
lp15@66154
   211
  proof
lp15@66154
   212
    fix i
lp15@66154
   213
    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
lp15@66154
   214
    show "?th i" by auto
lp15@66154
   215
  qed
lp15@66154
   216
  from choice[OF this] obtain a where
lp15@66154
   217
    a: "\<forall>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" ..
lp15@66154
   218
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
lp15@66154
   219
  proof
lp15@66154
   220
    fix i
lp15@66154
   221
    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
lp15@66154
   222
    show "?th i" by auto
lp15@66154
   223
  qed
lp15@66154
   224
  from choice[OF this] obtain b where
lp15@66154
   225
    b: "\<forall>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" ..
lp15@66154
   226
  let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
lp15@66154
   227
  show ?thesis
lp15@66154
   228
  proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
lp15@66154
   229
    fix y :: 'a
lp15@66154
   230
    assume *: "y \<in> cbox ?a ?b"
lp15@66154
   231
    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
nipkow@67155
   232
      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
lp15@66154
   233
    also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
lp15@66154
   234
    proof (rule real_sqrt_less_mono, rule sum_strict_mono)
lp15@66154
   235
      fix i :: "'a"
lp15@66154
   236
      assume i: "i \<in> Basis"
lp15@66154
   237
      have "a i \<le> y\<bullet>i \<and> y\<bullet>i \<le> b i"
lp15@66154
   238
        using * i by (auto simp: cbox_def)
lp15@66154
   239
      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
lp15@66154
   240
        using a by auto
lp15@66154
   241
      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
lp15@66154
   242
        using b by auto
lp15@66154
   243
      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
lp15@66154
   244
        by auto
lp15@66154
   245
      then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
lp15@66154
   246
        unfolding e'_def by (auto simp: dist_real_def)
lp15@66154
   247
      then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
lp15@66154
   248
        by (rule power_strict_mono) auto
lp15@66154
   249
      then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
lp15@66154
   250
        by (simp add: power_divide)
lp15@66154
   251
    qed auto
lp15@66154
   252
    also have "\<dots> = e"
lp15@66154
   253
      using \<open>0 < e\<close> by simp
lp15@66154
   254
    finally show "y \<in> ball x e"
lp15@66154
   255
      by (auto simp: ball_def)
lp15@66154
   256
  next
lp15@66154
   257
    show "x \<in> cbox (\<Sum>i\<in>Basis. a i *\<^sub>R i) (\<Sum>i\<in>Basis. b i *\<^sub>R i)"
lp15@66154
   258
      using a b less_imp_le by (auto simp: cbox_def)
lp15@66154
   259
  qed (use a b cbox_def in auto)
lp15@66154
   260
qed
lp15@66154
   261
lp15@66154
   262
lemma open_UNION_cbox:
lp15@66154
   263
  fixes M :: "'a::euclidean_space set"
lp15@66154
   264
  assumes "open M"
lp15@66154
   265
  defines "a' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
lp15@66154
   266
  defines "b' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
lp15@66154
   267
  defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (a' f) (b' f) \<subseteq> M}"
lp15@66154
   268
  shows "M = (\<Union>f\<in>I. cbox (a' f) (b' f))"
lp15@66154
   269
proof -
lp15@66154
   270
  have "x \<in> (\<Union>f\<in>I. cbox (a' f) (b' f))" if "x \<in> M" for x
lp15@66154
   271
  proof -
lp15@66154
   272
    obtain e where e: "e > 0" "ball x e \<subseteq> M"
lp15@66154
   273
      using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
lp15@66154
   274
    moreover obtain a b where ab: "x \<in> cbox a b" "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
lp15@66154
   275
                                  "\<forall>i \<in> Basis. b \<bullet> i \<in> \<rat>" "cbox a b \<subseteq> ball x e"
lp15@66154
   276
      using rational_cboxes[OF e(1)] by metis
lp15@66154
   277
    ultimately show ?thesis
lp15@66154
   278
       by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
lp15@66154
   279
          (auto simp: euclidean_representation I_def a'_def b'_def)
lp15@66154
   280
  qed
lp15@66154
   281
  then show ?thesis by (auto simp: I_def)
lp15@66154
   282
qed
lp15@66154
   283
lp15@66154
   284
corollary open_countable_Union_open_cbox:
lp15@66154
   285
  fixes S :: "'a :: euclidean_space set"
lp15@66154
   286
  assumes "open S"
lp15@66154
   287
  obtains \<D> where "countable \<D>" "\<D> \<subseteq> Pow S" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = S"
lp15@66154
   288
proof -
lp15@66154
   289
  let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
lp15@66154
   290
  let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
lp15@66154
   291
  let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (?a f) (?b f) \<subseteq> S}"
lp15@66154
   292
  let ?\<D> = "(\<lambda>f. cbox (?a f) (?b f)) ` ?I"
lp15@66154
   293
  show ?thesis
lp15@66154
   294
  proof
lp15@66154
   295
    have "countable ?I"
lp15@66154
   296
      by (simp add: countable_PiE countable_rat)
lp15@66154
   297
    then show "countable ?\<D>"
lp15@66154
   298
      by blast
lp15@66154
   299
    show "\<Union>?\<D> = S"
lp15@66154
   300
      using open_UNION_cbox [OF assms] by metis
lp15@66154
   301
  qed auto
lp15@66154
   302
qed
lp15@66154
   303
immler@56189
   304
lemma box_eq_empty:
immler@56189
   305
  fixes a :: "'a::euclidean_space"
immler@56189
   306
  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
immler@56189
   307
    and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
immler@56189
   308
proof -
immler@56189
   309
  {
immler@56189
   310
    fix i x
immler@56189
   311
    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
immler@56189
   312
    then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
immler@56189
   313
      unfolding mem_box by (auto simp: box_def)
immler@56189
   314
    then have "a\<bullet>i < b\<bullet>i" by auto
immler@56189
   315
    then have False using as by auto
immler@56189
   316
  }
immler@56189
   317
  moreover
immler@56189
   318
  {
immler@56189
   319
    assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
immler@56189
   320
    let ?x = "(1/2) *\<^sub>R (a + b)"
immler@56189
   321
    {
immler@56189
   322
      fix i :: 'a
immler@56189
   323
      assume i: "i \<in> Basis"
immler@56189
   324
      have "a\<bullet>i < b\<bullet>i"
immler@56189
   325
        using as[THEN bspec[where x=i]] i by auto
immler@56189
   326
      then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
immler@56189
   327
        by (auto simp: inner_add_left)
immler@56189
   328
    }
immler@56189
   329
    then have "box a b \<noteq> {}"
immler@56189
   330
      using mem_box(1)[of "?x" a b] by auto
immler@56189
   331
  }
immler@56189
   332
  ultimately show ?th1 by blast
immler@56189
   333
immler@56189
   334
  {
immler@56189
   335
    fix i x
immler@56189
   336
    assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
immler@56189
   337
    then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
immler@56189
   338
      unfolding mem_box by auto
immler@56189
   339
    then have "a\<bullet>i \<le> b\<bullet>i" by auto
immler@56189
   340
    then have False using as by auto
immler@56189
   341
  }
immler@56189
   342
  moreover
immler@56189
   343
  {
immler@56189
   344
    assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
immler@56189
   345
    let ?x = "(1/2) *\<^sub>R (a + b)"
immler@56189
   346
    {
immler@56189
   347
      fix i :: 'a
immler@56189
   348
      assume i:"i \<in> Basis"
immler@56189
   349
      have "a\<bullet>i \<le> b\<bullet>i"
immler@56189
   350
        using as[THEN bspec[where x=i]] i by auto
immler@56189
   351
      then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i"
immler@56189
   352
        by (auto simp: inner_add_left)
immler@56189
   353
    }
immler@56189
   354
    then have "cbox a b \<noteq> {}"
immler@56189
   355
      using mem_box(2)[of "?x" a b] by auto
immler@56189
   356
  }
immler@56189
   357
  ultimately show ?th2 by blast
immler@56189
   358
qed
immler@56189
   359
immler@56189
   360
lemma box_ne_empty:
immler@56189
   361
  fixes a :: "'a::euclidean_space"
immler@56189
   362
  shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
immler@56189
   363
  and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
immler@56189
   364
  unfolding box_eq_empty[of a b] by fastforce+
immler@56189
   365
immler@56189
   366
lemma
immler@56189
   367
  fixes a :: "'a::euclidean_space"
lp15@66112
   368
  shows cbox_sing [simp]: "cbox a a = {a}"
lp15@66112
   369
    and box_sing [simp]: "box a a = {}"
immler@56189
   370
  unfolding set_eq_iff mem_box eq_iff [symmetric]
immler@56189
   371
  by (auto intro!: euclidean_eqI[where 'a='a])
immler@56189
   372
     (metis all_not_in_conv nonempty_Basis)
immler@56189
   373
immler@56189
   374
lemma subset_box_imp:
immler@56189
   375
  fixes a :: "'a::euclidean_space"
immler@56189
   376
  shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> cbox a b"
immler@56189
   377
    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> box a b"
immler@56189
   378
    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> cbox a b"
immler@56189
   379
     and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b"
immler@56189
   380
  unfolding subset_eq[unfolded Ball_def] unfolding mem_box
wenzelm@58757
   381
  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
immler@56189
   382
immler@56189
   383
lemma box_subset_cbox:
immler@56189
   384
  fixes a :: "'a::euclidean_space"
immler@56189
   385
  shows "box a b \<subseteq> cbox a b"
immler@56189
   386
  unfolding subset_eq [unfolded Ball_def] mem_box
immler@56189
   387
  by (fast intro: less_imp_le)
immler@56189
   388
immler@56189
   389
lemma subset_box:
immler@56189
   390
  fixes a :: "'a::euclidean_space"
wenzelm@64539
   391
  shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
wenzelm@64539
   392
    and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
wenzelm@64539
   393
    and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
wenzelm@64539
   394
    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
immler@56189
   395
proof -
lp15@68120
   396
  let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
lp15@68120
   397
  let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
lp15@68120
   398
  show ?th1 ?th2
lp15@68120
   399
    by (fastforce simp: mem_box)+
lp15@68120
   400
  have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
lp15@68120
   401
    if i: "i \<in> Basis" and box: "box c d \<subseteq> cbox a b" and cd: "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
lp15@68120
   402
  proof -
lp15@68120
   403
    have "box c d \<noteq> {}"
lp15@68120
   404
      using that
lp15@68120
   405
      unfolding box_eq_empty by force
lp15@68120
   406
    { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
lp15@68120
   407
      assume *: "a\<bullet>i > c\<bullet>i"
lp15@68120
   408
      then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j
lp15@68120
   409
        using cd that by (fastforce simp add: i *)
lp15@68120
   410
      then have "?x \<in> box c d"
lp15@68120
   411
        unfolding mem_box by auto
lp15@68120
   412
      moreover have "?x \<notin> cbox a b"
lp15@68120
   413
        using i cd * by (force simp: mem_box)
lp15@68120
   414
      ultimately have False using box by auto
immler@56189
   415
    }
lp15@68120
   416
    then have "a\<bullet>i \<le> c\<bullet>i" by force
immler@56189
   417
    moreover
lp15@68120
   418
    { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
lp15@68120
   419
      assume *: "b\<bullet>i < d\<bullet>i"
lp15@68120
   420
      then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j
lp15@68120
   421
        using cd that by (fastforce simp add: i *)
lp15@68120
   422
      then have "?x \<in> box c d"
immler@56189
   423
        unfolding mem_box by auto
lp15@68120
   424
      moreover have "?x \<notin> cbox a b"
lp15@68120
   425
        using i cd * by (force simp: mem_box)
lp15@68120
   426
      ultimately have False using box by auto
immler@56189
   427
    }
immler@56189
   428
    then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
lp15@68120
   429
    ultimately show ?thesis by auto
lp15@68120
   430
  qed
immler@56189
   431
  show ?th3
lp15@68120
   432
    using acdb by (fastforce simp add: mem_box)
lp15@68120
   433
  have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
lp15@68120
   434
    if "i \<in> Basis" "box c d \<subseteq> box a b" "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
lp15@68120
   435
      using box_subset_cbox[of a b] that acdb by auto
immler@56189
   436
  show ?th4
lp15@68120
   437
    using acdb' by (fastforce simp add: mem_box)
immler@56189
   438
qed
immler@56189
   439
lp15@63945
   440
lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
lp15@63945
   441
      (is "?lhs = ?rhs")
lp15@63945
   442
proof
lp15@63945
   443
  assume ?lhs
lp15@63945
   444
  then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> cbox a b"
lp15@63945
   445
    by auto
lp15@63945
   446
  then show ?rhs
lp15@66643
   447
    by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
lp15@63945
   448
next
lp15@63945
   449
  assume ?rhs
lp15@63945
   450
  then show ?lhs
lp15@63945
   451
    by force
lp15@63945
   452
qed
lp15@63945
   453
lp15@63945
   454
lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
wenzelm@64539
   455
  (is "?lhs \<longleftrightarrow> ?rhs")
lp15@63945
   456
proof
lp15@68120
   457
  assume L: ?lhs
lp15@68120
   458
  then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
lp15@63945
   459
    by auto
lp15@63945
   460
  then show ?rhs
hoelzl@63957
   461
    apply (simp add: subset_box)
lp15@68120
   462
    using L box_ne_empty box_sing apply (fastforce simp add:)
lp15@63945
   463
    done
lp15@68120
   464
qed force
lp15@63945
   465
lp15@63945
   466
lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
lp15@63945
   467
  by (metis eq_cbox_box)
lp15@63945
   468
lp15@63945
   469
lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
wenzelm@64539
   470
  (is "?lhs \<longleftrightarrow> ?rhs")
lp15@63945
   471
proof
lp15@68120
   472
  assume L: ?lhs
lp15@63945
   473
  then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
lp15@63945
   474
    by auto
lp15@63945
   475
  then show ?rhs
lp15@63945
   476
    apply (simp add: subset_box)
lp15@68120
   477
    using box_ne_empty(2) L
lp15@63945
   478
    apply auto
lp15@63945
   479
     apply (meson euclidean_eqI less_eq_real_def not_less)+
lp15@63945
   480
    done
lp15@68120
   481
qed force
lp15@63945
   482
eberlm@66466
   483
lemma subset_box_complex:
lp15@66643
   484
   "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
eberlm@66466
   485
      (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
lp15@66643
   486
   "cbox a b \<subseteq> box c d \<longleftrightarrow>
eberlm@66466
   487
      (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a > Re c \<and> Im a > Im c \<and> Re b < Re d \<and> Im b < Im d"
eberlm@66466
   488
   "box a b \<subseteq> cbox c d \<longleftrightarrow>
eberlm@66466
   489
      (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
lp15@66643
   490
   "box a b \<subseteq> box c d \<longleftrightarrow>
eberlm@66466
   491
      (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
eberlm@66466
   492
  by (subst subset_box; force simp: Basis_complex_def)+
eberlm@66466
   493
lp15@63945
   494
lemma Int_interval:
immler@56189
   495
  fixes a :: "'a::euclidean_space"
immler@56189
   496
  shows "cbox a b \<inter> cbox c d =
immler@56189
   497
    cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
immler@56189
   498
  unfolding set_eq_iff and Int_iff and mem_box
immler@56189
   499
  by auto
immler@56189
   500
immler@56189
   501
lemma disjoint_interval:
immler@56189
   502
  fixes a::"'a::euclidean_space"
immler@56189
   503
  shows "cbox a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1)
immler@56189
   504
    and "cbox a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
immler@56189
   505
    and "box a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
immler@56189
   506
    and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
immler@56189
   507
proof -
immler@56189
   508
  let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a"
immler@56189
   509
  have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
immler@56189
   510
      (\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>Basis. P i)"
immler@56189
   511
    by blast
immler@56189
   512
  note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
immler@56189
   513
  show ?th1 unfolding * by (intro **) auto
immler@56189
   514
  show ?th2 unfolding * by (intro **) auto
immler@56189
   515
  show ?th3 unfolding * by (intro **) auto
immler@56189
   516
  show ?th4 unfolding * by (intro **) auto
immler@56189
   517
qed
immler@56189
   518
hoelzl@57447
   519
lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
hoelzl@57447
   520
proof -
wenzelm@61942
   521
  have "\<bar>x \<bullet> b\<bar> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
wenzelm@60462
   522
    if [simp]: "b \<in> Basis" for x b :: 'a
wenzelm@60462
   523
  proof -
wenzelm@61942
   524
    have "\<bar>x \<bullet> b\<bar> \<le> real_of_int \<lceil>\<bar>x \<bullet> b\<bar>\<rceil>"
lp15@61609
   525
      by (rule le_of_int_ceiling)
wenzelm@61942
   526
    also have "\<dots> \<le> real_of_int \<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil>"
nipkow@59587
   527
      by (auto intro!: ceiling_mono)
wenzelm@61942
   528
    also have "\<dots> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
hoelzl@57447
   529
      by simp
wenzelm@60462
   530
    finally show ?thesis .
wenzelm@60462
   531
  qed
wenzelm@60462
   532
  then have "\<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" for x :: 'a
nipkow@59587
   533
    by (metis order.strict_trans reals_Archimedean2)
hoelzl@57447
   534
  moreover have "\<And>x b::'a. \<And>n::nat.  \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n"
hoelzl@57447
   535
    by auto
hoelzl@57447
   536
  ultimately show ?thesis
nipkow@64267
   537
    by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
hoelzl@57447
   538
qed
hoelzl@57447
   539
immler@69516
   540
nipkow@69508
   541
subsection \<open>General Intervals\<close>
immler@67962
   542
immler@67962
   543
definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
immler@56189
   544
  (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
immler@56189
   545
immler@67685
   546
lemma is_interval_1:
immler@67685
   547
  "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
immler@67685
   548
  unfolding is_interval_def by auto
immler@67685
   549
immler@67685
   550
lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
immler@67685
   551
  unfolding is_interval_def
immler@67685
   552
  by blast
immler@67685
   553
lp15@66089
   554
lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
lp15@66089
   555
  and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
immler@56189
   556
  unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
immler@56189
   557
  by (meson order_trans le_less_trans less_le_trans less_trans)+
immler@56189
   558
lp15@61609
   559
lemma is_interval_empty [iff]: "is_interval {}"
lp15@61609
   560
  unfolding is_interval_def  by simp
lp15@61609
   561
lp15@61609
   562
lemma is_interval_univ [iff]: "is_interval UNIV"
lp15@61609
   563
  unfolding is_interval_def  by simp
immler@56189
   564
immler@56189
   565
lemma mem_is_intervalI:
immler@56189
   566
  assumes "is_interval s"
wenzelm@64539
   567
    and "a \<in> s" "b \<in> s"
wenzelm@64539
   568
    and "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i"
immler@56189
   569
  shows "x \<in> s"
immler@56189
   570
  by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
immler@56189
   571
immler@56189
   572
lemma interval_subst:
immler@56189
   573
  fixes S::"'a::euclidean_space set"
immler@56189
   574
  assumes "is_interval S"
wenzelm@64539
   575
    and "x \<in> S" "y j \<in> S"
wenzelm@64539
   576
    and "j \<in> Basis"
immler@56189
   577
  shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
immler@56189
   578
  by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
immler@56189
   579
immler@56189
   580
lemma mem_box_componentwiseI:
immler@56189
   581
  fixes S::"'a::euclidean_space set"
immler@56189
   582
  assumes "is_interval S"
immler@56189
   583
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
immler@56189
   584
  shows "x \<in> S"
immler@56189
   585
proof -
immler@56189
   586
  from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
immler@56189
   587
    by auto
wenzelm@64539
   588
  with finite_Basis obtain s and bs::"'a list"
wenzelm@64539
   589
    where s: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i = s i \<bullet> i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<in> S"
wenzelm@64539
   590
      and bs: "set bs = Basis" "distinct bs"
immler@56189
   591
    by (metis finite_distinct_list)
wenzelm@64539
   592
  from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S"
wenzelm@64539
   593
    by blast
wenzelm@63040
   594
  define y where
wenzelm@63040
   595
    "y = rec_list (s j) (\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
immler@56189
   596
  have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
lp15@66643
   597
    using bs by (auto simp: s(1)[symmetric] euclidean_representation)
immler@56189
   598
  also have [symmetric]: "y bs = \<dots>"
immler@56189
   599
    using bs(2) bs(1)[THEN equalityD1]
immler@56189
   600
    by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
immler@56189
   601
  also have "y bs \<in> S"
immler@56189
   602
    using bs(1)[THEN equalityD1]
immler@56189
   603
    apply (induct bs)
wenzelm@64539
   604
     apply (auto simp: y_def j)
immler@56189
   605
    apply (rule interval_subst[OF assms(1)])
wenzelm@64539
   606
      apply (auto simp: s)
immler@56189
   607
    done
immler@56189
   608
  finally show ?thesis .
immler@56189
   609
qed
immler@56189
   610
lp15@63007
   611
lemma cbox01_nonempty [simp]: "cbox 0 One \<noteq> {}"
nipkow@64267
   612
  by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
lp15@63007
   613
lp15@63007
   614
lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
lp15@66089
   615
  by (simp add: box_ne_empty inner_Basis inner_sum_left)
lp15@63075
   616
lp15@64773
   617
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
lp15@64773
   618
  using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
lp15@64773
   619
lp15@66089
   620
lemma interval_subset_is_interval:
lp15@66089
   621
  assumes "is_interval S"
lp15@66089
   622
  shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs")
lp15@66089
   623
proof
lp15@66089
   624
  assume ?lhs
lp15@66089
   625
  then show ?rhs  using box_ne_empty(1) mem_box(2) by fastforce
lp15@66089
   626
next
lp15@66089
   627
  assume ?rhs
lp15@66089
   628
  have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
lp15@66089
   629
    using assms unfolding is_interval_def
lp15@66089
   630
    apply (clarsimp simp add: mem_box)
lp15@66089
   631
    using that by blast
lp15@66089
   632
  with \<open>?rhs\<close> show ?lhs
lp15@66089
   633
    by blast
lp15@66089
   634
qed
lp15@66089
   635
immler@67685
   636
lemma is_real_interval_union:
immler@67685
   637
  "is_interval (X \<union> Y)"
immler@67685
   638
  if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
immler@67685
   639
  for X Y::"real set"
immler@67685
   640
proof -
immler@67685
   641
  consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
immler@67685
   642
  then show ?thesis
immler@67685
   643
  proof cases
immler@67685
   644
    case 1
immler@67685
   645
    then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
immler@67685
   646
      by blast
immler@67685
   647
    then show ?thesis
immler@67685
   648
      using I 1 X Y unfolding is_interval_1
immler@67685
   649
      by (metis (full_types) Un_iff le_cases)
immler@67685
   650
  qed (use that in auto)
immler@67685
   651
qed
immler@67685
   652
immler@67685
   653
lemma is_interval_translationI:
immler@67685
   654
  assumes "is_interval X"
immler@67685
   655
  shows "is_interval ((+) x ` X)"
immler@67685
   656
  unfolding is_interval_def
immler@67685
   657
proof safe
immler@67685
   658
  fix b d e
immler@67685
   659
  assume "b \<in> X" "d \<in> X"
immler@67685
   660
    "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
immler@67685
   661
       (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
immler@67685
   662
  hence "e - x \<in> X"
immler@67685
   663
    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
immler@67685
   664
      (auto simp: algebra_simps)
immler@67685
   665
  thus "e \<in> (+) x ` X" by force
immler@67685
   666
qed
immler@67685
   667
immler@67685
   668
lemma is_interval_uminusI:
immler@67685
   669
  assumes "is_interval X"
immler@67685
   670
  shows "is_interval (uminus ` X)"
immler@67685
   671
  unfolding is_interval_def
immler@67685
   672
proof safe
immler@67685
   673
  fix b d e
immler@67685
   674
  assume "b \<in> X" "d \<in> X"
immler@67685
   675
    "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
immler@67685
   676
       (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
immler@67685
   677
  hence "- e \<in> X"
immler@67685
   678
    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
immler@67685
   679
      (auto simp: algebra_simps)
immler@67685
   680
  thus "e \<in> uminus ` X" by force
immler@67685
   681
qed
immler@67685
   682
immler@67685
   683
lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
immler@67685
   684
  using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
immler@67685
   685
  by (auto simp: image_image)
immler@67685
   686
immler@67685
   687
lemma is_interval_neg_translationI:
immler@67685
   688
  assumes "is_interval X"
immler@67685
   689
  shows "is_interval ((-) x ` X)"
immler@67685
   690
proof -
immler@67685
   691
  have "(-) x ` X = (+) x ` uminus ` X"
immler@67685
   692
    by (force simp: algebra_simps)
immler@67685
   693
  also have "is_interval \<dots>"
immler@67685
   694
    by (metis is_interval_uminusI is_interval_translationI assms)
immler@67685
   695
  finally show ?thesis .
immler@67685
   696
qed
immler@67685
   697
immler@67685
   698
lemma is_interval_translation[simp]:
immler@67685
   699
  "is_interval ((+) x ` X) = is_interval X"
immler@67685
   700
  using is_interval_neg_translationI[of "(+) x ` X" x]
immler@67685
   701
  by (auto intro!: is_interval_translationI simp: image_image)
immler@67685
   702
immler@67685
   703
lemma is_interval_minus_translation[simp]:
immler@67685
   704
  shows "is_interval ((-) x ` X) = is_interval X"
immler@67685
   705
proof -
immler@67685
   706
  have "(-) x ` X = (+) x ` uminus ` X"
immler@67685
   707
    by (force simp: algebra_simps)
immler@67685
   708
  also have "is_interval \<dots> = is_interval X"
immler@67685
   709
    by simp
immler@67685
   710
  finally show ?thesis .
immler@67685
   711
qed
immler@67685
   712
immler@67685
   713
lemma is_interval_minus_translation'[simp]:
immler@67685
   714
  shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
immler@67685
   715
  using is_interval_translation[of "-c" X]
immler@67685
   716
  by (metis image_cong uminus_add_conv_diff)
immler@67685
   717
immler@62127
   718
lemma compact_lemma:
immler@62127
   719
  fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
immler@62127
   720
  assumes "bounded (range f)"
immler@62127
   721
  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
eberlm@66447
   722
    strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
immler@62127
   723
  by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
immler@62127
   724
     (auto intro!: assms bounded_linear_inner_left bounded_linear_image
immler@62127
   725
       simp: euclidean_representation)
immler@62127
   726
immler@67962
   727
instance%important euclidean_space \<subseteq> heine_borel
immler@67962
   728
proof%unimportant
hoelzl@50998
   729
  fix f :: "nat \<Rightarrow> 'a"
hoelzl@50998
   730
  assume f: "bounded (range f)"
eberlm@66447
   731
  then obtain l::'a and r where r: "strict_mono r"
hoelzl@50526
   732
    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
hoelzl@50998
   733
    using compact_lemma [OF f] by blast
wenzelm@52624
   734
  {
wenzelm@52624
   735
    fix e::real
wenzelm@53282
   736
    assume "e > 0"
nipkow@56541
   737
    hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
hoelzl@50526
   738
    with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
himmelma@33175
   739
      by simp
himmelma@33175
   740
    moreover
wenzelm@52624
   741
    {
wenzelm@52624
   742
      fix n
wenzelm@52624
   743
      assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
hoelzl@50526
   744
      have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
wenzelm@52624
   745
        apply (subst euclidean_dist_l2)
wenzelm@52624
   746
        using zero_le_dist
nipkow@67155
   747
        apply (rule L2_set_le_sum)
wenzelm@53282
   748
        done
hoelzl@50526
   749
      also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
nipkow@64267
   750
        apply (rule sum_strict_mono)
wenzelm@52624
   751
        using n
wenzelm@53282
   752
        apply auto
wenzelm@53282
   753
        done
wenzelm@53282
   754
      finally have "dist (f (r n)) l < e"
hoelzl@50526
   755
        by auto
himmelma@33175
   756
    }
himmelma@33175
   757
    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
lp15@61810
   758
      by (rule eventually_mono)
himmelma@33175
   759
  }
wenzelm@61973
   760
  then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
wenzelm@52624
   761
    unfolding o_def tendsto_iff by simp
eberlm@66447
   762
  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
wenzelm@52624
   763
    by auto
himmelma@33175
   764
qed
himmelma@33175
   765
huffman@44632
   766
instance euclidean_space \<subseteq> banach ..
huffman@44632
   767
wenzelm@53282
   768
immler@67962
   769
subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close>
himmelma@33175
   770
hoelzl@51361
   771
lemma continuous_infnorm[continuous_intros]:
wenzelm@53282
   772
  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
huffman@44647
   773
  unfolding continuous_def by (rule tendsto_infnorm)
himmelma@33175
   774
hoelzl@51361
   775
lemma continuous_inner[continuous_intros]:
wenzelm@53282
   776
  assumes "continuous F f"
wenzelm@53282
   777
    and "continuous F g"
huffman@44647
   778
  shows "continuous F (\<lambda>x. inner (f x) (g x))"
huffman@44647
   779
  using assms unfolding continuous_def by (rule tendsto_inner)
huffman@44647
   780
immler@69516
   781
immler@67962
   782
subsubsection%unimportant \<open>Structural rules for setwise continuity\<close>
himmelma@33175
   783
hoelzl@56371
   784
lemma continuous_on_infnorm[continuous_intros]:
wenzelm@53282
   785
  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
huffman@44647
   786
  unfolding continuous_on by (fast intro: tendsto_infnorm)
huffman@44647
   787
hoelzl@56371
   788
lemma continuous_on_inner[continuous_intros]:
huffman@44531
   789
  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
wenzelm@53282
   790
  assumes "continuous_on s f"
wenzelm@53282
   791
    and "continuous_on s g"
huffman@44531
   792
  shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
huffman@44531
   793
  using bounded_bilinear_inner assms
huffman@44531
   794
  by (rule bounded_bilinear.continuous_on)
huffman@44531
   795
immler@67962
   796
subsection%unimportant \<open>Intervals\<close>
lp15@60974
   797
wenzelm@60420
   798
text \<open>Openness of halfspaces.\<close>
himmelma@33175
   799
himmelma@33175
   800
lemma open_halfspace_lt: "open {x. inner a x < b}"
hoelzl@63332
   801
  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
himmelma@33175
   802
himmelma@33175
   803
lemma open_halfspace_gt: "open {x. inner a x > b}"
hoelzl@63332
   804
  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
himmelma@33175
   805
wenzelm@53282
   806
lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\<bullet>i < a}"
hoelzl@63332
   807
  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
himmelma@33175
   808
wenzelm@53282
   809
lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
hoelzl@63332
   810
  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
himmelma@33175
   811
wenzelm@60420
   812
text \<open>This gives a simple derivation of limit component bounds.\<close>
himmelma@33175
   813
immler@56189
   814
lemma open_box[intro]: "open (box a b)"
immler@56189
   815
proof -
nipkow@67399
   816
  have "open (\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i})"
lp15@62533
   817
    by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
nipkow@67399
   818
  also have "(\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
lp15@66643
   819
    by (auto simp: box_def inner_commute)
immler@56189
   820
  finally show ?thesis .
immler@56189
   821
qed
immler@56189
   822
immler@56189
   823
instance euclidean_space \<subseteq> second_countable_topology
immler@56189
   824
proof
wenzelm@63040
   825
  define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
immler@56189
   826
  then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
immler@56189
   827
    by simp
wenzelm@63040
   828
  define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
immler@56189
   829
  then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
immler@56189
   830
    by simp
wenzelm@63040
   831
  define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
immler@56189
   832
immler@56189
   833
  have "Ball B open" by (simp add: B_def open_box)
immler@56189
   834
  moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
immler@56189
   835
  proof safe
immler@56189
   836
    fix A::"'a set"
immler@56189
   837
    assume "open A"
immler@56189
   838
    show "\<exists>B'\<subseteq>B. \<Union>B' = A"
immler@56189
   839
      apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
wenzelm@60420
   840
      apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
lp15@66643
   841
      apply (auto simp: a b B_def)
immler@56189
   842
      done
immler@56189
   843
  qed
immler@56189
   844
  ultimately
immler@56189
   845
  have "topological_basis B"
immler@56189
   846
    unfolding topological_basis_def by blast
immler@56189
   847
  moreover
immler@56189
   848
  have "countable B"
immler@56189
   849
    unfolding B_def
immler@56189
   850
    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
immler@56189
   851
  ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
immler@56189
   852
    by (blast intro: topological_basis_imp_subbasis)
immler@56189
   853
qed
immler@56189
   854
immler@56189
   855
instance euclidean_space \<subseteq> polish_space ..
immler@56189
   856
immler@56189
   857
lemma closed_cbox[intro]:
immler@56189
   858
  fixes a b :: "'a::euclidean_space"
immler@56189
   859
  shows "closed (cbox a b)"
immler@56189
   860
proof -
immler@56189
   861
  have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
immler@56189
   862
    by (intro closed_INT ballI continuous_closed_vimage allI
immler@56189
   863
      linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
immler@56189
   864
  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
lp15@66643
   865
    by (auto simp: cbox_def)
immler@56189
   866
  finally show "closed (cbox a b)" .
immler@56189
   867
qed
immler@56189
   868
lp15@62618
   869
lemma interior_cbox [simp]:
immler@56189
   870
  fixes a b :: "'a::euclidean_space"
immler@56189
   871
  shows "interior (cbox a b) = box a b" (is "?L = ?R")
immler@56189
   872
proof(rule subset_antisym)
immler@56189
   873
  show "?R \<subseteq> ?L"
immler@56189
   874
    using box_subset_cbox open_box
immler@56189
   875
    by (rule interior_maximal)
immler@56189
   876
  {
immler@56189
   877
    fix x
immler@56189
   878
    assume "x \<in> interior (cbox a b)"
immler@56189
   879
    then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" ..
immler@56189
   880
    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b"
immler@56189
   881
      unfolding open_dist and subset_eq by auto
immler@56189
   882
    {
immler@56189
   883
      fix i :: 'a
immler@56189
   884
      assume i: "i \<in> Basis"
immler@56189
   885
      have "dist (x - (e / 2) *\<^sub>R i) x < e"
immler@56189
   886
        and "dist (x + (e / 2) *\<^sub>R i) x < e"
immler@56189
   887
        unfolding dist_norm
immler@56189
   888
        apply auto
immler@56189
   889
        unfolding norm_minus_cancel
wenzelm@60420
   890
        using norm_Basis[OF i] \<open>e>0\<close>
immler@56189
   891
        apply auto
immler@56189
   892
        done
immler@56189
   893
      then have "a \<bullet> i \<le> (x - (e / 2) *\<^sub>R i) \<bullet> i" and "(x + (e / 2) *\<^sub>R i) \<bullet> i \<le> b \<bullet> i"
immler@56189
   894
        using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
immler@56189
   895
          and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
immler@56189
   896
        unfolding mem_box
immler@56189
   897
        using i
immler@56189
   898
        by blast+
immler@56189
   899
      then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
wenzelm@60420
   900
        using \<open>e>0\<close> i
immler@56189
   901
        by (auto simp: inner_diff_left inner_Basis inner_add_left)
immler@56189
   902
    }
immler@56189
   903
    then have "x \<in> box a b"
immler@56189
   904
      unfolding mem_box by auto
immler@56189
   905
  }
immler@56189
   906
  then show "?L \<subseteq> ?R" ..
immler@56189
   907
qed
immler@56189
   908
lp15@63928
   909
lemma bounded_cbox [simp]:
immler@56189
   910
  fixes a :: "'a::euclidean_space"
immler@56189
   911
  shows "bounded (cbox a b)"
immler@56189
   912
proof -
immler@56189
   913
  let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
immler@56189
   914
  {
immler@56189
   915
    fix x :: "'a"
lp15@68120
   916
    assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
immler@56189
   917
    then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
lp15@68120
   918
      by (force simp: intro!: sum_mono)
immler@56189
   919
    then have "norm x \<le> ?b"
immler@56189
   920
      using norm_le_l1[of x] by auto
immler@56189
   921
  }
immler@56189
   922
  then show ?thesis
lp15@68120
   923
    unfolding cbox_def bounded_iff by force
immler@56189
   924
qed
immler@56189
   925
lp15@62618
   926
lemma bounded_box [simp]:
immler@56189
   927
  fixes a :: "'a::euclidean_space"
immler@56189
   928
  shows "bounded (box a b)"
lp15@68120
   929
  using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
immler@56189
   930
  by simp
immler@56189
   931
lp15@62618
   932
lemma not_interval_UNIV [simp]:
immler@56189
   933
  fixes a :: "'a::euclidean_space"
immler@56189
   934
  shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV"
lp15@62618
   935
  using bounded_box[of a b] bounded_cbox[of a b] by force+
lp15@62618
   936
lp15@63945
   937
lemma not_interval_UNIV2 [simp]:
lp15@63945
   938
  fixes a :: "'a::euclidean_space"
lp15@63945
   939
  shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b"
lp15@63945
   940
  using bounded_box[of a b] bounded_cbox[of a b] by force+
lp15@63945
   941
lp15@62618
   942
lemma compact_cbox [simp]:
immler@56189
   943
  fixes a :: "'a::euclidean_space"
immler@56189
   944
  shows "compact (cbox a b)"
immler@56189
   945
  using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
immler@56189
   946
  by (auto simp: compact_eq_seq_compact_metric)
immler@56189
   947
immler@56189
   948
lemma box_midpoint:
immler@56189
   949
  fixes a :: "'a::euclidean_space"
immler@56189
   950
  assumes "box a b \<noteq> {}"
immler@56189
   951
  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
immler@56189
   952
proof -
lp15@68120
   953
  have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
lp15@68120
   954
    using assms that by (auto simp: inner_add_left box_ne_empty)
immler@56189
   955
  then show ?thesis unfolding mem_box by auto
immler@56189
   956
qed
immler@56189
   957
immler@56189
   958
lemma open_cbox_convex:
immler@56189
   959
  fixes x :: "'a::euclidean_space"
immler@56189
   960
  assumes x: "x \<in> box a b"
immler@56189
   961
    and y: "y \<in> cbox a b"
immler@56189
   962
    and e: "0 < e" "e \<le> 1"
immler@56189
   963
  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
immler@56189
   964
proof -
immler@56189
   965
  {
immler@56189
   966
    fix i :: 'a
immler@56189
   967
    assume i: "i \<in> Basis"
immler@56189
   968
    have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
immler@56189
   969
      unfolding left_diff_distrib by simp
immler@56189
   970
    also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
lp15@68120
   971
    proof (rule add_less_le_mono)
lp15@68120
   972
      show "e * (a \<bullet> i) < e * (x \<bullet> i)"
lp15@68120
   973
        using \<open>0 < e\<close> i mem_box(1) x by auto
lp15@68120
   974
      show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)"
lp15@68120
   975
        by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
lp15@68120
   976
    qed
immler@56189
   977
    finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
immler@56189
   978
      unfolding inner_simps by auto
immler@56189
   979
    moreover
immler@56189
   980
    {
immler@56189
   981
      have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
immler@56189
   982
        unfolding left_diff_distrib by simp
immler@56189
   983
      also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
lp15@66827
   984
      proof (rule add_less_le_mono)
lp15@66827
   985
        show "e * (x \<bullet> i) < e * (b \<bullet> i)"
lp15@68120
   986
          using \<open>0 < e\<close> i mem_box(1) x by auto
lp15@66827
   987
        show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)"
lp15@68120
   988
          by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
lp15@66827
   989
      qed
immler@56189
   990
      finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
immler@56189
   991
        unfolding inner_simps by auto
immler@56189
   992
    }
immler@56189
   993
    ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
immler@56189
   994
      by auto
immler@56189
   995
  }
immler@56189
   996
  then show ?thesis
immler@56189
   997
    unfolding mem_box by auto
immler@56189
   998
qed
immler@56189
   999
lp15@63881
  1000
lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b"
lp15@63881
  1001
  by (simp add: closed_cbox)
lp15@63881
  1002
lp15@63881
  1003
lemma closure_box [simp]:
immler@56189
  1004
  fixes a :: "'a::euclidean_space"
immler@56189
  1005
   assumes "box a b \<noteq> {}"
immler@56189
  1006
  shows "closure (box a b) = cbox a b"
immler@56189
  1007
proof -
immler@56189
  1008
  have ab: "a <e b"
immler@56189
  1009
    using assms by (simp add: eucl_less_def box_ne_empty)
immler@56189
  1010
  let ?c = "(1 / 2) *\<^sub>R (a + b)"
immler@56189
  1011
  {
immler@56189
  1012
    fix x
immler@56189
  1013
    assume as:"x \<in> cbox a b"
wenzelm@63040
  1014
    define f where [abs_def]: "f n = x + (inverse (real n + 1)) *\<^sub>R (?c - x)" for n
immler@56189
  1015
    {
immler@56189
  1016
      fix n
immler@56189
  1017
      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
immler@56189
  1018
      have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
immler@56189
  1019
        unfolding inverse_le_1_iff by auto
immler@56189
  1020
      have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
immler@56189
  1021
        x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
lp15@66643
  1022
        by (auto simp: algebra_simps)
immler@56189
  1023
      then have "f n <e b" and "a <e f n"
immler@56189
  1024
        using open_cbox_convex[OF box_midpoint[OF assms] as *]
immler@56189
  1025
        unfolding f_def by (auto simp: box_def eucl_less_def)
immler@56189
  1026
      then have False
immler@56189
  1027
        using fn unfolding f_def using xc by auto
immler@56189
  1028
    }
immler@56189
  1029
    moreover
immler@56189
  1030
    {
wenzelm@61973
  1031
      assume "\<not> (f \<longlongrightarrow> x) sequentially"
immler@56189
  1032
      {
immler@56189
  1033
        fix e :: real
immler@56189
  1034
        assume "e > 0"
lp15@61609
  1035
        then obtain N :: nat where N: "inverse (real (N + 1)) < e"
lp15@68120
  1036
          using reals_Archimedean by auto
lp15@61609
  1037
        have "inverse (real n + 1) < e" if "N \<le> n" for n
lp15@61609
  1038
          by (auto intro!: that le_less_trans [OF _ N])
immler@56189
  1039
        then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
immler@56189
  1040
      }
wenzelm@61973
  1041
      then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially"
lp15@66643
  1042
        unfolding lim_sequentially by(auto simp: dist_norm)
wenzelm@61973
  1043
      then have "(f \<longlongrightarrow> x) sequentially"
immler@56189
  1044
        unfolding f_def
immler@56189
  1045
        using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
immler@56189
  1046
        using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
immler@56189
  1047
        by auto
immler@56189
  1048
    }
immler@56189
  1049
    ultimately have "x \<in> closure (box a b)"
lp15@68120
  1050
      using as box_midpoint[OF assms]
lp15@68120
  1051
      unfolding closure_def islimpt_sequential
immler@56189
  1052
      by (cases "x=?c") (auto simp: in_box_eucl_less)
immler@56189
  1053
  }
immler@56189
  1054
  then show ?thesis
immler@56189
  1055
    using closure_minimal[OF box_subset_cbox, of a b] by blast
immler@56189
  1056
qed
immler@56189
  1057
immler@56189
  1058
lemma bounded_subset_box_symmetric:
lp15@68120
  1059
  fixes S :: "('a::euclidean_space) set"
lp15@68120
  1060
  assumes "bounded S"
lp15@68120
  1061
  obtains a where "S \<subseteq> box (-a) a"
immler@56189
  1062
proof -
lp15@68120
  1063
  obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b"
immler@56189
  1064
    using assms[unfolded bounded_pos] by auto
wenzelm@63040
  1065
  define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)"
lp15@68120
  1066
  have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" if "x \<in> S" and i: "i \<in> Basis" for x i
lp15@68120
  1067
    using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
lp15@68120
  1068
  then have "S \<subseteq> box (-a) a"
lp15@68120
  1069
    by (auto simp: simp add: box_def)
lp15@68120
  1070
  then show ?thesis ..
immler@56189
  1071
qed
immler@56189
  1072
immler@56189
  1073
lemma bounded_subset_cbox_symmetric:
lp15@68120
  1074
  fixes S :: "('a::euclidean_space) set"
lp15@68120
  1075
  assumes "bounded S"
lp15@68120
  1076
  obtains a where "S \<subseteq> cbox (-a) a"
immler@56189
  1077
proof -
lp15@68120
  1078
  obtain a where "S \<subseteq> box (-a) a"
immler@56189
  1079
    using bounded_subset_box_symmetric[OF assms] by auto
immler@56189
  1080
  then show ?thesis
lp15@68120
  1081
    by (meson box_subset_cbox dual_order.trans that)
immler@56189
  1082
qed
immler@56189
  1083
immler@56189
  1084
lemma frontier_cbox:
immler@56189
  1085
  fixes a b :: "'a::euclidean_space"
immler@56189
  1086
  shows "frontier (cbox a b) = cbox a b - box a b"
immler@56189
  1087
  unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
immler@56189
  1088
immler@56189
  1089
lemma frontier_box:
immler@56189
  1090
  fixes a b :: "'a::euclidean_space"
immler@56189
  1091
  shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
immler@56189
  1092
proof (cases "box a b = {}")
immler@56189
  1093
  case True
immler@56189
  1094
  then show ?thesis
immler@56189
  1095
    using frontier_empty by auto
immler@56189
  1096
next
immler@56189
  1097
  case False
immler@56189
  1098
  then show ?thesis
immler@56189
  1099
    unfolding frontier_def and closure_box[OF False] and interior_open[OF open_box]
immler@56189
  1100
    by auto
immler@56189
  1101
qed
immler@56189
  1102
lp15@66884
  1103
lemma Int_interval_mixed_eq_empty:
immler@56189
  1104
  fixes a :: "'a::euclidean_space"
immler@56189
  1105
   assumes "box c d \<noteq> {}"
immler@56189
  1106
  shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
immler@56189
  1107
  unfolding closure_box[OF assms, symmetric]
lp15@62843
  1108
  unfolding open_Int_closure_eq_empty[OF open_box] ..
immler@56189
  1109
immler@56189
  1110
lemma eucl_less_eq_halfspaces:
wenzelm@61076
  1111
  fixes a :: "'a::euclidean_space"
immler@56189
  1112
  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
lp15@68120
  1113
        "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
immler@56189
  1114
  by (auto simp: eucl_less_def)
immler@56189
  1115
immler@56189
  1116
lemma open_Collect_eucl_less[simp, intro]:
wenzelm@61076
  1117
  fixes a :: "'a::euclidean_space"
lp15@68120
  1118
  shows "open {x. x <e a}" "open {x. a <e x}"
immler@56189
  1119
  by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
immler@56189
  1120
immler@54775
  1121
no_notation
immler@54775
  1122
  eucl_less (infix "<e" 50)
immler@54775
  1123
himmelma@33175
  1124
end