src/HOL/Analysis/Topology_Euclidean_Space.thy
author immler
Mon Jan 07 14:06:54 2019 +0100 (4 months ago)
changeset 69619 3f7d8e05e0f2
parent 69618 2be1baf40351
child 69676 56acd449da41
permissions -rw-r--r--
split off Convex.thy: material that does not require Topology_Euclidean_Space
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@69544
    11
    Elementary_Normed_Spaces
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
immler@69613
    34
subsection%unimportant\<open>Balls in Euclidean Space\<close>
immler@69613
    35
immler@69613
    36
lemma cball_subset_cball_iff:
immler@69613
    37
  fixes a :: "'a :: euclidean_space"
immler@69613
    38
  shows "cball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r < 0"
immler@69613
    39
    (is "?lhs \<longleftrightarrow> ?rhs")
immler@69613
    40
proof
immler@69613
    41
  assume ?lhs
immler@69613
    42
  then show ?rhs
immler@69613
    43
  proof (cases "r < 0")
immler@69613
    44
    case True
immler@69613
    45
    then show ?rhs by simp
immler@69613
    46
  next
immler@69613
    47
    case False
immler@69613
    48
    then have [simp]: "r \<ge> 0" by simp
immler@69613
    49
    have "norm (a - a') + r \<le> r'"
immler@69613
    50
    proof (cases "a = a'")
immler@69613
    51
      case True
immler@69613
    52
      then show ?thesis
immler@69613
    53
        using subsetD [where c = "a + r *\<^sub>R (SOME i. i \<in> Basis)", OF \<open>?lhs\<close>] subsetD [where c = a, OF \<open>?lhs\<close>]
immler@69613
    54
        by (force simp: SOME_Basis dist_norm)
immler@69613
    55
    next
immler@69613
    56
      case False
immler@69613
    57
      have "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = norm (a' - a - (r / norm (a - a')) *\<^sub>R (a - a'))"
immler@69613
    58
        by (simp add: algebra_simps)
immler@69613
    59
      also have "... = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))"
immler@69613
    60
        by (simp add: algebra_simps)
immler@69613
    61
      also from \<open>a \<noteq> a'\<close> have "... = \<bar>- norm (a - a') - r\<bar>"
immler@69613
    62
        by (simp add: abs_mult_pos field_simps)
immler@69613
    63
      finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \<bar>norm (a - a') + r\<bar>"
immler@69613
    64
        by linarith
immler@69613
    65
      from \<open>a \<noteq> a'\<close> show ?thesis
immler@69613
    66
        using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \<open>?lhs\<close>]
immler@69613
    67
        by (simp add: dist_norm scaleR_add_left)
immler@69613
    68
    qed
immler@69613
    69
    then show ?rhs
immler@69613
    70
      by (simp add: dist_norm)
immler@69613
    71
  qed
immler@69613
    72
next
immler@69613
    73
  assume ?rhs
immler@69613
    74
  then show ?lhs
immler@69613
    75
    by (auto simp: ball_def dist_norm)
immler@69613
    76
      (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans)
immler@69613
    77
qed
immler@69613
    78
immler@69613
    79
lemma cball_subset_ball_iff: "cball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r < r' \<or> r < 0"
immler@69613
    80
  (is "?lhs \<longleftrightarrow> ?rhs")
immler@69613
    81
  for a :: "'a::euclidean_space"
immler@69613
    82
proof
immler@69613
    83
  assume ?lhs
immler@69613
    84
  then show ?rhs
immler@69613
    85
  proof (cases "r < 0")
immler@69613
    86
    case True then
immler@69613
    87
    show ?rhs by simp
immler@69613
    88
  next
immler@69613
    89
    case False
immler@69613
    90
    then have [simp]: "r \<ge> 0" by simp
immler@69613
    91
    have "norm (a - a') + r < r'"
immler@69613
    92
    proof (cases "a = a'")
immler@69613
    93
      case True
immler@69613
    94
      then show ?thesis
immler@69613
    95
        using subsetD [where c = "a + r *\<^sub>R (SOME i. i \<in> Basis)", OF \<open>?lhs\<close>] subsetD [where c = a, OF \<open>?lhs\<close>]
immler@69613
    96
        by (force simp: SOME_Basis dist_norm)
immler@69613
    97
    next
immler@69613
    98
      case False
immler@69613
    99
      have False if "norm (a - a') + r \<ge> r'"
immler@69613
   100
      proof -
immler@69613
   101
        from that have "\<bar>r' - norm (a - a')\<bar> \<le> r"
immler@69613
   102
          by (simp split: abs_split)
immler@69613
   103
            (metis \<open>0 \<le> r\<close> \<open>?lhs\<close> centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq)
immler@69613
   104
        then show ?thesis
immler@69613
   105
          using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close>
immler@69613
   106
          by (simp add: dist_norm field_simps)
immler@69613
   107
            (simp add: diff_divide_distrib scaleR_left_diff_distrib)
immler@69613
   108
      qed
immler@69613
   109
      then show ?thesis by force
immler@69613
   110
    qed
immler@69613
   111
    then show ?rhs by (simp add: dist_norm)
immler@69613
   112
  qed
immler@69613
   113
next
immler@69613
   114
  assume ?rhs
immler@69613
   115
  then show ?lhs
immler@69613
   116
    by (auto simp: ball_def dist_norm)
immler@69613
   117
      (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans)
immler@69613
   118
qed
immler@69613
   119
immler@69613
   120
lemma ball_subset_cball_iff: "ball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
immler@69613
   121
  (is "?lhs = ?rhs")
immler@69613
   122
  for a :: "'a::euclidean_space"
immler@69613
   123
proof (cases "r \<le> 0")
immler@69613
   124
  case True
immler@69613
   125
  then show ?thesis
immler@69613
   126
    using dist_not_less_zero less_le_trans by force
immler@69613
   127
next
immler@69613
   128
  case False
immler@69613
   129
  show ?thesis
immler@69613
   130
  proof
immler@69613
   131
    assume ?lhs
immler@69613
   132
    then have "(cball a r \<subseteq> cball a' r')"
immler@69613
   133
      by (metis False closed_cball closure_ball closure_closed closure_mono not_less)
immler@69613
   134
    with False show ?rhs
immler@69613
   135
      by (fastforce iff: cball_subset_cball_iff)
immler@69613
   136
  next
immler@69613
   137
    assume ?rhs
immler@69613
   138
    with False show ?lhs
immler@69613
   139
      using ball_subset_cball cball_subset_cball_iff by blast
immler@69613
   140
  qed
immler@69613
   141
qed
immler@69613
   142
immler@69613
   143
lemma ball_subset_ball_iff:
immler@69613
   144
  fixes a :: "'a :: euclidean_space"
immler@69613
   145
  shows "ball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
immler@69613
   146
        (is "?lhs = ?rhs")
immler@69613
   147
proof (cases "r \<le> 0")
immler@69613
   148
  case True then show ?thesis
immler@69613
   149
    using dist_not_less_zero less_le_trans by force
immler@69613
   150
next
immler@69613
   151
  case False show ?thesis
immler@69613
   152
  proof
immler@69613
   153
    assume ?lhs
immler@69613
   154
    then have "0 < r'"
immler@69613
   155
      by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less set_mp)
immler@69613
   156
    then have "(cball a r \<subseteq> cball a' r')"
immler@69613
   157
      by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
immler@69613
   158
    then show ?rhs
immler@69613
   159
      using False cball_subset_cball_iff by fastforce
immler@69613
   160
  next
immler@69613
   161
  assume ?rhs then show ?lhs
immler@69613
   162
    apply (auto simp: ball_def)
immler@69613
   163
    apply (metis add.commute add_le_cancel_right dist_commute dist_triangle_lt not_le order_trans)
immler@69613
   164
    using dist_not_less_zero order.strict_trans2 apply blast
immler@69613
   165
    done
immler@69613
   166
  qed
immler@69613
   167
qed
immler@69613
   168
immler@69613
   169
immler@69613
   170
lemma ball_eq_ball_iff:
immler@69613
   171
  fixes x :: "'a :: euclidean_space"
immler@69613
   172
  shows "ball x d = ball y e \<longleftrightarrow> d \<le> 0 \<and> e \<le> 0 \<or> x=y \<and> d=e"
immler@69613
   173
        (is "?lhs = ?rhs")
immler@69613
   174
proof
immler@69613
   175
  assume ?lhs
immler@69613
   176
  then show ?rhs
immler@69613
   177
  proof (cases "d \<le> 0 \<or> e \<le> 0")
immler@69613
   178
    case True
immler@69613
   179
      with \<open>?lhs\<close> show ?rhs
immler@69613
   180
        by safe (simp_all only: ball_eq_empty [of y e, symmetric] ball_eq_empty [of x d, symmetric])
immler@69613
   181
  next
immler@69613
   182
    case False
immler@69613
   183
    with \<open>?lhs\<close> show ?rhs
