src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
author immler
Tue Mar 18 10:12:57 2014 +0100 (2014-03-18)
changeset 56188 0268784f60da
parent 56166 9a241bc276cd
child 56189 c4daa97ac57a
permissions -rw-r--r--
use cbox to relax class constraints
immler@54780
     1
theory Ordered_Euclidean_Space
immler@54780
     2
imports
immler@54780
     3
  Topology_Euclidean_Space
immler@54780
     4
  "~~/src/HOL/Library/Product_Order"
immler@54780
     5
begin
immler@54780
     6
immler@54780
     7
subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
immler@54780
     8
immler@54780
     9
class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
immler@54780
    10
  assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
immler@54780
    11
  assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
immler@54780
    12
  assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
immler@54780
    13
  assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
immler@54780
    14
  assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
immler@54780
    15
  assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
immler@54780
    16
  assumes eucl_abs: "abs x = (\<Sum>i\<in>Basis. abs (x \<bullet> i) *\<^sub>R i)"
immler@54780
    17
begin
immler@54780
    18
immler@54780
    19
subclass order
immler@54780
    20
  by default
immler@54780
    21
    (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
immler@54780
    22
immler@54780
    23
subclass ordered_ab_group_add_abs
immler@54780
    24
  by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
immler@54780
    25
immler@54780
    26
subclass ordered_real_vector
immler@54780
    27
  by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
immler@54780
    28
immler@54780
    29
subclass lattice
immler@54780
    30
  by default (auto simp: eucl_inf eucl_sup eucl_le)
immler@54780
    31
immler@54780
    32
subclass distrib_lattice
immler@54780
    33
  by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
immler@54780
    34
immler@54780
    35
subclass conditionally_complete_lattice
immler@54780
    36
proof
immler@54780
    37
  fix z::'a and X::"'a set"
immler@54780
    38
  assume "X \<noteq> {}"
immler@54780
    39
  hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
immler@54780
    40
  thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
immler@54780
    41
    by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
haftmann@56166
    42
      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq
immler@54780
    43
      intro!: cInf_greatest cSup_least)
immler@54780
    44
qed (force intro!: cInf_lower cSup_upper
immler@54780
    45
      simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
haftmann@56166
    46
        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
haftmann@56166
    47
      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+
immler@54780
    48
immler@54780
    49
lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
immler@54780
    50
  and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
immler@54780
    51
  by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib setsum_delta
immler@54780
    52
      cong: if_cong)
immler@54780
    53
immler@54780
    54
lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
immler@54780
    55
  and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
haftmann@56166
    56
  using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
immler@54780
    57
immler@54780
    58
lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
immler@54780
    59
  by (auto simp: eucl_abs)
immler@54780
    60
immler@54780
    61
lemma
immler@54780
    62
  abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
immler@54780
    63
  by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
immler@54780
    64
immler@54780
    65
lemma interval_inner_leI:
immler@54780
    66
  assumes "x \<in> {a .. b}" "0 \<le> i"
immler@54780
    67
  shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
immler@54780
    68
  using assms
immler@54780
    69
  unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
immler@54780
    70
  by (auto intro!: setsum_mono mult_right_mono simp: eucl_le)
immler@54780
    71
immler@54780
    72
lemma inner_nonneg_nonneg:
immler@54780
    73
  shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
immler@54780
    74
  using interval_inner_leI[of a 0 a b]
immler@54780
    75
  by auto
immler@54780
    76
immler@54780
    77
lemma inner_Basis_mono:
immler@54780
    78
  shows "a \<le> b \<Longrightarrow> c \<in> Basis  \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
immler@54780
    79
  by (simp add: eucl_le)
immler@54780
    80
immler@54780
    81
lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
immler@54780
    82
  by (auto simp: eucl_le inner_Basis)
immler@54780
    83
immler@54781
    84
lemma Sup_eq_maximum_componentwise:
immler@54781
    85
  fixes s::"'a set"
immler@54781
    86
  assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
immler@54781
    87
  assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b"
immler@54781
    88
  assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
immler@54781
    89
  shows "Sup s = X"
immler@54781
    90
  using assms
immler@54781
    91
  unfolding eucl_Sup euclidean_representation_setsum
haftmann@56166
    92
  by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
immler@54781
    93
immler@54781
    94
lemma Inf_eq_minimum_componentwise:
immler@54781
    95
  assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
immler@54781
    96
  assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b"
immler@54781
    97
  assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
immler@54781
    98
  shows "Inf s = X"
immler@54781
    99
  using assms
immler@54781
   100
  unfolding eucl_Inf euclidean_representation_setsum
haftmann@56166
   101
  by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
immler@54781
   102
immler@54780
   103
end
immler@54780
   104
immler@54781
   105
lemma
immler@54781
   106
  compact_attains_Inf_componentwise:
immler@54781
   107
  fixes b::"'a::ordered_euclidean_space"
immler@54781
   108
  assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
immler@54781
   109
  obtains x where "x \<in> X" "x \<bullet> b = Inf X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
immler@54781
   110
proof atomize_elim
immler@54781
   111
  let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
immler@54781
   112
  from assms have "compact ?proj" "?proj \<noteq> {}"
immler@54781
   113
    by (auto intro!: compact_continuous_image continuous_on_intros)
immler@54781
   114
  from compact_attains_inf[OF this]
immler@54781
   115
  obtain s x
immler@54781
   116
    where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t"
immler@54781
   117
      and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
immler@54781
   118
    by auto
immler@54781
   119
  hence "Inf ?proj = x \<bullet> b"
haftmann@56166
   120
    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq)
immler@54781
   121
  hence "x \<bullet> b = Inf X \<bullet> b"
