Theory HOL-Analysis.Ordered_Euclidean_Space

section ‹Ordered Euclidean Space›

theory Ordered_Euclidean_Space
imports
  Convex_Euclidean_Space Abstract_Limits
  "HOL-Library.Product_Order"
begin

text ‹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  (iBasis. x  i  y  i)"
  assumes eucl_less_le_not_le: "x < y  x  y  ¬ y  x"
  assumes eucl_inf: "inf x y = (iBasis. inf (x  i) (y  i) *R i)"
  assumes eucl_sup: "sup x y = (iBasis. sup (x  i) (y  i) *R i)"
  assumes eucl_Inf: "Inf X = (iBasis. (INF xX. x  i) *R i)"
  assumes eucl_Sup: "Sup X = (iBasis. (SUP xX. x  i) *R i)"
  assumes eucl_abs: "¦x¦ = (iBasis. ¦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_sum_left inner_Basis if_distrib
      cong: if_cong)

lemma inner_Basis_INF_left: "i  Basis  (INF xX. f x)  i = (INF xX. f x  i)"
  and inner_Basis_SUP_left: "i  Basis  (SUP xX. f x)  i = (SUP xX. 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 *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 "ai  xi" "xi  bi"
  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 b  Basis
      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 b  Basis
      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 iK. 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 iK. 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. (iBasis. max (f x  i) (g x  i) *R i))  (iBasis. max (l  i) (m  i) *R i)) F"
  by (intro tendsto_intros assms)

lemma tendsto_componentwise_min:
  assumes f: "(f  l) F" and g: "(g  m) F"
  shows "((λx. (iBasis. min (f x  i) (g x  i) *R i))  (iBasis. min (l  i) (m  i) *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)

instantiationtag unimportant› 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‹Instantiation for intervals on ordered_euclidean_space›

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. iBasis. x  i <= a  i} = {..a}"
    and eucl_le_atLeast: "{x. iBasis. 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 *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 [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 "<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

definitiontag important› "inf x y = (χ i. inf (x $ i) (y $ i))"
definitiontag important› "sup x y = (χ i. sup (x $ i) (y $ i))"
definitiontag important› "Inf X = (χ i. (INF xX. x $ i))"
definitiontag important› "Sup X = (χ i. (SUP xX. x $ i))"
definitiontag important› "¦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

end