immler@69613
   184
      apply (auto simp: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
immler@69613
   185
      apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
immler@69613
   186
      apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
immler@69613
   187
      done
immler@69613
   188
  qed
immler@69613
   189
next
immler@69613
   190
  assume ?rhs then show ?lhs
immler@69613
   191
    by (auto simp: set_eq_subset ball_subset_ball_iff)
immler@69613
   192
qed
immler@69613
   193
immler@69613
   194
lemma cball_eq_cball_iff:
immler@69613
   195
  fixes x :: "'a :: euclidean_space"
immler@69613
   196
  shows "cball x d = cball y e \<longleftrightarrow> d < 0 \<and> e < 0 \<or> x=y \<and> d=e"
immler@69613
   197
        (is "?lhs = ?rhs")
immler@69613
   198
proof
immler@69613
   199
  assume ?lhs
immler@69613
   200
  then show ?rhs
immler@69613
   201
  proof (cases "d < 0 \<or> e < 0")
immler@69613
   202
    case True
immler@69613
   203
      with \<open>?lhs\<close> show ?rhs
immler@69613
   204
        by safe (simp_all only: cball_eq_empty [of y e, symmetric] cball_eq_empty [of x d, symmetric])
immler@69613
   205
  next
immler@69613
   206
    case False
immler@69613
   207
    with \<open>?lhs\<close> show ?rhs
immler@69613
   208
      apply (auto simp: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
immler@69613
   209
      apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
immler@69613
   210
      apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
immler@69613
   211
      done
immler@69613
   212
  qed
immler@69613
   213
next
immler@69613
   214
  assume ?rhs then show ?lhs
immler@69613
   215
    by (auto simp: set_eq_subset cball_subset_cball_iff)
immler@69613
   216
qed
immler@69613
   217
immler@69613
   218
lemma ball_eq_cball_iff:
immler@69613
   219
  fixes x :: "'a :: euclidean_space"
immler@69613
   220
  shows "ball x d = cball y e \<longleftrightarrow> d \<le> 0 \<and> e < 0" (is "?lhs = ?rhs")
immler@69613
   221
proof
immler@69613
   222
  assume ?lhs
immler@69613
   223
  then show ?rhs
immler@69613
   224
    apply (auto simp: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
immler@69613
   225
    apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
immler@69613
   226
    apply (metis add_less_same_cancel1 dist_not_less_zero less_le_trans not_le)
immler@69613
   227
    using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
immler@69613
   228
    done
immler@69613
   229
next
immler@69613
   230
  assume ?rhs then show ?lhs by auto
immler@69613
   231
qed
immler@69613
   232
immler@69613
   233
lemma cball_eq_ball_iff:
immler@69613
   234
  fixes x :: "'a :: euclidean_space"
immler@69613
   235
  shows "cball x d = ball y e \<longleftrightarrow> d < 0 \<and> e \<le> 0"
immler@69613
   236
  using ball_eq_cball_iff by blast
immler@69613
   237
immler@69613
   238
lemma finite_ball_avoid:
immler@69613
   239
  fixes S :: "'a :: euclidean_space set"
immler@69613
   240
  assumes "open S" "finite X" "p \<in> S"
immler@69613
   241
  shows "\<exists>e>0. \<forall>w\<in>ball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
immler@69613
   242
proof -
immler@69613
   243
  obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S"
immler@69613
   244
    using open_contains_ball_eq[OF \<open>open S\<close>] assms by auto
immler@69613
   245
  obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
immler@69613
   246
    using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
immler@69613
   247
  hence "\<forall>w\<in>ball p (min e1 e2). w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" using e1_b by auto
immler@69613
   248
  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> \<open>e1>0\<close>
immler@69613
   249
    apply (rule_tac x="min e1 e2" in exI)
immler@69613
   250
    by auto
immler@69613
   251
qed
immler@69613
   252
immler@69613
   253
lemma finite_cball_avoid:
immler@69613
   254
  fixes S :: "'a :: euclidean_space set"
immler@69613
   255
  assumes "open S" "finite X" "p \<in> S"
immler@69613
   256
  shows "\<exists>e>0. \<forall>w\<in>cball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
immler@69613
   257
proof -
immler@69613
   258
  obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
immler@69613
   259
    using finite_ball_avoid[OF assms] by auto
immler@69613
   260
  define e2 where "e2 \<equiv> e1/2"
immler@69613
   261
  have "e2>0" and "e2 < e1" unfolding e2_def using \<open>e1>0\<close> by auto
immler@69613
   262
  then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto)
immler@69613
   263
  then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> e1 by auto
immler@69613
   264
qed
immler@69613
   265
immler@69619
   266
lemma dim_cball:
immler@69619
   267
  assumes "e > 0"
immler@69619
   268
  shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
immler@69619
   269
proof -
immler@69619
   270
  {
immler@69619
   271
    fix x :: "'n::euclidean_space"
immler@69619
   272
    define y where "y = (e / norm x) *\<^sub>R x"
immler@69619
   273
    then have "y \<in> cball 0 e"
immler@69619
   274
      using assms by auto
immler@69619
   275
    moreover have *: "x = (norm x / e) *\<^sub>R y"
immler@69619
   276
      using y_def assms by simp
immler@69619
   277
    moreover from * have "x = (norm x/e) *\<^sub>R y"
immler@69619
   278
      by auto
immler@69619
   279
    ultimately have "x \<in> span (cball 0 e)"
immler@69619
   280
      using span_scale[of y "cball 0 e" "norm x/e"]
immler@69619
   281
        span_superset[of "cball 0 e"]
immler@69619
   282
      by (simp add: span_base)
immler@69619
   283
  }
immler@69619
   284
  then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
immler@69619
   285
    by auto
immler@69619
   286
  then show ?thesis
immler@69619
   287
    using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp: dim_UNIV)
immler@69619
   288
qed
immler@69619
   289
immler@69613
   290
wenzelm@60420
   291
subsection \<open>Boxes\<close>
immler@56189
   292
hoelzl@57447
   293
abbreviation One :: "'a::euclidean_space"
hoelzl@57447
   294
  where "One \<equiv> \<Sum>Basis"
hoelzl@57447
   295
lp15@63114
   296
lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
lp15@63114
   297
proof -
lp15@63114
   298
  have "dependent (Basis :: 'a set)"
lp15@63114
   299
    apply (simp add: dependent_finite)
lp15@63114
   300
    apply (rule_tac x="\<lambda>i. 1" in exI)
lp15@63114
   301
    using SOME_Basis apply (auto simp: assms)
lp15@63114
   302
    done
lp15@63114
   303
  with independent_Basis show False by force
lp15@63114
   304
qed
lp15@63114
   305
lp15@63114
   306
corollary One_neq_0[iff]: "One \<noteq> 0"
lp15@63114
   307
  by (metis One_non_0)
lp15@63114
   308
lp15@63114
   309
corollary Zero_neq_One[iff]: "0 \<noteq> One"
lp15@63114
   310
  by (metis One_non_0)
lp15@63114
   311
immler@67962
   312
definition%important (in euclidean_space) eucl_less (infix "<e" 50)
immler@54775
   313
  where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
immler@54775
   314
immler@67962
   315
definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
immler@67962
   316
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
   317
immler@54775
   318
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
   319
  and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
immler@56188
   320
  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
   321
    "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
   322
  by (auto simp: box_eucl_less eucl_less_def cbox_def)
immler@56188
   323
lp15@60615
   324
lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \<times> cbox c d"
lp15@60615
   325
  by (force simp: cbox_def Basis_prod_def)
lp15@60615
   326
lp15@60615
   327
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
   328
  by (force simp: cbox_Pair_eq)
lp15@60615
   329
lp15@65587
   330
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
   331
  apply (auto simp: cbox_def Basis_complex_def)
lp15@65587
   332
  apply (rule_tac x = "(Re x, Im x)" in image_eqI)
lp15@65587
   333
  using complex_eq by auto
lp15@65587
   334
lp15@60615
   335
lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
lp15@60615
   336
  by (force simp: cbox_Pair_eq)
lp15@60615
   337
lp15@60615
   338
lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
lp15@60615
   339
  by auto
lp15@60615
   340
immler@56188
   341
lemma mem_box_real[simp]:
immler@56188
   342
  "(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b"
immler@56188
   343
  "(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b"
immler@56188
   344
  by (auto simp: mem_box)
immler@56188
   345
immler@56188
   346
lemma box_real[simp]:
immler@56188
   347
  fixes a b:: real
immler@56188
   348
  shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
immler@56188
   349
  by auto
hoelzl@50526
   350
hoelzl@57447
   351
lemma box_Int_box:
hoelzl@57447
   352
  fixes a :: "'a::euclidean_space"
hoelzl@57447
   353
  shows "box a b \<inter> box c d =
hoelzl@57447
   354
    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
   355
  unfolding set_eq_iff and Int_iff and mem_box by auto
hoelzl@57447
   356
immler@50087
   357
lemma rational_boxes:
wenzelm@61076
   358
  fixes x :: "'a::euclidean_space"
wenzelm@53291
   359
  assumes "e > 0"
lp15@66643
   360
  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
   361
proof -
wenzelm@63040
   362
  define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
wenzelm@53291
   363
  then have e: "e' > 0"
nipkow@56541
   364
    using assms by (auto simp: DIM_positive)
hoelzl@50526
   365
  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
   366
  proof
wenzelm@53255
   367
    fix i
wenzelm@53255
   368
    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
wenzelm@53255
   369
    show "?th i" by auto
immler@50087
   370
  qed
wenzelm@55522
   371
  from choice[OF this] obtain a where
wenzelm@55522
   372
    a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
hoelzl@50526
   373
  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
   374
  proof
wenzelm@53255
   375
    fix i
wenzelm@53255
   376
    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
wenzelm@53255
   377
    show "?th i" by auto
immler@50087
   378
  qed
wenzelm@55522
   379
  from choice[OF this] obtain b where
wenzelm@55522
   380
    b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
hoelzl@50526
   381
  let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
hoelzl@50526
   382
  show ?thesis
hoelzl@50526
   383
  proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
wenzelm@53255
   384
    fix y :: 'a
wenzelm@53255
   385
    assume *: "y \<in> box ?a ?b"
wenzelm@53015
   386
    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
nipkow@67155
   387
      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
hoelzl@50526
   388
    also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
nipkow@64267
   389
    proof (rule real_sqrt_less_mono, rule sum_strict_mono)
wenzelm@53255
   390
      fix i :: "'a"
wenzelm@53255
   391
      assume i: "i \<in> Basis"
wenzelm@53255
   392
      have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
wenzelm@53255
   393
        using * i by (auto simp: box_def)
wenzelm@53255
   394
      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
wenzelm@53255
   395
        using a by auto
wenzelm@53255
   396
      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
wenzelm@53255
   397
        using b by auto
wenzelm@53255
   398
      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
wenzelm@53255
   399
        by auto
hoelzl@50526
   400
      then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
immler@50087
   401
        unfolding e'_def by (auto simp: dist_real_def)
wenzelm@53015
   402
      then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
immler@50087
   403
        by (rule power_strict_mono) auto
wenzelm@53015
   404
      then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
immler@50087
   405
        by (simp add: power_divide)
immler@50087
   406
    qed auto
wenzelm@53255
   407
    also have "\<dots> = e"
lp15@61609
   408
      using \<open>0 < e\<close> by simp
wenzelm@53255
   409
    finally show "y \<in> ball x e"
wenzelm@53255
   410
      by (auto simp: ball_def)
hoelzl@50526
   411
  qed (insert a b, auto simp: box_def)
hoelzl@50526
   412
qed
immler@51103
   413
hoelzl@50526
   414
lemma open_UNION_box:
wenzelm@61076
   415
  fixes M :: "'a::euclidean_space set"
wenzelm@53282
   416
  assumes "open M"
hoelzl@50526
   417
  defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
hoelzl@50526
   418
  defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
wenzelm@53015
   419
  defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
hoelzl@50526
   420
  shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
wenzelm@52624
   421
proof -
wenzelm@60462
   422
  have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" if "x \<in> M" for x
wenzelm@60462
   423
  proof -
wenzelm@52624
   424
    obtain e where e: "e > 0" "ball x e \<subseteq> M"
wenzelm@60420
   425
      using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
wenzelm@53282
   426
    moreover obtain a b where ab:
wenzelm@53282
   427
      "x \<in> box a b"
wenzelm@53282
   428
      "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
wenzelm@53282
   429
      "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>"
wenzelm@53282
   430
      "box a b \<subseteq> ball x e"
wenzelm@52624
   431
      using rational_boxes[OF e(1)] by metis
wenzelm@60462
   432
    ultimately show ?thesis
wenzelm@52624
   433
       by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
wenzelm@52624
   434
          (auto simp: euclidean_representation I_def a'_def b'_def)
wenzelm@60462
   435
  qed
wenzelm@52624
   436
  then show ?thesis by (auto simp: I_def)
wenzelm@52624
   437
qed
wenzelm@52624
   438
lp15@66154
   439
corollary open_countable_Union_open_box:
lp15@66154
   440
  fixes S :: "'a :: euclidean_space set"
lp15@66154
   441
  assumes "open S"
lp15@66154
   442
  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
   443
proof -
lp15@66154
   444
  let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
lp15@66154
   445
  let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
lp15@66154
   446
  let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (?a f) (?b f) \<subseteq> S}"
lp15@66154
   447
  let ?\<D> = "(\<lambda>f. box (?a f) (?b f)) ` ?I"
lp15@66154
   448
  show ?thesis
lp15@66154
   449
  proof
lp15@66154
   450
    have "countable ?I"
lp15@66154
   451
      by (simp add: countable_PiE countable_rat)
lp15@66154
   452
    then show "countable ?\<D>"
lp15@66154
   453
      by blast
lp15@66154
   454
    show "\<Union>?\<D> = S"
lp15@66154
   455
      using open_UNION_box [OF assms] by metis
lp15@66154
   456
  qed auto
lp15@66154
   457
qed
lp15@66154
   458
lp15@66154
   459
lemma rational_cboxes:
lp15@66154
   460
  fixes x :: "'a::euclidean_space"
lp15@66154
   461
  assumes "e > 0"
lp15@66154
   462
  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
   463
proof -
lp15@66154
   464
  define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
lp15@66154
   465
  then have e: "e' > 0"
lp15@66154
   466
    using assms by auto
lp15@66154
   467
  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
   468
  proof
lp15@66154
   469
    fix i
lp15@66154
   470
    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
lp15@66154
   471
    show "?th i" by auto
lp15@66154
   472
  qed
lp15@66154
   473
  from choice[OF this] obtain a where
lp15@66154
   474
    a: "\<forall>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" ..
lp15@66154
   475
  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
   476
  proof
lp15@66154
   477
    fix i
lp15@66154
   478
    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
lp15@66154
   479
    show "?th i" by auto
lp15@66154
   480
  qed
lp15@66154
   481
  from choice[OF this] obtain b where
lp15@66154
   482
    b: "\<forall>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" ..
lp15@66154
   483
  let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
lp15@66154
   484
  show ?thesis
lp15@66154
   485
  proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
lp15@66154
   486
    fix y :: 'a
lp15@66154
   487
    assume *: "y \<in> cbox ?a ?b"
lp15@66154
   488
    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
nipkow@67155
   489
      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
lp15@66154
   490
    also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
lp15@66154
   491
    proof (rule real_sqrt_less_mono, rule sum_strict_mono)
lp15@66154
   492
      fix i :: "'a"
lp15@66154
   493
      assume i: "i \<in> Basis"
lp15@66154
   494
      have "a i \<le> y\<bullet>i \<and> y\<bullet>i \<le> b i"
lp15@66154
   495
        using * i by (auto simp: cbox_def)
lp15@66154
   496
      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
lp15@66154
   497
        using a by auto
lp15@66154
   498
      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
lp15@66154
   499
        using b by auto
lp15@66154
   500
      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
lp15@66154
   501
        by auto
lp15@66154
   502
      then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
lp15@66154
   503
        unfolding e'_def by (auto simp: dist_real_def)
lp15@66154
   504
      then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
lp15@66154
   505
        by (rule power_strict_mono) auto
lp15@66154
   506
      then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
lp15@66154
   507
        by (simp add: power_divide)
lp15@66154
   508
    qed auto
lp15@66154
   509
    also have "\<dots> = e"
lp15@66154
   510
      using \<open>0 < e\<close> by simp
lp15@66154
   511
    finally show "y \<in> ball x e"
lp15@66154
   512
      by (auto simp: ball_def)
lp15@66154
   513
  next
lp15@66154
   514
    show "x \<in> cbox (\<Sum>i\<in>Basis. a i *\<^sub>R i) (\<Sum>i\<in>Basis. b i *\<^sub>R i)"
lp15@66154
   515
      using a b less_imp_le by (auto simp: cbox_def)
lp15@66154
   516
  qed (use a b cbox_def in auto)
lp15@66154
   517
qed
lp15@66154
   518
lp15@66154
   519
lemma open_UNION_cbox:
lp15@66154
   520
  fixes M :: "'a::euclidean_space set"
lp15@66154
   521
  assumes "open M"
lp15@66154
   522
  defines "a' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
lp15@66154
   523
  defines "b' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
lp15@66154
   524
  defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (a' f) (b' f) \<subseteq> M}"
lp15@66154
   525
  shows "M = (\<Union>f\<in>I. cbox (a' f) (b' f))"
lp15@66154
   526
proof -
lp15@66154
   527
  have "x \<in> (\<Union>f\<in>I. cbox (a' f) (b' f))" if "x \<in> M" for x
lp15@66154
   528
  proof -
lp15@66154
   529
    obtain e where e: "e > 0" "ball x e \<subseteq> M"
lp15@66154
   530
      using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
lp15@66154
   531
    moreover obtain a b where ab: "x \<in> cbox a b" "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
lp15@66154
   532
                                  "\<forall>i \<in> Basis. b \<bullet> i \<in> \<rat>" "cbox a b \<subseteq> ball x e"
lp15@66154
   533
      using rational_cboxes[OF e(1)] by metis
lp15@66154
   534
    ultimately show ?thesis
lp15@66154
   535
       by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
lp15@66154
   536
          (auto simp: euclidean_representation I_def a'_def b'_def)
lp15@66154
   537
  qed
lp15@66154
   538
  then show ?thesis by (auto simp: I_def)
lp15@66154
   539
qed
lp15@66154
   540
lp15@66154
   541
corollary open_countable_Union_open_cbox:
lp15@66154
   542
  fixes S :: "'a :: euclidean_space set"
lp15@66154
   543
  assumes "open S"
lp15@66154
   544
  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
   545
proof -
lp15@66154
   546
  let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
lp15@66154
   547
  let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
lp15@66154
   548
  let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (?a f) (?b f) \<subseteq> S}"
lp15@66154
   549
  let ?\<D> = "(\<lambda>f. cbox (?a f) (?b f)) ` ?I"
lp15@66154
   550
  show ?thesis
lp15@66154
   551
  proof
lp15@66154
   552
    have "countable ?I"
lp15@66154
   553
      by (simp add: countable_PiE countable_rat)
lp15@66154
   554
    then show "countable ?\<D>"
lp15@66154
   555
      by blast
lp15@66154
   556
    show "\<Union>?\<D> = S"
lp15@66154
   557
      using open_UNION_cbox [OF assms] by metis
lp15@66154
   558
  qed auto
lp15@66154
   559
qed
lp15@66154
   560
immler@56189
   561
lemma box_eq_empty:
immler@56189
   562
  fixes a :: "'a::euclidean_space"
immler@56189
   563
  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
immler@56189
   564
    and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
immler@56189
   565
proof -
immler@56189
   566
  {
immler@56189
   567
    fix i x
immler@56189
   568
    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
immler@56189
   569
    then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
immler@56189
   570
      unfolding mem_box by (auto simp: box_def)
immler@56189
   571
    then have "a\<bullet>i < b\<bullet>i" by auto
immler@56189
   572
    then have False using as by auto
immler@56189
   573
  }
immler@56189
   574
  moreover
immler@56189
   575
  {
immler@56189
   576
    assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
immler@56189
   577
    let ?x = "(1/2) *\<^sub>R (a + b)"
immler@56189
   578
    {
immler@56189
   579
      fix i :: 'a
immler@56189
   580
      assume i: "i \<in> Basis"
immler@56189
   581
      have "a\<bullet>i < b\<bullet>i"
immler@56189
   582
        using as[THEN bspec[where x=i]] i by auto
immler@56189
   583
      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
   584
        by (auto simp: inner_add_left)
immler@56189
   585
    }
immler@56189
   586
    then have "box a b \<noteq> {}"
immler@56189
   587
      using mem_box(1)[of "?x" a b] by auto
immler@56189
   588
  }
immler@56189
   589
  ultimately show ?th1 by blast
immler@56189
   590
immler@56189
   591
  {
immler@56189
   592
    fix i x
immler@56189
   593
    assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
immler@56189
   594
    then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
immler@56189
   595
      unfolding mem_box by auto
immler@56189
   596
    then have "a\<bullet>i \<le> b\<bullet>i" by auto
immler@56189
   597
    then have False using as by auto
immler@56189
   598
  }
immler@56189
   599
  moreover
