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 \ y \ (\i\Basis. x \ i \ y \ i)" ``` immler@54780 ` 11` ``` assumes eucl_less_le_not_le: "x < y \ x \ y \ \ y \ x" ``` immler@54780 ` 12` ``` assumes eucl_inf: "inf x y = (\i\Basis. inf (x \ i) (y \ i) *\<^sub>R i)" ``` immler@54780 ` 13` ``` assumes eucl_sup: "sup x y = (\i\Basis. sup (x \ i) (y \ i) *\<^sub>R i)" ``` immler@54780 ` 14` ``` assumes eucl_Inf: "Inf X = (\i\Basis. (INF x:X. x \ i) *\<^sub>R i)" ``` immler@54780 ` 15` ``` assumes eucl_Sup: "Sup X = (\i\Basis. (SUP x:X. x \ i) *\<^sub>R i)" ``` immler@54780 ` 16` ``` assumes eucl_abs: "abs x = (\i\Basis. abs (x \ 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 \ {}" ``` immler@54780 ` 39` ``` hence "\i. (\x. x \ i) ` X \ {}" by simp ``` immler@54780 ` 40` ``` thus "(\x. x \ X \ z \ x) \ z \ Inf X" "(\x. x \ X \ x \ z) \ Sup X \ 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 \ Basis \ inf x y \ i = inf (x \ i) (y \ i)" ``` immler@54780 ` 50` ``` and inner_Basis_sup_left: "i \ Basis \ sup x y \ i = sup (x \ i) (y \ 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 \ Basis \ (INF x:X. f x) \ i = (INF x:X. f x \ i)" ``` immler@54780 ` 55` ``` and inner_Basis_SUP_left: "i \ Basis \ (SUP x:X. f x) \ i = (SUP x:X. f x \ 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 \ Basis \ abs x \ i = abs (x \ i)" ``` immler@54780 ` 59` ``` by (auto simp: eucl_abs) ``` immler@54780 ` 60` immler@54780 ` 61` ```lemma ``` immler@54780 ` 62` ``` abs_scaleR: "\a *\<^sub>R b\ = \a\ *\<^sub>R \b\" ``` 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 \ {a .. b}" "0 \ i" ``` immler@54780 ` 67` ``` shows "a\i \ x\i" "x\i \ b\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 \ a \ 0 \ b \ 0 \ a \ 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 \ b \ c \ Basis \ a \ c \ b \ c" ``` immler@54780 ` 79` ``` by (simp add: eucl_le) ``` immler@54780 ` 80` immler@54780 ` 81` ```lemma Basis_nonneg[intro, simp]: "i \ Basis \ 0 \ 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: "\b. b \ Basis \ X \ b = i b \ b" ``` immler@54781 ` 87` ``` assumes sup: "\b x. b \ Basis \ x \ s \ x \ b \ X \ b" ``` immler@54781 ` 88` ``` assumes i_s: "\b. b \ Basis \ (i b \ b) \ (\x. x \ 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: "\b. b \ Basis \ X \ b = i b \ b" ``` immler@54781 ` 96` ``` assumes sup: "\b x. b \ Basis \ x \ s \ X \ b \ x \ b" ``` immler@54781 ` 97` ``` assumes i_s: "\b. b \ Basis \ (i b \ b) \ (\x. x \ 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 \ Basis" assumes "X \ {}" "compact X" ``` immler@54781 ` 109` ``` obtains x where "x \ X" "x \ b = Inf X \ b" "\y. y \ X \ x \ b \ y \ b" ``` immler@54781 ` 110` ```proof atomize_elim ``` immler@54781 ` 111` ``` let ?proj = "(\x. x \ b) ` X" ``` immler@54781 ` 112` ``` from assms have "compact ?proj" "?proj \ {}" ``` 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\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ s \ t" ``` immler@54781 ` 117` ``` and x: "x \ X" "s = x \ b" "\y. y \ X \ x \ b \ y \ b" ``` immler@54781 ` 118` ``` by auto ``` immler@54781 ` 119` ``` hence "Inf ?proj = x \ 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 \ b = Inf X \ b" ``` haftmann@56166 ` 122` ``` by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \ 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 "\x. x \ X \ x \ b = Inf X \ b \ (\y. y \ X \ x \ b \ y \ 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 \ Basis" assumes "X \ {}" "compact X" ``` immler@54781 ` 132` ``` obtains x where "x \ X" "x \ b = Sup X \ b" "\y. y \ X \ y \ b \ x \ b" ``` immler@54781 ` 133` ```proof atomize_elim ``` immler@54781 ` 134` ``` let ?proj = "(\x. x \ b) ` X" ``` immler@54781 ` 135` ``` from assms have "compact ?proj" "?proj \ {}" ``` 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\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ t \ s" ``` immler@54781 ` 140` ``` and x: "x \ X" "s = x \ b" "\y. y \ X \ y \ b \ x \ b" ``` immler@54781 ` 141` ``` by auto ``` immler@54781 ` 142` ``` hence "Sup ?proj = x \ b" ``` haftmann@56166 ` 143` ``` by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq) ``` immler@54781 ` 144` ``` hence "x \ b = Sup X \ b" ``` haftmann@56166 ` 145` ``` by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum_delta ``` haftmann@56166 ` 146` ``` simp del: Sup_image_eq cong: if_cong) ``` immler@54781 ` 147` ``` with x show "\x. x \ X \ x \ b = Sup X \ b \ (\y. y \ X \ y \ b \ x \ b)" by blast ``` immler@54781 ` 148` ```qed ``` immler@54781 ` 149` immler@54780 ` 150` ```lemma (in order) atLeastatMost_empty'[simp]: ``` immler@54780 ` 151` ``` "(~ a <= b) \ {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 \ Basis \ fst i = 0 \ snd i \ Basis \ snd i = 0 \ fst i \ 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. \i\Basis. a\i < x\i \ x\i < b\i}" ``` immler@56188 ` 183` ``` and "cbox a b = {x::'a. \i\Basis. a\i \ x\i \ x\i \ b\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 \ box a b \ (\i\Basis. a\i < x\i \ x\i < b\i)" ``` immler@56188 ` 189` ``` and "x \ cbox a b \ (\i\Basis. a\i \ x\i \ x\i \ b\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 = {} \ (\i\Basis. b\i \ a\i))" (is ?th1) ``` immler@56188 ` 196` ``` and "(cbox a b = {} \ (\i\Basis. b\i < a\i))" (is ?th2) ``` immler@54780 ` 197` ```proof - ``` immler@54780 ` 198` ``` { ``` immler@54780 ` 199` ``` fix i x ``` immler@54780 ` 200` ``` assume i: "i\Basis" and as:"b\i \ a\i" and x:"x\box a b" ``` immler@54780 ` 201` ``` then have "a \ i < x \ i \ x \ i < b \ i" ``` immler@56188 ` 202` ``` unfolding mem_box by (auto simp: box_def) ``` immler@54780 ` 203` ``` then have "a\i < b\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: "\i\Basis. \ (b\i \ a\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 \ Basis" ``` immler@54780 ` 213` ``` have "a\i < b\i" ``` immler@54780 ` 214` ``` using as[THEN bspec[where x=i]] i by auto ``` immler@54780 ` 215` ``` then have "a\i < ((1/2) *\<^sub>R (a+b)) \ i" "((1/2) *\<^sub>R (a+b)) \ i < b\i" ``` immler@54780 ` 216` ``` by (auto simp: inner_add_left) ``` immler@54780 ` 217` ``` } ``` immler@54780 ` 218` ``` then have "box a b \ {}" ``` 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 \ Basis" and as:"b\i < a\i" and x:"x\cbox a b" ``` immler@54780 ` 226` ``` then have "a \ i \ x \ i \ x \ i \ b \ i" ``` immler@56188 ` 227` ``` unfolding mem_box by auto ``` immler@54780 ` 228` ``` then have "a\i \ b\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:"\i\Basis. \ (b\i < a\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 \ Basis" ``` immler@54780 ` 238` ``` have "a\i \ b\i" ``` immler@54780 ` 239` ``` using as[THEN bspec[where x=i]] i by auto ``` immler@54780 ` 240` ``` then have "a\i \ ((1/2) *\<^sub>R (a+b)) \ i" "((1/2) *\<^sub>R (a+b)) \ i \ b\i" ``` immler@54780 ` 241` ``` by (auto simp: inner_add_left) ``` immler@54780 ` 242` ``` } ``` immler@56188 ` 243` ``` then have "cbox a b \ {}" ``` 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 \ {} \ (\i\Basis. a\i \ b\i)" ``` immler@54780 ` 252` ``` and "box a b \ {} \ (\i\Basis. a\i < b\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 "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ cbox c d \ cbox a b" ``` immler@56188 ` 266` ``` and "(\i\Basis. a\i < c\i \ d\i < b\i) \ cbox c d \ box a b" ``` immler@56188 ` 267` ``` and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ box c d \ cbox a b" ``` immler@56188 ` 268` ``` and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ box c d \ 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 \ 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 \ cbox a b \ (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th1) ``` immler@56188 ` 281` ``` and "cbox c d \ box a b \ (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i < c\i \ d\i < b\i)" (is ?th2) ``` immler@56188 ` 282` ``` and "box c d \ cbox a b \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th3) ``` immler@54780 ` 283` ``` and "box c d \ box a b \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\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 \ cbox a b" "\i\Basis. c\i < d\i" ``` immler@54780 ` 293` ``` then have "box c d \ {}" ``` immler@56188 ` 294` ``` unfolding box_eq_empty by auto ``` immler@54780 ` 295` ``` fix i :: 'a ``` immler@54780 ` 296` ``` assume i: "i \ 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 = "(\j\Basis. (if j=i then ((min (a\j) (d\j))+c\j)/2 else (c\j+d\j)/2) *\<^sub>R j)::'a" ``` immler@54780 ` 300` ``` assume as2: "a\i > c\i" ``` immler@54780 ` 301` ``` { ``` immler@54780 ` 302` ``` fix j :: 'a ``` immler@54780 ` 303` ``` assume j: "j \ Basis" ``` immler@54780 ` 304` ``` then have "c \ j < ?x \ j \ ?x \ j < d \ 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\box c d" ``` immler@56188 ` 311` ``` using i unfolding mem_box by auto ``` immler@54780 ` 312` ``` moreover ``` immler@56188 ` 313` ``` have "?x \ 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\i \ c\i" by (rule ccontr) auto ``` immler@54780 ` 323` ``` moreover ``` immler@54780 ` 324` ``` { ``` immler@54780 ` 325` ``` let ?x = "(\j\Basis. (if j=i then ((max (b\j) (c\j))+d\j)/2 else (c\j+d\j)/2) *\<^sub>R j)::'a" ``` immler@54780 ` 326` ``` assume as2: "b\i < d\i" ``` immler@54780 ` 327` ``` { ``` immler@54780 ` 328` ``` fix j :: 'a ``` immler@54780 ` 329` ``` assume "j\Basis" ``` immler@54780 ` 330` ``` then have "d \ j > ?x \ j \ ?x \ j > c \ 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\box c d" ``` immler@56188 ` 337` ``` unfolding mem_box by auto ``` immler@54780 ` 338` ``` moreover ``` immler@56188 ` 339` ``` have "?x\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\i \ d\i" by (rule ccontr) auto ``` immler@54780 ` 349` ``` ultimately ``` immler@54780 ` 350` ``` have "a\i \ c\i \ d\i \ b\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 \ box a b" "\i\Basis. c\i < d\i" ``` immler@54780 ` 363` ``` fix i :: 'a ``` immler@54780 ` 364` ``` assume i:"i\Basis" ``` immler@56188 ` 365` ``` from as(1) have "box c d \ cbox a b" ``` immler@56188 ` 366` ``` using box_subset_cbox[of a b] by auto ``` immler@54780 ` 367` ``` then have "a\i \ c\i \ d\i \ b\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 \ cbox c d = ``` immler@56188 ` 384` ``` cbox (\i\Basis. max (a\i) (c\i) *\<^sub>R i) (\i\Basis. min (b\i) (d\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 \ cbox c d = {} \ (\i\Basis. (b\i < a\i \ d\i < c\i \ b\i < c\i \ d\i < a\i))" (is ?th1) ``` immler@56188 ` 391` ``` and "cbox a b \ box c d = {} \ (\i\Basis. (b\i < a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th2) ``` immler@56188 ` 392` ``` and "box a b \ cbox c d = {} \ (\i\Basis. (b\i \ a\i \ d\i < c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th3) ``` immler@54780 ` 393` ``` and "box a b \ box c d = {} \ (\i\Basis. (b\i \ a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th4) ``` immler@54780 ` 394` ```proof - ``` immler@54780 ` 395` ``` let ?z = "(\i\Basis. (((max (a\i) (c\i)) + (min (b\i) (d\i))) / 2) *\<^sub>R i)::'a" ``` immler@54780 ` 396` ``` have **: "\P Q. (\i :: 'a. i \ Basis \ Q ?z i \ P i) \ ``` immler@54780 ` 397` ``` (\i x :: 'a. i \ Basis \ P i \ Q x i) \ (\x. \i\Basis. Q x i) \ (\i\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 (\i\Basis. (\x. x\i) -` {a\i<..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 "(\i\Basis. (\x. x\i) -` {a\i<..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 (\i\Basis. (\x. x\i) -` {a\i .. b\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 "(\i\Basis. (\x. x\i) -` {a\i .. b\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 \ ?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 \ interior (cbox a b)" ``` immler@56188 ` 442` ``` then obtain s where s: "open s" "x \ s" "s \ cbox a b" .. ``` immler@56188 ` 443` ``` then obtain e where "e>0" and e:"\x'. dist x' x < e \ x' \ 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 \ 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 \ i \ (x - (e / 2) *\<^sub>R i) \ i" and "(x + (e / 2) *\<^sub>R i) \ i \ b \ 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 \ i < x \ i" and "x \ i < b \ 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 \ box a b" ``` immler@56188 ` 467` ``` unfolding mem_box by auto ``` immler@54780 ` 468` ``` } ``` immler@54780 ` 469` ``` then show "?L \ ?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 = "\i\Basis. \a\i\ + \b\i\" ``` immler@54780 ` 477` ``` { ``` immler@54780 ` 478` ``` fix x :: "'a" ``` immler@54780 ` 479` ``` assume x: "\i\Basis. a \ i \ x \ i \ x \ i \ b \ i" ``` immler@54780 ` 480` ``` { ``` immler@54780 ` 481` ``` fix i :: 'a ``` immler@54780 ` 482` ``` assume "i \ Basis" ``` immler@54780 ` 483` ``` then have "\x\i\ \ \a\i\ + \b\i\" ``` immler@54780 ` 484` ``` using x[THEN bspec[where x=i]] by auto ``` immler@54780 ` 485` ``` } ``` immler@54780 ` 486` ``` then have "(\i\Basis. \x \ i\) \ ?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 \ ?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) \ 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 \ UNIV \ box a b \ 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 \ {}" ``` immler@54780 ` 520` ``` shows "((1/2) *\<^sub>R (a + b)) \ box a b" ``` immler@54780 ` 521` ```proof - ``` immler@54780 ` 522` ``` { ``` immler@54780 ` 523` ``` fix i :: 'a ``` immler@54780 ` 524` ``` assume "i \ Basis" ``` immler@54780 ` 525` ``` then have "a \ i < ((1 / 2) *\<^sub>R (a + b)) \ i \ ((1 / 2) *\<^sub>R (a + b)) \ i < b \ 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 \ box a b" ``` immler@56188 ` 534` ``` and y: "y \ cbox a b" ``` immler@54780 ` 535` ``` and e: "0 < e" "e \ 1" ``` immler@54780 ` 536` ``` shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ box a b" ``` immler@54780 ` 537` ```proof - ``` immler@54780 ` 538` ``` { ``` immler@54780 ` 539` ``` fix i :: 'a ``` immler@54780 ` 540` ``` assume i: "i \ Basis" ``` immler@54780 ` 541` ``` have "a \ i = e * (a \ i) + (1 - e) * (a \ i)" ``` immler@54780 ` 542` ``` unfolding left_diff_distrib by simp ``` immler@54780 ` 543` ``` also have "\ < e * (x \ i) + (1 - e) * (y \ 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 \ i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i" ``` immler@54780 ` 553` ``` unfolding inner_simps by auto ``` immler@54780 ` 554` ``` moreover ``` immler@54780 ` 555` ``` { ``` immler@54780 ` 556` ``` have "b \ i = e * (b\i) + (1 - e) * (b\i)" ``` immler@54780 ` 557` ``` unfolding left_diff_distrib by simp ``` immler@54780 ` 558` ``` also have "\ > e * (x \ i) + (1 - e) * (y \ 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) \ i < b \ i" ``` immler@54780 ` 572` ``` unfolding inner_simps by auto ``` immler@54780 ` 573` ``` } ``` immler@54780 ` 574` ``` ultimately have "a \ i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i \ (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i < b \ 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 " {}" ``` immler@56188 ` 587` ``` shows "closure (box a b) = cbox a b" ``` immler@54780 ` 588` ```proof - ``` immler@54780 ` 589` ``` have ab: "a cbox a b" ``` immler@54780 ` 595` ``` def f \ "\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 a f n = x" and xc: "x \ ?c" ``` immler@54780 ` 599` ``` have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \ 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 (f ---> x) sequentially" ``` immler@54780 ` 613` ``` { ``` immler@54780 ` 614` ``` fix e :: real ``` immler@54780 ` 615` ``` assume "e > 0" ``` immler@54780 ` 616` ``` then have "\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 "\n\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 "\N::nat. \n\N. inverse (real n + 1) < e" by auto ``` immler@54780 ` 630` ``` } ``` immler@54780 ` 631` ``` then have "((\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 "\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 "\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 \ 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 "\a. s \ box (-a) a" ``` immler@54780 ` 653` ```proof - ``` immler@54780 ` 654` ``` obtain b where "b>0" and b: "\x\s. norm x \ b" ``` immler@54780 ` 655` ``` using assms[unfolded bounded_pos] by auto ``` immler@54780 ` 656` ``` def a \ "(\i\Basis. (b + 1) *\<^sub>R i)::'a" ``` immler@54780 ` 657` ``` { ``` immler@54780 ` 658` ``` fix x ``` immler@54780 ` 659` ``` assume "x \ s" ``` immler@54780 ` 660` ``` fix i :: 'a ``` immler@54780 ` 661` ``` assume i: "i \ Basis" ``` immler@54780 ` 662` ``` then have "(-a)\i < x\i" and "x\i < a\i" ``` immler@54780 ` 663` ``` using b[THEN bspec[where x=x], OF `x\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 \ (\a b. s \ 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 "\a. s \ cbox (-a) a" ``` immler@54780 ` 681` ```proof - ``` immler@54780 ` 682` ``` obtain a where "s \ 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 \ \a b. s \ 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 \ {}" ``` immler@56188 ` 715` ``` shows "box a b \ cbox c d = {} \ box a b \ 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 \ b \ 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) \ ``` immler@54780 ` 728` ``` (\a\s. \b\s. \x. (\i\Basis. ((a\i \ x\i \ x\i \ b\i) \ (b\i \ x\i \ x\i \ a\i))) \ x \ 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 \ s" "b \ s" ``` immler@54781 ` 748` ``` assumes "\i. i \ Basis \ a \ i \ x \ i \ x \ i \ b \ i \ b \ i \ x \ i \ x \ i \ a \ i" ``` immler@54781 ` 749` ``` shows "x \ 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 \ S" "y j \ S" ``` immler@54781 ` 756` ``` assumes "j \ Basis" ``` immler@54781 ` 757` ``` shows "(\i\Basis. (if i = j then y i \ i else x \ i) *\<^sub>R i) \ 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 "\i. i \ Basis \ x \ i \ ((\x. x \ i) ` S)" ``` immler@54781 ` 764` ``` shows "x \ S" ``` immler@54781 ` 765` ```proof - ``` immler@54781 ` 766` ``` from assms have "\i \ Basis. \s \ S. x \ i = s \ i" ``` immler@54781 ` 767` ``` by auto ``` immler@54781 ` 768` ``` with finite_Basis obtain s and bs::"'a list" where ``` immler@54781 ` 769` ``` s: "\i. i \ Basis \ x \ i = s i \ i" "\i. i \ Basis \ s i \ 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 \ Basis" "s j \ S" by blast ``` blanchet@55413 ` 773` ``` def y \ "rec_list ``` immler@54781 ` 774` ``` (s j) ``` immler@54781 ` 775` ``` (\j _ Y. (\i\Basis. (if i = j then s i \ i else Y \ i) *\<^sub>R i))" ``` immler@54781 ` 776` ``` have "x = (\i\Basis. (if i \ set bs then s i \ i else s j \ 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 = \" ``` 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 \ 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\euclidean_space" ``` immler@54780 ` 793` ``` shows "{x. x i\Basis. {x. x \ i < a \ i})" ``` immler@56188 ` 794` ``` "{x. a i\Basis. {x. a \ i < x \ 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\euclidean_space" ``` immler@56188 ` 799` ``` shows "{x. \i\Basis. x \ i \ a \ i} = (\i\Basis. {x. x \ i \ a \ i})" ``` immler@56188 ` 800` ``` "{x. \i\Basis. a \ i \ x \ i} = (\i\Basis. {x. a \ i \ x \ 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\euclidean_space" ``` immler@54780 ` 805` ``` shows "open {x. x euclidean_space" ``` immler@56188 ` 811` ``` shows "closed {x. \i\Basis. a \ i \ x \ i}" ``` immler@56188 ` 812` ``` "closed {x. \i\Basis. x \ i \ a \ 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 "(\x. m *\<^sub>R x + c) ` cbox a b = ``` immler@56188 ` 819` ``` (if cbox a b = {} then {} ``` immler@56188 ` 820` ``` else (if 0 \ 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 "\i\Basis. x \ i \ c \ i" "\i\Basis. c \ i \ x \ 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 \ 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 "\i\Basis. a \ i \ y \ i" "\i\Basis. y \ i \ b \ i" "m > 0" ``` immler@56188 ` 841` ``` then have "\i\Basis. (m *\<^sub>R a + c) \ i \ (m *\<^sub>R y + c) \ i" and "\i\Basis. (m *\<^sub>R y + c) \ i \ (m *\<^sub>R b + c) \ 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 "\i\Basis. a \ i \ y \ i" "\i\Basis. y \ i \ b \ i" "m < 0" ``` immler@56188 ` 848` ``` then have "\i\Basis. (m *\<^sub>R b + c) \ i \ (m *\<^sub>R y + c) \ i" and "\i\Basis. (m *\<^sub>R y + c) \ i \ (m *\<^sub>R a + c) \ 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 "\i\Basis. (m *\<^sub>R a + c) \ i \ y \ i" and "\i\Basis. y \ i \ (m *\<^sub>R b + c) \ i" ``` immler@56188 ` 855` ``` then have "y \ (\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 "\i\Basis. (m *\<^sub>R b + c) \ i \ y \ i" "\i\Basis. y \ i \ (m *\<^sub>R a + c) \ i" "m < 0" ``` immler@56188 ` 865` ``` then have "y \ (\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:"(\x. m *\<^sub>R (x::_::euclidean_space)) ` cbox a b = ``` immler@56188 ` 875` ``` (if cbox a b = {} then {} else if 0 \ 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\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. \i\Basis. x \ i <= a \ i} = {..a}" ``` immler@56188 ` 885` ``` and eucl_le_atLeast: "{x. \i\Basis. a \ i <= x \ 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\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\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\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 "(\x. m *\<^sub>R x + c) ` {a..b} = ``` immler@56188 ` 906` ``` (if {a..b} = {} then {} ``` immler@56188 ` 907` ``` else (if 0 \ 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:"(\x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} = ``` immler@56188 ` 913` ``` (if {a .. b} = {} then {} else if 0 \ 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 "