haftmann@56166
   122
    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
haftmann@56166
   123
      simp del: Inf_class.Inf_image_eq
haftmann@56166
   124
      cong: if_cong)
immler@54781
   125
  with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
immler@54781
   126
qed
immler@54781
   127
immler@54781
   128
lemma
immler@54781
   129
  compact_attains_Sup_componentwise:
immler@54781
   130
  fixes b::"'a::ordered_euclidean_space"
immler@54781
   131
  assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
immler@54781
   132
  obtains x where "x \<in> X" "x \<bullet> b = Sup X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
immler@54781
   133
proof atomize_elim
immler@54781
   134
  let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
immler@54781
   135
  from assms have "compact ?proj" "?proj \<noteq> {}"
immler@54781
   136
    by (auto intro!: compact_continuous_image continuous_on_intros)
immler@54781
   137
  from compact_attains_sup[OF this]
immler@54781
   138
  obtain s x
immler@54781
   139
    where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s"
immler@54781
   140
      and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
immler@54781
   141
    by auto
immler@54781
   142
  hence "Sup ?proj = x \<bullet> b"
haftmann@56166
   143
    by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq)
immler@54781
   144
  hence "x \<bullet> b = Sup X \<bullet> b"
haftmann@56166
   145
    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
haftmann@56166
   146
      simp del: Sup_image_eq cong: if_cong)
immler@54781
   147
  with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
immler@54781
   148
qed
immler@54781
   149
immler@54780
   150
lemma (in order) atLeastatMost_empty'[simp]:
immler@54780
   151
  "(~ a <= b) \<Longrightarrow> {a..b} = {}"
immler@54780
   152
  by (auto)
immler@54780
   153
immler@54780
   154
instance real :: ordered_euclidean_space
immler@54780
   155
  by default (auto simp: INF_def SUP_def)
immler@54780
   156
immler@54780
   157
lemma in_Basis_prod_iff:
immler@54780
   158
  fixes i::"'a::euclidean_space*'b::euclidean_space"
immler@54780
   159
  shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
immler@54780
   160
  by (cases i) (auto simp: Basis_prod_def)
immler@54780
   161
immler@54780
   162
instantiation prod::(abs, abs) abs
immler@54780
   163
begin
immler@54780
   164
immler@54780
   165
definition "abs x = (abs (fst x), abs (snd x))"
immler@54780
   166
immler@54780
   167
instance proof qed
immler@54780
   168
end
immler@54780
   169
immler@54780
   170
instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
immler@54780
   171
  by default
immler@54780
   172
    (auto intro!: add_mono simp add: euclidean_representation_setsum'  Ball_def inner_prod_def
immler@54780
   173
      in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
immler@54780
   174
      inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
immler@54780
   175
      eucl_le[where 'a='b] abs_prod_def abs_inner)
immler@54780
   176
immler@54780
   177
immler@56188
   178
subsection {* Boxes *}
immler@54780
   179
immler@56188
   180
lemma box:
immler@56188
   181
  fixes a :: "'a::euclidean_space"
immler@54780
   182
  shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
immler@56188
   183
    and "cbox a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
immler@56188
   184
  by (auto simp add:set_eq_iff box_def cbox_def)
immler@54780
   185
immler@56188
   186
lemma mem_box:
immler@56188
   187
  fixes a :: "'a::euclidean_space"
immler@54780
   188
  shows "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
   189
    and "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
   190
  using box[of a b]
immler@54780
   191
  by auto
immler@54780
   192
immler@56188
   193
lemma box_eq_empty:
immler@56188
   194
  fixes a :: "'a::euclidean_space"
immler@54780
   195
  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
immler@56188
   196
    and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
immler@54780
   197
proof -
immler@54780
   198
  {
immler@54780
   199
    fix i x
immler@54780
   200
    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
immler@54780
   201
    then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
immler@56188
   202
      unfolding mem_box by (auto simp: box_def)
immler@54780
   203
    then have "a\<bullet>i < b\<bullet>i" by auto
immler@54780
   204
    then have False using as by auto
immler@54780
   205
  }
immler@54780
   206
  moreover
immler@54780
   207
  {
immler@54780
   208
    assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
immler@54780
   209
    let ?x = "(1/2) *\<^sub>R (a + b)"
immler@54780
   210
    {
immler@54780
   211
      fix i :: 'a
immler@54780
   212
      assume i: "i \<in> Basis"
immler@54780
   213
      have "a\<bullet>i < b\<bullet>i"
immler@54780
   214
        using as[THEN bspec[where x=i]] i by auto
immler@54780
   215
      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@54780
   216
        by (auto simp: inner_add_left)
immler@54780
   217
    }
immler@54780
   218
    then have "box a b \<noteq> {}"
immler@56188
   219
      using mem_box(1)[of "?x" a b] by auto
immler@54780
   220
  }
immler@54780
   221
  ultimately show ?th1 by blast
immler@54780
   222
immler@54780
   223
  {
immler@54780
   224
    fix i x
immler@56188
   225
    assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
immler@54780
   226
    then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
immler@56188
   227
      unfolding mem_box by auto
immler@54780
   228
    then have "a\<bullet>i \<le> b\<bullet>i" by auto
immler@54780
   229
    then have False using as by auto
immler@54780
   230
  }
immler@54780
   231
  moreover