immler@56189
   600
  {
immler@56189
   601
    assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
immler@56189
   602
    let ?x = "(1/2) *\<^sub>R (a + b)"
immler@56189
   603
    {
immler@56189
   604
      fix i :: 'a
immler@56189
   605
      assume i:"i \<in> Basis"
immler@56189
   606
      have "a\<bullet>i \<le> b\<bullet>i"
immler@56189
   607
        using as[THEN bspec[where x=i]] i by auto
immler@56189
   608
      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
   609
        by (auto simp: inner_add_left)
immler@56189
   610
    }
immler@56189
   611
    then have "cbox a b \<noteq> {}"
immler@56189
   612
      using mem_box(2)[of "?x" a b] by auto
immler@56189
   613
  }
immler@56189
   614
  ultimately show ?th2 by blast
immler@56189
   615
qed
immler@56189
   616
immler@56189
   617
lemma box_ne_empty:
immler@56189
   618
  fixes a :: "'a::euclidean_space"
immler@56189
   619
  shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
immler@56189
   620
  and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
immler@56189
   621
  unfolding box_eq_empty[of a b] by fastforce+
immler@56189
   622
immler@56189
   623
lemma
immler@56189
   624
  fixes a :: "'a::euclidean_space"
lp15@66112
   625
  shows cbox_sing [simp]: "cbox a a = {a}"
lp15@66112
   626
    and box_sing [simp]: "box a a = {}"
immler@56189
   627
  unfolding set_eq_iff mem_box eq_iff [symmetric]
immler@56189
   628
  by (auto intro!: euclidean_eqI[where 'a='a])
immler@56189
   629
     (metis all_not_in_conv nonempty_Basis)
immler@56189
   630
immler@56189
   631
lemma subset_box_imp:
immler@56189
   632
  fixes a :: "'a::euclidean_space"
immler@56189
   633
  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
   634
    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
   635
    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
   636
     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
   637
  unfolding subset_eq[unfolded Ball_def] unfolding mem_box
wenzelm@58757
   638
  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
immler@56189
   639
immler@56189
   640
lemma box_subset_cbox:
immler@56189
   641
  fixes a :: "'a::euclidean_space"
immler@56189
   642
  shows "box a b \<subseteq> cbox a b"
immler@56189
   643
  unfolding subset_eq [unfolded Ball_def] mem_box
immler@56189
   644
  by (fast intro: less_imp_le)
immler@56189
   645
immler@56189
   646
lemma subset_box:
immler@56189
   647
  fixes a :: "'a::euclidean_space"
wenzelm@64539
   648
  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
   649
    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
   650
    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
   651
    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
   652
proof -
lp15@68120
   653
  let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
lp15@68120
   654
  let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
lp15@68120
   655
  show ?th1 ?th2
lp15@68120
   656
    by (fastforce simp: mem_box)+
lp15@68120
   657
  have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
lp15@68120
   658
    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
   659
  proof -
lp15@68120
   660
    have "box c d \<noteq> {}"
lp15@68120
   661
      using that
lp15@68120
   662
      unfolding box_eq_empty by force
lp15@68120
   663
    { 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
   664
      assume *: "a\<bullet>i > c\<bullet>i"
lp15@68120
   665
      then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j
lp15@68120
   666
        using cd that by (fastforce simp add: i *)
lp15@68120
   667
      then have "?x \<in> box c d"
lp15@68120
   668
        unfolding mem_box by auto
lp15@68120
   669
      moreover have "?x \<notin> cbox a b"
lp15@68120
   670
        using i cd * by (force simp: mem_box)
lp15@68120
   671
      ultimately have False using box by auto
immler@56189
   672
    }
lp15@68120
   673
    then have "a\<bullet>i \<le> c\<bullet>i" by force
immler@56189
   674
    moreover
lp15@68120
   675
    { 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
   676
      assume *: "b\<bullet>i < d\<bullet>i"
lp15@68120
   677
      then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j
lp15@68120
   678
        using cd that by (fastforce simp add: i *)
lp15@68120
   679
      then have "?x \<in> box c d"
immler@56189
   680
        unfolding mem_box by auto
lp15@68120
   681
      moreover have "?x \<notin> cbox a b"
lp15@68120
   682
        using i cd * by (force simp: mem_box)
lp15@68120
   683
      ultimately have False using box by auto
immler@56189
   684
    }
immler@56189
   685
    then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
lp15@68120
   686
    ultimately show ?thesis by auto
lp15@68120
   687
  qed
immler@56189
   688
  show ?th3
lp15@68120
   689
    using acdb by (fastforce simp add: mem_box)
lp15@68120
   690
  have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
lp15@68120
   691
    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
   692
      using box_subset_cbox[of a b] that acdb by auto
immler@56189
   693
  show ?th4
lp15@68120
   694
    using acdb' by (fastforce simp add: mem_box)
immler@56189
   695
qed
immler@56189
   696
lp15@63945
   697
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
   698
      (is "?lhs = ?rhs")
lp15@63945
   699
proof
lp15@63945
   700
  assume ?lhs
lp15@63945
   701
  then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> cbox a b"
lp15@63945
   702
    by auto
lp15@63945
   703
  then show ?rhs
lp15@66643
   704
    by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
lp15@63945
   705
next
lp15@63945
   706
  assume ?rhs
lp15@63945
   707
  then show ?lhs
lp15@63945
   708
    by force
lp15@63945
   709
qed
lp15@63945
   710
lp15@63945
   711
lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
wenzelm@64539
   712
  (is "?lhs \<longleftrightarrow> ?rhs")
lp15@63945
   713
proof
lp15@68120
   714
  assume L: ?lhs
lp15@68120
   715
  then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
lp15@63945
   716
    by auto
lp15@63945
   717
  then show ?rhs
hoelzl@63957
   718
    apply (simp add: subset_box)
lp15@68120
   719
    using L box_ne_empty box_sing apply (fastforce simp add:)
lp15@63945
   720
    done
lp15@68120
   721
qed force
lp15@63945
   722
lp15@63945
   723
lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
lp15@63945
   724
  by (metis eq_cbox_box)
lp15@63945
   725
lp15@63945
   726
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
   727
  (is "?lhs \<longleftrightarrow> ?rhs")
lp15@63945
   728
proof
lp15@68120
   729
  assume L: ?lhs
lp15@63945
   730
  then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
lp15@63945
   731
    by auto
lp15@63945
   732
  then show ?rhs
lp15@63945
   733
    apply (simp add: subset_box)
lp15@68120
   734
    using box_ne_empty(2) L
lp15@63945
   735
    apply auto
lp15@63945
   736
     apply (meson euclidean_eqI less_eq_real_def not_less)+
lp15@63945
   737
    done
lp15@68120
   738
qed force
lp15@63945
   739
eberlm@66466
   740
lemma subset_box_complex:
lp15@66643
   741
   "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
