Quellcode-Bibliothek Ordered_Euclidean_Space.thy Sprache: Isabelle

section \<open>Ordered Euclidean Space\<close>

theory Ordered_Euclidean_Space
imports
  Convex_Euclidean_Space Abstract_Limits
  "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_Inf[tendsto_intros]:
  fixes f :: "'a \ 'b \ 'c::ordered_euclidean_space"
  assumes "finite K" "\i. i \ K \ ((\x. f x i) \ l i) F"
  shows "((\x. Inf (f x ` K)) \ Inf (l ` K)) F"
  using assms
  by (induction K rule: finite_induct) (auto simp: cInf_insert_If tendsto_inf)

lemma tendsto_Sup[tendsto_intros]:
  fixes f :: "'a \ 'b \ 'c::ordered_euclidean_space"
  assumes "finite K" "\i. i \ K \ ((\x. f x i) \ l i) F"
  shows "((\x. Sup (f x ` K)) \ Sup (l ` K)) F"
  using assms
  by (induction K rule: finite_induct) (auto simp: cSup_insert_If tendsto_sup)

lemma continuous_map_Inf [continuous_intros]:
  fixes f :: "'a \ 'b \ 'c::ordered_euclidean_space"
  assumes "finite K" "\i. i \ K \ continuous_map X euclidean (\x. f x i)"
  shows "continuous_map X euclidean (\x. INF i\K. f x i)"
  using assms by (simp add: continuous_map_atin tendsto_Inf)

lemma continuous_map_Sup [continuous_intros]:
  fixes f :: "'a \ 'b \ 'c::ordered_euclidean_space"
  assumes "finite K" "\i. i \ K \ continuous_map X euclidean (\x. f x i)"
  shows "continuous_map X euclidean (\x. SUP i\K. f x i)"
  using assms by (simp add: continuous_map_atin tendsto_Sup)

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)

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 bounded_Ico [simp]: "bounded {a..
  and bounded_Ioc [simp]: "bounded {a<..b :: 'a :: ordered_euclidean_space}"
  and bounded_Ioo [simp]: "bounded {a<..
  by (rule bounded_subset[of "{a..b}"]; force; fail)+

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 \<open><e\<close> 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

quality97%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.