src/HOL/Analysis/Ordered_Euclidean_Space.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63886 685fb01256af
child 64267 b9a1486e79be
permissions -rw-r--r--
tuned proofs;
     1 theory Ordered_Euclidean_Space
     2 imports
     3   Cartesian_Euclidean_Space
     4   "~~/src/HOL/Library/Product_Order"
     5 begin
     6 
     7 subsection \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
     8 
     9 class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
    10   assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
    11   assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    12   assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
    13   assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
    14   assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
    15   assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
    16   assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)"
    17 begin
    18 
    19 subclass order
    20   by standard
    21     (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
    22 
    23 subclass ordered_ab_group_add_abs
    24   by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
    25 
    26 subclass ordered_real_vector
    27   by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
    28 
    29 subclass lattice
    30   by standard (auto simp: eucl_inf eucl_sup eucl_le)
    31 
    32 subclass distrib_lattice
    33   by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
    34 
    35 subclass conditionally_complete_lattice
    36 proof
    37   fix z::'a and X::"'a set"
    38   assume "X \<noteq> {}"
    39   hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
    40   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"
    41     by (auto simp: eucl_Inf eucl_Sup eucl_le
    42       intro!: cInf_greatest cSup_least)
    43 qed (force intro!: cInf_lower cSup_upper
    44       simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
    45         eucl_Inf eucl_Sup eucl_le)+
    46 
    47 lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
    48   and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
    49   by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.delta
    50       cong: if_cong)
    51 
    52 lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
    53   and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
    54   using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
    55 
    56 lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
    57   by (auto simp: eucl_abs)
    58 
    59 lemma
    60   abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
    61   by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
    62 
    63 lemma interval_inner_leI:
    64   assumes "x \<in> {a .. b}" "0 \<le> i"
    65   shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
    66   using assms
    67   unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
    68   by (auto intro!: ordered_comm_monoid_add_class.setsum_mono mult_right_mono simp: eucl_le)
    69 
    70 lemma inner_nonneg_nonneg:
    71   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
    72   using interval_inner_leI[of a 0 a b]
    73   by auto
    74 
    75 lemma inner_Basis_mono:
    76   shows "a \<le> b \<Longrightarrow> c \<in> Basis  \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
    77   by (simp add: eucl_le)
    78 
    79 lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
    80   by (auto simp: eucl_le inner_Basis)
    81 
    82 lemma Sup_eq_maximum_componentwise:
    83   fixes s::"'a set"
    84   assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
    85   assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b"
    86   assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
    87   shows "Sup s = X"
    88   using assms
    89   unfolding eucl_Sup euclidean_representation_setsum
    90   by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
    91 
    92 lemma Inf_eq_minimum_componentwise:
    93   assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
    94   assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b"
    95   assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
    96   shows "Inf s = X"
    97   using assms
    98   unfolding eucl_Inf euclidean_representation_setsum
    99   by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   100 
   101 end
   102 
   103 lemma
   104   compact_attains_Inf_componentwise:
   105   fixes b::"'a::ordered_euclidean_space"
   106   assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
   107   obtains x where "x \<in> X" "x \<bullet> b = Inf X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
   108 proof atomize_elim
   109   let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
   110   from assms have "compact ?proj" "?proj \<noteq> {}"
   111     by (auto intro!: compact_continuous_image continuous_intros)
   112   from compact_attains_inf[OF this]
   113   obtain s x
   114     where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t"
   115       and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
   116     by auto
   117   hence "Inf ?proj = x \<bullet> b"
   118     by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   119   hence "x \<bullet> b = Inf X \<bullet> b"
   120     by (auto simp: eucl_Inf inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
   121       cong: if_cong)
   122   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
   123 qed
   124 
   125 lemma
   126   compact_attains_Sup_componentwise:
   127   fixes b::"'a::ordered_euclidean_space"
   128   assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
   129   obtains x where "x \<in> X" "x \<bullet> b = Sup X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
   130 proof atomize_elim
   131   let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
   132   from assms have "compact ?proj" "?proj \<noteq> {}"
   133     by (auto intro!: compact_continuous_image continuous_intros)
   134   from compact_attains_sup[OF this]
   135   obtain s x
   136     where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s"
   137       and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
   138     by auto
   139   hence "Sup ?proj = x \<bullet> b"
   140     by (auto intro!: cSup_eq_maximum)
   141   hence "x \<bullet> b = Sup X \<bullet> b"
   142     by (auto simp: eucl_Sup[where 'a='a] inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
   143       cong: if_cong)
   144   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
   145 qed
   146 
   147 lemma (in order) atLeastatMost_empty'[simp]:
   148   "(~ a <= b) \<Longrightarrow> {a..b} = {}"
   149   by (auto)
   150 
   151 instance real :: ordered_euclidean_space
   152   by standard auto
   153 
   154 lemma in_Basis_prod_iff:
   155   fixes i::"'a::euclidean_space*'b::euclidean_space"
   156   shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
   157   by (cases i) (auto simp: Basis_prod_def)
   158 
   159 instantiation prod :: (abs, abs) abs
   160 begin
   161 
   162 definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)"
   163 
   164 instance ..
   165 
   166 end
   167 
   168 instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
   169   by standard
   170     (auto intro!: add_mono simp add: euclidean_representation_setsum'  Ball_def inner_prod_def
   171       in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
   172       inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
   173       eucl_le[where 'a='b] abs_prod_def abs_inner)
   174 
   175 text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close>
   176 
   177 lemma
   178   fixes a :: "'a::ordered_euclidean_space"
   179   shows cbox_interval: "cbox a b = {a..b}"
   180     and interval_cbox: "{a..b} = cbox a b"
   181     and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}"
   182     and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
   183     by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
   184 
   185 lemma closed_eucl_atLeastAtMost[simp, intro]:
   186   fixes a :: "'a::ordered_euclidean_space"
   187   shows "closed {a..b}"
   188   by (simp add: cbox_interval[symmetric] closed_cbox)
   189 
   190 lemma closed_eucl_atMost[simp, intro]:
   191   fixes a :: "'a::ordered_euclidean_space"
   192   shows "closed {..a}"
   193   by (simp add: eucl_le_atMost[symmetric])
   194 
   195 lemma closed_eucl_atLeast[simp, intro]:
   196   fixes a :: "'a::ordered_euclidean_space"
   197   shows "closed {a..}"
   198   by (simp add: eucl_le_atLeast[symmetric])
   199 
   200 lemma bounded_closed_interval:
   201   fixes a :: "'a::ordered_euclidean_space"
   202   shows "bounded {a .. b}"
   203   using bounded_cbox[of a b]
   204   by (metis interval_cbox)
   205 
   206 lemma convex_closed_interval:
   207   fixes a :: "'a::ordered_euclidean_space"
   208   shows "convex {a .. b}"
   209   using convex_box[of a b]
   210   by (metis interval_cbox)
   211 
   212 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
   213   (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})"
   214   using image_smult_cbox[of m a b]
   215   by (simp add: cbox_interval)
   216 
   217 lemma is_interval_closed_interval:
   218   "is_interval {a .. (b::'a::ordered_euclidean_space)}"
   219   by (metis cbox_interval is_interval_cbox)
   220 
   221 lemma compact_interval:
   222   fixes a b::"'a::ordered_euclidean_space"
   223   shows "compact {a .. b}"
   224   by (metis compact_cbox interval_cbox)
   225 
   226 lemma homeomorphic_closed_intervals:
   227   fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
   228   assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
   229     shows "(cbox a b) homeomorphic (cbox c d)"
   230 apply (rule homeomorphic_convex_compact)
   231 using assms apply auto
   232 done
   233 
   234 lemma homeomorphic_closed_intervals_real:
   235   fixes a::real and b and c::real and d
   236   assumes "a<b" and "c<d"
   237     shows "{a..b} homeomorphic {c..d}"
   238 by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt)
   239 
   240 no_notation
   241   eucl_less (infix "<e" 50)
   242 
   243 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
   244   by (auto intro: setsum_nonneg)
   245 
   246 lemma
   247   fixes a b::"'a::ordered_euclidean_space"
   248   shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
   249     and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)"
   250     and bdd_above_box[intro, simp]: "bdd_above (box a b)"
   251     and bdd_below_box[intro, simp]: "bdd_below (box a b)"
   252   unfolding atomize_conj
   253   by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
   254     bounded_subset_cbox interval_cbox)
   255 
   256 instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
   257 begin
   258 
   259 definition "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
   260 definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
   261 definition "Inf X = (\<chi> i. (INF x:X. x $ i))"
   262 definition "Sup X = (\<chi> i. (SUP x:X. x $ i))"
   263 definition "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
   264 
   265 instance
   266   apply standard
   267   unfolding euclidean_representation_setsum'
   268   apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
   269     Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
   270     inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
   271   done
   272 
   273 end
   274 
   275 lemma ANR_interval [iff]:
   276     fixes a :: "'a::ordered_euclidean_space"
   277     shows "ANR{a..b}"
   278 by (simp add: interval_cbox)
   279 
   280 lemma ENR_interval [iff]:
   281     fixes a :: "'a::ordered_euclidean_space"
   282     shows "ENR{a..b}"
   283   by (auto simp: interval_cbox)
   284 
   285 end
   286