eberlm@66466
   742
      (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
   743
   "cbox a b \<subseteq> box c d \<longleftrightarrow>
eberlm@66466
   744
      (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
   745
   "box a b \<subseteq> cbox c d \<longleftrightarrow>
eberlm@66466
   746
      (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
   747
   "box a b \<subseteq> box c d \<longleftrightarrow>
eberlm@66466
   748
      (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
   749
  by (subst subset_box; force simp: Basis_complex_def)+
eberlm@66466
   750
lp15@63945
   751
lemma Int_interval:
immler@56189
   752
  fixes a :: "'a::euclidean_space"
immler@56189
   753
  shows "cbox a b \<inter> cbox c d =
immler@56189
   754
    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
   755
  unfolding set_eq_iff and Int_iff and mem_box
immler@56189
   756
  by auto
immler@56189
   757
immler@56189
   758
lemma disjoint_interval:
immler@56189
   759
  fixes a::"'a::euclidean_space"
immler@56189
   760
  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
   761
    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
   762
    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
   763
    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
   764
proof -
immler@56189
   765
  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
   766
  have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
immler@56189
   767
      (\<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
   768
    by blast
immler@56189
   769
  note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
immler@56189
   770
  show ?th1 unfolding * by (intro **) auto
immler@56189
   771
  show ?th2 unfolding * by (intro **) auto
immler@56189
   772
  show ?th3 unfolding * by (intro **) auto
immler@56189
   773
  show ?th4 unfolding * by (intro **) auto
immler@56189
   774
qed
immler@56189
   775
hoelzl@57447
   776
lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
hoelzl@57447
   777
proof -
wenzelm@61942
   778
  have "\<bar>x \<bullet> b\<bar> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
wenzelm@60462
   779
    if [simp]: "b \<in> Basis" for x b :: 'a
wenzelm@60462
   780
  proof -
wenzelm@61942
   781
    have "\<bar>x \<bullet> b\<bar> \<le> real_of_int \<lceil>\<bar>x \<bullet> b\<bar>\<rceil>"
lp15@61609
   782
      by (rule le_of_int_ceiling)
wenzelm@61942
   783
    also have "\<dots> \<le> real_of_int \<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil>"
nipkow@59587
   784
      by (auto intro!: ceiling_mono)
wenzelm@61942
   785
    also have "\<dots> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
hoelzl@57447
   786
      by simp
wenzelm@60462
   787
    finally show ?thesis .
wenzelm@60462
   788
  qed
wenzelm@60462
   789
  then have "\<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" for x :: 'a
nipkow@59587
   790
    by (metis order.strict_trans reals_Archimedean2)
hoelzl@57447
   791
  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
   792
    by auto
hoelzl@57447
   793
  ultimately show ?thesis
nipkow@64267
   794
    by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
hoelzl@57447
   795
qed
hoelzl@57447
   796
immler@69613
   797
lemma image_affinity_cbox: fixes m::real
immler@69613
   798
  fixes a b c :: "'a::euclidean_space"
immler@69613
   799
  shows "(\<lambda>x. m *\<^sub>R x + c) ` cbox a b =
immler@69613
   800
    (if cbox a b = {} then {}
immler@69613
   801
     else (if 0 \<le> m then cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)
immler@69613
   802
     else cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c)))"
immler@69613
   803
proof (cases "m = 0")
immler@69613
   804
  case True
immler@69613
   805
  {
immler@69613
   806
    fix x
immler@69613
   807
    assume "\<forall>i\<in>Basis. x \<bullet> i \<le> c \<bullet> i" "\<forall>i\<in>Basis. c \<bullet> i \<le> x \<bullet> i"
immler@69613
   808
    then have "x = c"
immler@69613
   809
      by (simp add: dual_order.antisym euclidean_eqI)
immler@69613
   810
  }
immler@69613
   811
  moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
immler@69613
   812
    unfolding True by (auto simp: cbox_sing)
immler@69613
   813
  ultimately show ?thesis using True by (auto simp: cbox_def)
immler@69613
   814
next
immler@69613
   815
  case False
immler@69613
   816
  {
immler@69613
   817
    fix y
immler@69613
   818
    assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m > 0"
immler@69613
   819
    then have "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
immler@69613
   820
      by (auto simp: inner_distrib)
immler@69613
   821
  }
immler@69613
   822
  moreover
immler@69613
   823
  {
immler@69613
   824
    fix y
immler@69613
   825
    assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m < 0"
immler@69613
   826
    then have "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i"
immler@69613
   827
      by (auto simp: mult_left_mono_neg inner_distrib)
immler@69613
   828
  }
immler@69613
   829
  moreover
immler@69613
   830
  {
immler@69613
   831
    fix y
immler@69613
   832
    assume "m > 0" and "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> y \<bullet> i" and "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
immler@69613
   833
    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
immler@69613
   834
      unfolding image_iff Bex_def mem_box
immler@69613
   835
      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
immler@69613
   836
      apply (auto simp: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
immler@69613
   837
      done
immler@69613
   838
  }
immler@69613
   839
  moreover
immler@69613
   840
  {
immler@69613
   841
    fix y
immler@69613
   842
    assume "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i" "m < 0"
immler@69613
   843
    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
immler@69613
   844
      unfolding image_iff Bex_def mem_box
immler@69613
   845
      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
immler@69613
   846
      apply (auto simp: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
immler@69613
   847
      done
immler@69613
   848
  }
immler@69613
   849
  ultimately show ?thesis using False by (auto simp: cbox_def)
immler@69613
   850
qed
immler@69613
   851
immler@69613
   852
lemma image_smult_cbox:"(\<lambda>x. m *\<^sub>R (x::_::euclidean_space)) ` cbox a b =
immler@69613
   853
  (if cbox a b = {} then {} else if 0 \<le> m then cbox (m *\<^sub>R a) (m *\<^sub>R b) else cbox (m *\<^sub>R b) (m *\<^sub>R a))"
immler@69613
   854
  using image_affinity_cbox[of m 0 a b] by auto
immler@69613
   855
immler@69619
   856
lemma swap_continuous:
immler@69619
   857
  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
immler@69619
   858
    shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
immler@69619
   859
proof -
immler@69619
   860
  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
immler@69619
   861
    by auto
immler@69619
   862
  then show ?thesis
immler@69619
   863
    apply (rule ssubst)
immler@69619
   864
    apply (rule continuous_on_compose)
immler@69619
   865
    apply (simp add: split_def)
immler@69619
   866
    apply (rule continuous_intros | simp add: assms)+
immler@69619
   867
    done
immler@69619
   868
qed
immler@69619
   869
immler@69516
   870
nipkow@69508
   871
subsection \<open>General Intervals\<close>
immler@67962
   872
immler@67962
   873
definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
immler@56189
   874
  (\<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
   875
immler@67685
   876
lemma is_interval_1:
immler@67685
   877
  "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
   878
  unfolding is_interval_def by auto
immler@67685
   879
immler@67685
   880
lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
immler@67685
   881
  unfolding is_interval_def
immler@67685
   882
  by blast
immler@67685
   883
lp15@66089
   884
lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
lp15@66089
   885
  and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
immler@56189
   886
  unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
immler@56189
   887
  by (meson order_trans le_less_trans less_le_trans less_trans)+
immler@56189
   888
lp15@61609
   889
lemma is_interval_empty [iff]: "is_interval {}"
lp15@61609
   890
  unfolding is_interval_def  by simp
lp15@61609
   891
lp15@61609
   892
lemma is_interval_univ [iff]: "is_interval UNIV"
lp15@61609
   893
  unfolding is_interval_def  by simp
immler@56189
   894
immler@56189
   895
lemma mem_is_intervalI:
immler@56189
   896
  assumes "is_interval s"
wenzelm@64539
   897
    and "a \<in> s" "b \<in> s"
wenzelm@64539
   898
    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
   899
  shows "x \<in> s"
immler@56189
   900
  by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
immler@56189
   901
immler@56189
   902
lemma interval_subst:
immler@56189
   903
  fixes S::"'a::euclidean_space set"
immler@56189
   904
  assumes "is_interval S"
wenzelm@64539
   905
    and "x \<in> S" "y j \<in> S"
wenzelm@64539
   906
    and "j \<in> Basis"
immler@56189
   907
  shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
immler@56189
   908
  by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
immler@56189
   909
immler@56189
   910
lemma mem_box_componentwiseI:
immler@56189
   911
  fixes S::"'a::euclidean_space set"
immler@56189
   912
  assumes "is_interval S"
immler@56189
   913
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
immler@56189
   914
  shows "x \<in> S"
immler@56189
   915
proof -
immler@56189
   916
  from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
immler@56189
   917
    by auto
wenzelm@64539
   918
  with finite_Basis obtain s and bs::"'a list"
wenzelm@64539
   919
    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
   920
      and bs: "set bs = Basis" "distinct bs"
immler@56189
   921
    by (metis finite_distinct_list)
wenzelm@64539
   922
  from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S"
wenzelm@64539
   923
    by blast
wenzelm@63040
   924
  define y where
wenzelm@63040
   925
    "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
   926
  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
   927
    using bs by (auto simp: s(1)[symmetric] euclidean_representation)
immler@56189
   928
  also have [symmetric]: "y bs = \<dots>"
immler@56189
   929
    using bs(2) bs(1)[THEN equalityD1]
immler@56189
   930
    by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
immler@56189
   931
  also have "y bs \<in> S"
immler@56189
   932
    using bs(1)[THEN equalityD1]
immler@56189
   933
    apply (induct bs)
wenzelm@64539
   934
     apply (auto simp: y_def j)
immler@56189
   935
    apply (rule interval_subst[OF assms(1)])
wenzelm@64539
   936
      apply (auto simp: s)
immler@56189
   937
    done
immler@56189
   938
  finally show ?thesis .
immler@56189
   939
qed
immler@56189
   940
lp15@63007
   941
lemma cbox01_nonempty [simp]: "cbox 0 One \<noteq> {}"
nipkow@64267
   942
  by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
lp15@63007
   943
lp15@63007
   944
lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
lp15@66089
   945
  by (simp add: box_ne_empty inner_Basis inner_sum_left)
lp15@63075
   946
lp15@64773
   947
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
lp15@64773
   948
  using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
lp15@64773
   949
lp15@66089
   950
lemma interval_subset_is_interval:
lp15@66089
   951
  assumes "is_interval S"
lp15@66089
   952
  shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs")
lp15@66089
   953
proof
lp15@66089
   954
  assume ?lhs
lp15@66089
   955
  then show ?rhs  using box_ne_empty(1) mem_box(2) by fastforce
lp15@66089
   956
next
lp15@66089
   957
  assume ?rhs
lp15@66089
   958
  have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
lp15@66089
   959
    using assms unfolding is_interval_def
lp15@66089
   960
    apply (clarsimp simp add: mem_box)
lp15@66089
   961
    using that by blast
lp15@66089
   962
  with \<open>?rhs\<close> show ?lhs
lp15@66089
   963
    by blast
lp15@66089
   964
qed
lp15@66089
   965
immler@67685
   966
lemma is_real_interval_union:
immler@67685
   967
  "is_interval (X \<union> Y)"
immler@67685
   968
  if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
immler@67685
   969
  for X Y::"real set"
immler@67685
   970
proof -
immler@67685
   971
  consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
immler@67685
   972
  then show ?thesis
immler@67685
   973
  proof cases
immler@67685
   974
    case 1
immler@67685
   975
    then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
immler@67685
   976
      by blast
immler@67685
   977
    then show ?thesis
immler@67685
   978
      using I 1 X Y unfolding is_interval_1
immler@67685
   979
      by (metis (full_types) Un_iff le_cases)
immler@67685
   980
  qed (use that in auto)
immler@67685
   981
qed
immler@67685
   982
immler@67685
   983
lemma is_interval_translationI:
immler@67685
   984
  assumes "is_interval X"
immler@67685
   985
  shows "is_interval ((+) x ` X)"
immler@67685
   986
  unfolding is_interval_def
immler@67685
   987
proof safe
immler@67685
   988
  fix b d e
immler@67685
   989
  assume "b \<in> X" "d \<in> X"
immler@67685
   990
    "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
immler@67685
   991
       (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
immler@67685
   992
  hence "e - x \<in> X"
immler@67685
   993
    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
immler@67685
   994
      (auto simp: algebra_simps)
immler@67685
   995
  thus "e \<in> (+) x ` X" by force
immler@67685
   996
qed
immler@67685
   997
immler@67685
   998
lemma is_interval_uminusI:
immler@67685
   999
  assumes "is_interval X"
immler@67685
  1000
  shows "is_interval (uminus ` X)"
immler@67685
  1001
  unfolding is_interval_def
immler@67685
  1002
proof safe
immler@67685
  1003
  fix b d e
immler@67685
  1004
  assume "b \<in> X" "d \<in> X"
immler@67685
  1005
    "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
immler@67685
  1006
       (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
immler@67685
  1007
  hence "- e \<in> X"
immler@67685
  1008
    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
immler@67685
  1009
      (auto simp: algebra_simps)
immler@67685
  1010
  thus "e \<in> uminus ` X" by force
immler@67685
  1011
qed
immler@67685
  1012
immler@67685
  1013
lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
immler@67685
  1014
  using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
immler@67685
  1015
  by (auto simp: image_image)
immler@67685
  1016
immler@67685
  1017
lemma is_interval_neg_translationI:
immler@67685
  1018
  assumes "is_interval X"
immler@67685
  1019
  shows "is_interval ((-) x ` X)"
immler@67685
  1020
proof -
immler@67685
  1021
  have "(-) x ` X = (+) x ` uminus ` X"
immler@67685
  1022
    by (force simp: algebra_simps)
immler@67685
  1023
  also have "is_interval \<dots>"
immler@67685
  1024
    by (metis is_interval_uminusI is_interval_translationI assms)
immler@67685
  1025
  finally show ?thesis .
immler@67685
  1026
qed
immler@67685
  1027
immler@67685
  1028
lemma is_interval_translation[simp]:
immler@67685
  1029
  "is_interval ((+) x ` X) = is_interval X"
immler@67685
  1030
  using is_interval_neg_translationI[of "(+) x ` X" x]
immler@67685
  1031
  by (auto intro!: is_interval_translationI simp: image_image)
immler@67685
  1032
immler@67685
  1033
lemma is_interval_minus_translation[simp]:
immler@67685
  1034
  shows "is_interval ((-) x ` X) = is_interval X"
immler@67685
  1035
proof -
immler@67685
  1036
  have "(-) x ` X = (+) x ` uminus ` X"
immler@67685
  1037
    by (force simp: algebra_simps)
immler@67685
  1038
  also have "is_interval \<dots> = is_interval X"
immler@67685
  1039
    by simp
immler@67685
  1040
  finally show ?thesis .
immler@67685
  1041
qed
immler@67685
  1042
immler@67685
  1043
lemma is_interval_minus_translation'[simp]:
immler@67685
  1044
  shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
immler@67685
  1045
  using is_interval_translation[of "-c" X]
immler@67685
  1046
  by (metis image_cong uminus_add_conv_diff)
immler@67685
  1047
immler@69611
  1048
immler@69611
  1049
subsection%unimportant \<open>Bounded Projections\<close>
immler@62127
  1050
immler@69611
  1051
lemma bounded_inner_imp_bdd_above:
immler@69611
  1052
  assumes "bounded s"
immler@69611
  1053
    shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
immler@69611
  1054
by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
himmelma@33175
  1055
immler@69611
  1056
lemma bounded_inner_imp_bdd_below:
immler@69611
  1057
  assumes "bounded s"
immler@69611
  1058
    shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
immler@69611
  1059
by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
huffman@44632
  1060
wenzelm@53282
  1061
immler@69611
  1062
subsection%unimportant \<open>Structural rules for pointwise continuity\<close>
himmelma@33175
  1063
hoelzl@51361
  1064
lemma continuous_infnorm[continuous_intros]:
wenzelm@53282
  1065
  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
huffman@44647
  1066
  unfolding continuous_def by (rule tendsto_infnorm)
himmelma@33175
  1067
hoelzl@51361
  1068
lemma continuous_inner[continuous_intros]:
wenzelm@53282
  1069
  assumes "continuous F f"
wenzelm@53282
  1070
    and "continuous F g"
huffman@44647
  1071
  shows "continuous F (\<lambda>x. inner (f x) (g x))"
huffman@44647
  1072
  using assms unfolding continuous_def by (rule tendsto_inner)
huffman@44647
  1073
immler@69516
  1074
immler@69611
  1075
subsection%unimportant \<open>Structural rules for setwise continuity\<close>
himmelma@33175
  1076
hoelzl@56371
  1077
lemma continuous_on_infnorm[continuous_intros]:
wenzelm@53282
  1078
  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
huffman@44647
  1079
  unfolding continuous_on by (fast intro: tendsto_infnorm)
huffman@44647
  1080
hoelzl@56371
  1081
lemma continuous_on_inner[continuous_intros]:
huffman@44531
  1082
  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
wenzelm@53282
  1083
  assumes "continuous_on s f"
wenzelm@53282
  1084
    and "continuous_on s g"
huffman@44531
  1085
  shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
huffman@44531
  1086
  using bounded_bilinear_inner assms
huffman@44531
  1087
  by (rule bounded_bilinear.continuous_on)
huffman@44531
  1088
immler@69613
  1089
immler@69613
  1090
subsection%unimportant \<open>Openness of halfspaces.\<close>
himmelma@33175
  1091
himmelma@33175
  1092
lemma open_halfspace_lt: "open {x. inner a x < b}"
hoelzl@63332
  1093
  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
himmelma@33175
  1094
himmelma@33175
  1095
lemma open_halfspace_gt: "open {x. inner a x > b}"
hoelzl@63332
  1096
  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
himmelma@33175
  1097
wenzelm@53282
  1098
lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\<bullet>i < a}"
hoelzl@63332
  1099
  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
himmelma@33175
  1100
wenzelm@53282
  1101
lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
hoelzl@63332
  1102
  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
himmelma@33175
  1103
immler@69611
  1104
lemma eucl_less_eq_halfspaces:
immler@69611
  1105
  fixes a :: "'a::euclidean_space"
immler@69611
  1106
  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
immler@69611
  1107
        "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
immler@69611
  1108
  by (auto simp: eucl_less_def)
immler@69611
  1109
immler@69611
  1110
lemma open_Collect_eucl_less[simp, intro]:
immler@69611
  1111
  fixes a :: "'a::euclidean_space"
immler@69611
  1112
  shows "open {x. x <e a}" "open {x. a <e x}"
immler@69611
  1113
  by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
immler@69611
  1114
immler@69613
  1115
subsection%unimportant \<open>Closure of halfspaces and hyperplanes\<close>
immler@69613
  1116
immler@69613
  1117
lemma continuous_at_inner: "continuous (at x) (inner a)"
immler@69613
  1118
  unfolding continuous_at by (intro tendsto_intros)
immler@69613
  1119
immler@69613
  1120
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
immler@69613
  1121
  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
immler@69613
  1122
immler@69613
  1123
lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
immler@69613
  1124
  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
immler@69613
  1125
immler@69613
  1126
lemma closed_hyperplane: "closed {x. inner a x = b}"
immler@69613
  1127
  by (simp add: closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id)
immler@69613
  1128
immler@69613
  1129
lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x\<bullet>i \<le> a}"
immler@69613
  1130
  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
immler@69613
  1131
immler@69613
  1132
lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\<bullet>i \<ge> a}"
immler@69613
  1133
  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
immler@69613
  1134
immler@69613
  1135
lemma closed_interval_left:
immler@69613
  1136
  fixes b :: "'a::euclidean_space"
immler@69613
  1137
  shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
immler@69613
  1138
  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
immler@69613
  1139
immler@69613
  1140
lemma closed_interval_right:
immler@69613
  1141
  fixes a :: "'a::euclidean_space"
immler@69613
  1142
  shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
immler@69613
  1143
  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
immler@69613
  1144
immler@69613
  1145
immler@69613
  1146
subsection%unimportant\<open>Some more convenient intermediate-value theorem formulations\<close>
immler@69613
  1147
immler@69613
  1148
lemma connected_ivt_hyperplane:
immler@69613
  1149
  assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
immler@69613
  1150
  shows "\<exists>z \<in> S. inner a z = b"
immler@69613
  1151
proof (rule ccontr)
immler@69613
  1152
  assume as:"\<not> (\<exists>z\<in>S. inner a z = b)"
immler@69613
  1153
  let ?A = "{x. inner a x < b}"
immler@69613
  1154
  let ?B = "{x. inner a x > b}"
immler@69613
  1155
  have "open ?A" "open ?B"
immler@69613
  1156
    using open_halfspace_lt and open_halfspace_gt by auto
immler@69613
  1157
  moreover have "?A \<inter> ?B = {}" by auto
immler@69613
  1158
  moreover have "S \<subseteq> ?A \<union> ?B" using as by auto
immler@69613
  1159
  ultimately show False
immler@69613
  1160
    using \<open>connected S\<close>[unfolded connected_def not_ex,
immler@69613
  1161
      THEN spec[where x="?A"], THEN spec[where x="?B"]]
immler@69613
  1162
    using xy b by auto
immler@69613
  1163
qed
immler@69613
  1164
immler@69613
  1165
lemma connected_ivt_component:
immler@69613
  1166
  fixes x::"'a::euclidean_space"
immler@69613
  1167
  shows "connected S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>S.  z\<bullet>k = a)"
immler@69613
  1168
  using connected_ivt_hyperplane[of S x y "k::'a" a]
immler@69613
  1169
  by (auto simp: inner_commute)
immler@69613
  1170
immler@69611
  1171
immler@69611
  1172
subsection \<open>Limit Component Bounds\<close>
himmelma@33175
  1173
immler@69613
  1174
lemma Lim_component_le:
immler@69613
  1175
  fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
immler@69613
  1176
  assumes "(f \<longlongrightarrow> l) net"
immler@69613
  1177
    and "\<not> (trivial_limit net)"
immler@69613
  1178
    and "eventually (\<lambda>x. f(x)\<bullet>i \<le> b) net"
immler@69613
  1179
  shows "l\<bullet>i \<le> b"
immler@69613
  1180
  by (rule tendsto_le[OF assms(2) tendsto_const tendsto_inner[OF assms(1) tendsto_const] assms(3)])
immler@69613
  1181
immler@69613
  1182
lemma Lim_component_ge:
immler@69613
  1183
  fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
immler@69613
  1184
  assumes "(f \<longlongrightarrow> l) net"
immler@69613
  1185
    and "\<not> (trivial_limit net)"
immler@69613
  1186
    and "eventually (\<lambda>x. b \<le> (f x)\<bullet>i) net"
immler@69613
  1187
  shows "b \<le> l\<bullet>i"
immler@69613
  1188
  by (rule tendsto_le[OF assms(2) tendsto_inner[OF assms(1) tendsto_const] tendsto_const assms(3)])
immler@69613
  1189
immler@69613
  1190
lemma Lim_component_eq:
immler@69613
  1191
  fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
immler@69613
  1192
  assumes net: "(f \<longlongrightarrow> l) net" "\<not> trivial_limit net"
immler@69613
  1193
    and ev:"eventually (\<lambda>x. f(x)\<bullet>i = b) net"
immler@69613
  1194
  shows "l\<bullet>i = b"
immler@69613
  1195
  using ev[unfolded order_eq_iff eventually_conj_iff]
immler@69613
  1196
  using Lim_component_ge[OF net, of b i]
immler@69613
  1197
  using Lim_component_le[OF net, of i b]
immler@69613
  1198
  by auto
immler@69613
  1199
immler@56189
  1200
lemma open_box[intro]: "open (box a b)"
immler@56189
  1201
proof -
nipkow@67399
  1202
  have "open (\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i})"
lp15@62533
  1203
    by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
nipkow@67399
  1204
  also have "(\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
lp15@66643
  1205
    by (auto simp: box_def inner_commute)
immler@56189
  1206
  finally show ?thesis .
immler@56189
  1207
qed
immler@56189
  1208
immler@56189
  1209
lemma closed_cbox[intro]:
immler@56189
  1210
  fixes a b :: "'a::euclidean_space"
immler@56189
  1211
  shows "closed (cbox a b)"
immler@56189
  1212
proof -
immler@56189
  1213
  have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
immler@56189
  1214
    by (intro closed_INT ballI continuous_closed_vimage allI
immler@56189
  1215
      linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
immler@56189
  1216
  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
lp15@66643
  1217
    by (auto simp: cbox_def)
immler@56189
  1218
  finally show "closed (cbox a b)" .
immler@56189
  1219
qed
immler@56189
  1220
lp15@62618
  1221
lemma interior_cbox [simp]:
immler@56189
  1222
  fixes a b :: "'a::euclidean_space"
immler@56189
  1223
  shows "interior (cbox a b) = box a b" (is "?L = ?R")
immler@56189
  1224
proof(rule subset_antisym)
immler@56189
  1225
  show "?R \<subseteq> ?L"
immler@56189
  1226
    using box_subset_cbox open_box
immler@56189
  1227
    by (rule interior_maximal)
immler@56189
  1228
  {
immler@56189
  1229
    fix x
immler@56189
  1230
    assume "x \<in> interior (cbox a b)"
immler@56189
  1231
    then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" ..
immler@56189
  1232
    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b"
immler@56189
  1233
      unfolding open_dist and subset_eq by auto
immler@56189
  1234
    {
immler@56189
  1235
      fix i :: 'a
immler@56189
  1236
      assume i: "i \<in> Basis"
immler@56189
  1237
      have "dist (x - (e / 2) *\<^sub>R i) x < e"
immler@56189
  1238
        and "dist (x + (e / 2) *\<^sub>R i) x < e"
immler@56189
  1239
        unfolding dist_norm
immler@56189
  1240
        apply auto
immler@56189
  1241
        unfolding norm_minus_cancel
wenzelm@60420
  1242
        using norm_Basis[OF i] \<open>e>0\<close>
immler@56189
  1243
        apply auto
immler@56189
  1244
        done
immler@56189
  1245
      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
  1246
        using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
immler@56189
  1247
          and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
immler@56189
  1248
        unfolding mem_box
immler@56189
  1249
        using i
immler@56189
  1250
        by blast+
immler@56189
  1251
      then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
wenzelm@60420
  1252
        using \<open>e>0\<close> i
immler@56189
  1253
        by (auto simp: inner_diff_left inner_Basis inner_add_left)
immler@56189
  1254
    }
immler@56189
  1255
    then have "x \<in> box a b"
immler@56189
  1256
      unfolding mem_box by auto
immler@56189
  1257
  }
immler@56189
  1258
  then show "?L \<subseteq> ?R" ..
immler@56189
  1259
qed
immler@56189
  1260
lp15@63928
  1261
lemma bounded_cbox [simp]:
immler@56189
  1262
  fixes a :: "'a::euclidean_space"
immler@56189
  1263
  shows "bounded (cbox a b)"
immler@56189
  1264
proof -
immler@56189
  1265
  let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
immler@56189
  1266
  {
immler@56189
  1267
    fix x :: "'a"
lp15@68120
  1268
    assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
immler@56189
  1269
    then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
lp15@68120
  1270
      by (force simp: intro!: sum_mono)
immler@56189
  1271
    then have "norm x \<le> ?b"
immler@56189
  1272
      using norm_le_l1[of x] by auto
immler@56189
  1273
  }
immler@56189
  1274
  then show ?thesis
lp15@68120
  1275
    unfolding cbox_def bounded_iff by force
immler@56189
  1276
qed
immler@56189
  1277
lp15@62618
  1278
lemma bounded_box [simp]:
immler@56189
  1279
  fixes a :: "'a::euclidean_space"
immler@56189
  1280
  shows "bounded (box a b)"
lp15@68120
  1281
  using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
immler@56189
  1282
  by simp
immler@56189
  1283
lp15@62618
  1284
lemma not_interval_UNIV [simp]:
immler@56189
  1285
  fixes a :: "'a::euclidean_space"
immler@56189
  1286
  shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV"
lp15@62618
  1287
  using bounded_box[of a b] bounded_cbox[of a b] by force+
lp15@62618
  1288
lp15@63945
  1289
lemma not_interval_UNIV2 [simp]:
lp15@63945
  1290
  fixes a :: "'a::euclidean_space"
lp15@63945
  1291
  shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b"
lp15@63945
  1292
  using bounded_box[of a b] bounded_cbox[of a b] by force+
lp15@63945
  1293
immler@56189
  1294
lemma box_midpoint:
immler@56189
  1295
  fixes a :: "'a::euclidean_space"
immler@56189
  1296
  assumes "box a b \<noteq> {}"
immler@56189
  1297
  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
immler@56189
  1298
proof -
lp15@68120
  1299
  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
  1300
    using assms that by (auto simp: inner_add_left box_ne_empty)
immler@56189
  1301
  then show ?thesis unfolding mem_box by auto
immler@56189
  1302
qed
immler@56189
  1303
immler@56189
  1304
lemma open_cbox_convex:
immler@56189
  1305
  fixes x :: "'a::euclidean_space"
immler@56189
  1306
  assumes x: "x \<in> box a b"
immler@56189
  1307
    and y: "y \<in> cbox a b"
immler@56189
  1308
    and e: "0 < e" "e \<le> 1"
immler@56189
  1309
  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
immler@56189
  1310
proof -
immler@56189
  1311
  {
immler@56189
  1312
    fix i :: 'a
immler@56189
  1313
    assume i: "i \<in> Basis"
immler@56189
  1314
    have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
immler@56189
  1315
      unfolding left_diff_distrib by simp
immler@56189
  1316
    also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
lp15@68120
  1317
    proof (rule add_less_le_mono)
lp15@68120
  1318
      show "e * (a \<bullet> i) < e * (x \<bullet> i)"
lp15@68120
  1319
        using \<open>0 < e\<close> i mem_box(1) x by auto
lp15@68120
  1320
      show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)"
lp15@68120
  1321
        by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
lp15@68120
  1322
    qed
immler@56189
  1323
    finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
immler@56189
  1324
      unfolding inner_simps by auto
immler@56189
  1325
    moreover
immler@56189
  1326
    {
immler@56189
  1327
      have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
immler@56189
  1328
        unfolding left_diff_distrib by simp
immler@56189
  1329
      also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
lp15@66827
  1330
      proof (rule add_less_le_mono)
lp15@66827
  1331
        show "e * (x \<bullet> i) < e * (b \<bullet> i)"
lp15@68120
  1332
          using \<open>0 < e\<close> i mem_box(1) x by auto
lp15@66827
  1333
        show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)"
lp15@68120
  1334
          by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
lp15@66827
  1335
      qed
immler@56189
  1336
      finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
immler@56189
  1337
        unfolding inner_simps by auto
immler@56189
  1338
    }
immler@56189
  1339
    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
  1340
      by auto
immler@56189
  1341
  }
immler@56189
  1342
  then show ?thesis
immler@56189
  1343
    unfolding mem_box by auto
immler@56189
  1344
qed
immler@56189
  1345
lp15@63881
  1346
lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b"
lp15@63881
  1347
  by (simp add: closed_cbox)
lp15@63881
  1348
lp15@63881
  1349
lemma closure_box [simp]:
immler@56189
  1350
  fixes a :: "'a::euclidean_space"
immler@56189
  1351
   assumes "box a b \<noteq> {}"
immler@56189
  1352
  shows "closure (box a b) = cbox a b"
immler@56189
  1353
proof -
immler@56189
  1354
  have ab: "a <e b"
immler@56189
  1355
    using assms by (simp add: eucl_less_def box_ne_empty)
immler@56189
  1356
  let ?c = "(1 / 2) *\<^sub>R (a + b)"
immler@56189
  1357
  {
immler@56189
  1358
    fix x
immler@56189
  1359
    assume as:"x \<in> cbox a b"
wenzelm@63040
  1360
    define f where [abs_def]: "f n = x + (inverse (real n + 1)) *\<^sub>R (?c - x)" for n
immler@56189
  1361
    {
immler@56189
  1362
      fix n
immler@56189
  1363
      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
immler@56189
  1364
      have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
immler@56189
  1365
        unfolding inverse_le_1_iff by auto
immler@56189
  1366
      have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
immler@56189
  1367
        x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
lp15@66643
  1368
        by (auto simp: algebra_simps)
immler@56189
  1369
      then have "f n <e b" and "a <e f n"
immler@56189
  1370
        using open_cbox_convex[OF box_midpoint[OF assms] as *]
immler@56189
  1371
        unfolding f_def by (auto simp: box_def eucl_less_def)
immler@56189
  1372
      then have False
immler@56189
  1373
        using fn unfolding f_def using xc by auto
immler@56189
  1374
    }
immler@56189
  1375
    moreover
immler@56189
  1376
    {
wenzelm@61973
  1377
      assume "\<not> (f \<longlongrightarrow> x) sequentially"
immler@56189
  1378
      {
immler@56189
  1379
        fix e :: real
immler@56189
  1380
        assume "e > 0"
lp15@61609
  1381
        then obtain N :: nat where N: "inverse (real (N + 1)) < e"
lp15@68120
  1382
          using reals_Archimedean by auto
lp15@61609
  1383
        have "inverse (real n + 1) < e" if "N \<le> n" for n
lp15@61609
  1384
          by (auto intro!: that le_less_trans [OF _ N])
immler@56189
  1385
        then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
immler@56189
  1386
      }
wenzelm@61973
  1387
      then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially"
lp15@66643
  1388
        unfolding lim_sequentially by(auto simp: dist_norm)
wenzelm@61973
  1389
      then have "(f \<longlongrightarrow> x) sequentially"
immler@56189
  1390
        unfolding f_def
immler@56189
  1391
        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
  1392
        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
  1393
        by auto
immler@56189
  1394
    }
immler@56189
  1395
    ultimately have "x \<in> closure (box a b)"
lp15@68120
  1396
      using as box_midpoint[OF assms]
lp15@68120
  1397
      unfolding closure_def islimpt_sequential
immler@56189
  1398
      by (cases "x=?c") (auto simp: in_box_eucl_less)
immler@56189
  1399
  }
immler@56189
  1400
  then show ?thesis
immler@56189
  1401
    using closure_minimal[OF box_subset_cbox, of a b] by blast
immler@56189
  1402
qed
immler@56189
  1403
immler@56189
  1404
lemma bounded_subset_box_symmetric:
lp15@68120
  1405
  fixes S :: "('a::euclidean_space) set"
lp15@68120
  1406
  assumes "bounded S"
lp15@68120
  1407
  obtains a where "S \<subseteq> box (-a) a"
immler@56189
  1408
proof -
lp15@68120
  1409
  obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b"
immler@56189
  1410
    using assms[unfolded bounded_pos] by auto
wenzelm@63040
  1411
  define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)"
lp15@68120
  1412
  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
  1413
    using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
lp15@68120
  1414
  then have "S \<subseteq> box (-a) a"
lp15@68120
  1415
    by (auto simp: simp add: box_def)
lp15@68120
  1416
  then show ?thesis ..
immler@56189
  1417
qed
immler@56189
  1418
immler@56189
  1419
lemma bounded_subset_cbox_symmetric:
lp15@68120
  1420
  fixes S :: "('a::euclidean_space) set"
lp15@68120
  1421
  assumes "bounded S"
lp15@68120
  1422
  obtains a where "S \<subseteq> cbox (-a) a"
immler@56189
  1423
proof -
lp15@68120
  1424
  obtain a where "S \<subseteq> box (-a) a"
immler@56189
  1425
    using bounded_subset_box_symmetric[OF assms] by auto
immler@56189
  1426
  then show ?thesis
lp15@68120
  1427
    by (meson box_subset_cbox dual_order.trans that)
immler@56189
  1428
qed
immler@56189
  1429
immler@56189
  1430
lemma frontier_cbox:
immler@56189
  1431
  fixes a b :: "'a::euclidean_space"
immler@56189
  1432
  shows "frontier (cbox a b) = cbox a b - box a b"
immler@56189
  1433
  unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
immler@56189
  1434
immler@56189
  1435
lemma frontier_box:
immler@56189
  1436
  fixes a b :: "'a::euclidean_space"
immler@56189
  1437
  shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
immler@56189
  1438
proof (cases "box a b = {}")
immler@56189
  1439
  case True
immler@56189
  1440
  then show ?thesis
immler@56189
  1441
    using frontier_empty by auto
immler@56189
  1442
next
immler@56189
  1443
  case False
immler@56189
  1444
  then show ?thesis
immler@56189
  1445
    unfolding frontier_def and closure_box[OF False] and interior_open[OF open_box]
immler@56189
  1446
    by auto
immler@56189
  1447
qed
immler@56189
  1448
lp15@66884
  1449
lemma Int_interval_mixed_eq_empty:
immler@56189
  1450
  fixes a :: "'a::euclidean_space"
immler@56189
  1451
   assumes "box c d \<noteq> {}"
immler@56189
  1452
  shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
immler@56189
  1453
  unfolding closure_box[OF assms, symmetric]
lp15@62843
  1454
  unfolding open_Int_closure_eq_empty[OF open_box] ..
immler@56189
  1455
immler@69611
  1456
subsection \<open>Class Instances\<close>
immler@69611
  1457
immler@69611
  1458
lemma compact_lemma:
immler@69611
  1459
  fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
immler@69611
  1460
  assumes "bounded (range f)"
immler@69611
  1461
  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
immler@69611
  1462
    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@69611
  1463
  by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
immler@69611
  1464
     (auto intro!: assms bounded_linear_inner_left bounded_linear_image
immler@69611
  1465
       simp: euclidean_representation)
immler@69611
  1466
immler@69611
  1467
instance%important euclidean_space \<subseteq> heine_borel
immler@69611
  1468
proof%unimportant
immler@69611
  1469
  fix f :: "nat \<Rightarrow> 'a"
immler@69611
  1470
  assume f: "bounded (range f)"
immler@69611
  1471
  then obtain l::'a and r where r: "strict_mono r"
immler@69611
  1472
    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
immler@69611
  1473
    using compact_lemma [OF f] by blast
immler@69611
  1474
  {
immler@69611
  1475
    fix e::real
immler@69611
  1476
    assume "e > 0"
immler@69611
  1477
    hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
immler@69611
  1478
    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"
immler@69611
  1479
      by simp
immler@69611
  1480
    moreover
immler@69611
  1481
    {
immler@69611
  1482
      fix n
immler@69611
  1483
      assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
immler@69611
  1484
      have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
immler@69611
  1485
        apply (subst euclidean_dist_l2)
immler@69611
  1486
        using zero_le_dist
immler@69611
  1487
        apply (rule L2_set_le_sum)
immler@69611
  1488
        done
immler@69611
  1489
      also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
immler@69611
  1490
        apply (rule sum_strict_mono)
immler@69611
  1491
        using n
immler@69611
  1492
        apply auto
immler@69611
  1493
        done
immler@69611
  1494
      finally have "dist (f (r n)) l < e"
immler@69611
  1495
        by auto
immler@69611
  1496
    }
immler@69611
  1497
    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
immler@69611
  1498
      by (rule eventually_mono)
immler@69611
  1499
  }
immler@69611
  1500
  then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69611
  1501
    unfolding o_def tendsto_iff by simp
immler@69611
  1502
  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69611
  1503
    by auto
immler@69611
  1504
qed
immler@69611
  1505
immler@69611
  1506
instance%important euclidean_space \<subseteq> banach ..
immler@69611
  1507
immler@69611
  1508
instance euclidean_space \<subseteq> second_countable_topology
immler@69611
  1509
proof
immler@69611
  1510
  define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
immler@69611
  1511
  then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
immler@69611
  1512
    by simp
immler@69611
  1513
  define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
immler@69611
  1514
  then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
immler@69611
  1515
    by simp
immler@69611
  1516
  define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
immler@69611
  1517
immler@69611
  1518
  have "Ball B open" by (simp add: B_def open_box)
immler@69611
  1519
  moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
immler@69611
  1520
  proof safe
immler@69611
  1521
    fix A::"'a set"
immler@69611
  1522
    assume "open A"
immler@69611
  1523
    show "\<exists>B'\<subseteq>B. \<Union>B' = A"
immler@69611
  1524
      apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
immler@69611
  1525
      apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
immler@69611
  1526
      apply (auto simp: a b B_def)
immler@69611
  1527
      done
immler@69611
  1528
  qed
immler@69611
  1529
  ultimately
immler@69611
  1530
  have "topological_basis B"
immler@69611
  1531
    unfolding topological_basis_def by blast
immler@69611
  1532
  moreover
immler@69611
  1533
  have "countable B"
immler@69611
  1534
    unfolding B_def
immler@69611
  1535
    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
immler@69611
  1536
  ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
immler@69611
  1537
    by (blast intro: topological_basis_imp_subbasis)
immler@69611
  1538
qed
immler@69611
  1539
immler@69611
  1540
instance euclidean_space \<subseteq> polish_space ..
immler@69611
  1541
immler@69611
  1542
immler@69611
  1543
subsection \<open>Compact Boxes\<close>
immler@69611
  1544
immler@69611
  1545
lemma compact_cbox [simp]:
wenzelm@61076
  1546
  fixes a :: "'a::euclidean_space"
immler@69611
  1547
  shows "compact (cbox a b)"
immler@69611
  1548
  using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
immler@69611
  1549
  by (auto simp: compact_eq_seq_compact_metric)
immler@69611
  1550
immler@69611
  1551
proposition is_interval_compact:
immler@69611
  1552
   "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)"   (is "?lhs = ?rhs")
immler@69611
  1553
proof (cases "S = {}")
immler@69611
  1554
  case True
immler@69611
  1555
  with empty_as_interval show ?thesis by auto
immler@69611
  1556
next
immler@69611
  1557
  case False
immler@69611
  1558
  show ?thesis
immler@69611
  1559
  proof
immler@69611
  1560
    assume L: ?lhs
immler@69611
  1561
    then have "is_interval S" "compact S" by auto
immler@69611
  1562
    define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x\<in>S. x \<bullet> i) *\<^sub>R i"
immler@69611
  1563
    define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x\<in>S. x \<bullet> i) *\<^sub>R i"
immler@69611
  1564
    have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
immler@69611
  1565
      by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
immler@69611
  1566
    have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
immler@69611
  1567
      by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
immler@69611
  1568
    have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
immler@69611
  1569
                   and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)" for x