immler@54780
   232
  {
immler@54780
   233
    assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
immler@54780
   234
    let ?x = "(1/2) *\<^sub>R (a + b)"
immler@54780
   235
    {
immler@54780
   236
      fix i :: 'a
immler@54780
   237
      assume i:"i \<in> Basis"
immler@54780
   238
      have "a\<bullet>i \<le> b\<bullet>i"
immler@54780
   239
        using as[THEN bspec[where x=i]] i by auto
immler@54780
   240
      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@54780
   241
        by (auto simp: inner_add_left)
immler@54780
   242
    }
immler@56188
   243
    then have "cbox a b \<noteq> {}"
immler@56188
   244
      using mem_box(2)[of "?x" a b] by auto
immler@54780
   245
  }
immler@54780
   246
  ultimately show ?th2 by blast
immler@54780
   247
qed
immler@54780
   248
immler@56188
   249
lemma box_ne_empty:
immler@56188
   250
  fixes a :: "'a::euclidean_space"
immler@56188
   251
  shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
immler@54780
   252
  and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
immler@56188
   253
  unfolding box_eq_empty[of a b] by fastforce+
immler@54780
   254
immler@56188
   255
lemma
immler@56188
   256
  fixes a :: "'a::euclidean_space"
immler@56188
   257
  shows cbox_sing: "cbox a a = {a}"
immler@56188
   258
    and box_sing: "box a a = {}"
immler@56188
   259
  unfolding set_eq_iff mem_box eq_iff [symmetric]
immler@56188
   260
  by (auto intro!: euclidean_eqI[where 'a='a])
immler@56188
   261
     (metis all_not_in_conv nonempty_Basis)
immler@54780
   262
immler@56188
   263
lemma subset_box_imp:
immler@56188
   264
  fixes a :: "'a::euclidean_space"
immler@56188
   265
  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@56188
   266
    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@56188
   267
    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@56188
   268
     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@56188
   269
  unfolding subset_eq[unfolded Ball_def] unfolding mem_box
immler@56188
   270
   by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
immler@54780
   271
immler@56188
   272
lemma box_subset_cbox:
immler@56188
   273
  fixes a :: "'a::euclidean_space"
immler@56188
   274
  shows "box a b \<subseteq> cbox a b"
immler@56188
   275
  unfolding subset_eq [unfolded Ball_def] mem_box
immler@54780
   276
  by (fast intro: less_imp_le)
immler@54780
   277
immler@56188
   278
lemma subset_box:
immler@56188
   279
  fixes a :: "'a::euclidean_space"
immler@56188
   280
  shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
immler@56188
   281
    and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
immler@56188
   282
    and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
immler@54780
   283
    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
immler@54780
   284
proof -
immler@54780
   285
  show ?th1
immler@56188
   286
    unfolding subset_eq and Ball_def and mem_box
immler@54780
   287
    by (auto intro: order_trans)
immler@54780
   288
  show ?th2
immler@56188
   289
    unfolding subset_eq and Ball_def and mem_box
immler@54780
   290
    by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
immler@54780
   291
  {
immler@56188
   292
    assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
immler@54780
   293
    then have "box c d \<noteq> {}"
immler@56188
   294
      unfolding box_eq_empty by auto
immler@54780
   295
    fix i :: 'a
immler@54780
   296
    assume i: "i \<in> Basis"
immler@54780
   297
    (** TODO combine the following two parts as done in the HOL_light version. **)
immler@54780
   298
    {
immler@54780
   299
      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"
immler@54780
   300
      assume as2: "a\<bullet>i > c\<bullet>i"
immler@54780
   301
      {
immler@54780
   302
        fix j :: 'a
immler@54780
   303
        assume j: "j \<in> Basis"
immler@54780
   304
        then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
immler@54780
   305
          apply (cases "j = i")
immler@54780
   306
          using as(2)[THEN bspec[where x=j]] i
immler@54780
   307
          apply (auto simp add: as2)
immler@54780
   308
          done
immler@54780
   309
      }
immler@54780
   310
      then have "?x\<in>box c d"
immler@56188
   311
        using i unfolding mem_box by auto
immler@54780
   312
      moreover
immler@56188
   313
      have "?x \<notin> cbox a b"
immler@56188
   314
        unfolding mem_box
immler@54780
   315
        apply auto
immler@54780
   316
        apply (rule_tac x=i in bexI)
immler@54780
   317
        using as(2)[THEN bspec[where x=i]] and as2 i
immler@54780
   318
        apply auto
immler@54780
   319
        done
immler@54780
   320
      ultimately have False using as by auto
immler@54780
   321
    }
immler@54780
   322
    then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
immler@54780
   323
    moreover
immler@54780
   324
    {
immler@54780
   325
      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"
immler@54780
   326
      assume as2: "b\<bullet>i < d\<bullet>i"
immler@54780
   327
      {
immler@54780
   328
        fix j :: 'a
immler@54780
   329
        assume "j\<in>Basis"
immler@54780
   330
        then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
immler@54780
   331
          apply (cases "j = i")
immler@54780
   332
          using as(2)[THEN bspec[where x=j]]
immler@54780
   333
          apply (auto simp add: as2)
immler@54780
   334
          done
immler@54780
   335
      }
immler@54780
   336
      then have "?x\<in>box c d"
immler@56188
   337
        unfolding mem_box by auto
immler@54780
   338
      moreover
immler@56188
   339
      have "?x\<notin>cbox a b"
immler@56188
   340
        unfolding mem_box
immler@54780
   341
        apply auto
immler@54780
   342
        apply (rule_tac x=i in bexI)
immler@54780
   343
        using as(2)[THEN bspec[where x=i]] and as2 using i
immler@54780
   344
        apply auto
immler@54780
   345
        done
immler@54780
   346
      ultimately have False using as by auto
immler@54780
   347
    }
immler@54780
   348
    then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
immler@54780
   349
    ultimately
immler@54780
   350
    have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
immler@54780
   351
  } note part1 = this
immler@54780
   352
  show ?th3
