summarized notions related to ordered_euclidean_space and intervals in separate theory
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
@@ -7,7 +7,7 @@
theory Convex_Euclidean_Space
imports
- Topology_Euclidean_Space
+ Ordered_Euclidean_Space
"~~/src/HOL/Library/Convex"
"~~/src/HOL/Library/Set_Algebras"
begin
@@ -343,11 +343,6 @@
lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)"
by auto
-lemma image_smult_interval:
- "(\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space)) ` {a..b} =
- (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})"
- using image_affinity_interval[of m 0 a b] by auto
-
lemma dist_triangle_eq:
fixes x y z :: "'a::real_inner"
shows "dist x z = dist x y + dist y z \<longleftrightarrow>
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Dec 16 17:08:22 2013 +0100
@@ -8,7 +8,6 @@
imports
Euclidean_Space
"~~/src/HOL/Library/Infinite_Set"
- "~~/src/HOL/Library/Product_Order"
begin
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
@@ -3109,110 +3108,5 @@
apply simp
done
-
-subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
-
-class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
- assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
- assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
- assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
- assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
- assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
- assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
- assumes eucl_abs: "abs x = (\<Sum>i\<in>Basis. abs (x \<bullet> i) *\<^sub>R i)"
-begin
-
-subclass order
- by default
- (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
-
-subclass ordered_ab_group_add_abs
- by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
-
-subclass ordered_real_vector
- by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
-
-subclass lattice
- by default (auto simp: eucl_inf eucl_sup eucl_le)
-
-subclass distrib_lattice
- by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
-
-subclass conditionally_complete_lattice
-proof
- fix z::'a and X::"'a set"
- assume "X \<noteq> {}"
- hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
- 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"
- by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
- intro!: cInf_greatest cSup_least)
-qed (force intro!: cInf_lower cSup_upper
- simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
- eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def)+
-
-lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
- and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
- by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib setsum_delta
- cong: if_cong)
-
-lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
- and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
- by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf)
-
-lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
- by (auto simp: eucl_abs)
-
-lemma
- abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
- by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
-
-lemma interval_inner_leI:
- assumes "x \<in> {a .. b}" "0 \<le> i"
- shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
- using assms
- unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
- by (auto intro!: setsum_mono mult_right_mono simp: eucl_le)
-
-lemma inner_nonneg_nonneg:
- shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
- using interval_inner_leI[of a 0 a b]
- by auto
-
-lemma inner_Basis_mono:
- shows "a \<le> b \<Longrightarrow> c \<in> Basis \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
- by (simp add: eucl_le)
-
-lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
- by (auto simp: eucl_le inner_Basis)
-
end
-lemma (in order) atLeastatMost_empty'[simp]:
- "(~ a <= b) \<Longrightarrow> {a..b} = {}"
- by (auto)
-
-instance real :: ordered_euclidean_space
- by default (auto simp: INF_def SUP_def)
-
-lemma in_Basis_prod_iff:
- fixes i::"'a::euclidean_space*'b::euclidean_space"
- shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
- by (cases i) (auto simp: Basis_prod_def)
-
-instantiation prod::(abs, abs) abs
-begin
-
-definition "abs x = (abs (fst x), abs (snd x))"
-
-instance proof qed
-end
-
-instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
- by default
- (auto intro!: add_mono simp add: euclidean_representation_setsum' Ball_def inner_prod_def
- in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
- inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
- eucl_le[where 'a='b] abs_prod_def abs_inner)
-
-end
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
@@ -0,0 +1,783 @@
+theory Ordered_Euclidean_Space
+imports
+ Topology_Euclidean_Space
+ "~~/src/HOL/Library/Product_Order"
+begin
+
+subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
+
+class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
+ assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
+ assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+ assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
+ assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
+ assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
+ assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
+ assumes eucl_abs: "abs x = (\<Sum>i\<in>Basis. abs (x \<bullet> i) *\<^sub>R i)"
+begin
+
+subclass order
+ by default
+ (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
+
+subclass ordered_ab_group_add_abs
+ by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
+
+subclass ordered_real_vector
+ by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
+
+subclass lattice
+ by default (auto simp: eucl_inf eucl_sup eucl_le)
+
+subclass distrib_lattice
+ by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
+
+subclass conditionally_complete_lattice
+proof
+ fix z::'a and X::"'a set"
+ assume "X \<noteq> {}"
+ hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
+ 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"
+ by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
+ intro!: cInf_greatest cSup_least)
+qed (force intro!: cInf_lower cSup_upper
+ simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
+ eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def)+
+
+lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
+ and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
+ by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib setsum_delta
+ cong: if_cong)
+
+lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
+ and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
+ by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf)
+
+lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
+ by (auto simp: eucl_abs)
+
+lemma
+ abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
+ by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
+
+lemma interval_inner_leI:
+ assumes "x \<in> {a .. b}" "0 \<le> i"
+ shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
+ using assms
+ unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
+ by (auto intro!: setsum_mono mult_right_mono simp: eucl_le)
+
+lemma inner_nonneg_nonneg:
+ shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
+ using interval_inner_leI[of a 0 a b]
+ by auto
+
+lemma inner_Basis_mono:
+ shows "a \<le> b \<Longrightarrow> c \<in> Basis \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
+ by (simp add: eucl_le)
+
+lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
+ by (auto simp: eucl_le inner_Basis)
+
+end
+
+lemma (in order) atLeastatMost_empty'[simp]:
+ "(~ a <= b) \<Longrightarrow> {a..b} = {}"
+ by (auto)
+
+instance real :: ordered_euclidean_space
+ by default (auto simp: INF_def SUP_def)
+
+lemma in_Basis_prod_iff:
+ fixes i::"'a::euclidean_space*'b::euclidean_space"
+ shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
+ by (cases i) (auto simp: Basis_prod_def)
+
+instantiation prod::(abs, abs) abs
+begin
+
+definition "abs x = (abs (fst x), abs (snd x))"
+
+instance proof qed
+end
+
+instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
+ by default
+ (auto intro!: add_mono simp add: euclidean_representation_setsum' Ball_def inner_prod_def
+ in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
+ inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
+ eucl_le[where 'a='b] abs_prod_def abs_inner)
+
+
+subsection {* Intervals *}
+
+lemma interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
+ and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
+ by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def)
+
+lemma mem_interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
+ 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)"
+ using interval[of a b]
+ by auto
+
+lemma interval_eq_empty:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
+ and "({a .. b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
+proof -
+ {
+ fix i x
+ assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
+ then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
+ unfolding mem_interval by auto
+ then have "a\<bullet>i < b\<bullet>i" by auto
+ then have False using as by auto
+ }
+ moreover
+ {
+ assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
+ let ?x = "(1/2) *\<^sub>R (a + b)"
+ {
+ fix i :: 'a
+ assume i: "i \<in> Basis"
+ have "a\<bullet>i < b\<bullet>i"
+ using as[THEN bspec[where x=i]] i by auto
+ then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
+ by (auto simp: inner_add_left)
+ }
+ then have "box a b \<noteq> {}"
+ using mem_interval(1)[of "?x" a b] by auto
+ }
+ ultimately show ?th1 by blast
+
+ {
+ fix i x
+ assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>{a .. b}"
+ then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
+ unfolding mem_interval by auto
+ then have "a\<bullet>i \<le> b\<bullet>i" by auto
+ then have False using as by auto
+ }
+ moreover
+ {
+ assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
+ let ?x = "(1/2) *\<^sub>R (a + b)"
+ {
+ fix i :: 'a
+ assume i:"i \<in> Basis"
+ have "a\<bullet>i \<le> b\<bullet>i"
+ using as[THEN bspec[where x=i]] i by auto
+ 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"
+ by (auto simp: inner_add_left)
+ }
+ then have "{a .. b} \<noteq> {}"
+ using mem_interval(2)[of "?x" a b] by auto
+ }
+ ultimately show ?th2 by blast
+qed
+
+lemma interval_ne_empty:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
+ and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
+ unfolding interval_eq_empty[of a b] by fastforce+
+
+lemma interval_sing:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "{a .. a} = {a}"
+ and "box a a = {}"
+ unfolding set_eq_iff mem_interval eq_iff [symmetric]
+ by (auto intro: euclidean_eqI simp: ex_in_conv)
+
+lemma subset_interval_imp:
+ fixes a :: "'a::ordered_euclidean_space"
+ 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}"
+ 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"
+ 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}"
+ 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"
+ unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
+ by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
+
+lemma interval_open_subset_closed:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "box a b \<subseteq> {a .. b}"
+ unfolding subset_eq [unfolded Ball_def] mem_interval
+ by (fast intro: less_imp_le)
+
+lemma subset_interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ 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)
+ 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)
+ 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)
+ 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)
+proof -
+ show ?th1
+ unfolding subset_eq and Ball_def and mem_interval
+ by (auto intro: order_trans)
+ show ?th2
+ unfolding subset_eq and Ball_def and mem_interval
+ by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
+ {
+ assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
+ then have "box c d \<noteq> {}"
+ unfolding interval_eq_empty by auto
+ fix i :: 'a
+ assume i: "i \<in> Basis"
+ (** TODO combine the following two parts as done in the HOL_light version. **)
+ {
+ 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"
+ assume as2: "a\<bullet>i > c\<bullet>i"
+ {
+ fix j :: 'a
+ assume j: "j \<in> Basis"
+ then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
+ apply (cases "j = i")
+ using as(2)[THEN bspec[where x=j]] i
+ apply (auto simp add: as2)
+ done
+ }
+ then have "?x\<in>box c d"
+ using i unfolding mem_interval by auto
+ moreover
+ have "?x \<notin> {a .. b}"
+ unfolding mem_interval
+ apply auto
+ apply (rule_tac x=i in bexI)
+ using as(2)[THEN bspec[where x=i]] and as2 i
+ apply auto
+ done
+ ultimately have False using as by auto
+ }
+ then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
+ moreover
+ {
+ 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"
+ assume as2: "b\<bullet>i < d\<bullet>i"
+ {
+ fix j :: 'a
+ assume "j\<in>Basis"
+ then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
+ apply (cases "j = i")
+ using as(2)[THEN bspec[where x=j]]
+ apply (auto simp add: as2)
+ done
+ }
+ then have "?x\<in>box c d"
+ unfolding mem_interval by auto
+ moreover
+ have "?x\<notin>{a .. b}"
+ unfolding mem_interval
+ apply auto
+ apply (rule_tac x=i in bexI)
+ using as(2)[THEN bspec[where x=i]] and as2 using i
+ apply auto
+ done
+ ultimately have False using as by auto
+ }
+ then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
+ ultimately
+ have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
+ } note part1 = this
+ show ?th3
+ unfolding subset_eq and Ball_def and mem_interval
+ apply (rule, rule, rule, rule)
+ apply (rule part1)
+ unfolding subset_eq and Ball_def and mem_interval
+ prefer 4
+ apply auto
+ apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
+ done
+ {
+ assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
+ fix i :: 'a
+ assume i:"i\<in>Basis"
+ from as(1) have "box c d \<subseteq> {a..b}"
+ using interval_open_subset_closed[of a b] by auto
+ then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
+ using part1 and as(2) using i by auto
+ } note * = this
+ show ?th4
+ unfolding subset_eq and Ball_def and mem_interval
+ apply (rule, rule, rule, rule)
+ apply (rule *)
+ unfolding subset_eq and Ball_def and mem_interval
+ prefer 4
+ apply auto
+ apply (erule_tac x=xa in allE, simp)+
+ done
+qed
+
+lemma inter_interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "{a .. b} \<inter> {c .. d} =
+ {(\<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)}"
+ unfolding set_eq_iff and Int_iff and mem_interval
+ by auto
+
+lemma disjoint_interval:
+ fixes a::"'a::ordered_euclidean_space"
+ 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)
+ 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)
+ 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)
+ 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)
+proof -
+ 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"
+ have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
+ (\<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)"
+ by blast
+ note * = set_eq_iff Int_iff empty_iff mem_interval ball_conj_distrib[symmetric] eq_False ball_simps(10)
+ show ?th1 unfolding * by (intro **) auto
+ show ?th2 unfolding * by (intro **) auto
+ show ?th3 unfolding * by (intro **) auto
+ show ?th4 unfolding * by (intro **) auto
+qed
+
+(* Moved interval_open_subset_closed a bit upwards *)
+
+lemma open_interval[intro]:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "open (box a b)"
+proof -
+ have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
+ by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
+ linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
+ also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
+ by (auto simp add: interval)
+ finally show "open (box a b)" .
+qed
+
+lemma closed_interval[intro]:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "closed {a .. b}"
+proof -
+ have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
+ by (intro closed_INT ballI continuous_closed_vimage allI
+ linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
+ also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = {a .. b}"
+ by (auto simp add: eucl_le [where 'a='a])
+ finally show "closed {a .. b}" .
+qed
+
+lemma interior_closed_interval [intro]:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "interior {a..b} = box a b" (is "?L = ?R")
+proof(rule subset_antisym)
+ show "?R \<subseteq> ?L"
+ using interval_open_subset_closed open_interval
+ by (rule interior_maximal)
+ {
+ fix x
+ assume "x \<in> interior {a..b}"
+ then obtain s where s: "open s" "x \<in> s" "s \<subseteq> {a..b}" ..
+ then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}"
+ unfolding open_dist and subset_eq by auto
+ {
+ fix i :: 'a
+ assume i: "i \<in> Basis"
+ have "dist (x - (e / 2) *\<^sub>R i) x < e"
+ and "dist (x + (e / 2) *\<^sub>R i) x < e"
+ unfolding dist_norm
+ apply auto
+ unfolding norm_minus_cancel
+ using norm_Basis[OF i] `e>0`
+ apply auto
+ done
+ 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"
+ using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
+ and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
+ unfolding mem_interval
+ using i
+ by blast+
+ then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
+ using `e>0` i
+ by (auto simp: inner_diff_left inner_Basis inner_add_left)
+ }
+ then have "x \<in> box a b"
+ unfolding mem_interval by auto
+ }
+ then show "?L \<subseteq> ?R" ..
+qed
+
+lemma bounded_closed_interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "bounded {a .. b}"
+proof -
+ let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
+ {
+ fix x :: "'a"
+ assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
+ {
+ fix i :: 'a
+ assume "i \<in> Basis"
+ then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
+ using x[THEN bspec[where x=i]] by auto
+ }
+ then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
+ apply -
+ apply (rule setsum_mono)
+ apply auto
+ done
+ then have "norm x \<le> ?b"
+ using norm_le_l1[of x] by auto
+ }
+ then show ?thesis
+ unfolding interval and bounded_iff by auto
+qed
+
+lemma bounded_interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "bounded {a .. b} \<and> bounded (box a b)"
+ using bounded_closed_interval[of a b]
+ using interval_open_subset_closed[of a b]
+ using bounded_subset[of "{a..b}" "box a b"]
+ by simp
+
+lemma not_interval_univ:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV"
+ using bounded_interval[of a b] by auto
+
+lemma compact_interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "compact {a .. b}"
+ using bounded_closed_imp_seq_compact[of "{a..b}"] using bounded_interval[of a b]
+ by (auto simp: compact_eq_seq_compact_metric)
+
+lemma open_interval_midpoint:
+ fixes a :: "'a::ordered_euclidean_space"
+ assumes "box a b \<noteq> {}"
+ shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
+proof -
+ {
+ fix i :: 'a
+ assume "i \<in> Basis"
+ 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"
+ using assms[unfolded interval_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
+ }
+ then show ?thesis unfolding mem_interval by auto
+qed
+
+lemma open_closed_interval_convex:
+ fixes x :: "'a::ordered_euclidean_space"
+ assumes x: "x \<in> box a b"
+ and y: "y \<in> {a .. b}"
+ and e: "0 < e" "e \<le> 1"
+ shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
+proof -
+ {
+ fix i :: 'a
+ assume i: "i \<in> Basis"
+ have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
+ unfolding left_diff_distrib by simp
+ also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
+ apply (rule add_less_le_mono)
+ using e unfolding mult_less_cancel_left and mult_le_cancel_left
+ apply simp_all
+ using x unfolding mem_interval using i
+ apply simp
+ using y unfolding mem_interval using i
+ apply simp
+ done
+ finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
+ unfolding inner_simps by auto
+ moreover
+ {
+ have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
+ unfolding left_diff_distrib by simp
+ also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
+ apply (rule add_less_le_mono)
+ using e unfolding mult_less_cancel_left and mult_le_cancel_left
+ apply simp_all
+ using x
+ unfolding mem_interval
+ using i
+ apply simp
+ using y
+ unfolding mem_interval
+ using i
+ apply simp
+ done
+ finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
+ unfolding inner_simps by auto
+ }
+ 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"
+ by auto
+ }
+ then show ?thesis
+ unfolding mem_interval by auto
+qed
+
+notation
+ eucl_less (infix "<e" 50)
+
+lemma closure_open_interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ assumes "box a b \<noteq> {}"
+ shows "closure (box a b) = {a .. b}"
+proof -
+ have ab: "a <e b"
+ using assms by (simp add: eucl_less_def interval_ne_empty)
+ let ?c = "(1 / 2) *\<^sub>R (a + b)"
+ {
+ fix x
+ assume as:"x \<in> {a .. b}"
+ def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
+ {
+ fix n
+ assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
+ have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
+ unfolding inverse_le_1_iff by auto
+ have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
+ x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
+ by (auto simp add: algebra_simps)
+ then have "f n <e b" and "a <e f n"
+ using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
+ unfolding f_def by (auto simp: interval eucl_less_def)
+ then have False
+ using fn unfolding f_def using xc by auto
+ }
+ moreover
+ {
+ assume "\<not> (f ---> x) sequentially"
+ {
+ fix e :: real
+ assume "e > 0"
+ then have "\<exists>N::nat. inverse (real (N + 1)) < e"
+ using real_arch_inv[of e]
+ apply (auto simp add: Suc_pred')
+ apply (rule_tac x="n - 1" in exI)
+ apply auto
+ done
+ then obtain N :: nat where "inverse (real (N + 1)) < e"
+ by auto
+ then have "\<forall>n\<ge>N. inverse (real n + 1) < e"
+ apply auto
+ apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans
+ real_of_nat_Suc real_of_nat_Suc_gt_zero)
+ done
+ then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
+ }
+ then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
+ unfolding LIMSEQ_def by(auto simp add: dist_norm)
+ then have "(f ---> x) sequentially"
+ unfolding f_def
+ 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]
+ using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
+ by auto
+ }
+ ultimately have "x \<in> closure (box a b)"
+ using as and open_interval_midpoint[OF assms]
+ unfolding closure_def
+ unfolding islimpt_sequential
+ by (cases "x=?c") (auto simp: in_box_eucl_less)
+ }
+ then show ?thesis
+ using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
+qed
+
+lemma bounded_subset_open_interval_symmetric:
+ fixes s::"('a::ordered_euclidean_space) set"
+ assumes "bounded s"
+ shows "\<exists>a. s \<subseteq> box (-a) a"
+proof -
+ obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
+ using assms[unfolded bounded_pos] by auto
+ def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a"
+ {
+ fix x
+ assume "x \<in> s"
+ fix i :: 'a
+ assume i: "i \<in> Basis"
+ then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
+ using b[THEN bspec[where x=x], OF `x\<in>s`]
+ using Basis_le_norm[OF i, of x]
+ unfolding inner_simps and a_def
+ by auto
+ }
+ then show ?thesis
+ by (auto intro: exI[where x=a] simp add: interval)
+qed
+
+lemma bounded_subset_open_interval:
+ fixes s :: "('a::ordered_euclidean_space) set"
+ shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
+ by (auto dest!: bounded_subset_open_interval_symmetric)
+
+lemma bounded_subset_closed_interval_symmetric:
+ fixes s :: "('a::ordered_euclidean_space) set"
+ assumes "bounded s"
+ shows "\<exists>a. s \<subseteq> {-a .. a}"
+proof -
+ obtain a where "s \<subseteq> box (-a) a"
+ using bounded_subset_open_interval_symmetric[OF assms] by auto
+ then show ?thesis
+ using interval_open_subset_closed[of "-a" a] by auto
+qed
+
+lemma bounded_subset_closed_interval:
+ fixes s :: "('a::ordered_euclidean_space) set"
+ shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> {a .. b}"
+ using bounded_subset_closed_interval_symmetric[of s] by auto
+
+lemma frontier_closed_interval:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "frontier {a .. b} = {a .. b} - box a b"
+ unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
+
+lemma frontier_open_interval:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)"
+proof (cases "box a b = {}")
+ case True
+ then show ?thesis
+ using frontier_empty by auto
+next
+ case False
+ then show ?thesis
+ unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval]
+ by auto
+qed
+
+lemma inter_interval_mixed_eq_empty:
+ fixes a :: "'a::ordered_euclidean_space"
+ assumes "box c d \<noteq> {}"
+ shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
+ unfolding closure_open_interval[OF assms, symmetric]
+ unfolding open_inter_closure_eq_empty[OF open_interval] ..
+
+text {* Intervals in general, including infinite and mixtures of open and closed. *}
+
+definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
+ (\<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)"
+
+lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
+ "is_interval (box a b)" (is ?th2) proof -
+ show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
+ by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
+
+lemma is_interval_empty:
+ "is_interval {}"
+ unfolding is_interval_def
+ by simp
+
+lemma is_interval_univ:
+ "is_interval UNIV"
+ unfolding is_interval_def
+ by simp
+
+text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
+
+lemma eucl_lessThan_eq_halfspaces:
+ fixes a :: "'a\<Colon>ordered_euclidean_space"
+ shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
+ by (auto simp: eucl_less_def)
+
+lemma eucl_greaterThan_eq_halfspaces:
+ fixes a :: "'a\<Colon>ordered_euclidean_space"
+ shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
+ by (auto simp: eucl_less_def)
+
+lemma eucl_atMost_eq_halfspaces:
+ fixes a :: "'a\<Colon>ordered_euclidean_space"
+ shows "{.. a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})"
+ by (auto simp: eucl_le[where 'a='a])
+
+lemma eucl_atLeast_eq_halfspaces:
+ fixes a :: "'a\<Colon>ordered_euclidean_space"
+ shows "{a ..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})"
+ by (auto simp: eucl_le[where 'a='a])
+
+lemma open_eucl_lessThan[simp, intro]:
+ fixes a :: "'a\<Colon>ordered_euclidean_space"
+ shows "open {x. x <e a}"
+ by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt)
+
+lemma open_eucl_greaterThan[simp, intro]:
+ fixes a :: "'a\<Colon>ordered_euclidean_space"
+ shows "open {x. a <e x}"
+ by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt)
+
+lemma closed_eucl_atMost[simp, intro]:
+ fixes a :: "'a\<Colon>ordered_euclidean_space"
+ shows "closed {.. a}"
+ unfolding eucl_atMost_eq_halfspaces
+ by (simp add: closed_INT closed_Collect_le)
+
+lemma closed_eucl_atLeast[simp, intro]:
+ fixes a :: "'a\<Colon>ordered_euclidean_space"
+ shows "closed {a ..}"
+ unfolding eucl_atLeast_eq_halfspaces
+ by (simp add: closed_INT closed_Collect_le)
+
+
+lemma image_affinity_interval: fixes m::real
+ fixes a b c :: "'a::ordered_euclidean_space"
+ shows "(\<lambda>x. m *\<^sub>R x + c) ` {a .. b} =
+ (if {a .. b} = {} then {}
+ else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
+ else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
+proof (cases "m = 0")
+ case True
+ {
+ fix x
+ assume "x \<le> c" "c \<le> x"
+ then have "x = c"
+ unfolding eucl_le[where 'a='a]
+ apply -
+ apply (subst euclidean_eq_iff)
+ apply (auto intro: order_antisym)
+ done
+ }
+ moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}"
+ unfolding True by (auto simp add: eucl_le[where 'a='a])
+ ultimately show ?thesis using True by auto
+next
+ case False
+ {
+ fix y
+ assume "a \<le> y" "y \<le> b" "m > 0"
+ 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"
+ unfolding eucl_le[where 'a='a] by (auto simp: inner_distrib)
+ }
+ moreover
+ {
+ fix y
+ assume "a \<le> y" "y \<le> b" "m < 0"
+ 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"
+ unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_distrib)
+ }
+ moreover
+ {
+ fix y
+ assume "m > 0" and "m *\<^sub>R a + c \<le> y" and "y \<le> m *\<^sub>R b + c"
+ then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
+ unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
+ done
+ }
+ moreover
+ {
+ fix y
+ assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
+ then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
+ unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
+ done
+ }
+ ultimately show ?thesis using False by auto
+qed
+
+lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a..b} =
+ (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})"
+ using image_affinity_interval[of m 0 a b] by auto
+
+no_notation
+ eucl_less (infix "<e" 50)
+
+end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
@@ -5993,544 +5993,8 @@
done
qed
-
subsection {* Intervals *}
-lemma interval:
- fixes a :: "'a::ordered_euclidean_space"
- shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
- and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
- by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def)
-
-lemma mem_interval:
- fixes a :: "'a::ordered_euclidean_space"
- shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
- 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)"
- using interval[of a b]
- by auto
-
-lemma interval_eq_empty:
- fixes a :: "'a::ordered_euclidean_space"
- shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
- and "({a .. b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
-proof -
- {
- fix i x
- assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
- then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
- unfolding mem_interval by auto
- then have "a\<bullet>i < b\<bullet>i" by auto
- then have False using as by auto
- }
- moreover
- {
- assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
- let ?x = "(1/2) *\<^sub>R (a + b)"
- {
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "a\<bullet>i < b\<bullet>i"
- using as[THEN bspec[where x=i]] i by auto
- then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
- by (auto simp: inner_add_left)
- }
- then have "box a b \<noteq> {}"
- using mem_interval(1)[of "?x" a b] by auto
- }
- ultimately show ?th1 by blast
-
- {
- fix i x
- assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>{a .. b}"
- then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
- unfolding mem_interval by auto
- then have "a\<bullet>i \<le> b\<bullet>i" by auto
- then have False using as by auto
- }
- moreover
- {
- assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
- let ?x = "(1/2) *\<^sub>R (a + b)"
- {
- fix i :: 'a
- assume i:"i \<in> Basis"
- have "a\<bullet>i \<le> b\<bullet>i"
- using as[THEN bspec[where x=i]] i by auto
- 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"
- by (auto simp: inner_add_left)
- }
- then have "{a .. b} \<noteq> {}"
- using mem_interval(2)[of "?x" a b] by auto
- }
- ultimately show ?th2 by blast
-qed
-
-lemma interval_ne_empty:
- fixes a :: "'a::ordered_euclidean_space"
- shows "{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
- and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
- unfolding interval_eq_empty[of a b] by fastforce+
-
-lemma interval_sing:
- fixes a :: "'a::ordered_euclidean_space"
- shows "{a .. a} = {a}"
- and "box a a = {}"
- unfolding set_eq_iff mem_interval eq_iff [symmetric]
- by (auto intro: euclidean_eqI simp: ex_in_conv)
-
-lemma subset_interval_imp:
- fixes a :: "'a::ordered_euclidean_space"
- 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}"
- 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"
- 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}"
- 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"
- unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
- by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
-
-lemma interval_open_subset_closed:
- fixes a :: "'a::ordered_euclidean_space"
- shows "box a b \<subseteq> {a .. b}"
- unfolding subset_eq [unfolded Ball_def] mem_interval
- by (fast intro: less_imp_le)
-
-lemma subset_interval:
- fixes a :: "'a::ordered_euclidean_space"
- 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)
- 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)
- 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)
- 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)
-proof -
- show ?th1
- unfolding subset_eq and Ball_def and mem_interval
- by (auto intro: order_trans)
- show ?th2
- unfolding subset_eq and Ball_def and mem_interval
- by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
- {
- assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
- then have "box c d \<noteq> {}"
- unfolding interval_eq_empty by auto
- fix i :: 'a
- assume i: "i \<in> Basis"
- (** TODO combine the following two parts as done in the HOL_light version. **)
- {
- 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"
- assume as2: "a\<bullet>i > c\<bullet>i"
- {
- fix j :: 'a
- assume j: "j \<in> Basis"
- then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
- apply (cases "j = i")
- using as(2)[THEN bspec[where x=j]] i
- apply (auto simp add: as2)
- done
- }
- then have "?x\<in>box c d"
- using i unfolding mem_interval by auto
- moreover
- have "?x \<notin> {a .. b}"
- unfolding mem_interval
- apply auto
- apply (rule_tac x=i in bexI)
- using as(2)[THEN bspec[where x=i]] and as2 i
- apply auto
- done
- ultimately have False using as by auto
- }
- then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
- moreover
- {
- 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"
- assume as2: "b\<bullet>i < d\<bullet>i"
- {
- fix j :: 'a
- assume "j\<in>Basis"
- then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
- apply (cases "j = i")
- using as(2)[THEN bspec[where x=j]]
- apply (auto simp add: as2)
- done
- }
- then have "?x\<in>box c d"
- unfolding mem_interval by auto
- moreover
- have "?x\<notin>{a .. b}"
- unfolding mem_interval
- apply auto
- apply (rule_tac x=i in bexI)
- using as(2)[THEN bspec[where x=i]] and as2 using i
- apply auto
- done
- ultimately have False using as by auto
- }
- then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
- ultimately
- have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
- } note part1 = this
- show ?th3
- unfolding subset_eq and Ball_def and mem_interval
- apply (rule, rule, rule, rule)
- apply (rule part1)
- unfolding subset_eq and Ball_def and mem_interval
- prefer 4
- apply auto
- apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
- done
- {
- assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
- fix i :: 'a
- assume i:"i\<in>Basis"
- from as(1) have "box c d \<subseteq> {a..b}"
- using interval_open_subset_closed[of a b] by auto
- then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
- using part1 and as(2) using i by auto
- } note * = this
- show ?th4
- unfolding subset_eq and Ball_def and mem_interval
- apply (rule, rule, rule, rule)
- apply (rule *)
- unfolding subset_eq and Ball_def and mem_interval
- prefer 4
- apply auto
- apply (erule_tac x=xa in allE, simp)+
- done
-qed
-
-lemma inter_interval:
- fixes a :: "'a::ordered_euclidean_space"
- shows "{a .. b} \<inter> {c .. d} =
- {(\<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)}"
- unfolding set_eq_iff and Int_iff and mem_interval
- by auto
-
-lemma disjoint_interval:
- fixes a::"'a::ordered_euclidean_space"
- 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)
- 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)
- 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)
- 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)
-proof -
- 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"
- have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
- (\<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)"
- by blast
- note * = set_eq_iff Int_iff empty_iff mem_interval ball_conj_distrib[symmetric] eq_False ball_simps(10)
- show ?th1 unfolding * by (intro **) auto
- show ?th2 unfolding * by (intro **) auto
- show ?th3 unfolding * by (intro **) auto
- show ?th4 unfolding * by (intro **) auto
-qed
-
-(* Moved interval_open_subset_closed a bit upwards *)
-
-lemma open_interval[intro]:
- fixes a b :: "'a::ordered_euclidean_space"
- shows "open (box a b)"
-proof -
- have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
- by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
- linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
- also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
- by (auto simp add: interval)
- finally show "open (box a b)" .
-qed
-
-lemma closed_interval[intro]:
- fixes a b :: "'a::ordered_euclidean_space"
- shows "closed {a .. b}"
-proof -
- have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
- by (intro closed_INT ballI continuous_closed_vimage allI
- linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
- also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = {a .. b}"
- by (auto simp add: eucl_le [where 'a='a])
- finally show "closed {a .. b}" .
-qed
-
-lemma interior_closed_interval [intro]:
- fixes a b :: "'a::ordered_euclidean_space"
- shows "interior {a..b} = box a b" (is "?L = ?R")
-proof(rule subset_antisym)
- show "?R \<subseteq> ?L"
- using interval_open_subset_closed open_interval
- by (rule interior_maximal)
- {
- fix x
- assume "x \<in> interior {a..b}"
- then obtain s where s: "open s" "x \<in> s" "s \<subseteq> {a..b}" ..
- then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}"
- unfolding open_dist and subset_eq by auto
- {
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "dist (x - (e / 2) *\<^sub>R i) x < e"
- and "dist (x + (e / 2) *\<^sub>R i) x < e"
- unfolding dist_norm
- apply auto
- unfolding norm_minus_cancel
- using norm_Basis[OF i] `e>0`
- apply auto
- done
- 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"
- using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
- and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
- unfolding mem_interval
- using i
- by blast+
- then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
- using `e>0` i
- by (auto simp: inner_diff_left inner_Basis inner_add_left)
- }
- then have "x \<in> box a b"
- unfolding mem_interval by auto
- }
- then show "?L \<subseteq> ?R" ..
-qed
-
-lemma bounded_closed_interval:
- fixes a :: "'a::ordered_euclidean_space"
- shows "bounded {a .. b}"
-proof -
- let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
- {
- fix x :: "'a"
- assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
- {
- fix i :: 'a
- assume "i \<in> Basis"
- then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
- using x[THEN bspec[where x=i]] by auto
- }
- then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
- apply -
- apply (rule setsum_mono)
- apply auto
- done
- then have "norm x \<le> ?b"
- using norm_le_l1[of x] by auto
- }
- then show ?thesis
- unfolding interval and bounded_iff by auto
-qed
-
-lemma bounded_interval:
- fixes a :: "'a::ordered_euclidean_space"
- shows "bounded {a .. b} \<and> bounded (box a b)"
- using bounded_closed_interval[of a b]
- using interval_open_subset_closed[of a b]
- using bounded_subset[of "{a..b}" "box a b"]
- by simp
-
-lemma not_interval_univ:
- fixes a :: "'a::ordered_euclidean_space"
- shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV"
- using bounded_interval[of a b] by auto
-
-lemma compact_interval:
- fixes a :: "'a::ordered_euclidean_space"
- shows "compact {a .. b}"
- using bounded_closed_imp_seq_compact[of "{a..b}"] using bounded_interval[of a b]
- by (auto simp: compact_eq_seq_compact_metric)
-
-lemma open_interval_midpoint:
- fixes a :: "'a::ordered_euclidean_space"
- assumes "box a b \<noteq> {}"
- shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
-proof -
- {
- fix i :: 'a
- assume "i \<in> Basis"
- 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"
- using assms[unfolded interval_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
- }
- then show ?thesis unfolding mem_interval by auto
-qed
-
-lemma open_closed_interval_convex:
- fixes x :: "'a::ordered_euclidean_space"
- assumes x: "x \<in> box a b"
- and y: "y \<in> {a .. b}"
- and e: "0 < e" "e \<le> 1"
- shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
-proof -
- {
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
- unfolding left_diff_distrib by simp
- also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
- apply (rule add_less_le_mono)
- using e unfolding mult_less_cancel_left and mult_le_cancel_left
- apply simp_all
- using x unfolding mem_interval using i
- apply simp
- using y unfolding mem_interval using i
- apply simp
- done
- finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
- unfolding inner_simps by auto
- moreover
- {
- have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
- unfolding left_diff_distrib by simp
- also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
- apply (rule add_less_le_mono)
- using e unfolding mult_less_cancel_left and mult_le_cancel_left
- apply simp_all
- using x
- unfolding mem_interval
- using i
- apply simp
- using y
- unfolding mem_interval
- using i
- apply simp
- done
- finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
- unfolding inner_simps by auto
- }
- 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"
- by auto
- }
- then show ?thesis
- unfolding mem_interval by auto
-qed
-
-lemma closure_open_interval:
- fixes a :: "'a::ordered_euclidean_space"
- assumes "box a b \<noteq> {}"
- shows "closure (box a b) = {a .. b}"
-proof -
- have ab: "a <e b"
- using assms by (simp add: eucl_less_def interval_ne_empty)
- let ?c = "(1 / 2) *\<^sub>R (a + b)"
- {
- fix x
- assume as:"x \<in> {a .. b}"
- def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
- {
- fix n
- assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
- have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
- unfolding inverse_le_1_iff by auto
- have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
- x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
- by (auto simp add: algebra_simps)
- then have "f n <e b" and "a <e f n"
- using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
- unfolding f_def by (auto simp: interval eucl_less_def)
- then have False
- using fn unfolding f_def using xc by auto
- }
- moreover
- {
- assume "\<not> (f ---> x) sequentially"
- {
- fix e :: real
- assume "e > 0"
- then have "\<exists>N::nat. inverse (real (N + 1)) < e"
- using real_arch_inv[of e]
- apply (auto simp add: Suc_pred')
- apply (rule_tac x="n - 1" in exI)
- apply auto
- done
- then obtain N :: nat where "inverse (real (N + 1)) < e"
- by auto
- then have "\<forall>n\<ge>N. inverse (real n + 1) < e"
- apply auto
- apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans
- real_of_nat_Suc real_of_nat_Suc_gt_zero)
- done
- then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
- }
- then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
- unfolding LIMSEQ_def by(auto simp add: dist_norm)
- then have "(f ---> x) sequentially"
- unfolding f_def
- 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]
- using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
- by auto
- }
- ultimately have "x \<in> closure (box a b)"
- using as and open_interval_midpoint[OF assms]
- unfolding closure_def
- unfolding islimpt_sequential
- by (cases "x=?c") (auto simp: in_box_eucl_less)
- }
- then show ?thesis
- using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
-qed
-
-lemma bounded_subset_open_interval_symmetric:
- fixes s::"('a::ordered_euclidean_space) set"
- assumes "bounded s"
- shows "\<exists>a. s \<subseteq> box (-a) a"
-proof -
- obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
- using assms[unfolded bounded_pos] by auto
- def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a"
- {
- fix x
- assume "x \<in> s"
- fix i :: 'a
- assume i: "i \<in> Basis"
- then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
- using b[THEN bspec[where x=x], OF `x\<in>s`]
- using Basis_le_norm[OF i, of x]
- unfolding inner_simps and a_def
- by auto
- }
- then show ?thesis
- by (auto intro: exI[where x=a] simp add: interval)
-qed
-
-lemma bounded_subset_open_interval:
- fixes s :: "('a::ordered_euclidean_space) set"
- shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
- by (auto dest!: bounded_subset_open_interval_symmetric)
-
-lemma bounded_subset_closed_interval_symmetric:
- fixes s :: "('a::ordered_euclidean_space) set"
- assumes "bounded s"
- shows "\<exists>a. s \<subseteq> {-a .. a}"
-proof -
- obtain a where "s \<subseteq> box (-a) a"
- using bounded_subset_open_interval_symmetric[OF assms] by auto
- then show ?thesis
- using interval_open_subset_closed[of "-a" a] by auto
-qed
-
-lemma bounded_subset_closed_interval:
- fixes s :: "('a::ordered_euclidean_space) set"
- shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> {a .. b}"
- using bounded_subset_closed_interval_symmetric[of s] by auto
-
-lemma frontier_closed_interval:
- fixes a b :: "'a::ordered_euclidean_space"
- shows "frontier {a .. b} = {a .. b} - box a b"
- unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
-
-lemma frontier_open_interval:
- fixes a b :: "'a::ordered_euclidean_space"
- shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)"
-proof (cases "box a b = {}")
- case True
- then show ?thesis
- using frontier_empty by auto
-next
- case False
- then show ?thesis
- unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval]
- by auto
-qed
-
-lemma inter_interval_mixed_eq_empty:
- fixes a :: "'a::ordered_euclidean_space"
- assumes "box c d \<noteq> {}"
- shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
- unfolding closure_open_interval[OF assms, symmetric]
- unfolding open_inter_closure_eq_empty[OF open_interval] ..
-
lemma open_box: "open (box a b)"
proof -
have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
@@ -6574,26 +6038,6 @@
instance euclidean_space \<subseteq> polish_space ..
-text {* Intervals in general, including infinite and mixtures of open and closed. *}
-
-definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
- (\<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)"
-
-lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
- "is_interval (box a b)" (is ?th2) proof -
- show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
- by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
-
-lemma is_interval_empty:
- "is_interval {}"
- unfolding is_interval_def
- by simp
-
-lemma is_interval_univ:
- "is_interval UNIV"
- unfolding is_interval_def
- by simp
-
subsection {* Closure of halfspaces and hyperplanes *}
@@ -6704,50 +6148,6 @@
lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
by (simp add: open_Collect_less)
-text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
-
-lemma eucl_lessThan_eq_halfspaces:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
- by (auto simp: eucl_less_def)
-
-lemma eucl_greaterThan_eq_halfspaces:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
- by (auto simp: eucl_less_def)
-
-lemma eucl_atMost_eq_halfspaces:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{.. a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})"
- by (auto simp: eucl_le[where 'a='a])
-
-lemma eucl_atLeast_eq_halfspaces:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{a ..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})"
- by (auto simp: eucl_le[where 'a='a])
-
-lemma open_eucl_lessThan[simp, intro]:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "open {x. x <e a}"
- by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt)
-
-lemma open_eucl_greaterThan[simp, intro]:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "open {x. a <e x}"
- by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt)
-
-lemma closed_eucl_atMost[simp, intro]:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "closed {.. a}"
- unfolding eucl_atMost_eq_halfspaces
- by (simp add: closed_INT closed_Collect_le)
-
-lemma closed_eucl_atLeast[simp, intro]:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "closed {a ..}"
- unfolding eucl_atLeast_eq_halfspaces
- by (simp add: closed_INT closed_Collect_le)
-
text {* This gives a simple derivation of limit component bounds. *}
lemma Lim_component_le:
@@ -7339,69 +6739,6 @@
"(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
by (simp add: field_simps inverse_eq_divide)
-lemma image_affinity_interval: fixes m::real
- fixes a b c :: "'a::ordered_euclidean_space"
- shows "(\<lambda>x. m *\<^sub>R x + c) ` {a .. b} =
- (if {a .. b} = {} then {}
- else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
- else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
-proof (cases "m = 0")
- case True
- {
- fix x
- assume "x \<le> c" "c \<le> x"
- then have "x = c"
- unfolding eucl_le[where 'a='a]
- apply -
- apply (subst euclidean_eq_iff)
- apply (auto intro: order_antisym)
- done
- }
- moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}"
- unfolding True by (auto simp add: eucl_le[where 'a='a])
- ultimately show ?thesis using True by auto
-next
- case False
- {
- fix y
- assume "a \<le> y" "y \<le> b" "m > 0"
- 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"
- unfolding eucl_le[where 'a='a] by (auto simp: inner_distrib)
- }
- moreover
- {
- fix y
- assume "a \<le> y" "y \<le> b" "m < 0"
- 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"
- unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_distrib)
- }
- moreover
- {
- fix y
- assume "m > 0" and "m *\<^sub>R a + c \<le> y" and "y \<le> m *\<^sub>R b + c"
- then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
- unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
- apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
- done
- }
- moreover
- {
- fix y
- assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
- then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
- unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
- apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
- done
- }
- ultimately show ?thesis using False by auto
-qed
-
-lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a..b} =
- (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})"
- using image_affinity_interval[of m 0 a b] by auto
-
subsection {* Banach fixed point theorem (not really topological...) *}