immler@69611
  1570
    proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
immler@69611
  1571
      fix i::'a
immler@69611
  1572
      assume i: "i \<in> Basis"
immler@69611
  1573
      have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
immler@69611
  1574
        by (intro continuous_intros)
immler@69611
  1575
      obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
immler@69611
  1576
        using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
immler@69611
  1577
      obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
immler@69611
  1578
        using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
immler@69611
  1579
      have "a \<bullet> i \<le> (INF x\<in>S. x \<bullet> i)"
immler@69611
  1580
        by (simp add: False a cINF_greatest)
immler@69611
  1581
      also have "\<dots> \<le> x \<bullet> i"
immler@69611
  1582
        by (simp add: i inf)
immler@69611
  1583
      finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
immler@69611
  1584
      have "x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
immler@69611
  1585
        by (simp add: i sup)
immler@69611
  1586
      also have "(SUP x\<in>S. x \<bullet> i) \<le> b \<bullet> i"
immler@69611
  1587
        by (simp add: False b cSUP_least)
immler@69611
  1588
      finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
immler@69611
  1589
      show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
immler@69611
  1590
        apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
immler@69611
  1591
        apply (simp add: i)
immler@69611
  1592
        apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
immler@69611
  1593
        using i ai bi apply force
