section \<open>Ordered Euclidean Space\<close>
theory Ordered_Euclidean_Space
imports
Convex_Euclidean_Space
"HOL-Library.Product_Order"
begin
text \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
assumes eucl_le: "x \ y \ (\i\Basis. x \ i \ y \ i)"
assumes eucl_less_le_not_le: "x < y \ x \ y \ \ y \ x"
assumes eucl_inf: "inf x y = (\i\Basis. inf (x \ i) (y \ i) *\<^sub>R i)"
assumes eucl_sup: "sup x y = (\i\Basis. sup (x \ i) (y \ i) *\<^sub>R i)"
assumes eucl_Inf: "Inf X = (\i\Basis. (INF x\X. x \ i) *\<^sub>R i)"
assumes eucl_Sup: "Sup X = (\i\Basis. (SUP x\X. x \ i) *\<^sub>R i)"
assumes eucl_abs: "\x\ = (\i\Basis. \x \ i\ *\<^sub>R i)"
begin
subclass order
by standard
(auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
subclass ordered_ab_group_add_abs
by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
subclass ordered_real_vector
by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
subclass lattice
by standard (auto simp: eucl_inf eucl_sup eucl_le)
subclass distrib_lattice
by standard (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 \ {}"
hence "\i. (\x. x \ i) ` X \ {}" by simp
thus "(\x. x \ X \ z \ x) \ z \ Inf X" "(\x. x \ X \ x \ z) \ Sup X \ z"
by (auto simp: eucl_Inf eucl_Sup eucl_le
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)+
lemma inner_Basis_inf_left: "i \ Basis \ inf x y \ i = inf (x \ i) (y \ i)"
and inner_Basis_sup_left: "i \ Basis \ sup x y \ i = sup (x \ i) (y \ i)"
by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib
cong: if_cong)
lemma inner_Basis_INF_left: "i \ Basis \ (INF x\X. f x) \ i = (INF x\X. f x \ i)"
and inner_Basis_SUP_left: "i \ Basis \ (SUP x\X. f x) \ i = (SUP x\X. f x \ i)"
using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: image_comp)
lemma abs_inner: "i \ Basis \ \x\ \ i = \x \ i\"
by (auto simp: eucl_abs)
lemma
abs_scaleR: "\a *\<^sub>R b\ = \a\ *\<^sub>R \b\"
by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
lemma interval_inner_leI:
assumes "x \ {a .. b}" "0 \ i"
shows "a\i \ x\i" "x\i \ b\i"
using assms
unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
by (auto intro!: ordered_comm_monoid_add_class.sum_mono mult_right_mono simp: eucl_le)
lemma inner_nonneg_nonneg:
shows "0 \ a \ 0 \ b \ 0 \ a \ b"
using interval_inner_leI[of a 0 a b]
by auto
lemma inner_Basis_mono:
shows "a \ b \ c \ Basis \ a \ c \ b \ c"
by (simp add: eucl_le)
lemma Basis_nonneg[intro, simp]: "i \ Basis \ 0 \ i"
by (auto simp: eucl_le inner_Basis)
lemma Sup_eq_maximum_componentwise:
fixes s::"'a set"
assumes i: "\b. b \ Basis \ X \ b = i b \ b"
assumes sup: "\b x. b \ Basis \ x \ s \ x \ b \ X \ b"
assumes i_s: "\b. b \ Basis \ (i b \ b) \ (\x. x \ b) ` s"
shows "Sup s = X"
using assms
unfolding eucl_Sup euclidean_representation_sum
by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
lemma Inf_eq_minimum_componentwise:
assumes i: "\b. b \ Basis \ X \ b = i b \ b"
assumes sup: "\b x. b \ Basis \ x \ s \ X \ b \ x \ b"
assumes i_s: "\b. b \ Basis \ (i b \ b) \ (\x. x \ b) ` s"
shows "Inf s = X"
using assms
unfolding eucl_Inf euclidean_representation_sum
by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
end
proposition compact_attains_Inf_componentwise:
fixes b::"'a::ordered_euclidean_space"
assumes "b \ Basis" assumes "X \ {}" "compact X"
obtains x where "x \ X" "x \ b = Inf X \ b" "\y. y \ X \ x \ b \ y \ b"
proof atomize_elim
let ?proj = "(\x. x \ b) ` X"
from assms have "compact ?proj" "?proj \ {}"
by (auto intro!: compact_continuous_image continuous_intros)
from compact_attains_inf[OF this]
obtain s x
where s: "s\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ s \ t"
and x: "x \ X" "s = x \ b" "\y. y \ X \ x \ b \ y \ b"
by auto
hence "Inf ?proj = x \ b"
by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
hence "x \ b = Inf X \ b"
by (auto simp: eucl_Inf inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close>
cong: if_cong)
with x show "\x. x \ X \ x \ b = Inf X \ b \ (\y. y \ X \ x \ b \ y \ b)" by blast
qed
proposition
compact_attains_Sup_componentwise:
fixes b::"'a::ordered_euclidean_space"
assumes "b \ Basis" assumes "X \ {}" "compact X"
obtains x where "x \ X" "x \ b = Sup X \ b" "\y. y \ X \ y \ b \ x \ b"
proof atomize_elim
let ?proj = "(\x. x \ b) ` X"
from assms have "compact ?proj" "?proj \ {}"
by (auto intro!: compact_continuous_image continuous_intros)
from compact_attains_sup[OF this]
obtain s x
where s: "s\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ t \ s"
and x: "x \ X" "s = x \ b" "\y. y \ X \ y \ b \ x \ b"
by auto
hence "Sup ?proj = x \ b"
by (auto intro!: cSup_eq_maximum)
hence "x \ b = Sup X \ b"
by (auto simp: eucl_Sup[where 'a='a] inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close>
cong: if_cong)
with x show "\x. x \ X \ x \ b = Sup X \ b \ (\y. y \ X \ y \ b \ x \ b)" by blast
qed
lemma tendsto_sup[tendsto_intros]:
fixes X :: "'a \ 'b::ordered_euclidean_space"
assumes "(X \ x) net" "(Y \ y) net"
shows "((\i. sup (X i) (Y i)) \ sup x y) net"
unfolding sup_max eucl_sup by (intro assms tendsto_intros)
lemma tendsto_inf[tendsto_intros]:
fixes X :: "'a \ 'b::ordered_euclidean_space"
assumes "(X \ x) net" "(Y \ y) net"
shows "((\i. inf (X i) (Y i)) \ inf x y) net"
unfolding inf_min eucl_inf by (intro assms tendsto_intros)
lemma tendsto_componentwise_max:
assumes f: "(f \ l) F" and g: "(g \ m) F"
shows "((\x. (\i\Basis. max (f x \ i) (g x \ i) *\<^sub>R i)) \ (\i\Basis. max (l \ i) (m \ i) *\<^sub>R i)) F"
by (intro tendsto_intros assms)
lemma tendsto_componentwise_min:
assumes f: "(f \ l) F" and g: "(g \ m) F"
shows "((\x. (\i\Basis. min (f x \ i) (g x \ i) *\<^sub>R i)) \ (\i\Basis. min (l \ i) (m \ i) *\<^sub>R i)) F"
by (intro tendsto_intros assms)
lemma (in order) atLeastatMost_empty'[simp]:
"(\ a \ b) \ {a..b} = {}"
by (auto)
instance real :: ordered_euclidean_space
by standard auto
lemma in_Basis_prod_iff:
fixes i::"'a::euclidean_space*'b::euclidean_space"
shows "i \ Basis \ fst i = 0 \ snd i \ Basis \ snd i = 0 \ fst i \ Basis"
by (cases i) (auto simp: Basis_prod_def)
instantiation\<^marker>\<open>tag unimportant\<close> prod :: (abs, abs) abs
begin
definition "\x\ = (\fst x\, \snd x\)"
instance ..
end
instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
by standard
(auto intro!: add_mono simp add: euclidean_representation_sum' 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)
text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close>
proposition
fixes a :: "'a::ordered_euclidean_space"
shows cbox_interval: "cbox a b = {a..b}"
and interval_cbox: "{a..b} = cbox a b"
and eucl_le_atMost: "{x. \i\Basis. x \ i <= a \ i} = {..a}"
and eucl_le_atLeast: "{x. \i\Basis. a \ i <= x \ i} = {a..}"
by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
lemma sums_vec_nth :
assumes "f sums a"
shows "(\x. f x $ i) sums a $ i"
using assms unfolding sums_def
by (auto dest: tendsto_vec_nth [where i=i])
lemma summable_vec_nth :
assumes "summable f"
shows "summable (\x. f x $ i)"
using assms unfolding summable_def
by (blast intro: sums_vec_nth)
lemma closed_eucl_atLeastAtMost[simp, intro]:
fixes a :: "'a::ordered_euclidean_space"
shows "closed {a..b}"
by (simp add: cbox_interval[symmetric] closed_cbox)
lemma closed_eucl_atMost[simp, intro]:
fixes a :: "'a::ordered_euclidean_space"
shows "closed {..a}"
by (simp add: closed_interval_left eucl_le_atMost[symmetric])
lemma closed_eucl_atLeast[simp, intro]:
fixes a :: "'a::ordered_euclidean_space"
shows "closed {a..}"
by (simp add: closed_interval_right eucl_le_atLeast[symmetric])
lemma bounded_closed_interval [simp]:
fixes a :: "'a::ordered_euclidean_space"
shows "bounded {a .. b}"
using bounded_cbox[of a b]
by (metis interval_cbox)
lemma convex_closed_interval [simp]:
fixes a :: "'a::ordered_euclidean_space"
shows "convex {a .. b}"
using convex_box[of a b]
by (metis interval_cbox)
lemma image_smult_interval:"(\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_smult_cbox[of m a b]
by (simp add: cbox_interval)
lemma [simp]:
fixes a b::"'a::ordered_euclidean_space"
shows is_interval_ic: "is_interval {..a}"
and is_interval_ci: "is_interval {a..}"
and is_interval_cc: "is_interval {b..a}"
by (force simp: is_interval_def eucl_le[where 'a='a])+
lemma connected_interval [simp]:
fixes a b::"'a::ordered_euclidean_space"
shows "connected {a..b}"
using is_interval_cc is_interval_connected by blast
lemma compact_interval [simp]:
fixes a b::"'a::ordered_euclidean_space"
shows "compact {a .. b}"
by (metis compact_cbox interval_cbox)
no_notation
eucl_less (infix " 50)
lemma One_nonneg: "0 \ (\Basis::'a::ordered_euclidean_space)"
by (auto intro: sum_nonneg)
lemma
fixes a b::"'a::ordered_euclidean_space"
shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)"
and bdd_above_box[intro, simp]: "bdd_above (box a b)"
and bdd_below_box[intro, simp]: "bdd_below (box a b)"
unfolding atomize_conj
by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
bounded_subset_cbox_symmetric interval_cbox)
instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
begin
definition\<^marker>\<open>tag important\<close> "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
definition\<^marker>\<open>tag important\<close> "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
definition\<^marker>\<open>tag important\<close> "Inf X = (\<chi> i. (INF x\<in>X. x $ i))"
definition\<^marker>\<open>tag important\<close> "Sup X = (\<chi> i. (SUP x\<in>X. x $ i))"
definition\<^marker>\<open>tag important\<close> "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
instance
apply standard
unfolding euclidean_representation_sum'
apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
done
end
end
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
