# Theory Ordered_Euclidean_Space

theory Ordered_Euclidean_Space
imports Cartesian_Euclidean_Space Product_Order
```theory Ordered_Euclidean_Space
imports
Cartesian_Euclidean_Space
"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 ≤ 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) *⇩R i)"
assumes eucl_sup: "sup x y = (∑i∈Basis. sup (x ∙ i) (y ∙ i) *⇩R i)"
assumes eucl_Inf: "Inf X = (∑i∈Basis. (INF x:X. x ∙ i) *⇩R i)"
assumes eucl_Sup: "Sup X = (∑i∈Basis. (SUP x:X. x ∙ i) *⇩R i)"
assumes eucl_abs: "¦x¦ = (∑i∈Basis. ¦x ∙ i¦ *⇩R i)"
begin

subclass order
by standard
(auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)

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)"
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: comp_def)

lemma abs_inner: "i ∈ Basis ⟹ ¦x¦ ∙ i = ¦x ∙ i¦"
by (auto simp: eucl_abs)

lemma
abs_scaleR: "¦a *⇩R b¦ = ¦a¦ *⇩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"

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

lemma
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 ‹b ∈ Basis› sum.delta
cong: if_cong)
with x show "∃x. x ∈ X ∧ x ∙ b = Inf X ∙ b ∧ (∀y. y ∈ X ⟶ x ∙ b ≤ y ∙ b)" by blast
qed

lemma
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 ‹b ∈ Basis› sum.delta
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 (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 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
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‹Instantiation for intervals on ‹ordered_euclidean_space››

lemma
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 vec_nth_real_1_iff_cbox [simp]:
fixes a b :: real
shows "(λx::real^1. x \$ 1) ` S = {a..b} ⟷ S = cbox (vec a) (vec b)"
by (metis interval_cbox vec_nth_1_iff_cbox)

lemma closed_eucl_atLeastAtMost[simp, intro]:
fixes a :: "'a::ordered_euclidean_space"
shows "closed {a..b}"

lemma closed_eucl_atMost[simp, intro]:
fixes a :: "'a::ordered_euclidean_space"
shows "closed {..a}"

lemma closed_eucl_atLeast[simp, intro]:
fixes a :: "'a::ordered_euclidean_space"
shows "closed {a..}"

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 *⇩R (x::_::ordered_euclidean_space)) ` {a .. b} =
(if {a .. b} = {} then {} else if 0 ≤ m then {m *⇩R a .. m *⇩R b} else {m *⇩R b .. m *⇩R a})"
using image_smult_cbox[of m a b]

lemma [simp]:
fixes a b::"'a::ordered_euclidean_space" and r s::real
shows is_interval_io: "is_interval {..<r}"
and is_interval_ic: "is_interval {..a}"
and is_interval_oi: "is_interval {r<..}"
and is_interval_ci: "is_interval {a..}"
and is_interval_oo: "is_interval {r<..<s}"
and is_interval_oc: "is_interval {r<..s}"
and is_interval_co: "is_interval {r..<s}"
and is_interval_cc: "is_interval {b..a}"
by (force simp: is_interval_def eucl_le[where 'a='a])+

lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
by (auto simp: real_atLeastGreaterThan_eq)

lemma compact_interval [simp]:
fixes a b::"'a::ordered_euclidean_space"
shows "compact {a .. b}"
by (metis compact_cbox interval_cbox)

lemma homeomorphic_closed_intervals:
fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
assumes "box a b ≠ {}" and "box c d ≠ {}"
shows "(cbox a b) homeomorphic (cbox c d)"
apply (rule homeomorphic_convex_compact)
using assms apply auto
done

lemma homeomorphic_closed_intervals_real:
fixes a::real and b and c::real and d
assumes "a<b" and "c<d"
shows "{a..b} homeomorphic {c..d}"
using assms by (auto intro: homeomorphic_convex_compact)

no_notation
eucl_less (infix "<e" 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 "inf x y = (χ i. inf (x \$ i) (y \$ i))"
definition "sup x y = (χ i. sup (x \$ i) (y \$ i))"
definition "Inf X = (χ i. (INF x:X. x \$ i))"
definition "Sup X = (χ i. (SUP x:X. x \$ i))"
definition "¦x¦ = (χ i. ¦x \$ i¦)"

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

lemma ANR_interval [iff]:
fixes a :: "'a::ordered_euclidean_space"
shows "ANR{a..b}"