immler@69611
  1594
        done
immler@69611
  1595
    qed
immler@69611
  1596
    have "S = cbox a b"
immler@69611
  1597
      by (auto simp: a_def b_def mem_box intro: 1 2 3)
immler@69611
  1598
    then show ?rhs
immler@69611
  1599
      by blast
immler@69611
  1600
  next
immler@69611
  1601
    assume R: ?rhs
immler@69611
  1602
    then show ?lhs
immler@69611
  1603
      using compact_cbox is_interval_cbox by blast
immler@69611
  1604
  qed
immler@69611
  1605
qed
immler@69611
  1606
immler@69611
  1607
immler@69615
  1608
subsection%unimportant\<open>Componentwise limits and continuity\<close>
immler@69615
  1609
immler@69615
  1610
text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
immler@69615
  1611
lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
immler@69615
  1612
  by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
immler@69615
  1613
immler@69615
  1614
text\<open>But is the premise \<^term>\<open>i \<in> Basis\<close> really necessary?\<close>
immler@69615
  1615
lemma open_preimage_inner:
immler@69615
  1616
  assumes "open S" "i \<in> Basis"
immler@69615
  1617
    shows "open {x. x \<bullet> i \<in> S}"
immler@69615
  1618
proof (rule openI, simp)
immler@69615
  1619
  fix x
immler@69615
  1620
  assume x: "x \<bullet> i \<in> S"
immler@69615
  1621
  with assms obtain e where "0 < e" and e: "ball (x \<bullet> i) e \<subseteq> S"
immler@69615
  1622
    by (auto simp: open_contains_ball_eq)
immler@69615
  1623
  have "\<exists>e>0. ball (y \<bullet> i) e \<subseteq> S" if dxy: "dist x y < e / 2" for y
immler@69615
  1624
  proof (intro exI conjI)
immler@69615
  1625
    have "dist (x \<bullet> i) (y \<bullet> i) < e / 2"
immler@69615
  1626
      by (meson \<open>i \<in> Basis\<close> dual_order.trans Euclidean_dist_upper not_le that)
immler@69615
  1627
    then have "dist (x \<bullet> i) z < e" if "dist (y \<bullet> i) z < e / 2" for z
immler@69615
  1628
      by (metis dist_commute dist_triangle_half_l that)
immler@69615
  1629
    then have "ball (y \<bullet> i) (e / 2) \<subseteq> ball (x \<bullet> i) e"
immler@69615
  1630
      using mem_ball by blast
immler@69615
  1631
      with e show "ball (y \<bullet> i) (e / 2) \<subseteq> S"
immler@69615
  1632
        by (metis order_trans)
immler@69615
  1633
  qed (simp add: \<open>0 < e\<close>)
immler@69615
  1634
  then show "\<exists>e>0. ball x e \<subseteq> {s. s \<bullet> i \<in> S}"
immler@69615
  1635
    by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
immler@69615
  1636
qed
immler@69615
  1637
immler@69615
  1638
proposition tendsto_componentwise_iff:
immler@69615
  1639
  fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
immler@69615
  1640
  shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
immler@69615
  1641
         (is "?lhs = ?rhs")
immler@69615
  1642
proof
immler@69615
  1643
  assume ?lhs
immler@69615
  1644
  then show ?rhs
immler@69615
  1645
    unfolding tendsto_def
immler@69615
  1646
    apply clarify
immler@69615
  1647
    apply (drule_tac x="{s. s \<bullet> i \<in> S}" in spec)
immler@69615
  1648
    apply (auto simp: open_preimage_inner)
immler@69615
  1649
    done
immler@69615
  1650
next
immler@69615
  1651
  assume R: ?rhs
immler@69615
  1652
  then have "\<And>e. e > 0 \<Longrightarrow> \<forall>i\<in>Basis. \<forall>\<^sub>F x in F. dist (f x \<bullet> i) (l \<bullet> i) < e"
immler@69615
  1653
    unfolding tendsto_iff by blast
immler@69615
  1654
  then have R': "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e"
immler@69615
  1655
      by (simp add: eventually_ball_finite_distrib [symmetric])
immler@69615
  1656
  show ?lhs
immler@69615
  1657
  unfolding tendsto_iff
immler@69615
  1658
  proof clarify
immler@69615
  1659
    fix e::real
immler@69615
  1660
    assume "0 < e"
immler@69615
  1661
    have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
immler@69615
  1662
             if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
immler@69615
  1663
    proof -
immler@69615
  1664
      have "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
immler@69615
  1665
        by (simp add: L2_set_le_sum)
immler@69615
  1666
      also have "... < DIM('b) * (e / real DIM('b))"
immler@69615
  1667
        apply (rule sum_bounded_above_strict)
immler@69615
  1668
        using that by auto
immler@69615
  1669
      also have "... = e"
immler@69615
  1670
        by (simp add: field_simps)
immler@69615
  1671
      finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
immler@69615
  1672
    qed
immler@69615
  1673
    have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
immler@69615
  1674
      apply (rule R')
immler@69615
  1675
      using \<open>0 < e\<close> by simp
immler@69615
  1676
    then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
immler@69615
  1677
      apply (rule eventually_mono)
immler@69615
  1678
      apply (subst euclidean_dist_l2)
immler@69615
  1679
      using * by blast
immler@69615
  1680
  qed
immler@69615
  1681
qed
immler@69615
  1682
immler@69615
  1683
immler@69615
  1684
corollary continuous_componentwise:
immler@69615
  1685
   "continuous F f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous F (\<lambda>x. (f x \<bullet> i)))"
immler@69615
  1686
by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
immler@69615
  1687
immler@69615
  1688
corollary continuous_on_componentwise:
immler@69615
  1689
  fixes S :: "'a :: t2_space set"
immler@69615
  1690
  shows "continuous_on S f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous_on S (\<lambda>x. (f x \<bullet> i)))"
immler@69615
  1691
  apply (simp add: continuous_on_eq_continuous_within)
immler@69615
  1692
  using continuous_componentwise by blast
immler@69615
  1693
immler@69615
  1694
lemma linear_componentwise_iff:
immler@69615
  1695
     "(linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. linear (\<lambda>x. f' x \<bullet> i))"
immler@69615
  1696
  apply (auto simp: linear_iff inner_left_distrib)
immler@69615
  1697
   apply (metis inner_left_distrib euclidean_eq_iff)
immler@69615
  1698
  by (metis euclidean_eqI inner_scaleR_left)
immler@69615
  1699
immler@69615
  1700
lemma bounded_linear_componentwise_iff:
immler@69615
  1701
     "(bounded_linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. bounded_linear (\<lambda>x. f' x \<bullet> i))"
immler@69615
  1702
     (is "?lhs = ?rhs")
immler@69615
  1703
proof
immler@69615
  1704
  assume ?lhs then show ?rhs
immler@69615
  1705
    by (simp add: bounded_linear_inner_left_comp)
immler@69615
  1706
next
immler@69615
  1707
  assume ?rhs
immler@69615
  1708
  then have "(\<forall>i\<in>Basis. \<exists>K. \<forall>x. \<bar>f' x \<bullet> i\<bar> \<le> norm x * K)" "linear f'"
immler@69615
  1709
    by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
immler@69615
  1710
  then obtain F where F: "\<And>i x. i \<in> Basis \<Longrightarrow> \<bar>f' x \<bullet> i\<bar> \<le> norm x * F i"
immler@69615
  1711
    by metis
immler@69615
  1712
  have "norm (f' x) \<le> norm x * sum F Basis" for x
immler@69615
  1713
  proof -
immler@69615
  1714
    have "norm (f' x) \<le> (\<Sum>i\<in>Basis. \<bar>f' x \<bullet> i\<bar>)"
immler@69615
  1715
      by (rule norm_le_l1)
immler@69615
  1716
    also have "... \<le> (\<Sum>i\<in>Basis. norm x * F i)"
immler@69615
  1717
      by (metis F sum_mono)
immler@69615
  1718
    also have "... = norm x * sum F Basis"
immler@69615
  1719
      by (simp add: sum_distrib_left)
immler@69615
  1720
    finally show ?thesis .
immler@69615
  1721
  qed
immler@69615
  1722
  then show ?lhs
immler@69615
  1723
    by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
immler@69615
  1724
qed
immler@69615
  1725
immler@69615
  1726
subsection%unimportant \<open>Continuous Extension\<close>
immler@69615
  1727
immler@69615
  1728
definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
immler@69615
  1729
  "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
immler@69615
  1730
    then (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)
immler@69615
  1731
    else a)"
immler@69615
  1732
immler@69615
  1733
lemma clamp_in_interval[simp]:
immler@69615
  1734
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
immler@69615
  1735
  shows "clamp a b x \<in> cbox a b"
immler@69615
  1736
  unfolding clamp_def
immler@69615
  1737
  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
immler@69615
  1738
immler@69615
  1739
lemma clamp_cancel_cbox[simp]:
immler@69615
  1740
  fixes x a b :: "'a::euclidean_space"
immler@69615
  1741
  assumes x: "x \<in> cbox a b"
immler@69615
  1742
  shows "clamp a b x = x"
immler@69615
  1743
  using assms
immler@69615
  1744
  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
immler@69615
  1745
immler@69615
  1746
lemma clamp_empty_interval:
immler@69615
  1747
  assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
immler@69615
  1748
  shows "clamp a b = (\<lambda>_. a)"
immler@69615
  1749
  using assms
immler@69615
  1750
  by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
immler@69615
  1751
immler@69615
  1752
lemma dist_clamps_le_dist_args:
immler@69615
  1753
  fixes x :: "'a::euclidean_space"
immler@69615
  1754
  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
immler@69615
  1755
proof cases
immler@69615
  1756
  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
immler@69615
  1757
  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
immler@69615
  1758
    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
immler@69615
  1759
    by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
immler@69615
  1760
  then show ?thesis
