theory Ordered_Euclidean_Space imports Cartesian_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 ≤ 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) 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_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.delta 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.setsum_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_setsum 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_setsum 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_setsum_left inner_Basis if_distrib ‹b ∈ Basis› setsum.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_setsum_left inner_Basis if_distrib ‹b ∈ Basis› setsum.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 (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) 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 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: eucl_le_atMost[symmetric]) lemma closed_eucl_atLeast[simp, intro]: fixes a :: "'a::ordered_euclidean_space" shows "closed {a..}" by (simp add: eucl_le_atLeast[symmetric]) lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}" using bounded_cbox[of a b] by (metis interval_cbox) lemma convex_closed_interval: 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] by (simp add: cbox_interval) lemma is_interval_closed_interval: "is_interval {a .. (b::'a::ordered_euclidean_space)}" by (metis cbox_interval is_interval_cbox) lemma compact_interval: 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}" by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt) no_notation eucl_less (infix "<e" 50) lemma One_nonneg: "0 ≤ (∑Basis::'a::ordered_euclidean_space)" by (auto intro: setsum_nonneg) lemma content_closed_interval: fixes a :: "'a::ordered_euclidean_space" assumes "a ≤ b" shows "content {a .. b} = (∏i∈Basis. b∙i - a∙i)" using content_cbox[of a b] assms by (simp add: cbox_interval eucl_le[where 'a='a]) lemma integrable_const_ivl[intro]: fixes a::"'a::ordered_euclidean_space" shows "(λx. c) integrable_on {a .. b}" unfolding cbox_interval[symmetric] by (rule integrable_const) lemma integrable_on_subinterval: fixes f :: "'n::ordered_euclidean_space ⇒ 'a::banach" assumes "f integrable_on s" and "{a .. b} ⊆ s" shows "f integrable_on {a .. b}" using integrable_on_subcbox[of f s a b] assms by (simp add: cbox_interval) 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 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_setsum' 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