src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
author haftmann
Sun Mar 16 18:09:04 2014 +0100 (2014-03-16)
changeset 56166 9a241bc276cd
parent 55413 a8e96847523c
child 56188 0268784f60da
permissions -rw-r--r--
normalising simp rules for compound operators
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@54780
   178
subsection {* Intervals *}
immler@54780
   179
immler@54780
   180
lemma interval:
immler@54780
   181
  fixes a :: "'a::ordered_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@54780
   183
    and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
immler@54780
   184
  by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def)
immler@54780
   185
immler@54780
   186
lemma mem_interval:
immler@54780
   187
  fixes a :: "'a::ordered_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@54780
   189
    and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i)"
immler@54780
   190
  using interval[of a b]
immler@54780
   191
  by auto
immler@54780
   192
immler@54780
   193
lemma interval_eq_empty:
immler@54780
   194
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   195
  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
immler@54780
   196
    and "({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@54780
   202
      unfolding mem_interval by auto
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@54780
   219
      using mem_interval(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@54780
   225
    assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>{a .. b}"
immler@54780
   226
    then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
immler@54780
   227
      unfolding mem_interval 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@54780
   243
    then have "{a .. b} \<noteq> {}"
immler@54780
   244
      using mem_interval(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@54780
   249
lemma interval_ne_empty:
immler@54780
   250
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   251
  shows "{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@54780
   253
  unfolding interval_eq_empty[of a b] by fastforce+
immler@54780
   254
immler@54780
   255
lemma interval_sing:
immler@54780
   256
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   257
  shows "{a .. a} = {a}"
immler@54780
   258
    and "box a a = {}"
immler@54780
   259
  unfolding set_eq_iff mem_interval eq_iff [symmetric]
immler@54780
   260
  by (auto intro: euclidean_eqI simp: ex_in_conv)
immler@54780
   261
immler@54780
   262
lemma subset_interval_imp:
immler@54780
   263
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   264
  shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}"
immler@54780
   265
    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> box a b"
immler@54780
   266
    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> {a .. b}"
immler@54780
   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> box a b"
immler@54780
   268
  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
immler@54780
   269
  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
immler@54780
   270
immler@54780
   271
lemma interval_open_subset_closed:
immler@54780
   272
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   273
  shows "box a b \<subseteq> {a .. b}"
immler@54780
   274
  unfolding subset_eq [unfolded Ball_def] mem_interval
immler@54780
   275
  by (fast intro: less_imp_le)
immler@54780
   276
immler@54780
   277
lemma subset_interval:
immler@54780
   278
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   279
  shows "{c .. d} \<subseteq> {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@54780
   280
    and "{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@54780
   281
    and "box c d \<subseteq> {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
   282
    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
   283
proof -
immler@54780
   284
  show ?th1
immler@54780
   285
    unfolding subset_eq and Ball_def and mem_interval
immler@54780
   286
    by (auto intro: order_trans)
immler@54780
   287
  show ?th2
immler@54780
   288
    unfolding subset_eq and Ball_def and mem_interval
immler@54780
   289
    by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
immler@54780
   290
  {
immler@54780
   291
    assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
immler@54780
   292
    then have "box c d \<noteq> {}"
immler@54780
   293
      unfolding interval_eq_empty by auto
immler@54780
   294
    fix i :: 'a
immler@54780
   295
    assume i: "i \<in> Basis"
immler@54780
   296
    (** TODO combine the following two parts as done in the HOL_light version. **)
immler@54780
   297
    {
immler@54780
   298
      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
   299
      assume as2: "a\<bullet>i > c\<bullet>i"
immler@54780
   300
      {
immler@54780
   301
        fix j :: 'a
immler@54780
   302
        assume j: "j \<in> Basis"
immler@54780
   303
        then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
immler@54780
   304
          apply (cases "j = i")
immler@54780
   305
          using as(2)[THEN bspec[where x=j]] i
immler@54780
   306
          apply (auto simp add: as2)
immler@54780
   307
          done
immler@54780
   308
      }
immler@54780
   309
      then have "?x\<in>box c d"
immler@54780
   310
        using i unfolding mem_interval by auto
immler@54780
   311
      moreover
immler@54780
   312
      have "?x \<notin> {a .. b}"
immler@54780
   313
        unfolding mem_interval
immler@54780
   314
        apply auto
immler@54780
   315
        apply (rule_tac x=i in bexI)
immler@54780
   316
        using as(2)[THEN bspec[where x=i]] and as2 i
immler@54780
   317
        apply auto
immler@54780
   318
        done
immler@54780
   319
      ultimately have False using as by auto
immler@54780
   320
    }
immler@54780
   321
    then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
immler@54780
   322
    moreover
immler@54780
   323
    {
immler@54780
   324
      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
   325
      assume as2: "b\<bullet>i < d\<bullet>i"
immler@54780
   326
      {
immler@54780
   327
        fix j :: 'a
immler@54780
   328
        assume "j\<in>Basis"
immler@54780
   329
        then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
immler@54780
   330
          apply (cases "j = i")
immler@54780
   331
          using as(2)[THEN bspec[where x=j]]
immler@54780
   332
          apply (auto simp add: as2)
immler@54780
   333
          done
immler@54780
   334
      }
immler@54780
   335
      then have "?x\<in>box c d"
immler@54780
   336
        unfolding mem_interval by auto
immler@54780
   337
      moreover
immler@54780
   338
      have "?x\<notin>{a .. b}"
immler@54780
   339
        unfolding mem_interval
immler@54780
   340
        apply auto
immler@54780
   341
        apply (rule_tac x=i in bexI)
immler@54780
   342
        using as(2)[THEN bspec[where x=i]] and as2 using i
immler@54780
   343
        apply auto
immler@54780
   344
        done
immler@54780
   345
      ultimately have False using as by auto
immler@54780
   346
    }
immler@54780
   347
    then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
immler@54780
   348
    ultimately
immler@54780
   349
    have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
immler@54780
   350
  } note part1 = this
immler@54780
   351
  show ?th3
immler@54780
   352
    unfolding subset_eq and Ball_def and mem_interval
immler@54780
   353
    apply (rule, rule, rule, rule)
immler@54780
   354
    apply (rule part1)
immler@54780
   355
    unfolding subset_eq and Ball_def and mem_interval
immler@54780
   356
    prefer 4
immler@54780
   357
    apply auto
immler@54780
   358
    apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
immler@54780
   359
    done
immler@54780
   360
  {
immler@54780
   361
    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
immler@54780
   362
    fix i :: 'a
immler@54780
   363
    assume i:"i\<in>Basis"
immler@54780
   364
    from as(1) have "box c d \<subseteq> {a..b}"
immler@54780
   365
      using interval_open_subset_closed[of a b] by auto
immler@54780
   366
    then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
immler@54780
   367
      using part1 and as(2) using i by auto
immler@54780
   368
  } note * = this
immler@54780
   369
  show ?th4
immler@54780
   370
    unfolding subset_eq and Ball_def and mem_interval
immler@54780
   371
    apply (rule, rule, rule, rule)
immler@54780
   372
    apply (rule *)
immler@54780
   373
    unfolding subset_eq and Ball_def and mem_interval
immler@54780
   374
    prefer 4
immler@54780
   375
    apply auto
immler@54780
   376
    apply (erule_tac x=xa in allE, simp)+
immler@54780
   377
    done
immler@54780
   378
qed
immler@54780
   379
immler@54780
   380
lemma inter_interval:
immler@54780
   381
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   382
  shows "{a .. b} \<inter> {c .. d} =
immler@54780
   383
    {(\<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@54780
   384
  unfolding set_eq_iff and Int_iff and mem_interval
immler@54780
   385
  by auto
immler@54780
   386
immler@54780
   387
lemma disjoint_interval:
immler@54780
   388
  fixes a::"'a::ordered_euclidean_space"
immler@54780
   389
  shows "{a .. b} \<inter> {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@54780
   390
    and "{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@54780
   391
    and "box a b \<inter> {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
   392
    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
   393
proof -
immler@54780
   394
  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
   395
  have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
immler@54780
   396
      (\<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
   397
    by blast
immler@54780
   398
  note * = set_eq_iff Int_iff empty_iff mem_interval ball_conj_distrib[symmetric] eq_False ball_simps(10)
immler@54780
   399
  show ?th1 unfolding * by (intro **) auto
immler@54780
   400
  show ?th2 unfolding * by (intro **) auto
immler@54780
   401
  show ?th3 unfolding * by (intro **) auto
immler@54780
   402
  show ?th4 unfolding * by (intro **) auto
immler@54780
   403
qed
immler@54780
   404
immler@54780
   405
(* Moved interval_open_subset_closed a bit upwards *)
immler@54780
   406
immler@54780
   407
lemma open_interval[intro]:
immler@54780
   408
  fixes a b :: "'a::ordered_euclidean_space"
immler@54780
   409
  shows "open (box a b)"
immler@54780
   410
proof -
immler@54780
   411
  have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
immler@54780
   412
    by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
immler@54780
   413
      linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
immler@54780
   414
  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
immler@54780
   415
    by (auto simp add: interval)
immler@54780
   416
  finally show "open (box a b)" .
immler@54780
   417
qed
immler@54780
   418
immler@54780
   419
lemma closed_interval[intro]:
immler@54780
   420
  fixes a b :: "'a::ordered_euclidean_space"
immler@54780
   421
  shows "closed {a .. b}"
immler@54780
   422
proof -
immler@54780
   423
  have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
immler@54780
   424
    by (intro closed_INT ballI continuous_closed_vimage allI
immler@54780
   425
      linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
immler@54780
   426
  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = {a .. b}"
immler@54780
   427
    by (auto simp add: eucl_le [where 'a='a])
immler@54780
   428
  finally show "closed {a .. b}" .
immler@54780
   429
qed
immler@54780
   430
immler@54780
   431
lemma interior_closed_interval [intro]:
immler@54780
   432
  fixes a b :: "'a::ordered_euclidean_space"
immler@54780
   433
  shows "interior {a..b} = box a b" (is "?L = ?R")
immler@54780
   434
proof(rule subset_antisym)
immler@54780
   435
  show "?R \<subseteq> ?L"
immler@54780
   436
    using interval_open_subset_closed open_interval
immler@54780
   437
    by (rule interior_maximal)
immler@54780
   438
  {
immler@54780
   439
    fix x
immler@54780
   440
    assume "x \<in> interior {a..b}"
immler@54780
   441
    then obtain s where s: "open s" "x \<in> s" "s \<subseteq> {a..b}" ..
immler@54780
   442
    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}"
immler@54780
   443
      unfolding open_dist and subset_eq by auto
immler@54780
   444
    {
immler@54780
   445
      fix i :: 'a
immler@54780
   446
      assume i: "i \<in> Basis"
immler@54780
   447
      have "dist (x - (e / 2) *\<^sub>R i) x < e"
immler@54780
   448
        and "dist (x + (e / 2) *\<^sub>R i) x < e"
immler@54780
   449
        unfolding dist_norm
immler@54780
   450
        apply auto
immler@54780
   451
        unfolding norm_minus_cancel
immler@54780
   452
        using norm_Basis[OF i] `e>0`
immler@54780
   453
        apply auto
immler@54780
   454
        done
immler@54780
   455
      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
   456
        using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
immler@54780
   457
          and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
immler@54780
   458
        unfolding mem_interval
immler@54780
   459
        using i
immler@54780
   460
        by blast+
immler@54780
   461
      then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
immler@54780
   462
        using `e>0` i
immler@54780
   463
        by (auto simp: inner_diff_left inner_Basis inner_add_left)
immler@54780
   464
    }
immler@54780
   465
    then have "x \<in> box a b"
immler@54780
   466
      unfolding mem_interval by auto
immler@54780
   467
  }
immler@54780
   468
  then show "?L \<subseteq> ?R" ..
immler@54780
   469
qed
immler@54780
   470
immler@54780
   471
lemma bounded_closed_interval:
immler@54780
   472
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   473
  shows "bounded {a .. b}"
immler@54780
   474
proof -
immler@54780
   475
  let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
immler@54780
   476
  {
immler@54780
   477
    fix x :: "'a"
immler@54780
   478
    assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
immler@54780
   479
    {
immler@54780
   480
      fix i :: 'a
immler@54780
   481
      assume "i \<in> Basis"
immler@54780
   482
      then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
immler@54780
   483
        using x[THEN bspec[where x=i]] by auto
immler@54780
   484
    }
immler@54780
   485
    then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
immler@54780
   486
      apply -
immler@54780
   487
      apply (rule setsum_mono)
immler@54780
   488
      apply auto
immler@54780
   489
      done
immler@54780
   490
    then have "norm x \<le> ?b"
immler@54780
   491
      using norm_le_l1[of x] by auto
immler@54780
   492
  }
immler@54780
   493
  then show ?thesis
immler@54780
   494
    unfolding interval and bounded_iff by auto
immler@54780
   495
qed
immler@54780
   496
immler@54780
   497
lemma bounded_interval:
immler@54780
   498
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   499
  shows "bounded {a .. b} \<and> bounded (box a b)"
immler@54780
   500
  using bounded_closed_interval[of a b]
immler@54780
   501
  using interval_open_subset_closed[of a b]
immler@54780
   502
  using bounded_subset[of "{a..b}" "box a b"]
immler@54780
   503
  by simp
immler@54780
   504
immler@54780
   505
lemma not_interval_univ:
immler@54780
   506
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   507
  shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV"
immler@54780
   508
  using bounded_interval[of a b] by auto
immler@54780
   509
immler@54780
   510
lemma compact_interval:
immler@54780
   511
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   512
  shows "compact {a .. b}"
immler@54780
   513
  using bounded_closed_imp_seq_compact[of "{a..b}"] using bounded_interval[of a b]
immler@54780
   514
  by (auto simp: compact_eq_seq_compact_metric)
immler@54780
   515
immler@54780
   516
lemma open_interval_midpoint:
immler@54780
   517
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   518
  assumes "box a b \<noteq> {}"
immler@54780
   519
  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
immler@54780
   520
proof -
immler@54780
   521
  {
immler@54780
   522
    fix i :: 'a
immler@54780
   523
    assume "i \<in> Basis"
immler@54780
   524
    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@54780
   525
      using assms[unfolded interval_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
immler@54780
   526
  }
immler@54780
   527
  then show ?thesis unfolding mem_interval by auto
immler@54780
   528
qed
immler@54780
   529
immler@54780
   530
lemma open_closed_interval_convex:
immler@54780
   531
  fixes x :: "'a::ordered_euclidean_space"
immler@54780
   532
  assumes x: "x \<in> box a b"
immler@54780
   533
    and y: "y \<in> {a .. b}"
immler@54780
   534
    and e: "0 < e" "e \<le> 1"
immler@54780
   535
  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
immler@54780
   536
proof -
immler@54780
   537
  {
immler@54780
   538
    fix i :: 'a
immler@54780
   539
    assume i: "i \<in> Basis"
immler@54780
   540
    have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
immler@54780
   541
      unfolding left_diff_distrib by simp
immler@54780
   542
    also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
immler@54780
   543
      apply (rule add_less_le_mono)
immler@54780
   544
      using e unfolding mult_less_cancel_left and mult_le_cancel_left
immler@54780
   545
      apply simp_all
immler@54780
   546
      using x unfolding mem_interval using i
immler@54780
   547
      apply simp
immler@54780
   548
      using y unfolding mem_interval using i
immler@54780
   549
      apply simp
immler@54780
   550
      done
immler@54780
   551
    finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
immler@54780
   552
      unfolding inner_simps by auto
immler@54780
   553
    moreover
immler@54780
   554
    {
immler@54780
   555
      have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
immler@54780
   556
        unfolding left_diff_distrib by simp
immler@54780
   557
      also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
immler@54780
   558
        apply (rule add_less_le_mono)
immler@54780
   559
        using e unfolding mult_less_cancel_left and mult_le_cancel_left
immler@54780
   560
        apply simp_all
immler@54780
   561
        using x
immler@54780
   562
        unfolding mem_interval
immler@54780
   563
        using i
immler@54780
   564
        apply simp
immler@54780
   565
        using y
immler@54780
   566
        unfolding mem_interval
immler@54780
   567
        using i
immler@54780
   568
        apply simp
immler@54780
   569
        done
immler@54780
   570
      finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
immler@54780
   571
        unfolding inner_simps by auto
immler@54780
   572
    }
immler@54780
   573
    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
   574
      by auto
immler@54780
   575
  }
immler@54780
   576
  then show ?thesis
immler@54780
   577
    unfolding mem_interval by auto
immler@54780
   578
qed
immler@54780
   579
immler@54780
   580
notation
immler@54780
   581
  eucl_less (infix "<e" 50)
immler@54780
   582
immler@54780
   583
lemma closure_open_interval:
immler@54780
   584
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   585
  assumes "box a b \<noteq> {}"
immler@54780
   586
  shows "closure (box a b) = {a .. b}"
immler@54780
   587
proof -
immler@54780
   588
  have ab: "a <e b"
immler@54780
   589
    using assms by (simp add: eucl_less_def interval_ne_empty)
immler@54780
   590
  let ?c = "(1 / 2) *\<^sub>R (a + b)"
immler@54780
   591
  {
immler@54780
   592
    fix x
immler@54780
   593
    assume as:"x \<in> {a .. b}"
immler@54780
   594
    def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
immler@54780
   595
    {
immler@54780
   596
      fix n
immler@54780
   597
      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
immler@54780
   598
      have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
immler@54780
   599
        unfolding inverse_le_1_iff by auto
immler@54780
   600
      have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
immler@54780
   601
        x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
immler@54780
   602
        by (auto simp add: algebra_simps)
immler@54780
   603
      then have "f n <e b" and "a <e f n"
immler@54780
   604
        using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
immler@54780
   605
        unfolding f_def by (auto simp: interval eucl_less_def)
immler@54780
   606
      then have False
immler@54780
   607
        using fn unfolding f_def using xc by auto
immler@54780
   608
    }
immler@54780
   609
    moreover
immler@54780
   610
    {
immler@54780
   611
      assume "\<not> (f ---> x) sequentially"
immler@54780
   612
      {
immler@54780
   613
        fix e :: real
immler@54780
   614
        assume "e > 0"
immler@54780
   615
        then have "\<exists>N::nat. inverse (real (N + 1)) < e"
immler@54780
   616
          using real_arch_inv[of e]
immler@54780
   617
          apply (auto simp add: Suc_pred')
immler@54780
   618
          apply (rule_tac x="n - 1" in exI)
immler@54780
   619
          apply auto
immler@54780
   620
          done
immler@54780
   621
        then obtain N :: nat where "inverse (real (N + 1)) < e"
immler@54780
   622
          by auto
immler@54780
   623
        then have "\<forall>n\<ge>N. inverse (real n + 1) < e"
immler@54780
   624
          apply auto
immler@54780
   625
          apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans
immler@54780
   626
            real_of_nat_Suc real_of_nat_Suc_gt_zero)
immler@54780
   627
          done
immler@54780
   628
        then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
immler@54780
   629
      }
immler@54780
   630
      then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
immler@54780
   631
        unfolding LIMSEQ_def by(auto simp add: dist_norm)
immler@54780
   632
      then have "(f ---> x) sequentially"
immler@54780
   633
        unfolding f_def
immler@54780
   634
        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
   635
        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
   636
        by auto
immler@54780
   637
    }
immler@54780
   638
    ultimately have "x \<in> closure (box a b)"
immler@54780
   639
      using as and open_interval_midpoint[OF assms]
immler@54780
   640
      unfolding closure_def
immler@54780
   641
      unfolding islimpt_sequential
immler@54780
   642
      by (cases "x=?c") (auto simp: in_box_eucl_less)
immler@54780
   643
  }
immler@54780
   644
  then show ?thesis
immler@54780
   645
    using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
immler@54780
   646
qed
immler@54780
   647
immler@54780
   648
lemma bounded_subset_open_interval_symmetric:
immler@54780
   649
  fixes s::"('a::ordered_euclidean_space) set"
immler@54780
   650
  assumes "bounded s"
immler@54780
   651
  shows "\<exists>a. s \<subseteq> box (-a) a"
immler@54780
   652
proof -
immler@54780
   653
  obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
immler@54780
   654
    using assms[unfolded bounded_pos] by auto
immler@54780
   655
  def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a"
immler@54780
   656
  {
immler@54780
   657
    fix x
immler@54780
   658
    assume "x \<in> s"
immler@54780
   659
    fix i :: 'a
immler@54780
   660
    assume i: "i \<in> Basis"
immler@54780
   661
    then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
immler@54780
   662
      using b[THEN bspec[where x=x], OF `x\<in>s`]
immler@54780
   663
      using Basis_le_norm[OF i, of x]
immler@54780
   664
      unfolding inner_simps and a_def
immler@54780
   665
      by auto
immler@54780
   666
  }
immler@54780
   667
  then show ?thesis
immler@54780
   668
    by (auto intro: exI[where x=a] simp add: interval)
immler@54780
   669
qed
immler@54780
   670
immler@54780
   671
lemma bounded_subset_open_interval:
immler@54780
   672
  fixes s :: "('a::ordered_euclidean_space) set"
immler@54780
   673
  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
immler@54780
   674
  by (auto dest!: bounded_subset_open_interval_symmetric)
immler@54780
   675
immler@54780
   676
lemma bounded_subset_closed_interval_symmetric:
immler@54780
   677
  fixes s :: "('a::ordered_euclidean_space) set"
immler@54780
   678
  assumes "bounded s"
immler@54780
   679
  shows "\<exists>a. s \<subseteq> {-a .. a}"
immler@54780
   680
proof -
immler@54780
   681
  obtain a where "s \<subseteq> box (-a) a"
immler@54780
   682
    using bounded_subset_open_interval_symmetric[OF assms] by auto
immler@54780
   683
  then show ?thesis
immler@54780
   684
    using interval_open_subset_closed[of "-a" a] by auto
immler@54780
   685
qed
immler@54780
   686
immler@54780
   687
lemma bounded_subset_closed_interval:
immler@54780
   688
  fixes s :: "('a::ordered_euclidean_space) set"
immler@54780
   689
  shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> {a .. b}"
immler@54780
   690
  using bounded_subset_closed_interval_symmetric[of s] by auto
immler@54780
   691
immler@54780
   692
lemma frontier_closed_interval:
immler@54780
   693
  fixes a b :: "'a::ordered_euclidean_space"
immler@54780
   694
  shows "frontier {a .. b} = {a .. b} - box a b"
immler@54780
   695
  unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
immler@54780
   696
immler@54780
   697
lemma frontier_open_interval:
immler@54780
   698
  fixes a b :: "'a::ordered_euclidean_space"
immler@54780
   699
  shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)"
immler@54780
   700
proof (cases "box a b = {}")
immler@54780
   701
  case True
immler@54780
   702
  then show ?thesis
immler@54780
   703
    using frontier_empty by auto
immler@54780
   704
next
immler@54780
   705
  case False
immler@54780
   706
  then show ?thesis
immler@54780
   707
    unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval]
immler@54780
   708
    by auto
immler@54780
   709
qed
immler@54780
   710
immler@54780
   711
lemma inter_interval_mixed_eq_empty:
immler@54780
   712
  fixes a :: "'a::ordered_euclidean_space"
immler@54780
   713
  assumes "box c d \<noteq> {}"
immler@54780
   714
  shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
immler@54780
   715
  unfolding closure_open_interval[OF assms, symmetric]
immler@54780
   716
  unfolding open_inter_closure_eq_empty[OF open_interval] ..
immler@54780
   717
immler@54781
   718
lemma diameter_closed_interval:
immler@54781
   719
  fixes a b::"'a::ordered_euclidean_space"
immler@54781
   720
  shows "a \<le> b \<Longrightarrow> diameter {a..b} = dist a b"
haftmann@56166
   721
  by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
immler@54781
   722
     simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm)
immler@54781
   723
immler@54780
   724
text {* Intervals in general, including infinite and mixtures of open and closed. *}
immler@54780
   725
immler@54780
   726
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
immler@54780
   727
  (\<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
   728
immler@54780
   729
lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
immler@54780
   730
  "is_interval (box a b)" (is ?th2) proof -
immler@54780
   731
  show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
immler@54780
   732
    by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
immler@54780
   733
immler@54780
   734
lemma is_interval_empty:
immler@54780
   735
 "is_interval {}"
immler@54780
   736
  unfolding is_interval_def
immler@54780
   737
  by simp
immler@54780
   738
immler@54780
   739
lemma is_interval_univ:
immler@54780
   740
 "is_interval UNIV"
immler@54780
   741
  unfolding is_interval_def
immler@54780
   742
  by simp
immler@54780
   743
immler@54781
   744
lemma mem_is_intervalI:
immler@54781
   745
  assumes "is_interval s"
immler@54781
   746
  assumes "a \<in> s" "b \<in> s"
immler@54781
   747
  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
   748
  shows "x \<in> s"
immler@54781
   749
  by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
immler@54781
   750
immler@54781
   751
lemma interval_subst:
immler@54781
   752
  fixes S::"'a::ordered_euclidean_space set"
immler@54781
   753
  assumes "is_interval S"
immler@54781
   754
  assumes "x \<in> S" "y j \<in> S"
immler@54781
   755
  assumes "j \<in> Basis"
immler@54781
   756
  shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
immler@54781
   757
  by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
immler@54781
   758
immler@54781
   759
lemma mem_interval_componentwiseI:
immler@54781
   760
  fixes S::"'a::ordered_euclidean_space set"
immler@54781
   761
  assumes "is_interval S"
immler@54781
   762
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
immler@54781
   763
  shows "x \<in> S"
immler@54781
   764
proof -
immler@54781
   765
  from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
immler@54781
   766
    by auto
immler@54781
   767
  with finite_Basis obtain s and bs::"'a list" where
immler@54781
   768
    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
   769
    bs: "set bs = Basis" "distinct bs"
immler@54781
   770
    by (metis finite_distinct_list)
immler@54781
   771
  from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" by blast
blanchet@55413
   772
  def y \<equiv> "rec_list
immler@54781
   773
    (s j)
immler@54781
   774
    (\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
immler@54781
   775
  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
   776
    using bs by (auto simp add: s(1)[symmetric] euclidean_representation)
immler@54781
   777
  also have [symmetric]: "y bs = \<dots>"
immler@54781
   778
    using bs(2) bs(1)[THEN equalityD1]
immler@54781
   779
    by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
immler@54781
   780
  also have "y bs \<in> S"
immler@54781
   781
    using bs(1)[THEN equalityD1]
immler@54781
   782
    apply (induct bs)
immler@54781
   783
    apply (auto simp: y_def j)
immler@54781
   784
    apply (rule interval_subst[OF assms(1)])
immler@54781
   785
    apply (auto simp: s)
immler@54781
   786
    done
immler@54781
   787
  finally show ?thesis .
immler@54781
   788
qed
immler@54781
   789
immler@54780
   790
text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
immler@54780
   791
immler@54780
   792
lemma eucl_lessThan_eq_halfspaces:
immler@54780
   793
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@54780
   794
  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
immler@54780
   795
  by (auto simp: eucl_less_def)
immler@54780
   796
immler@54780
   797
lemma eucl_greaterThan_eq_halfspaces:
immler@54780
   798
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@54780
   799
  shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
immler@54780
   800
  by (auto simp: eucl_less_def)
immler@54780
   801
immler@54780
   802
lemma eucl_atMost_eq_halfspaces:
immler@54780
   803
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@54780
   804
  shows "{.. a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})"
immler@54780
   805
  by (auto simp: eucl_le[where 'a='a])
immler@54780
   806
immler@54780
   807
lemma eucl_atLeast_eq_halfspaces:
immler@54780
   808
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@54780
   809
  shows "{a ..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})"
immler@54780
   810
  by (auto simp: eucl_le[where 'a='a])
immler@54780
   811
immler@54780
   812
lemma open_eucl_lessThan[simp, intro]:
immler@54780
   813
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@54780
   814
  shows "open {x. x <e a}"
immler@54780
   815
  by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt)
immler@54780
   816
immler@54780
   817
lemma open_eucl_greaterThan[simp, intro]:
immler@54780
   818
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@54780
   819
  shows "open {x. a <e x}"
immler@54780
   820
  by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt)
immler@54780
   821
immler@54780
   822
lemma closed_eucl_atMost[simp, intro]:
immler@54780
   823
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@54780
   824
  shows "closed {.. a}"
immler@54780
   825
  unfolding eucl_atMost_eq_halfspaces
immler@54780
   826
  by (simp add: closed_INT closed_Collect_le)
immler@54780
   827
immler@54780
   828
lemma closed_eucl_atLeast[simp, intro]:
immler@54780
   829
  fixes a :: "'a\<Colon>ordered_euclidean_space"
immler@54780
   830
  shows "closed {a ..}"
immler@54780
   831
  unfolding eucl_atLeast_eq_halfspaces
immler@54780
   832
  by (simp add: closed_INT closed_Collect_le)
immler@54780
   833
immler@54780
   834
immler@54780
   835
lemma image_affinity_interval: fixes m::real
immler@54780
   836
  fixes a b c :: "'a::ordered_euclidean_space"
immler@54780
   837
  shows "(\<lambda>x. m *\<^sub>R x + c) ` {a .. b} =
immler@54780
   838
    (if {a .. b} = {} then {}
immler@54780
   839
     else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
immler@54780
   840
     else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
immler@54780
   841
proof (cases "m = 0")
immler@54780
   842
  case True
immler@54780
   843
  {
immler@54780
   844
    fix x
immler@54780
   845
    assume "x \<le> c" "c \<le> x"
immler@54780
   846
    then have "x = c"
immler@54780
   847
      unfolding eucl_le[where 'a='a]
immler@54780
   848
      apply -
immler@54780
   849
      apply (subst euclidean_eq_iff)
immler@54780
   850
      apply (auto intro: order_antisym)
immler@54780
   851
      done
immler@54780
   852
  }
immler@54780
   853
  moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}"
immler@54780
   854
    unfolding True by (auto simp add: eucl_le[where 'a='a])
immler@54780
   855
  ultimately show ?thesis using True by auto
immler@54780
   856
next
immler@54780
   857
  case False
immler@54780
   858
  {
immler@54780
   859
    fix y
immler@54780
   860
    assume "a \<le> y" "y \<le> b" "m > 0"
immler@54780
   861
    then have "m *\<^sub>R a + c \<le> m *\<^sub>R y + c" and "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
immler@54780
   862
      unfolding eucl_le[where 'a='a] by (auto simp: inner_distrib)
immler@54780
   863
  }
immler@54780
   864
  moreover
immler@54780
   865
  {
immler@54780
   866
    fix y
immler@54780
   867
    assume "a \<le> y" "y \<le> b" "m < 0"
immler@54780
   868
    then have "m *\<^sub>R b + c \<le> m *\<^sub>R y + c" and "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
immler@54780
   869
      unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_distrib)
immler@54780
   870
  }
immler@54780
   871
  moreover
immler@54780
   872
  {
immler@54780
   873
    fix y
immler@54780
   874
    assume "m > 0" and "m *\<^sub>R a + c \<le> y" and "y \<le> m *\<^sub>R b + c"
immler@54780
   875
    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
immler@54780
   876
      unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
immler@54780
   877
      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
immler@54780
   878
      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
immler@54780
   879
      done
immler@54780
   880
  }
immler@54780
   881
  moreover
immler@54780
   882
  {
immler@54780
   883
    fix y
immler@54780
   884
    assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
immler@54780
   885
    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
immler@54780
   886
      unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
immler@54780
   887
      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
immler@54780
   888
      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
immler@54780
   889
      done
immler@54780
   890
  }
immler@54780
   891
  ultimately show ?thesis using False by auto
immler@54780
   892
qed
immler@54780
   893
immler@54780
   894
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a..b} =
immler@54780
   895
  (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@54780
   896
  using image_affinity_interval[of m 0 a b] by auto
immler@54780
   897
immler@54780
   898
no_notation
immler@54780
   899
  eucl_less (infix "<e" 50)
immler@54780
   900
immler@54780
   901
end