immler@69615
  1761
    by (auto intro: real_sqrt_le_mono
immler@69615
  1762
      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
immler@69615
  1763
qed (auto simp: clamp_def)
immler@69615
  1764
immler@69615
  1765
lemma clamp_continuous_at:
immler@69615
  1766
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
immler@69615
  1767
    and x :: 'a
immler@69615
  1768
  assumes f_cont: "continuous_on (cbox a b) f"
immler@69615
  1769
  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
immler@69615
  1770
proof cases
immler@69615
  1771
  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
immler@69615
  1772
  show ?thesis
immler@69615
  1773
    unfolding continuous_at_eps_delta
immler@69615
  1774
  proof safe
immler@69615
  1775
    fix x :: 'a
immler@69615
  1776
    fix e :: real
immler@69615
  1777
    assume "e > 0"
immler@69615
  1778
    moreover have "clamp a b x \<in> cbox a b"
immler@69615
  1779
      by (simp add: clamp_in_interval le)
immler@69615
  1780
    moreover note f_cont[simplified continuous_on_iff]
immler@69615
  1781
    ultimately
immler@69615
  1782
    obtain d where d: "0 < d"
immler@69615
  1783
      "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
immler@69615
  1784
      by force
immler@69615
  1785
    show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
immler@69615
  1786
      dist (f (clamp a b x')) (f (clamp a b x)) < e"
immler@69615
  1787
      using le
immler@69615
  1788
      by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
immler@69615
  1789
  qed
immler@69615
  1790
qed (auto simp: clamp_empty_interval)
immler@69615
  1791
immler@69615
  1792
lemma clamp_continuous_on:
immler@69615
  1793
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
immler@69615
  1794
  assumes f_cont: "continuous_on (cbox a b) f"
immler@69615
  1795
  shows "continuous_on S (\<lambda>x. f (clamp a b x))"
immler@69615
  1796
  using assms
immler@69615
  1797
  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
immler@69615
  1798
immler@69615
  1799
lemma clamp_bounded:
immler@69615
  1800
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
immler@69615
  1801
  assumes bounded: "bounded (f ` (cbox a b))"
immler@69615
  1802
  shows "bounded (range (\<lambda>x. f (clamp a b x)))"
immler@69615
  1803
proof cases
immler@69615
  1804
  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
immler@69615
  1805
  from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
immler@69615
  1806
    by (auto simp: bounded_any_center[where a=undefined])
immler@69615
  1807
  then show ?thesis
immler@69615
  1808
    by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
immler@69615
  1809
        simp: bounded_any_center[where a=undefined])
immler@69615
  1810
qed (auto simp: clamp_empty_interval image_def)
immler@69615
  1811
immler@69615
  1812
immler@69615
  1813
definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
immler@69615
  1814
  where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
immler@69615
  1815
immler@69615
  1816
lemma ext_cont_cancel_cbox[simp]:
immler@69615
  1817
  fixes x a b :: "'a::euclidean_space"
immler@69615
  1818
  assumes x: "x \<in> cbox a b"
immler@69615
  1819
  shows "ext_cont f a b x = f x"
immler@69615
  1820
  using assms
immler@69615
  1821
  unfolding ext_cont_def
immler@69615
  1822
  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
immler@69615
  1823
immler@69615
  1824
lemma continuous_on_ext_cont[continuous_intros]:
immler@69615
  1825
  "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
immler@69615
  1826
  by (auto intro!: clamp_continuous_on simp: ext_cont_def)
immler@69615
  1827
immler@69615
  1828
immler@69615
  1829
subsection \<open>Separability\<close>
immler@69615
  1830
immler@69615
  1831
lemma univ_second_countable_sequence:
immler@69615
  1832
  obtains B :: "nat \<Rightarrow> 'a::euclidean_space set"
immler@69615
  1833
    where "inj B" "\<And>n. open(B n)" "\<And>S. open S \<Longrightarrow> \<exists>k. S = \<Union>{B n |n. n \<in> k}"
immler@69615
  1834
proof -
immler@69615
  1835
  obtain \<B> :: "'a set set"
immler@69615
  1836
  where "countable \<B>"
immler@69615
  1837
    and opn: "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
immler@69615
  1838
    and Un: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
immler@69615
  1839
    using univ_second_countable by blast
immler@69615
  1840
  have *: "infinite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
immler@69615
  1841
    apply (rule Infinite_Set.range_inj_infinite)
immler@69615
  1842
    apply (simp add: inj_on_def ball_eq_ball_iff)
immler@69615
  1843
    done
immler@69615
  1844
  have "infinite \<B>"
immler@69615
  1845
  proof
immler@69615
  1846
    assume "finite \<B>"
immler@69615
  1847
    then have "finite (Union ` (Pow \<B>))"
immler@69615
  1848
      by simp
immler@69615
  1849
    then have "finite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
immler@69615
  1850
      apply (rule rev_finite_subset)
immler@69615
  1851
      by (metis (no_types, lifting) PowI image_eqI image_subset_iff Un [OF open_ball])
immler@69615
  1852
    with * show False by simp
immler@69615
  1853
  qed
immler@69615
  1854
  obtain f :: "nat \<Rightarrow> 'a set" where "\<B> = range f" "inj f"
immler@69615
  1855
    by (blast intro: countable_as_injective_image [OF \<open>countable \<B>\<close> \<open>infinite \<B>\<close>])
immler@69615
  1856
  have *: "\<exists>k. S = \<Union>{f n |n. n \<in> k}" if "open S" for S
immler@69615
  1857
    using Un [OF that]
immler@69615
  1858
    apply clarify
immler@69615
  1859
    apply (rule_tac x="f-`U" in exI)
immler@69615
  1860
    using \<open>inj f\<close> \<open>\<B> = range f\<close> apply force
immler@69615
  1861
    done
immler@69615
  1862
  show ?thesis
immler@69615
  1863
    apply (rule that [OF \<open>inj f\<close> _ *])
immler@69615
  1864
    apply (auto simp: \<open>\<B> = range f\<close> opn)
immler@69615
  1865
    done
immler@69615
  1866
qed
immler@69615
  1867
immler@69615
  1868
proposition separable:
immler@69615
  1869
  fixes S :: "'a::{metric_space, second_countable_topology} set"
immler@69615
  1870
  obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
immler@69615
  1871
proof -
immler@69615
  1872
  obtain \<B> :: "'a set set"
immler@69615
  1873
    where "countable \<B>"
immler@69615
  1874
      and "{} \<notin> \<B>"
immler@69615
  1875
      and ope: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
immler@69615
  1876
      and if_ope: "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
immler@69615
  1877
    by (meson subset_second_countable)
immler@69615
  1878
  then obtain f where f: "\<And>C. C \<in> \<B> \<Longrightarrow> f C \<in> C"
immler@69615
  1879
    by (metis equals0I)
immler@69615
  1880
  show ?thesis
immler@69615
  1881
  proof
immler@69615
  1882
    show "countable (f ` \<B>)"
immler@69615
  1883
      by (simp add: \<open>countable \<B>\<close>)
immler@69615
  1884
    show "f ` \<B> \<subseteq> S"
immler@69615
  1885
      using ope f openin_imp_subset by blast
immler@69615
  1886
    show "S \<subseteq> closure (f ` \<B>)"
immler@69615
  1887
    proof (clarsimp simp: closure_approachable)
immler@69615
  1888
      fix x and e::real
immler@69615
  1889
      assume "x \<in> S" "0 < e"
immler@69615
  1890
      have "openin (subtopology euclidean S) (S \<inter> ball x e)"
immler@69615
  1891
        by (simp add: openin_Int_open)
immler@69615
  1892
      with if_ope obtain \<U> where  \<U>: "\<U> \<subseteq> \<B>" "S \<inter> ball x e = \<Union>\<U>"
immler@69615
  1893
        by meson
immler@69615
  1894
      show "\<exists>C \<in> \<B>. dist (f C) x < e"
immler@69615
  1895
      proof (cases "\<U> = {}")
immler@69615
  1896
        case True
immler@69615
  1897
        then show ?thesis
immler@69615
  1898
          using \<open>0 < e\<close>  \<U> \<open>x \<in> S\<close> by auto
immler@69615
  1899
      next
immler@69615
  1900
        case False
immler@69615
  1901
        then obtain C where "C \<in> \<U>" by blast
immler@69615
  1902
        show ?thesis
immler@69615
  1903
        proof
immler@69615
  1904
          show "dist (f C) x < e"
immler@69615
  1905
            by (metis Int_iff Union_iff \<U> \<open>C \<in> \<U>\<close> dist_commute f mem_ball subsetCE)
immler@69615
  1906
          show "C \<in> \<B>"
immler@69615
  1907
            using \<open>\<U> \<subseteq> \<B>\<close> \<open>C \<in> \<U>\<close> by blast
immler@69615
  1908
        qed
immler@69615
  1909
      qed
immler@69615
  1910
    qed
immler@69615
  1911
  qed
immler@69615
  1912
qed
immler@69615
  1913
immler@69615
  1914
immler@69613
  1915
subsection%unimportant \<open>Diameter\<close>
immler@69613
  1916
immler@69613
  1917
lemma diameter_cball [simp]:
immler@69613
  1918
  fixes a :: "'a::euclidean_space"
immler@69613
  1919
  shows "diameter(cball a r) = (if r < 0 then 0 else 2*r)"
immler@69613
  1920
proof -
immler@69613
  1921
  have "diameter(cball a r) = 2*r" if "r \<ge> 0"
immler@69613
  1922
  proof (rule order_antisym)
immler@69613
  1923
    show "diameter (cball a r) \<le> 2*r"
immler@69613
  1924
    proof (rule diameter_le)
immler@69613
  1925
      fix x y assume "x \<in> cball a r" "y \<in> cball a r"
immler@69613
  1926
      then have "norm (x - a) \<le> r" "norm (a - y) \<le> r"
immler@69613
  1927
        by (auto simp: dist_norm norm_minus_commute)
immler@69613
  1928
      then have "norm (x - y) \<le> r+r"
immler@69613
  1929
        using norm_diff_triangle_le by blast
immler@69613
  1930
      then show "norm (x - y) \<le> 2*r" by simp
immler@69613
  1931
    qed (simp add: that)
immler@69613
  1932
    have "2*r = dist (a + r *\<^sub>R (SOME i. i \<in> Basis)) (a - r *\<^sub>R (SOME i. i \<in> Basis))"
immler@69613
  1933
      apply (simp add: dist_norm)
immler@69613
  1934
      by (metis abs_of_nonneg mult.right_neutral norm_numeral norm_scaleR norm_some_Basis real_norm_def scaleR_2 that)
immler@69613
  1935
    also have "... \<le> diameter (cball a r)"
immler@69613
  1936
      apply (rule diameter_bounded_bound)
immler@69613
  1937
      using that by (auto simp: dist_norm)
immler@69613
  1938
    finally show "2*r \<le> diameter (cball a r)" .
immler@69613
  1939
  qed
immler@69613
  1940
  then show ?thesis by simp
immler@69613
  1941
qed
immler@69613
  1942
immler@69613
  1943
lemma diameter_ball [simp]:
immler@69613
  1944
  fixes a :: "'a::euclidean_space"
immler@69613
  1945
  shows "diameter(ball a r) = (if r < 0 then 0 else 2*r)"
immler@69613
  1946
proof -
immler@69613
  1947
  have "diameter(ball a r) = 2*r" if "r > 0"
immler@69613
  1948
    by (metis bounded_ball diameter_closure closure_ball diameter_cball less_eq_real_def linorder_not_less that)
immler@69613
  1949
  then show ?thesis
immler@69613
  1950
    by (simp add: diameter_def)
immler@69613
  1951
qed
immler@69613
  1952
immler@69613
  1953
lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)"
immler@69613
  1954
proof -
immler@69613
  1955
  have "{a .. b} = cball ((a+b)/2) ((b-a)/2)"
immler@69613
  1956
    by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
immler@69613
  1957
  then show ?thesis
immler@69613
  1958
    by simp
immler@69613
  1959
qed
immler@69613
  1960
immler@69613
  1961
lemma diameter_open_interval [simp]: "diameter {a<..<b} = (if b < a then 0 else b-a)"
immler@69613
  1962
proof -
immler@69613
  1963
  have "{a <..< b} = ball ((a+b)/2) ((b-a)/2)"
immler@69613
  1964
    by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
immler@69613
  1965
  then show ?thesis
immler@69613
  1966
    by simp
immler@69613
  1967
qed
immler@69613
  1968
immler@69613
  1969
lemma diameter_cbox:
immler@69613
  1970
  fixes a b::"'a::euclidean_space"
immler@69613
  1971
  shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
immler@69613
  1972
  by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono
immler@69613
  1973
     simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
immler@69613
  1974
immler@69613
  1975
immler@69617
  1976
subsection%unimportant\<open>Relating linear images to open/closed/interior/closure/connected\<close>
immler@56189
  1977
immler@69611
  1978
proposition open_surjective_linear_image:
immler@69611
  1979
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
immler@69611
  1980
  assumes "open A" "linear f" "surj f"
immler@69611
  1981
    shows "open(f ` A)"
immler@69611
  1982
unfolding open_dist
immler@69611
  1983
proof clarify
immler@69611
  1984
  fix x
immler@69611
  1985
  assume "x \<in> A"
immler@69611
  1986
  have "bounded (inv f ` Basis)"
immler@69611
  1987
    by (simp add: finite_imp_bounded)
immler@69611
  1988
  with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
immler@69611
  1989
    by metis
immler@69611
  1990
  obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
immler@69611
  1991
    by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
immler@69611
  1992
  define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
immler@69611
  1993
  show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
immler@69611
  1994
  proof (intro exI conjI)
immler@69611
  1995
    show "\<delta> > 0"
immler@69611
  1996
      using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def divide_simps)
immler@69611
  1997
    have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
immler@69611
  1998
    proof -
immler@69611
  1999
      define u where "u \<equiv> y - f x"
immler@69611
  2000
      show ?thesis
immler@69611
  2001
      proof (rule image_eqI)
immler@69611
  2002
        show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