immler@56188
   353
    unfolding subset_eq and Ball_def and mem_box
immler@54780
   354
    apply (rule, rule, rule, rule)
immler@54780
   355
    apply (rule part1)
immler@56188
   356
    unfolding subset_eq and Ball_def and mem_box
immler@54780
   357
    prefer 4
immler@54780
   358
    apply auto
immler@54780
   359
    apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
immler@54780
   360
    done
immler@54780
   361
  {
immler@54780
   362
    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
immler@54780
   363
    fix i :: 'a
immler@54780
   364
    assume i:"i\<in>Basis"
immler@56188
   365
    from as(1) have "box c d \<subseteq> cbox a b"
immler@56188
   366
      using box_subset_cbox[of a b] by auto
immler@54780
   367
    then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
immler@54780
   368
      using part1 and as(2) using i by auto
immler@54780
   369
  } note * = this
immler@54780
   370
  show ?th4
immler@56188
   371
    unfolding subset_eq and Ball_def and mem_box
immler@54780
   372
    apply (rule, rule, rule, rule)
immler@54780
   373
    apply (rule *)
immler@56188
   374
    unfolding subset_eq and Ball_def and mem_box
immler@54780
   375
    prefer 4
immler@54780
   376
    apply auto
immler@54780
   377
    apply (erule_tac x=xa in allE, simp)+
immler@54780
   378
    done
immler@54780
   379
qed
immler@54780
   380
immler@54780
   381
lemma inter_interval:
immler@56188
   382
  fixes a :: "'a::euclidean_space"
immler@56188
   383
  shows "cbox a b \<inter> cbox c d =
immler@56188
   384
    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@56188
   385
  unfolding set_eq_iff and Int_iff and mem_box
immler@54780
   386
  by auto
immler@54780
   387
immler@54780
   388
lemma disjoint_interval:
immler@56188
   389
  fixes a::"'a::euclidean_space"
immler@56188
   390
  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@56188
   391
    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@56188
   392
    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@54780
   393
    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@54780
   394
proof -
immler@54780
   395
  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@54780
   396
  have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
immler@54780
   397
      (\<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@54780
   398
    by blast
immler@56188
   399
  note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
immler@54780
   400
  show ?th1 unfolding * by (intro **) auto
immler@54780
   401
  show ?th2 unfolding * by (intro **) auto
immler@54780
   402
  show ?th3 unfolding * by (intro **) auto
immler@54780
   403
  show ?th4 unfolding * by (intro **) auto
immler@54780
   404
qed
immler@54780
   405
immler@56188
   406
(* Moved box_subset_cbox a bit upwards *)
immler@54780
   407
immler@56188
   408
lemma open_box[intro]:
immler@56188
   409
  fixes a b :: "'a::euclidean_space"
immler@54780
   410
  shows "open (box a b)"
immler@54780
   411
proof -
immler@54780
   412
  have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
immler@54780
   413
    by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
immler@54780
   414
      linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
immler@54780
   415
  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
immler@56188
   416
    by (auto simp add: box)
immler@54780
   417
  finally show "open (box a b)" .
immler@54780
   418
qed
immler@54780
   419
immler@56188
   420
lemma closed_cbox[intro]:
immler@56188
   421
  fixes a b :: "'a::euclidean_space"
immler@56188
   422
  shows "closed (cbox a b)"
immler@54780
   423
proof -
immler@54780
   424
  have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
immler@54780
   425
    by (intro closed_INT ballI continuous_closed_vimage allI
immler@54780
   426
      linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
immler@56188
   427
  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
immler@56188
   428
    by (auto simp add: cbox_def)
immler@56188
   429
  finally show "closed (cbox a b)" .
immler@54780
   430
qed
immler@54780
   431
immler@56188
   432
lemma interior_cbox [intro]:
immler@56188
   433
  fixes a b :: "'a::euclidean_space"
immler@56188
   434
  shows "interior (cbox a b) = box a b" (is "?L = ?R")
immler@54780
   435
proof(rule subset_antisym)
immler@54780
   436
  show "?R \<subseteq> ?L"
immler@56188
   437
    using box_subset_cbox open_box
immler@54780
   438
    by (rule interior_maximal)
immler@54780
   439
  {
immler@54780
   440
    fix x
immler@56188
   441
    assume "x \<in> interior (cbox a b)"
immler@56188
   442
    then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" ..
immler@56188
   443
    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b"
immler@54780
   444
      unfolding open_dist and subset_eq by auto
immler@54780
   445
    {
immler@54780
   446
      fix i :: 'a
immler@54780
   447
      assume i: "i \<in> Basis"
immler@54780
   448
      have "dist (x - (e / 2) *\<^sub>R i) x < e"
immler@54780
   449
        and "dist (x + (e / 2) *\<^sub>R i) x < e"
immler@54780
   450
        unfolding dist_norm
immler@54780
   451
        apply auto
immler@54780
   452
        unfolding norm_minus_cancel
immler@54780
   453
        using norm_Basis[OF i] `e>0`
immler@54780
   454
        apply auto
immler@54780
   455
        done
immler@54780
   456
      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@54780
   457
        using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
immler@54780
   458
          and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
immler@56188
   459
        unfolding mem_box
immler@54780
   460
        using i
immler@54780
   461
        by blast+
immler@54780
   462
      then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
immler@54780
   463
        using `e>0` i
immler@54780
   464
        by (auto simp: inner_diff_left inner_Basis inner_add_left)
immler@54780
   465
    }
immler@54780
   466
    then have "x \<in> box a b"
immler@56188
   467
      unfolding mem_box by auto
immler@54780
   468
  }
immler@54780
   469
  then show "?L \<subseteq> ?R" ..
immler@54780
   470
qed
immler@54780
   471
immler@56188
   472
lemma bounded_cbox:
immler@56188
   473
  fixes a :: "'a::euclidean_space"
immler@56188
   474
  shows "bounded (cbox a b)"
immler@54780
   475
proof -
immler@54780
   476
  let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
immler@54780
   477
  {
immler@54780
   478
    fix x :: "'a"
immler@54780
   479
    assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
immler@54780
   480
    {
immler@54780
   481
      fix i :: 'a
immler@54780
   482
      assume "i \<in> Basis"
immler@54780
   483
      then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
immler@54780
   484
        using x[THEN bspec[where x=i]] by auto
immler@54780
   485
    }
immler@54780
   486
    then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
immler@54780
   487
      apply -
immler@54780
   488
      apply (rule setsum_mono)
immler@54780
   489
      apply auto
immler@54780
   490
      done
immler@54780
   491
    then have "norm x \<le> ?b"
immler@54780
   492
      using norm_le_l1[of x] by auto
immler@54780
   493
  }
immler@54780
   494
  then show ?thesis
immler@56188
   495
    unfolding box and bounded_iff by auto
immler@54780
   496
qed
immler@54780
   497
immler@54780
   498
lemma bounded_interval:
immler@56188
   499
  fixes a :: "'a::euclidean_space"
immler@56188
   500
  shows "bounded (cbox a b) \<and> bounded (box a b)"
immler@56188
   501
  using bounded_cbox[of a b]
immler@56188
   502
  using box_subset_cbox[of a b]
immler@56188
   503
  using bounded_subset[of "cbox a b" "box a b"]
immler@54780
   504
  by simp
immler@54780
   505
immler@54780
   506
lemma not_interval_univ:
immler@56188
   507
  fixes a :: "'a::euclidean_space"
immler@56188
   508
  shows "cbox a b \<noteq> UNIV \<and> box a b \<noteq> UNIV"
immler@54780
   509
  using bounded_interval[of a b] by auto
immler@54780
   510
immler@56188
   511
lemma compact_cbox:
immler@56188
   512
  fixes a :: "'a::euclidean_space"
immler@56188
   513
  shows "compact (cbox a b)"
immler@56188
   514
  using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_interval[of a b]
immler@54780
   515
  by (auto simp: compact_eq_seq_compact_metric)
immler@54780
   516
immler@54780
   517
lemma open_interval_midpoint:
immler@56188
   518
  fixes a :: "'a::euclidean_space"
immler@54780
   519
  assumes "box a b \<noteq> {}"
immler@54780
   520
  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
immler@54780
   521
proof -
immler@54780
   522
  {
immler@54780
   523
    fix i :: 'a
immler@54780
   524
    assume "i \<in> Basis"
immler@54780
   525
    then have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i"
immler@56188
   526
      using assms[unfolded box_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
immler@54780
   527
  }
immler@56188
   528
  then show ?thesis unfolding mem_box by auto
immler@54780
   529
qed
immler@54780
   530
immler@54780
   531
lemma open_closed_interval_convex:
immler@56188
   532
  fixes x :: "'a::euclidean_space"
immler@54780
   533
  assumes x: "x \<in> box a b"
immler@56188
   534
    and y: "y \<in> cbox a b"
immler@54780
   535
    and e: "0 < e" "e \<le> 1"
immler@54780
   536
  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
immler@54780
   537
proof -
immler@54780
   538
  {
immler@54780
   539
    fix i :: 'a
immler@54780
   540
    assume i: "i \<in> Basis"
immler@54780
   541
    have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
immler@54780
   542
      unfolding left_diff_distrib by simp
immler@54780
   543
    also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
immler@54780
   544
      apply (rule add_less_le_mono)
immler@54780
   545
      using e unfolding mult_less_cancel_left and mult_le_cancel_left
immler@54780
   546
      apply simp_all
immler@56188
   547
      using x unfolding mem_box using i
immler@54780
   548
      apply simp
immler@56188
   549
      using y unfolding mem_box using i
immler@54780
   550
      apply simp
immler@54780
   551
      done
immler@54780
   552
    finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
immler@54780
   553
      unfolding inner_simps by auto
immler@54780
   554
    moreover
immler@54780
   555
    {
immler@54780
   556
      have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
immler@54780
   557
        unfolding left_diff_distrib by simp
immler@54780
   558
      also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
immler@54780
   559
        apply (rule add_less_le_mono)
immler@54780
   560
        using e unfolding mult_less_cancel_left and mult_le_cancel_left
immler@54780
   561
        apply simp_all
immler@54780
   562
        using x
immler@56188
   563
        unfolding mem_box
immler@54780
   564
        using i
immler@54780
   565
        apply simp
immler@54780
   566
        using y
immler@56188
   567
        unfolding mem_box
immler@54780
   568
        using i
immler@54780
   569
        apply simp
immler@54780
   570
        done
immler@54780
   571
      finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
immler@54780
   572
        unfolding inner_simps by auto
immler@54780
   573
    }
immler@54780
   574
    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@54780
   575
      by auto
immler@54780
   576
  }
immler@54780
   577
  then show ?thesis
immler@56188
   578
    unfolding mem_box by auto
immler@54780
   579
qed
immler@54780
   580
immler@54780
   581
notation
immler@54780
   582
  eucl_less (infix "<e" 50)
immler@54780
   583
immler@54780
   584
lemma closure_open_interval:
immler@56188
   585
  fixes a :: "'a::euclidean_space"
immler@56188
   586
   assumes "box a b \<noteq> {}"
immler@56188
   587
  shows "closure (box a b) = cbox a b"
immler@54780
   588
proof -
immler@54780
   589
  have ab: "a <e b"
immler@56188
   590
    using assms by (simp add: eucl_less_def box_ne_empty)
immler@54780
   591
  let ?c = "(1 / 2) *\<^sub>R (a + b)"
immler@54780
   592
  {
immler@54780
   593
    fix x
immler@56188
   594
    assume as:"x \<in> cbox a b"
immler@54780
   595
    def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
immler@54780
   596
    {
immler@54780
   597
      fix n
immler@54780
   598
      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
immler@54780
   599
      have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
immler@54780
   600
        unfolding inverse_le_1_iff by auto
immler@54780
   601
      have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
immler@54780
   602
        x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
immler@54780
   603
        by (auto simp add: algebra_simps)
immler@54780
   604
      then have "f n <e b" and "a <e f n"
immler@54780
   605
        using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
immler@56188
   606
        unfolding f_def by (auto simp: box eucl_less_def)
immler@54780
   607
      then have False
immler@54780
   608
        using fn unfolding f_def using xc by auto
immler@54780
   609
    }
immler@54780
   610
    moreover
immler@54780
   611
    {
immler@54780
   612
      assume "\<not> (f ---> x) sequentially"
immler@54780
   613
      {
immler@54780
   614
        fix e :: real
immler@54780
   615
        assume "e > 0"
immler@54780
   616
        then have "\<exists>N::nat. inverse (real (N + 1)) < e"
immler@54780
   617
          using real_arch_inv[of e]
immler@54780
   618
          apply (auto simp add: Suc_pred')
immler@54780
   619
          apply (rule_tac x="n - 1" in exI)
immler@54780
   620
          apply auto
immler@54780
   621
          done
immler@54780
   622
        then obtain N :: nat where "inverse (real (N + 1)) < e"
immler@54780
   623
          by auto
immler@54780
   624
        then have "\<forall>n\<ge>N. inverse (real n + 1) < e"
immler@54780
   625
          apply auto
immler@54780
   626
          apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans
immler@54780
   627
            real_of_nat_Suc real_of_nat_Suc_gt_zero)
immler@54780
   628
          done
immler@54780
   629
        then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
immler@54780
   630
      }
immler@54780
   631
      then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
immler@54780
   632
        unfolding LIMSEQ_def by(auto simp add: dist_norm)
immler@54780
   633
      then have "(f ---> x) sequentially"
immler@54780
   634
        unfolding f_def
immler@54780
   635
        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@54780
   636
        using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
immler@54780
   637
        by auto
immler@54780
   638
    }
immler@54780
   639
    ultimately have "x \<in> closure (box a b)"
immler@54780
   640
      using as and open_interval_midpoint[OF assms]
immler@54780
   641
      unfolding closure_def
immler@54780
   642
      unfolding islimpt_sequential
immler@54780
   643
      by (cases "x=?c") (auto simp: in_box_eucl_less)
immler@54780
   644
  }
immler@54780
   645
  then show ?thesis
immler@56188
   646
    using closure_minimal[OF box_subset_cbox, of a b] by blast
immler@54780
   647
qed
immler@54780
   648
immler@54780
   649
lemma bounded_subset_open_interval_symmetric:
immler@56188
   650
  fixes s::"('a::euclidean_space) set"
immler@54780
   651
  assumes "bounded s"
immler@54780
   652
  shows "\<exists>a. s \<subseteq> box (-a) a"
immler@54780
   653
proof -
immler@54780
   654
  obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
immler@54780
   655
    using assms[unfolded bounded_pos] by auto
immler@54780
   656
  def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a"
immler@54780
   657
  {
immler@54780
   658
    fix x
immler@54780
   659
    assume "x \<in> s"
immler@54780
   660
    fix i :: 'a
immler@54780
   661
    assume i: "i \<in> Basis"
immler@54780
   662
    then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
immler@54780
   663
      using b[THEN bspec[where x=x], OF `x\<in>s`]
immler@54780
   664
      using Basis_le_norm[OF i, of x]
immler@54780
   665
      unfolding inner_simps and a_def
immler@54780
   666
      by auto
immler@54780
   667
  }
immler@54780
   668
  then show ?thesis
immler@56188
   669
    by (auto intro: exI[where x=a] simp add: box)
immler@54780
   670
qed
immler@54780
   671
immler@54780
   672
lemma bounded_subset_open_interval:
immler@56188
   673
  fixes s :: "('a::euclidean_space) set"
immler@54780
   674
  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
immler@54780
   675
  by (auto dest!: bounded_subset_open_interval_symmetric)
immler@54780
   676
immler@56188
   677
lemma bounded_subset_cbox_symmetric:
immler@56188
   678
  fixes s :: "('a::euclidean_space) set"
immler@56188
   679
   assumes "bounded s"
immler@56188
   680
  shows "\<exists>a. s \<subseteq> cbox (-a) a"
immler@54780
   681
proof -
immler@54780
   682
  obtain a where "s \<subseteq> box (-a) a"
immler@54780
   683
    using bounded_subset_open_interval_symmetric[OF assms] by auto
immler@54780
   684
  then show ?thesis
immler@56188
   685
    using box_subset_cbox[of "-a" a] by auto
immler@54780
   686
qed
immler@54780
   687
immler@56188
   688
lemma bounded_subset_cbox:
immler@56188
   689
  fixes s :: "('a::euclidean_space) set"
immler@56188
   690
  shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a b"
immler@56188
   691
  using bounded_subset_cbox_symmetric[of s] by auto
immler@54780
   692
immler@54780
   693
lemma frontier_closed_interval:
immler@56188
   694
  fixes a b :: "'a::euclidean_space"
immler@56188
   695
  shows "frontier (cbox a b) = cbox a b - box a b"
immler@56188
   696
  unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
immler@54780
   697
immler@54780
   698
lemma frontier_open_interval:
immler@56188
   699
  fixes a b :: "'a::euclidean_space"
immler@56188
   700
  shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
immler@54780
   701
proof (cases "box a b = {}")
immler@54780
   702
  case True
immler@54780
   703
  then show ?thesis
immler@54780
   704
    using frontier_empty by auto
immler@54780
   705
next
immler@54780
   706
  case False
immler@54780
   707
  then show ?thesis
immler@56188
   708
    unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_box]
immler@54780
   709
    by auto
immler@54780
   710
qed
immler@54780
   711
immler@54780
   712
lemma inter_interval_mixed_eq_empty:
immler@56188
   713
  fixes a :: "'a::euclidean_space"
immler@56188
   714
   assumes "box c d \<noteq> {}"
immler@56188
   715
  shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
immler@54780
   716
  unfolding closure_open_interval[OF assms, symmetric]
immler@56188
   717
  unfolding open_inter_closure_eq_empty[OF open_box] ..
immler@54780
   718
immler@54781
   719
lemma diameter_closed_interval:
immler@54781
   720
  fixes a b::"'a::ordered_euclidean_space"
immler@54781
   721
  shows "a \<le> b \<Longrightarrow> diameter {a..b} = dist a b"
haftmann@56166
   722
  by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
immler@54781
   723
     simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm)
immler@54781
   724
immler@54780
   725
text {* Intervals in general, including infinite and mixtures of open and closed. *}
immler@54780
   726
immler@54780
   727
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
immler@54780
   728
  (\<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@54780
   729
immler@56188
   730
lemma is_interval_interval: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
immler@54780
   731
  "is_interval (box a b)" (is ?th2) proof -
immler@56188
   732
  show ?th1 ?th2  unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
immler@54780
   733
    by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
immler@54780
   734
immler@54780
   735
lemma is_interval_empty:
immler@54780
   736
 "is_interval {}"
immler@54780
   737
  unfolding is_interval_def
immler@54780
   738
  by simp
immler@54780
   739
immler@54780
   740
lemma is_interval_univ:
immler@54780
   741
 "is_interval UNIV"
immler@54780
   742
  unfolding is_interval_def
immler@54780
   743
  by simp
immler@54780
   744
immler@54781
   745
lemma mem_is_intervalI:
immler@54781
   746
  assumes "is_interval s"
immler@54781
   747
  assumes "a \<in> s" "b \<in> s"
immler@54781
   748
  assumes "\<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@54781
   749
  shows "x \<in> s"
immler@54781
   750
  by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
immler@54781
   751
immler@54781
   752
lemma interval_subst:
immler@54781
   753
  fixes S::"'a::ordered_euclidean_space set"
immler@54781
   754
  assumes "is_interval S"
immler@54781
   755
  assumes "x \<in> S" "y j \<in> S"
immler@54781
   756
  assumes "j \<in> Basis"
immler@54781
   757
  shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
immler@54781
   758
  by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
immler@54781
   759
immler@56188
   760
lemma mem_box_componentwiseI:
immler@54781
   761
  fixes S::"'a::ordered_euclidean_space set"
immler@54781
   762
  assumes "is_interval S"
immler@54781
   763
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
immler@54781
   764
  shows "x \<in> S"
immler@54781
   765
proof -
immler@54781
   766
  from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
immler@54781
   767
    by auto
immler@54781
   768
  with finite_Basis obtain s and bs::"'a list" where
immler@54781
   769
    s: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i = s i \<bullet> i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<in> S" and
immler@54781
   770
    bs: "set bs = Basis" "distinct bs"
immler@54781
   771
    by (metis finite_distinct_list)
immler@54781
   772
  from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" by blast
blanchet@55413
   773
  def y \<equiv> "rec_list
immler@54781
   774
    (s j)
immler@54781
   775
    (\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
immler@54781
   776
  have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
immler@54781
   777
    using bs by (auto simp add: s(1)[symmetric] euclidean_representation)
immler@54781
   778
  also have [symmetric]: "y bs = \<dots>"
immler@54781
   779
    using bs(2) bs(1)[THEN equalityD1]
immler@54781
   780
    by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
immler@54781
   781
  also have "y bs \<in> S"
immler@54781
   782
    using bs(1)[THEN equalityD1]
immler@54781
   783
    apply (induct bs)
immler@54781
   784
    apply (auto simp: y_def j)
immler@54781
   785
    apply (rule interval_subst[OF assms(1)])
immler@54781
   786
    apply (auto simp: s)
immler@54781
   787
    done
immler@54781
   788
  finally show ?thesis .
immler@54781
   789
qed
immler@54781
   790
immler@56188
   791
lemma eucl_less_eq_halfspaces:
immler@56188
   792
  fixes a :: "'a\<Colon>euclidean_space"
immler@54780
   793
  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
immler@56188
   794
    "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
immler@54780
   795
  by (auto simp: eucl_less_def)
immler@54780
   796
immler@56188
   797
lemma eucl_le_eq_halfspaces:
immler@56188
   798
  fixes a :: "'a\<Colon>euclidean_space"
immler@56188
   799
  shows "{x. \<forall>i\<in>Basis. x \<bullet> i \<le> a \<bullet> i} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})"
immler@56188
   800
    "{x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})"
immler@56188
   801
  by auto
immler@54780
   802
immler@56188
   803
lemma open_Collect_eucl_less[simp, intro]:
immler@56188
   804
  fixes a :: "'a\<Colon>euclidean_space"
immler@54780
   805
  shows "open {x. x <e a}"
immler@56188
   806
    "open {x. a <e x}"
immler@56188
   807
  by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
immler@54780
   808
immler@56188
   809
lemma closed_Collect_eucl_le[simp, intro]:
immler@56188
   810
  fixes a :: "'a\<Colon>euclidean_space"
immler@56188
   811
  shows "closed {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i}"
immler@56188
   812
    "closed {x. \<forall>i\<in>Basis. x \<bullet> i \<le> a \<bullet> i}"
immler@56188
   813
  unfolding eucl_le_eq_halfspaces
immler@56188
   814
  by (simp_all add: closed_INT closed_Collect_le)
immler@54780
   815
immler@56188
   816
lemma image_affinity_cbox: fixes m::real
immler@56188
   817
  fixes a b c :: "'a::euclidean_space"
immler@56188
   818
  shows "(\<lambda>x. m *\<^sub>R x + c) ` cbox a b =
immler@56188
   819
    (if cbox a b = {} then {}
immler@56188
   820
     else (if 0 \<le> m then cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)
immler@56188
   821
     else cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c)))"
immler@54780
   822
proof (cases "m = 0")
immler@54780
   823
  case True
immler@54780
   824
  {
immler@54780
   825
    fix x
immler@56188
   826
    assume "\<forall>i\<in>Basis. x \<bullet> i \<le> c \<bullet> i" "\<forall>i\<in>Basis. c \<bullet> i \<le> x \<bullet> i"
immler@54780
   827
    then have "x = c"
immler@54780
   828
      apply -
immler@54780
   829
      apply (subst euclidean_eq_iff)
immler@54780
   830
      apply (auto intro: order_antisym)
immler@54780
   831
      done
immler@54780
   832
  }
immler@56188
   833
  moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
immler@56188
   834
    unfolding True by (auto simp add: cbox_sing)
immler@56188
   835
  ultimately show ?thesis using True by (auto simp: cbox_def)
immler@54780
   836
next
immler@54780
   837
  case False
immler@54780
   838
  {
immler@54780
   839
    fix y
immler@56188
   840
    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@56188
   841
    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@56188
   842
      by (auto simp: inner_distrib)
immler@54780
   843
  }
immler@54780
   844
  moreover
immler@54780
   845
  {
immler@54780
   846
    fix y
immler@56188
   847
    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@56188
   848
    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@56188
   849
      by (auto simp add: mult_left_mono_neg inner_distrib)
immler@54780
   850
  }
immler@54780
   851
  moreover
immler@54780
   852
  {
immler@54780
   853
    fix y
immler@56188
   854
    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@56188
   855
    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
immler@56188
   856
      unfolding image_iff Bex_def mem_box
immler@54780
   857
      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
immler@54780
   858
      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
immler@54780
   859
      done
immler@54780
   860
  }
immler@54780
   861
  moreover
immler@54780
   862
  {
immler@54780
   863
    fix y
immler@56188
   864
    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@56188
   865
    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
immler@56188
   866
      unfolding image_iff Bex_def mem_box
immler@54780
   867
      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
immler@54780
   868
      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
immler@54780
   869
      done
immler@54780
   870
  }
immler@56188
   871
  ultimately show ?thesis using False by (auto simp: cbox_def)
immler@54780
   872
qed
immler@54780
   873
immler@56188
   874
lemma image_smult_cbox:"(\<lambda>x. m *\<^sub>R (x::_::euclidean_space)) ` cbox a b =
immler@56188
   875
  (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@56188
   876
  using image_affinity_cbox[of m 0 a b] by auto
immler@56188
   877
immler@56188
   878
text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
immler@56188
   879
immler@56188
   880
lemma
immler@56188
   881
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@56188
   882
  shows cbox_interval: "cbox a b = {a..b}"
immler@56188
   883
    and interval_cbox: "{a..b} = cbox a b"
immler@56188
   884
    and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}"
immler@56188
   885
    and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
immler@56188
   886
    by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
immler@56188
   887
immler@56188
   888
lemma closed_eucl_atLeastAtMost[simp, intro]:
immler@56188
   889
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@56188
   890
  shows "closed {a..b}"
immler@56188
   891
  by (simp add: cbox_interval[symmetric] closed_cbox)
immler@56188
   892
immler@56188
   893
lemma closed_eucl_atMost[simp, intro]:
immler@56188
   894
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@56188
   895
  shows "closed {..a}"
immler@56188
   896
  by (simp add: eucl_le_atMost[symmetric])
immler@56188
   897
immler@56188
   898
lemma closed_eucl_atLeast[simp, intro]:
immler@56188
   899
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@56188
   900
  shows "closed {a..}"
immler@56188
   901
  by (simp add: eucl_le_atLeast[symmetric])
immler@56188
   902
immler@56188
   903
lemma image_affinity_interval: fixes m::real
immler@56188
   904
  fixes a b c :: "'a::ordered_euclidean_space"
immler@56188
   905
  shows "(\<lambda>x. m *\<^sub>R x + c) ` {a..b} =
immler@56188
   906
    (if {a..b} = {} then {}
immler@56188
   907
     else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
immler@56188
   908
     else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
immler@56188
   909
  using image_affinity_cbox[of m c a b]
immler@56188
   910
  by (simp add: cbox_interval)
immler@56188
   911
immler@56188
   912
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
immler@56188
   913
  (if {a .. b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a .. m *\<^sub>R b} else {m *\<^sub>R b .. m *\<^sub>R a})"
immler@56188
   914
  using image_smult_cbox[of m a b]
immler@56188
   915
  by (simp add: cbox_interval)
immler@54780
   916
immler@54780
   917
no_notation
immler@54780
   918
  eucl_less (infix "<e" 50)
immler@54780
   919
immler@54780
   920
end