immler@69611
  2003
          apply (simp add: linear_add linear_sum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
immler@69611
  2004
          apply (simp add: euclidean_representation u_def)
immler@69611
  2005
          done
immler@69611
  2006
        have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
immler@69611
  2007
          by (simp add: dist_norm sum_norm_le)
immler@69611
  2008
        also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
immler@69611
  2009
          by simp
immler@69611
  2010
        also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
immler@69611
  2011
          by (simp add: B sum_distrib_right sum_mono mult_left_mono)
immler@69611
  2012
        also have "... \<le> DIM('b) * dist y (f x) * B"
immler@69611
  2013
          apply (rule mult_right_mono [OF sum_bounded_above])
immler@69611
  2014
          using \<open>0 < B\<close> by (auto simp: Basis_le_norm dist_norm u_def)
immler@69611
  2015
        also have "... < e"
immler@69611
  2016
          by (metis mult.commute mult.left_commute that)
immler@69611
  2017
        finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
immler@69611
  2018
          by (rule e)
immler@69611
  2019
      qed
immler@69611
  2020
    qed
immler@69611
  2021
    then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
immler@69611
  2022
      using \<open>e > 0\<close> \<open>B > 0\<close>
immler@69611
  2023
      by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
immler@69611
  2024
  qed
immler@69611
  2025
qed
immler@69611
  2026
immler@69611
  2027
corollary open_bijective_linear_image_eq:
immler@69611
  2028
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
immler@69611
  2029
  assumes "linear f" "bij f"
immler@69611
  2030
    shows "open(f ` A) \<longleftrightarrow> open A"
immler@69611
  2031
proof
immler@69611
  2032
  assume "open(f ` A)"
immler@69611
  2033
  then have "open(f -` (f ` A))"
immler@69611
  2034
    using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
immler@69611
  2035
  then show "open A"
immler@69611
  2036
    by (simp add: assms bij_is_inj inj_vimage_image_eq)
immler@69611
  2037
next
immler@69611
  2038
  assume "open A"
immler@69611
  2039
  then show "open(f ` A)"
immler@69611
  2040
    by (simp add: assms bij_is_surj open_surjective_linear_image)
immler@69611
  2041
qed
immler@69611
  2042
immler@69611
  2043
corollary interior_bijective_linear_image:
immler@69611
  2044
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
immler@69611
  2045
  assumes "linear f" "bij f"
immler@69611
  2046
  shows "interior (f ` S) = f ` interior S"  (is "?lhs = ?rhs")
immler@69611
  2047
proof safe
immler@69611
  2048
  fix x
immler@69611
  2049
  assume x: "x \<in> ?lhs"
immler@69611
  2050
  then obtain T where "open T" and "x \<in> T" and "T \<subseteq> f ` S"
immler@69611
  2051
    by (metis interiorE)
immler@69611
  2052
  then show "x \<in> ?rhs"
immler@69611
  2053
    by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
immler@69611
  2054
next
immler@69611
  2055
  fix x
immler@69611
  2056
  assume x: "x \<in> interior S"
immler@69611
  2057
  then show "f x \<in> interior (f ` S)"
immler@69611
  2058
    by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
immler@69611
  2059
qed
immler@69611
  2060
immler@69611
  2061
lemma interior_injective_linear_image:
immler@69611
  2062
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
immler@69611
  2063
  assumes "linear f" "inj f"
immler@69611
  2064
   shows "interior(f ` S) = f ` (interior S)"
immler@69611
  2065
  by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
immler@69611
  2066
immler@69611
  2067
lemma interior_surjective_linear_image:
immler@69611
  2068
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
immler@69611
  2069
  assumes "linear f" "surj f"
immler@69611
  2070
   shows "interior(f ` S) = f ` (interior S)"
immler@69611
  2071
  by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
immler@69611
  2072
immler@69611
  2073
lemma interior_negations:
immler@69611
  2074
  fixes S :: "'a::euclidean_space set"
immler@69611
  2075
  shows "interior(uminus ` S) = image uminus (interior S)"
immler@69611
  2076
  by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
immler@56189
  2077
immler@69617
  2078
lemma connected_linear_image:
immler@69617
  2079
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
immler@69617
  2080
  assumes "linear f" and "connected s"
immler@69617
  2081
  shows "connected (f ` s)"
immler@69617
  2082
using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast
immler@69617
  2083
immler@69617
  2084
immler@69613
  2085
subsection%unimportant \<open>"Isometry" (up to constant bounds) of Injective Linear Map\<close>
immler@69613
  2086
immler@69613
  2087
proposition injective_imp_isometric:
immler@69613
  2088
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
immler@69613
  2089
  assumes s: "closed s" "subspace s"
immler@69613
  2090
    and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
immler@69613
  2091
  shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
immler@69613
  2092
proof (cases "s \<subseteq> {0::'a}")
immler@69613
  2093
  case True
immler@69613
  2094
  have "norm x \<le> norm (f x)" if "x \<in> s" for x
immler@69613
  2095
  proof -
immler@69613
  2096
    from True that have "x = 0" by auto
immler@69613
  2097
    then show ?thesis by simp
immler@69613
  2098
  qed
immler@69613
  2099
  then show ?thesis
immler@69613
  2100
    by (auto intro!: exI[where x=1])
immler@69613
  2101
next
immler@69613
  2102
  case False
immler@69613
  2103
  interpret f: bounded_linear f by fact
immler@69613
  2104
  from False obtain a where a: "a \<noteq> 0" "a \<in> s"
immler@69613
  2105
    by auto
immler@69613
  2106
  from False have "s \<noteq> {}"
immler@69613
  2107
    by auto
immler@69613
  2108
  let ?S = "{f x| x. x \<in> s \<and> norm x = norm a}"
immler@69613
  2109
  let ?S' = "{x::'a. x\<in>s \<and> norm x = norm a}"
immler@69613
  2110
  let ?S'' = "{x::'a. norm x = norm a}"
immler@69613
  2111
immler@69613
  2112
  have "?S'' = frontier (cball 0 (norm a))"
immler@69613
  2113
    by (simp add: sphere_def dist_norm)
immler@69613
  2114
  then have "compact ?S''" by (metis compact_cball compact_frontier)
immler@69613
  2115
  moreover have "?S' = s \<inter> ?S''" by auto
immler@69613
  2116
  ultimately have "compact ?S'"
immler@69613
  2117
    using closed_Int_compact[of s ?S''] using s(1) by auto
immler@69613
  2118
  moreover have *:"f ` ?S' = ?S" by auto
immler@69613
  2119
  ultimately have "compact ?S"
immler@69613
  2120
    using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto
immler@69613
  2121
  then have "closed ?S"
immler@69613
  2122
    using compact_imp_closed by auto
immler@69613
  2123
  moreover from a have "?S \<noteq> {}" by auto
immler@69613
  2124
  ultimately obtain b' where "b'\<in>?S" "\<forall>y\<in>?S. norm b' \<le> norm y"
immler@69613
  2125
    using distance_attains_inf[of ?S 0] unfolding dist_0_norm by auto
immler@69613
  2126
  then obtain b where "b\<in>s"
immler@69613
  2127
    and ba: "norm b = norm a"
immler@69613
  2128
    and b: "\<forall>x\<in>{x \<in> s. norm x = norm a}. norm (f b) \<le> norm (f x)"
immler@69613
  2129
    unfolding *[symmetric] unfolding image_iff by auto
immler@69613
  2130
immler@69613
  2131
  let ?e = "norm (f b) / norm b"
immler@69613
  2132
  have "norm b > 0"
immler@69613
  2133
    using ba and a and norm_ge_zero by auto
immler@69613
  2134
  moreover have "norm (f b) > 0"
immler@69613
  2135
    using f(2)[THEN bspec[where x=b], OF \<open>b\<in>s\<close>]
immler@69613
  2136
    using \<open>norm b >0\<close> by simp
immler@69613
  2137
  ultimately have "0 < norm (f b) / norm b" by simp
immler@69613
  2138
  moreover
immler@69613
  2139
  have "norm (f b) / norm b * norm x \<le> norm (f x)" if "x\<in>s" for x
immler@69613
  2140
  proof (cases "x = 0")
immler@69613
  2141
    case True
immler@69613
  2142
    then show "norm (f b) / norm b * norm x \<le> norm (f x)"
immler@69613
  2143
      by auto
immler@69613
  2144
  next
immler@69613
  2145
    case False
immler@69613
  2146
    with \<open>a \<noteq> 0\<close> have *: "0 < norm a / norm x"
immler@69613
  2147
      unfolding zero_less_norm_iff[symmetric] by simp
immler@69613
  2148
    have "\<forall>x\<in>s. c *\<^sub>R x \<in> s" for c
immler@69613
  2149
      using s[unfolded subspace_def] by simp
immler@69613
  2150
    with \<open>x \<in> s\<close> \<open>x \<noteq> 0\<close> have "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}"
immler@69613
  2151
      by simp
immler@69613
  2152
    with \<open>x \<noteq> 0\<close> \<open>a \<noteq> 0\<close> show "norm (f b) / norm b * norm x \<le> norm (f x)"
immler@69613
  2153
      using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
immler@69613
  2154
      unfolding f.scaleR and ba
immler@69613
  2155
      by (auto simp: mult.commute pos_le_divide_eq pos_divide_le_eq)
immler@69613
  2156
  qed
immler@69613
  2157
  ultimately show ?thesis by auto
immler@69613
  2158
qed
immler@69613
  2159
immler@69613
  2160
proposition closed_injective_image_subspace:
immler@69613
  2161
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
immler@69613
  2162
  assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
immler@69613
  2163
  shows "closed(f ` s)"
immler@69613
  2164
proof -
immler@69613
  2165
  obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
immler@69613
  2166
    using injective_imp_isometric[OF assms(4,1,2,3)] by auto
immler@69613
  2167
  show ?thesis
immler@69613
  2168
    using complete_isometric_image[OF \<open>e>0\<close> assms(1,2) e] and assms(4)
immler@69613
  2169
    unfolding complete_eq_closed[symmetric] by auto
immler@69613
  2170
qed
immler@69613
  2171
immler@69613
  2172
immler@69613
  2173
subsection%unimportant \<open>Some properties of a canonical subspace\<close>
immler@69613
  2174
immler@69613
  2175
lemma closed_substandard: "closed {x::'a::euclidean_space. \<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0}"
immler@69613
  2176
  (is "closed ?A")
immler@69613
  2177
proof -
immler@69613
  2178
  let ?D = "{i\<in>Basis. P i}"
immler@69613
  2179
  have "closed (\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0})"
immler@69613
  2180
    by (simp add: closed_INT closed_Collect_eq continuous_on_inner
immler@69613
  2181
        continuous_on_const continuous_on_id)
immler@69613
  2182
  also have "(\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0}) = ?A"
immler@69613
  2183
    by auto
immler@69613
  2184
  finally show "closed ?A" .
immler@69613
  2185
qed
immler@69613
  2186
immler@69613
  2187
lemma closed_subspace:
immler@69613
  2188
  fixes s :: "'a::euclidean_space set"
immler@69613
  2189
  assumes "subspace s"
immler@69613
  2190
  shows "closed s"
immler@69613
  2191
proof -
immler@69613
  2192
  have "dim s \<le> card (Basis :: 'a set)"
immler@69613
  2193
    using dim_subset_UNIV by auto
immler@69613
  2194
  with ex_card[OF this] obtain d :: "'a set" where t: "card d = dim s" and d: "d \<subseteq> Basis"
immler@69613
  2195
    by auto
immler@69613
  2196
  let ?t = "{x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
immler@69613
  2197
  have "\<exists>f. linear f \<and> f ` {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s \<and>
immler@69613
  2198
      inj_on f {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
immler@69613
  2199
    using dim_substandard[of d] t d assms
immler@69613
  2200
    by (intro subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]]) (auto simp: inner_Basis)
immler@69613
  2201
  then obtain f where f:
immler@69613
  2202
      "linear f"
immler@69613
  2203
      "f ` {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s"
immler@69613
  2204
      "inj_on f {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
immler@69613
  2205
    by blast
immler@69613
  2206
  interpret f: bounded_linear f
immler@69613
  2207
    using f by (simp add: linear_conv_bounded_linear)
immler@69613
  2208
  have "x \<in> ?t \<Longrightarrow> f x = 0 \<Longrightarrow> x = 0" for x
immler@69613
  2209
    using f.zero d f(3)[THEN inj_onD, of x 0] by auto
immler@69613
  2210
  moreover have "closed ?t" by (rule closed_substandard)
immler@69613
  2211
  moreover have "subspace ?t" by (rule subspace_substandard)
immler@69613
  2212
  ultimately show ?thesis
immler@69613
  2213
    using closed_injective_image_subspace[of ?t f]
immler@69613
  2214
    unfolding f(2) using f(1) unfolding linear_conv_bounded_linear by auto
immler@69613
  2215
qed
immler@69613
  2216
immler@69613
  2217
lemma complete_subspace: "subspace s \<Longrightarrow> complete s"
immler@69613
  2218
  for s :: "'a::euclidean_space set"
immler@69613
  2219
  using complete_eq_closed closed_subspace by auto
immler@69613
  2220
immler@69613
  2221
lemma closed_span [iff]: "closed (span s)"
immler@69613
  2222
  for s :: "'a::euclidean_space set"
immler@69613
  2223
  by (simp add: closed_subspace subspace_span)
immler@69613
  2224
immler@69613
  2225
lemma dim_closure [simp]: "dim (closure s) = dim s" (is "?dc = ?d")
immler@69613
  2226
  for s :: "'a::euclidean_space set"
immler@69613
  2227
proof -
immler@69613
  2228
  have "?dc \<le> ?d"
immler@69613
  2229
    using closure_minimal[OF span_superset, of s]
immler@69613
  2230
    using closed_subspace[OF subspace_span, of s]
immler@69613
  2231
    using dim_subset[of "closure s" "span s"]
immler@69613
  2232
    by simp
immler@69613
  2233
  then show ?thesis
immler@69613
  2234
    using dim_subset[OF closure_subset, of s]
immler@69613
  2235
    by simp
immler@69613
  2236
qed
immler@69613
  2237
immler@69613
  2238
immler@69618
  2239
subsection \<open>Set Distance\<close>
immler@69618
  2240
immler@69618
  2241
lemma setdist_compact_closed:
immler@69618
  2242
  fixes S :: "'a::{heine_borel,real_normed_vector} set"
immler@69618
  2243
  assumes S: "compact S" and T: "closed T"
immler@69618
  2244
      and "S \<noteq> {}" "T \<noteq> {}"
immler@69618
  2245
    shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
immler@69618
  2246
proof -
immler@69618
  2247
  have "(\<Union>x\<in> S. \<Union>y \<in> T. {x - y}) \<noteq> {}"
immler@69618
  2248
    using assms by blast
immler@69618
  2249
  then have "\<exists>x \<in> S. \<exists>y \<in> T. dist x y \<le> setdist S T"
immler@69618
  2250
    apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF S T]])
immler@69618
  2251
    apply (simp add: dist_norm le_setdist_iff)
immler@69618
  2252
    apply blast
immler@69618
  2253
    done
immler@69618
  2254
  then show ?thesis
immler@69618
  2255
    by (blast intro!: antisym [OF _ setdist_le_dist] )
immler@69618
  2256
qed
immler@69618
  2257
immler@69618
  2258
lemma setdist_closed_compact:
immler@69618
  2259
  fixes S :: "'a::{heine_borel,real_normed_vector} set"
immler@69618
  2260
  assumes S: "closed S" and T: "compact T"
immler@69618
  2261
      and "S \<noteq> {}" "T \<noteq> {}"
immler@69618
  2262
    shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
immler@69618
  2263
  using setdist_compact_closed [OF T S \<open>T \<noteq> {}\<close> \<open>S \<noteq> {}\<close>]
immler@69618
  2264
  by (metis dist_commute setdist_sym)
immler@69618
  2265
immler@69618
  2266
lemma setdist_eq_0_compact_closed:
immler@69618
  2267
  fixes S :: "'a::{heine_borel,real_normed_vector} set"
immler@69618
  2268
  assumes S: "compact S" and T: "closed T"
immler@69618
  2269
    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
immler@69618
  2270
  apply (cases "S = {} \<or> T = {}", force)
immler@69618
  2271
  using setdist_compact_closed [OF S T]
immler@69618
  2272
  apply (force intro: setdist_eq_0I )
immler@69618
  2273
  done