src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
author hoelzl
Mon, 21 Jun 2010 19:33:51 +0200
changeset 37489 44e42d392c6e
parent 36844 5f9385ecc1a7
child 37647 a5400b94d2dd
permissions -rw-r--r--
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     1
(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     2
    Author:     Robert Himmelmann, TU Muenchen
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     3
*)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     4
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     5
header {* Convex sets, functions and related things. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     6
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     7
theory Convex_Euclidean_Space
36623
d26348b667f2 Moved Convex theory to library.
hoelzl
parents: 36590
diff changeset
     8
imports Topology_Euclidean_Space Convex
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     9
begin
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    10
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    11
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    12
(* ------------------------------------------------------------------------- *)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    13
(* To be moved elsewhere                                                     *)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    14
(* ------------------------------------------------------------------------- *)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    15
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    16
lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \<longleftrightarrow> i\<ge>DIM('a)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    17
  using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    18
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    19
lemma scaleR_2:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    20
  fixes x :: "'a::real_vector"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    21
  shows "scaleR 2 x = x + x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    22
unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp
34964
4e8be3c04d37 Replaced vec1 and dest_vec1 by abbreviation.
hoelzl
parents: 34915
diff changeset
    23
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    24
declare euclidean_simps[simp]
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    25
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    26
lemma vector_choose_size: "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    27
  apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"]) using DIM_positive[where 'a='a] by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    28
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    29
lemma setsum_delta_notmem: assumes "x\<notin>s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    30
  shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    31
        "setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    32
        "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    33
        "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    34
  apply(rule_tac [!] setsum_cong2) using assms by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    35
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    36
lemma setsum_delta'':
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    37
  fixes s::"'a::real_vector set" assumes "finite s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    38
  shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *\<^sub>R x) = (if y\<in>s then (f y) *\<^sub>R y else 0)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    39
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    40
  have *:"\<And>x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    41
  show ?thesis unfolding * using setsum_delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    42
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    43
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    44
lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    45
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    46
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space)) ` {a..b} =
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    47
  (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})"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    48
  using image_affinity_interval[of m 0 a b] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    49
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    50
lemma dist_triangle_eq:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    51
  fixes x y z :: "'a::euclidean_space"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    52
  shows "dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    53
proof- have *:"x - y + (y - z) = x - z" by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    54
  show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    55
    by(auto simp add:norm_minus_commute) qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    56
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    57
lemma norm_minus_eqI:"x = - y \<Longrightarrow> norm x = norm y" by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    58
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    59
lemma Min_grI: assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a" shows "x < Min A"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    60
  unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    61
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    62
lemma dimindex_ge_1:"CARD(_::finite) \<ge> 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    63
  using one_le_card_finite by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    64
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    65
lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    66
  unfolding norm_eq_sqrt_inner by simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    67
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    68
lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    69
  unfolding norm_eq_sqrt_inner by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    70
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    71
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    72
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    73
subsection {* Affine set and affine hull.*}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    74
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    75
definition
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    76
  affine :: "'a::real_vector set \<Rightarrow> bool" where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    77
  "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    78
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    79
lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
    80
unfolding affine_def by(metis eq_diff_eq')
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    81
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    82
lemma affine_empty[intro]: "affine {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    83
  unfolding affine_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    84
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    85
lemma affine_sing[intro]: "affine {x}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    86
  unfolding affine_alt by (auto simp add: scaleR_left_distrib [symmetric])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    87
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    88
lemma affine_UNIV[intro]: "affine UNIV"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    89
  unfolding affine_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    90
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    91
lemma affine_Inter: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter> f)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    92
  unfolding affine_def by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    93
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    94
lemma affine_Int: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    95
  unfolding affine_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    96
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    97
lemma affine_affine_hull: "affine(affine hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    98
  unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    99
  unfolding mem_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   100
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   101
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   102
by (metis affine_affine_hull hull_same mem_def)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   103
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   104
lemma setsum_restrict_set'': assumes "finite A"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   105
  shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   106
  unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] ..
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   107
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   108
subsection {* Some explicit formulations (from Lars Schewe). *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   109
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   110
lemma affine: fixes V::"'a::real_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   111
  shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   112
unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   113
defer apply(rule, rule, rule, rule, rule) proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   114
  fix x y u v assume as:"x \<in> V" "y \<in> V" "u + v = (1::real)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   115
    "\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   116
  thus "u *\<^sub>R x + v *\<^sub>R y \<in> V" apply(cases "x=y")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   117
    using as(4)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>w. if w = x then u else v"]] and as(1-3) 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   118
    by(auto simp add: scaleR_left_distrib[THEN sym])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   119
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   120
  fix s u assume as:"\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   121
    "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = (1::real)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   122
  def n \<equiv> "card s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   123
  have "card s = 0 \<or> card s = 1 \<or> card s = 2 \<or> card s > 2" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   124
  thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" proof(auto simp only: disjE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   125
    assume "card s = 2" hence "card s = Suc (Suc 0)" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   126
    then obtain a b where "s = {a, b}" unfolding card_Suc_eq by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   127
    thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   128
      by(auto simp add: setsum_clauses(2))
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   129
  next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   130
      case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   131
      assume IA:"\<And>u s.  \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s;
34915
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 34291
diff changeset
   132
               s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 34291
diff changeset
   133
        as:"Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   134
           "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   135
      have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   136
        assume " \<not> (\<exists>x\<in>s. u x \<noteq> 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   137
        thus False using as(7) and `card s > 2` by (metis Numeral1_eq1_nat less_0_number_of less_int_code(15)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   138
          less_nat_number_of not_less_iff_gr_or_eq of_nat_1 of_nat_eq_iff pos2 rel_simps(4)) qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   139
      then obtain x where x:"x\<in>s" "u x \<noteq> 1" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   140
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   141
      have c:"card (s - {x}) = card s - 1" apply(rule card_Diff_singleton) using `x\<in>s` as(4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   142
      have *:"s = insert x (s - {x})" "finite (s - {x})" using `x\<in>s` and as(4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   143
      have **:"setsum u (s - {x}) = 1 - u x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   144
        using setsum_clauses(2)[OF *(2), of u x, unfolded *(1)[THEN sym] as(7)] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   145
      have ***:"inverse (1 - u x) * setsum u (s - {x}) = 1" unfolding ** using `u x \<noteq> 1` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   146
      have "(\<Sum>xa\<in>s - {x}. (inverse (1 - u x) * u xa) *\<^sub>R xa) \<in> V" proof(cases "card (s - {x}) > 2")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   147
        case True hence "s - {x} \<noteq> {}" "card (s - {x}) = n" unfolding c and as(1)[symmetric] proof(rule_tac ccontr) 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   148
          assume "\<not> s - {x} \<noteq> {}" hence "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   149
          thus False using True by auto qed auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   150
        thus ?thesis apply(rule_tac IA[of "s - {x}" "\<lambda>y. (inverse (1 - u x) * u y)"])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   151
        unfolding setsum_right_distrib[THEN sym] using as and *** and True by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   152
      next case False hence "card (s - {x}) = Suc (Suc 0)" using as(2) and c by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   153
        then obtain a b where "(s - {x}) = {a, b}" "a\<noteq>b" unfolding card_Suc_eq by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   154
        thus ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   155
          using *** *(2) and `s \<subseteq> V` unfolding setsum_right_distrib by(auto simp add: setsum_clauses(2)) qed
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   156
      hence "u x + (1 - u x) = 1 \<Longrightarrow> u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>xa\<in>s - {x}. u xa *\<^sub>R xa) /\<^sub>R (1 - u x)) \<in> V"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   157
        apply-apply(rule as(3)[rule_format]) 
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   158
        unfolding  RealVector.scaleR_right.setsum using x(1) as(6) by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   159
      thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   160
         apply(subst *) unfolding setsum_clauses(2)[OF *(2)]
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   161
         using `u x \<noteq> 1` by auto 
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   162
    qed auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   163
  next assume "card s = 1" then obtain a where "s={a}" by(auto simp add: card_Suc_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   164
    thus ?thesis using as(4,5) by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   165
  qed(insert `s\<noteq>{}` `finite s`, auto)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   166
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   167
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   168
lemma affine_hull_explicit:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   169
  "affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   170
  apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   171
  apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   172
  fix x assume "x\<in>p" thus "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   173
    apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   174
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   175
  fix t x s u assume as:"p \<subseteq> t" "affine t" "finite s" "s \<noteq> {}" "s \<subseteq> p" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   176
  thus "x \<in> t" using as(2)[unfolded affine, THEN spec[where x=s], THEN spec[where x=u]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   177
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   178
  show "affine {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y}" unfolding affine_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   179
    apply(rule,rule,rule,rule,rule) unfolding mem_Collect_eq proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   180
    fix u v ::real assume uv:"u + v = 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   181
    fix x assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   182
    then obtain sx ux where x:"finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "setsum ux sx = 1" "(\<Sum>v\<in>sx. ux v *\<^sub>R v) = x" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   183
    fix y assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   184
    then obtain sy uy where y:"finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "setsum uy sy = 1" "(\<Sum>v\<in>sy. uy v *\<^sub>R v) = y" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   185
    have xy:"finite (sx \<union> sy)" using x(1) y(1) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   186
    have **:"(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   187
    show "\<exists>s ua. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum ua s = 1 \<and> (\<Sum>v\<in>s. ua v *\<^sub>R v) = u *\<^sub>R x + v *\<^sub>R y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   188
      apply(rule_tac x="sx \<union> sy" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   189
      apply(rule_tac x="\<lambda>a. (if a\<in>sx then u * ux a else 0) + (if a\<in>sy then v * uy a else 0)" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   190
      unfolding scaleR_left_distrib setsum_addf if_smult scaleR_zero_left  ** setsum_restrict_set[OF xy, THEN sym]
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   191
      unfolding scaleR_scaleR[THEN sym] RealVector.scaleR_right.setsum [symmetric] and setsum_right_distrib[THEN sym]
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   192
      unfolding x y using x(1-3) y(1-3) uv by simp qed qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   193
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   194
lemma affine_hull_finite:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   195
  assumes "finite s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   196
  shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   197
  unfolding affine_hull_explicit and expand_set_eq and mem_Collect_eq apply (rule,rule)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   198
  apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   199
  fix x u assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   200
  thus "\<exists>sa u. finite sa \<and> \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   201
    apply(rule_tac x=s in exI, rule_tac x=u in exI) using assms by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   202
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   203
  fix x t u assume "t \<subseteq> s" hence *:"s \<inter> t = t" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   204
  assume "finite t" "\<not> (\<forall>x. (x \<in> t) = (x \<in> {}))" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   205
  thus "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   206
    unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and * by auto qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   207
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   208
subsection {* Stepping theorems and hence small special cases. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   209
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   210
lemma affine_hull_empty[simp]: "affine hull {} = {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   211
  apply(rule hull_unique) unfolding mem_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   212
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   213
lemma affine_hull_finite_step:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   214
  fixes y :: "'a::real_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   215
  shows "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   216
  "finite s \<Longrightarrow> (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   217
                (\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   218
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   219
  show ?th1 by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   220
  assume ?as 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   221
  { assume ?lhs
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   222
    then obtain u where u:"setsum u (insert a s) = w \<and> (\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   223
    have ?rhs proof(cases "a\<in>s")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   224
      case True hence *:"insert a s = s" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   225
      show ?thesis using u[unfolded *] apply(rule_tac x=0 in exI) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   226
    next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   227
      case False thus ?thesis apply(rule_tac x="u a" in exI) using u and `?as` by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   228
    qed  } moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   229
  { assume ?rhs
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   230
    then obtain v u where vu:"setsum u s = w - v"  "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   231
    have *:"\<And>x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   232
    have ?lhs proof(cases "a\<in>s")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   233
      case True thus ?thesis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   234
        apply(rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   235
        unfolding setsum_clauses(2)[OF `?as`]  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   236
        unfolding scaleR_left_distrib and setsum_addf 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   237
        unfolding vu and * and scaleR_zero_left
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   238
        by (auto simp add: setsum_delta[OF `?as`])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   239
    next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   240
      case False 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   241
      hence **:"\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   242
               "\<And>x. x \<in> s \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   243
      from False show ?thesis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   244
        apply(rule_tac x="\<lambda>x. if x=a then v else u x" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   245
        unfolding setsum_clauses(2)[OF `?as`] and * using vu
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   246
        using setsum_cong2[of s "\<lambda>x. u x *\<^sub>R x" "\<lambda>x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF **(2)]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   247
        using setsum_cong2[of s u "\<lambda>x. if x = a then v else u x", OF **(1)] by auto  
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   248
    qed }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   249
  ultimately show "?lhs = ?rhs" by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   250
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   251
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   252
lemma affine_hull_2:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   253
  fixes a b :: "'a::real_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   254
  shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   255
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   256
  have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   257
         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   258
  have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   259
    using affine_hull_finite[of "{a,b}"] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   260
  also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   261
    by(simp add: affine_hull_finite_step(2)[of "{b}" a]) 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   262
  also have "\<dots> = ?rhs" unfolding * by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   263
  finally show ?thesis by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   264
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   265
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   266
lemma affine_hull_3:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   267
  fixes a b c :: "'a::real_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   268
  shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   269
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   270
  have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   271
         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   272
  show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   273
    unfolding * apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   274
    apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   275
    apply(rule_tac x=u in exI) by(auto intro!: exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   276
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   277
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   278
subsection {* Some relations between affine hull and subspaces. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   279
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   280
lemma affine_hull_insert_subset_span:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   281
  fixes a :: "'a::euclidean_space"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   282
  shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   283
  unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   284
  apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   285
  fix x t u assume as:"finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   286
  have "(\<lambda>x. x - a) ` (t - {a}) \<subseteq> {x - a |x. x \<in> s}" using as(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   287
  thus "\<exists>v. x = a + v \<and> (\<exists>S u. finite S \<and> S \<subseteq> {x - a |x. x \<in> s} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = v)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   288
    apply(rule_tac x="x - a" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   289
    apply (rule conjI, simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   290
    apply(rule_tac x="(\<lambda>x. x - a) ` (t - {a})" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   291
    apply(rule_tac x="\<lambda>x. u (x + a)" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   292
    apply (rule conjI) using as(1) apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   293
    apply (erule conjI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   294
    using as(1)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   295
    apply (simp add: setsum_reindex[unfolded inj_on_def] scaleR_right_diff_distrib setsum_subtractf scaleR_left.setsum[THEN sym] setsum_diff1 scaleR_left_diff_distrib)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   296
    unfolding as by simp qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   297
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   298
lemma affine_hull_insert_span:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   299
  fixes a :: "'a::euclidean_space"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   300
  assumes "a \<notin> s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   301
  shows "affine hull (insert a s) =
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   302
            {a + v | v . v \<in> span {x - a | x.  x \<in> s}}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   303
  apply(rule, rule affine_hull_insert_subset_span) unfolding subset_eq Ball_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   304
  unfolding affine_hull_explicit and mem_Collect_eq proof(rule,rule,erule exE,erule conjE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   305
  fix y v assume "y = a + v" "v \<in> span {x - a |x. x \<in> s}"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   306
  then obtain t u where obt:"finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y" unfolding span_explicit by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   307
  def f \<equiv> "(\<lambda>x. x + a) ` t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   308
  have f:"finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v - a) *\<^sub>R (v - a)) = y - a" unfolding f_def using obt 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   309
    by(auto simp add: setsum_reindex[unfolded inj_on_def])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   310
  have *:"f \<inter> {a} = {}" "f \<inter> - {a} = f" using f(2) assms by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   311
  show "\<exists>sa u. finite sa \<and> sa \<noteq> {} \<and> sa \<subseteq> insert a s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   312
    apply(rule_tac x="insert a f" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   313
    apply(rule_tac x="\<lambda>x. if x=a then 1 - setsum (\<lambda>x. u (x - a)) f else u (x - a)" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   314
    using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult
35577
43b93e294522 Generalized setsum_cases
hoelzl
parents: 35542
diff changeset
   315
    unfolding setsum_cases[OF f(1), of "\<lambda>x. x = a"]
43b93e294522 Generalized setsum_cases
hoelzl
parents: 35542
diff changeset
   316
    by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) qed
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   317
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   318
lemma affine_hull_span:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   319
  fixes a :: "'a::euclidean_space"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   320
  assumes "a \<in> s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   321
  shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   322
  using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   323
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   324
subsection {* Cones. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   325
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   326
definition
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   327
  cone :: "'a::real_vector set \<Rightarrow> bool" where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   328
  "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   329
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   330
lemma cone_empty[intro, simp]: "cone {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   331
  unfolding cone_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   332
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   333
lemma cone_univ[intro, simp]: "cone UNIV"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   334
  unfolding cone_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   335
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   336
lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   337
  unfolding cone_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   338
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   339
subsection {* Conic hull. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   340
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   341
lemma cone_cone_hull: "cone (cone hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   342
  unfolding hull_def using cone_Inter[of "{t \<in> conic. s \<subseteq> t}"] 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   343
  by (auto simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   344
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   345
lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   346
  apply(rule hull_eq[unfolded mem_def])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   347
  using cone_Inter unfolding subset_eq by (auto simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   348
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   349
subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   350
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   351
definition
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   352
  affine_dependent :: "'a::real_vector set \<Rightarrow> bool" where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   353
  "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   354
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   355
lemma affine_dependent_explicit:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   356
  "affine_dependent p \<longleftrightarrow>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   357
    (\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   358
    (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   359
  unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq apply(rule)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   360
  apply(erule bexE,erule exE,erule exE) apply(erule conjE)+ defer apply(erule exE,erule exE) apply(erule conjE)+ apply(erule bexE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   361
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   362
  fix x s u assume as:"x \<in> p" "finite s" "s \<noteq> {}" "s \<subseteq> p - {x}" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   363
  have "x\<notin>s" using as(1,4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   364
  show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   365
    apply(rule_tac x="insert x s" in exI, rule_tac x="\<lambda>v. if v = x then - 1 else u v" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   366
    unfolding if_smult and setsum_clauses(2)[OF as(2)] and setsum_delta_notmem[OF `x\<notin>s`] and as using as by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   367
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   368
  fix s u v assume as:"finite s" "s \<subseteq> p" "setsum u s = 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" "v \<in> s" "u v \<noteq> 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   369
  have "s \<noteq> {v}" using as(3,6) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   370
  thus "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   371
    apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   372
    unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   373
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   374
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   375
lemma affine_dependent_explicit_finite:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   376
  fixes s :: "'a::real_vector set" assumes "finite s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   377
  shows "affine_dependent s \<longleftrightarrow> (\<exists>u. setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   378
  (is "?lhs = ?rhs")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   379
proof
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   380
  have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   381
  assume ?lhs
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   382
  then obtain t u v where "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0"  "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   383
    unfolding affine_dependent_explicit by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   384
  thus ?rhs apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   385
    apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   386
    unfolding Int_absorb1[OF `t\<subseteq>s`] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   387
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   388
  assume ?rhs
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   389
  then obtain u v where "setsum u s = 0"  "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   390
  thus ?lhs unfolding affine_dependent_explicit using assms by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   391
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   392
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   393
subsection {* A general lemma. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   394
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   395
lemma convex_connected:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   396
  fixes s :: "'a::real_normed_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   397
  assumes "convex s" shows "connected s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   398
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   399
  { fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   400
    assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   401
    then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   402
    hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   403
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   404
    { fix x e::real assume as:"0 \<le> x" "x \<le> 1" "0 < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   405
      { fix y have *:"(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   406
          by (simp add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   407
        assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   408
        hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   409
          unfolding * and scaleR_right_diff_distrib[THEN sym]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   410
          unfolding less_divide_eq using n by auto  }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   411
      hence "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   412
        apply(rule_tac x="e / norm (x1 - x2)" in exI) using as
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   413
        apply auto unfolding zero_less_divide_iff using n by simp  }  note * = this
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   414
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   415
    have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   416
      apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   417
      using * apply(simp add: dist_norm)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   418
      using as(1,2)[unfolded open_dist] apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   419
      using as(1,2)[unfolded open_dist] apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   420
      using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   421
      using as(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   422
    then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1"  "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   423
    hence False using as(4) 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   424
      using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   425
      using x1(2) x2(2) by auto  }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   426
  thus ?thesis unfolding connected_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   427
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   428
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   429
subsection {* One rather trivial consequence. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   430
34964
4e8be3c04d37 Replaced vec1 and dest_vec1 by abbreviation.
hoelzl
parents: 34915
diff changeset
   431
lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   432
  by(simp add: convex_connected convex_UNIV)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   433
36623
d26348b667f2 Moved Convex theory to library.
hoelzl
parents: 36590
diff changeset
   434
subsection {* Balls, being convex, are connected. *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   435
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   436
lemma convex_box: fixes a::"'a::euclidean_space"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   437
  assumes "\<And>i. i<DIM('a) \<Longrightarrow> convex {x. P i x}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   438
  shows "convex {x. \<forall>i<DIM('a). P i (x$$i)}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   439
  using assms unfolding convex_def by(auto simp add:euclidean_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   440
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   441
lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i<DIM('a). 0 \<le> x$$i)}"
36623
d26348b667f2 Moved Convex theory to library.
hoelzl
parents: 36590
diff changeset
   442
  by (rule convex_box) (simp add: atLeast_def[symmetric] convex_real_interval)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   443
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   444
lemma convex_local_global_minimum:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   445
  fixes s :: "'a::real_normed_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   446
  assumes "0<e" "convex_on s f" "ball x e \<subseteq> s" "\<forall>y\<in>ball x e. f x \<le> f y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   447
  shows "\<forall>y\<in>s. f x \<le> f y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   448
proof(rule ccontr)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   449
  have "x\<in>s" using assms(1,3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   450
  assume "\<not> (\<forall>y\<in>s. f x \<le> f y)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   451
  then obtain y where "y\<in>s" and y:"f x > f y" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   452
  hence xy:"0 < dist x y" by (auto simp add: dist_nz[THEN sym])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   453
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   454
  then obtain u where "0 < u" "u \<le> 1" and u:"u < e / dist x y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   455
    using real_lbound_gt_zero[of 1 "e / dist x y"] using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   456
  hence "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y" using `x\<in>s` `y\<in>s`
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   457
    using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   458
  moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   459
  have *:"x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" by (simp add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   460
  have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`] unfolding dist_norm[THEN sym]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   461
    using u unfolding pos_less_divide_eq[OF xy] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   462
  hence "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   463
  ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   464
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   465
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   466
lemma convex_ball:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   467
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   468
  shows "convex (ball x e)" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   469
proof(auto simp add: convex_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   470
  fix y z assume yz:"dist x y < e" "dist x z < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   471
  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   472
  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   473
    using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
36623
d26348b667f2 Moved Convex theory to library.
hoelzl
parents: 36590
diff changeset
   474
  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   475
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   476
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   477
lemma convex_cball:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   478
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   479
  shows "convex(cball x e)"
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
   480
proof(auto simp add: convex_def Ball_def)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   481
  fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   482
  fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   483
  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   484
    using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
36623
d26348b667f2 Moved Convex theory to library.
hoelzl
parents: 36590
diff changeset
   485
  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using convex_bound_le[OF yz uv] by auto 
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   486
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   487
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   488
lemma connected_ball:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   489
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   490
  shows "connected (ball x e)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   491
  using convex_connected convex_ball by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   492
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   493
lemma connected_cball:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   494
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   495
  shows "connected(cball x e)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   496
  using convex_connected convex_cball by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   497
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   498
subsection {* Convex hull. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   499
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   500
lemma convex_convex_hull: "convex(convex hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   501
  unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   502
  unfolding mem_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   503
34064
eee04bbbae7e avoid dependency on implicit dest rule predicate1D in proofs
haftmann
parents: 33758
diff changeset
   504
lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   505
by (metis convex_convex_hull hull_same mem_def)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   506
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   507
lemma bounded_convex_hull:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   508
  fixes s :: "'a::real_normed_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   509
  assumes "bounded s" shows "bounded(convex hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   510
proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   511
  show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   512
    unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   513
    unfolding subset_eq mem_cball dist_norm using B by auto qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   514
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   515
lemma finite_imp_bounded_convex_hull:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   516
  fixes s :: "'a::real_normed_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   517
  shows "finite s \<Longrightarrow> bounded(convex hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   518
  using bounded_convex_hull finite_imp_bounded by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   519
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   520
subsection {* Stepping theorems for convex hulls of finite sets. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   521
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   522
lemma convex_hull_empty[simp]: "convex hull {} = {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   523
  apply(rule hull_unique) unfolding mem_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   524
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   525
lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   526
  apply(rule hull_unique) unfolding mem_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   527
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   528
lemma convex_hull_insert:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   529
  fixes s :: "'a::real_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   530
  assumes "s \<noteq> {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   531
  shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   532
                                    b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   533
 apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   534
 fix x assume x:"x = a \<or> x \<in> s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   535
 thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   536
   apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   537
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   538
  fix x assume "x\<in>?hull"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   539
  then obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   540
  have "a\<in>convex hull insert a s" "b\<in>convex hull insert a s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   541
    using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   542
  thus "x\<in> convex hull insert a s" unfolding obt(5) using convex_convex_hull[of "insert a s", unfolded convex_def]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   543
    apply(erule_tac x=a in ballE) apply(erule_tac x=b in ballE) apply(erule_tac x=u in allE) using obt by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   544
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   545
  show "convex ?hull" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   546
    fix x y u v assume as:"(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   547
    from as(4) obtain u1 v1 b1 where obt1:"u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   548
    from as(5) obtain u2 v2 b2 where obt2:"u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   549
    have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   550
    have "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   551
    proof(cases "u * v1 + v * v2 = 0")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   552
      have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   553
      case True hence **:"u * v1 = 0" "v * v2 = 0"
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   554
        using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by arith+
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   555
      hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   556
      thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   557
    next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   558
      have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   559
      also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   560
      also have "\<dots> = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   561
      case False have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2" apply -
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   562
        apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   563
        using as(1,2) obt1(1,2) obt2(1,2) by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   564
      thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   565
        apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   566
        apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   567
        unfolding add_divide_distrib[THEN sym] and real_0_le_divide_iff
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   568
        by (auto simp add: scaleR_left_distrib scaleR_right_distrib)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   569
    qed note * = this
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   570
    have u1:"u1 \<le> 1" unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   571
    have u2:"u2 \<le> 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   572
    have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   573
      apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   574
    also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   575
    finally 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   576
    show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   577
      apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   578
      using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   579
  qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   580
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   581
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   582
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   583
subsection {* Explicit expression for convex hull. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   584
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   585
lemma convex_hull_indexed:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   586
  fixes s :: "'a::real_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   587
  shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   588
                            (setsum u {1..k} = 1) \<and>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   589
                            (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   590
  apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   591
  apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   592
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   593
  fix x assume "x\<in>s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   594
  thus "x \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   595
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   596
  fix t assume as:"s \<subseteq> t" "convex t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   597
  show "?hull \<subseteq> t" apply(rule) unfolding mem_Collect_eq apply(erule exE | erule conjE)+ proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   598
    fix x k u y assume assm:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   599
    show "x\<in>t" unfolding assm(3)[THEN sym] apply(rule as(2)[unfolded convex, rule_format])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   600
      using assm(1,2) as(1) by auto qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   601
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   602
  fix x y u v assume uv:"0\<le>u" "0\<le>v" "u+v=(1::real)" and xy:"x\<in>?hull" "y\<in>?hull"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   603
  from xy obtain k1 u1 x1 where x:"\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   604
  from xy obtain k2 u2 x2 where y:"\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   605
  have *:"\<And>P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   606
    "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   607
    prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   608
  have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto  
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   609
  show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   610
    apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   611
    apply(rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule)
35577
43b93e294522 Generalized setsum_cases
hoelzl
parents: 35542
diff changeset
   612
    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def Collect_mem_eq
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   613
    unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] setsum_right_distrib[THEN sym] proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   614
    fix i assume i:"i \<in> {1..k1+k2}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   615
    show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and> (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   616
    proof(cases "i\<in>{1..k1}")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   617
      case True thus ?thesis using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   618
    next def j \<equiv> "i - k1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   619
      case False with i have "j \<in> {1..k2}" unfolding j_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   620
      thus ?thesis unfolding j_def[symmetric] using False
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   621
        using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] by auto qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   622
  qed(auto simp add: not_le x(2,3) y(2,3) uv(3))
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   623
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   624
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   625
lemma convex_hull_finite:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   626
  fixes s :: "'a::real_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   627
  assumes "finite s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   628
  shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   629
         setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   630
proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   631
  fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   632
    apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   633
    unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   634
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   635
  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   636
  fix ux assume ux:"\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   637
  fix uy assume uy:"\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   638
  { fix x assume "x\<in>s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   639
    hence "0 \<le> u * ux x + v * uy x" using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   640
      by (auto, metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))  }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   641
  moreover have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   642
    unfolding setsum_addf and setsum_right_distrib[THEN sym] and ux(2) uy(2) using uv(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   643
  moreover have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   644
    unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   645
  ultimately show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and> (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   646
    apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   647
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   648
  fix t assume t:"s \<subseteq> t" "convex t" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   649
  fix u assume u:"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   650
  thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   651
    using assms and t(1) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   652
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   653
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   654
subsection {* Another formulation from Lars Schewe. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   655
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   656
lemma setsum_constant_scaleR:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   657
  fixes y :: "'a::real_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   658
  shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   659
apply (cases "finite A")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   660
apply (induct set: finite)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   661
apply (simp_all add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   662
done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   663
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   664
lemma convex_hull_explicit:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   665
  fixes p :: "'a::real_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   666
  shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   667
             (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   668
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   669
  { fix x assume "x\<in>?lhs"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   670
    then obtain k u y where obt:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   671
      unfolding convex_hull_indexed by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   672
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   673
    have fin:"finite {1..k}" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   674
    have fin':"\<And>v. finite {i \<in> {1..k}. y i = v}" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   675
    { fix j assume "j\<in>{1..k}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   676
      hence "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   677
        using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   678
        apply(rule setsum_nonneg) using obt(1) by auto } 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   679
    moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   680
    have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1"  
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   681
      unfolding setsum_image_gen[OF fin, THEN sym] using obt(2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   682
    moreover have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   683
      using setsum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, THEN sym]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   684
      unfolding scaleR_left.setsum using obt(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   685
    ultimately have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   686
      apply(rule_tac x="y ` {1..k}" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   687
      apply(rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   688
    hence "x\<in>?rhs" by auto  }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   689
  moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   690
  { fix y assume "y\<in>?rhs"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   691
    then obtain s u where obt:"finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   692
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   693
    obtain f where f:"inj_on f {1..card s}" "f ` {1..card s} = s" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   694
    
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   695
    { fix i::nat assume "i\<in>{1..card s}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   696
      hence "f i \<in> s"  apply(subst f(2)[THEN sym]) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   697
      hence "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto  }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   698
    moreover have *:"finite {1..card s}" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   699
    { fix y assume "y\<in>s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   700
      then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   701
      hence "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   702
      hence "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   703
      hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   704
            "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   705
        by (auto simp add: setsum_constant_scaleR)   }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   706
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   707
    hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   708
      unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f] 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   709
      unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   710
      using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   711
    
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   712
    ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   713
      apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastsimp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   714
    hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto  }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   715
  ultimately show ?thesis unfolding expand_set_eq by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   716
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   717
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   718
subsection {* A stepping theorem for that expansion. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   719
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   720
lemma convex_hull_finite_step:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   721
  fixes s :: "'a::real_vector set" assumes "finite s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   722
  shows "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   723
     \<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   724
proof(rule, case_tac[!] "a\<in>s")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   725
  assume "a\<in>s" hence *:"insert a s = s" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   726
  assume ?lhs thus ?rhs unfolding * apply(rule_tac x=0 in exI) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   727
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   728
  assume ?lhs then obtain u where u:"\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   729
  assume "a\<notin>s" thus ?rhs apply(rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   730
    apply(rule_tac x=u in exI) using u[unfolded setsum_clauses(2)[OF assms]] and `a\<notin>s` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   731
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   732
  assume "a\<in>s" hence *:"insert a s = s" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   733
  have fin:"finite (insert a s)" using assms by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   734
  assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   735
  show ?lhs apply(rule_tac x="\<lambda>x. (if a = x then v else 0) + u x" in exI) unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   736
    unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\<in>s` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   737
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   738
  assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   739
  moreover assume "a\<notin>s" moreover have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   740
    apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\<notin>s` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   741
  ultimately show ?lhs apply(rule_tac x="\<lambda>x. if a = x then v else u x" in exI)  unfolding setsum_clauses(2)[OF assms] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   742
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   743
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   744
subsection {* Hence some special cases. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   745
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   746
lemma convex_hull_2:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   747
  "convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b | u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   748
proof- have *:"\<And>u. (\<forall>x\<in>{a, b}. 0 \<le> u x) \<longleftrightarrow> 0 \<le> u a \<and> 0 \<le> u b" by auto have **:"finite {b}" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   749
show ?thesis apply(simp add: convex_hull_finite) unfolding convex_hull_finite_step[OF **, of a 1, unfolded * conj_assoc]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   750
  apply auto apply(rule_tac x=v in exI) apply(rule_tac x="1 - v" in exI) apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   751
  apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\<lambda>x. v" in exI) by simp qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   752
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   753
lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b - a) | u.  0 \<le> u \<and> u \<le> 1}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   754
  unfolding convex_hull_2 unfolding Collect_def 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   755
proof(rule ext) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   756
  fix x show "(\<exists>v u. x = v *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> v \<and> 0 \<le> u \<and> v + u = 1) = (\<exists>u. x = a + u *\<^sub>R (b - a) \<and> 0 \<le> u \<and> u \<le> 1)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   757
    unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   758
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   759
lemma convex_hull_3:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   760
  "convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   761
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   762
  have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   763
  have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   764
         "\<And>x y z ::_::euclidean_space. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   765
  show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   766
    unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   767
    apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   768
    apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   769
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   770
lemma convex_hull_3_alt:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   771
  "convex hull {a,b,c} = {a + u *\<^sub>R (b - a) + v *\<^sub>R (c - a) | u v.  0 \<le> u \<and> 0 \<le> v \<and> u + v \<le> 1}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   772
proof- have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   773
  show ?thesis unfolding convex_hull_3 apply (auto simp add: *) apply(rule_tac x=v in exI) apply(rule_tac x=w in exI) apply (simp add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   774
    apply(rule_tac x=u in exI) apply(rule_tac x=v in exI) by (simp add: algebra_simps) qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   775
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   776
subsection {* Relations among closure notions and corresponding hulls. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   777
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   778
text {* TODO: Generalize linear algebra concepts defined in @{text
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   779
Euclidean_Space.thy} so that we can generalize these lemmas. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   780
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   781
lemma subspace_imp_affine:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   782
  fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> affine s"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   783
  unfolding subspace_def affine_def by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   784
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   785
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   786
  unfolding affine_def convex_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   787
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   788
lemma subspace_imp_convex:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   789
  fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> convex s"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   790
  using subspace_imp_affine affine_imp_convex by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   791
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   792
lemma affine_hull_subset_span:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   793
  fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \<subseteq> (span s)"
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   794
by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   795
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   796
lemma convex_hull_subset_span:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   797
  fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \<subseteq> (span s)"
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   798
by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   799
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   800
lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   801
by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def)
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
   802
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   803
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   804
lemma affine_dependent_imp_dependent:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   805
  fixes s :: "(_::euclidean_space) set" shows "affine_dependent s \<Longrightarrow> dependent s"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   806
  unfolding affine_dependent_def dependent_def 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   807
  using affine_hull_subset_span by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   808
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   809
lemma dependent_imp_affine_dependent:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   810
  fixes s :: "(_::euclidean_space) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   811
  assumes "dependent {x - a| x . x \<in> s}" "a \<notin> s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   812
  shows "affine_dependent (insert a s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   813
proof-
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   814
  from assms(1)[unfolded dependent_explicit] obtain S u v 
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   815
    where obt:"finite S" "S \<subseteq> {x - a |x. x \<in> s}" "v\<in>S" "u v  \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   816
  def t \<equiv> "(\<lambda>x. x + a) ` S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   817
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   818
  have inj:"inj_on (\<lambda>x. x + a) S" unfolding inj_on_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   819
  have "0\<notin>S" using obt(2) assms(2) unfolding subset_eq by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   820
  have fin:"finite t" and  "t\<subseteq>s" unfolding t_def using obt(1,2) by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   821
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   822
  hence "finite (insert a t)" and "insert a t \<subseteq> insert a s" by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   823
  moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x)) = (\<Sum>x\<in>t. Q x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   824
    apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   825
  have "(\<Sum>x\<in>insert a t. if x = a then - (\<Sum>x\<in>t. u (x - a)) else u (x - a)) = 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   826
    unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` apply auto unfolding * by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   827
  moreover have "\<exists>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) \<noteq> 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   828
    apply(rule_tac x="v + a" in bexI) using obt(3,4) and `0\<notin>S` unfolding t_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   829
  moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>t. Q x *\<^sub>R x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   830
    apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   831
  have "(\<Sum>x\<in>t. u (x - a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v - a) *\<^sub>R v)" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   832
    unfolding scaleR_left.setsum unfolding t_def and setsum_reindex[OF inj] and o_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   833
    using obt(5) by (auto simp add: setsum_addf scaleR_right_distrib)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   834
  hence "(\<Sum>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   835
    unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` by (auto simp add: *)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   836
  ultimately show ?thesis unfolding affine_dependent_explicit
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   837
    apply(rule_tac x="insert a t" in exI) by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   838
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   839
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   840
lemma convex_cone:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   841
  "convex s \<and> cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. (x + y) \<in> s) \<and> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)" (is "?lhs = ?rhs")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   842
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   843
  { fix x y assume "x\<in>s" "y\<in>s" and ?lhs
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   844
    hence "2 *\<^sub>R x \<in>s" "2 *\<^sub>R y \<in> s" unfolding cone_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   845
    hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   846
      apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   847
      apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
   848
  thus ?thesis unfolding convex_def cone_def by blast
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   849
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   850
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   851
lemma affine_dependent_biggerset: fixes s::"('a::euclidean_space) set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   852
  assumes "finite s" "card s \<ge> DIM('a) + 2"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   853
  shows "affine_dependent s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   854
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   855
  have "s\<noteq>{}" using assms by auto then obtain a where "a\<in>s" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   856
  have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   857
  have "card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding * 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   858
    apply(rule card_image) unfolding inj_on_def by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   859
  also have "\<dots> > DIM('a)" using assms(2)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   860
    unfolding card_Diff_singleton[OF assms(1) `a\<in>s`] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   861
  finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   862
    apply(rule dependent_imp_affine_dependent)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   863
    apply(rule dependent_biggerset) by auto qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   864
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   865
lemma affine_dependent_biggerset_general:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   866
  assumes "finite (s::('a::euclidean_space) set)" "card s \<ge> dim s + 2"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   867
  shows "affine_dependent s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   868
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   869
  from assms(2) have "s \<noteq> {}" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   870
  then obtain a where "a\<in>s" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   871
  have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   872
  have **:"card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding * 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   873
    apply(rule card_image) unfolding inj_on_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   874
  have "dim {x - a |x. x \<in> s - {a}} \<le> dim s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   875
    apply(rule subset_le_dim) unfolding subset_eq
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   876
    using `a\<in>s` by (auto simp add:span_superset span_sub)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   877
  also have "\<dots> < dim s + 1" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   878
  also have "\<dots> \<le> card (s - {a})" using assms
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   879
    using card_Diff_singleton[OF assms(1) `a\<in>s`] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   880
  finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   881
    apply(rule dependent_imp_affine_dependent) apply(rule dependent_biggerset_general) unfolding ** by auto qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   882
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   883
subsection {* Caratheodory's theorem. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   884
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   885
lemma convex_hull_caratheodory: fixes p::"('a::euclidean_space) set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   886
  shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   887
  (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   888
  unfolding convex_hull_explicit expand_set_eq mem_Collect_eq
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   889
proof(rule,rule)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   890
  fix y let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   891
  assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   892
  then obtain N where "?P N" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   893
  hence "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n" apply(rule_tac ex_least_nat_le) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   894
  then obtain n where "?P n" and smallest:"\<forall>k<n. \<not> ?P k" by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   895
  then obtain s u where obt:"finite s" "card s = n" "s\<subseteq>p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1"  "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   896
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   897
  have "card s \<le> DIM('a) + 1" proof(rule ccontr, simp only: not_le)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   898
    assume "DIM('a) + 1 < card s"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   899
    hence "affine_dependent s" using affine_dependent_biggerset[OF obt(1)] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   900
    then obtain w v where wv:"setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   901
      using affine_dependent_explicit_finite[OF obt(1)] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   902
    def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"  def t \<equiv> "Min i"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   903
    have "\<exists>x\<in>s. w x < 0" proof(rule ccontr, simp add: not_less)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   904
      assume as:"\<forall>x\<in>s. 0 \<le> w x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   905
      hence "setsum w (s - {v}) \<ge> 0" apply(rule_tac setsum_nonneg) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   906
      hence "setsum w s > 0" unfolding setsum_diff1'[OF obt(1) `v\<in>s`]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   907
        using as[THEN bspec[where x=v]] and `v\<in>s` using `w v \<noteq> 0` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   908
      thus False using wv(1) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   909
    qed hence "i\<noteq>{}" unfolding i_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   910
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   911
    hence "t \<ge> 0" using Min_ge_iff[of i 0 ] and obt(1) unfolding t_def i_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   912
      using obt(4)[unfolded le_less] apply auto unfolding divide_le_0_iff by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   913
    have t:"\<forall>v\<in>s. u v + t * w v \<ge> 0" proof
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   914
      fix v assume "v\<in>s" hence v:"0\<le>u v" using obt(4)[THEN bspec[where x=v]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   915
      show"0 \<le> u v + t * w v" proof(cases "w v < 0")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   916
        case False thus ?thesis apply(rule_tac add_nonneg_nonneg) 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   917
          using v apply simp apply(rule mult_nonneg_nonneg) using `t\<ge>0` by auto next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   918
        case True hence "t \<le> u v / (- w v)" using `v\<in>s`
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   919
          unfolding t_def i_def apply(rule_tac Min_le) using obt(1) by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   920
        thus ?thesis unfolding real_0_le_add_iff
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   921
          using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[THEN sym]]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   922
      qed qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   923
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   924
    obtain a where "a\<in>s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   925
      using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   926
    hence a:"a\<in>s" "u a + t * w a = 0" by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   927
    have *:"\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   928
      unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto 
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   929
    have "(\<Sum>v\<in>s. u v + t * w v) = 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   930
      unfolding setsum_addf wv(1) setsum_right_distrib[THEN sym] obt(5) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   931
    moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   932
      unfolding setsum_addf obt(6) scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] wv(4)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   933
      using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   934
    ultimately have "?P (n - 1)" apply(rule_tac x="(s - {a})" in exI)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   935
      apply(rule_tac x="\<lambda>v. u v + t * w v" in exI) using obt(1-3) and t and a
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   936
      by (auto simp add: * scaleR_left_distrib)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   937
    thus False using smallest[THEN spec[where x="n - 1"]] by auto qed
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   938
  thus "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   939
    \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" using obt by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   940
qed auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   941
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   942
lemma caratheodory:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   943
 "convex hull p = {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   944
      card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   945
  unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   946
  fix x assume "x \<in> convex hull p"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   947
  then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   948
     "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"unfolding convex_hull_caratheodory by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   949
  thus "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   950
    apply(rule_tac x=s in exI) using hull_subset[of s convex]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   951
  using convex_convex_hull[unfolded convex_explicit, of s, THEN spec[where x=s], THEN spec[where x=u]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   952
next
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   953
  fix x assume "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   954
  then obtain s where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s" by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   955
  thus "x \<in> convex hull p" using hull_mono[OF `s\<subseteq>p`] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   956
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   957
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   958
subsection {* Openness and compactness are preserved by convex hull operation. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   959
34964
4e8be3c04d37 Replaced vec1 and dest_vec1 by abbreviation.
hoelzl
parents: 34915
diff changeset
   960
lemma open_convex_hull[intro]:
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   961
  fixes s :: "'a::real_normed_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   962
  assumes "open s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   963
  shows "open(convex hull s)"
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
   964
  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   965
proof(rule, rule) fix a
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   966
  assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   967
  then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   968
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   969
  from assms[unfolded open_contains_cball] obtain b where b:"\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   970
    using bchoice[of s "\<lambda>x e. e>0 \<and> cball x e \<subseteq> s"] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   971
  have "b ` t\<noteq>{}" unfolding i_def using obt by auto  def i \<equiv> "b ` t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   972
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   973
  show "\<exists>e>0. cball a e \<subseteq> {y. \<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   974
    apply(rule_tac x="Min i" in exI) unfolding subset_eq apply rule defer apply rule unfolding mem_Collect_eq
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   975
  proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   976
    show "0 < Min i" unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] `b \` t\<noteq>{}`]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   977
      using b apply simp apply rule apply(erule_tac x=x in ballE) using `t\<subseteq>s` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   978
  next  fix y assume "y \<in> cball a (Min i)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   979
    hence y:"norm (a - y) \<le> Min i" unfolding dist_norm[THEN sym] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   980
    { fix x assume "x\<in>t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   981
      hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   982
      hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   983
      moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
   984
      ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast }
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   985
    moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   986
    have *:"inj_on (\<lambda>v. v + (y - a)) t" unfolding inj_on_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   987
    have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   988
      unfolding setsum_reindex[OF *] o_def using obt(4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   989
    moreover have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a)) *\<^sub>R v) = y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   990
      unfolding setsum_reindex[OF *] o_def using obt(4,5)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   991
      by (simp add: setsum_addf setsum_subtractf scaleR_left.setsum[THEN sym] scaleR_right_distrib)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   992
    ultimately show "\<exists>sa u. finite sa \<and> (\<forall>x\<in>sa. x \<in> s) \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   993
      apply(rule_tac x="(\<lambda>v. v + (y - a)) ` t" in exI) apply(rule_tac x="\<lambda>v. u (v - (y - a))" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   994
      using obt(1, 3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   995
  qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   996
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   997
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   998
lemma compact_convex_combinations:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   999
  fixes s t :: "'a::real_normed_vector set"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1000
  assumes "compact s" "compact t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1001
  shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1002
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1003
  let ?X = "{0..1} \<times> s \<times> t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1004
  let ?h = "(\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1005
  have *:"{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t} = ?h ` ?X"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1006
    apply(rule set_ext) unfolding image_iff mem_Collect_eq
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1007
    apply rule apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1008
    apply (rule_tac x=u in rev_bexI, simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1009
    apply (erule rev_bexI, erule rev_bexI, simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1010
    by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1011
  have "continuous_on ({0..1} \<times> s \<times> t)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1012
     (\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1013
    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1014
  thus ?thesis unfolding *
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1015
    apply (rule compact_continuous_image)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1016
    apply (intro compact_Times compact_interval assms)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1017
    done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1018
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1019
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1020
lemma compact_convex_hull: fixes s::"('a::euclidean_space) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1021
  assumes "compact s"  shows "compact(convex hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1022
proof(cases "s={}")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1023
  case True thus ?thesis using compact_empty by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1024
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1025
  case False then obtain w where "w\<in>s" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1026
  show ?thesis unfolding caratheodory[of s]
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1027
  proof(induct ("DIM('a) + 1"))
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1028
    have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" 
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
  1029
      using compact_empty by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1030
    case 0 thus ?case unfolding * by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1031
  next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1032
    case (Suc n)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1033
    show ?case proof(cases "n=0")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1034
      case True have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1035
        unfolding expand_set_eq and mem_Collect_eq proof(rule, rule)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1036
        fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1037
        then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1038
        show "x\<in>s" proof(cases "card t = 0")
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
  1039
          case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1040
        next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1041
          case False hence "card t = Suc 0" using t(3) `n=0` by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1042
          then obtain a where "t = {a}" unfolding card_Suc_eq by auto
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
  1043
          thus ?thesis using t(2,4) by simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1044
        qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1045
      next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1046
        fix x assume "x\<in>s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1047
        thus "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1048
          apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1049
      qed thus ?thesis using assms by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1050
    next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1051
      case False have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} =
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1052
        { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1053
        0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> {x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> x \<in> convex hull t}}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1054
        unfolding expand_set_eq and mem_Collect_eq proof(rule,rule)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1055
        fix x assume "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1056
          0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1057
        then obtain u v c t where obt:"x = (1 - c) *\<^sub>R u + c *\<^sub>R v"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1058
          "0 \<le> c \<and> c \<le> 1" "u \<in> s" "finite t" "t \<subseteq> s" "card t \<le> n"  "v \<in> convex hull t" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1059
        moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \<in> convex hull insert u t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1060
          apply(rule mem_convex) using obt(2) and convex_convex_hull and hull_subset[of "insert u t" convex]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1061
          using obt(7) and hull_mono[of t "insert u t"] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1062
        ultimately show "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1063
          apply(rule_tac x="insert u t" in exI) by (auto simp add: card_insert_if)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1064
      next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1065
        fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1066
        then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1067
        let ?P = "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1068
          0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1069
        show ?P proof(cases "card t = Suc n")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1070
          case False hence "card t \<le> n" using t(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1071
          thus ?P apply(rule_tac x=w in exI, rule_tac x=x in exI, rule_tac x=1 in exI) using `w\<in>s` and t
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1072
            by(auto intro!: exI[where x=t])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1073
        next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1074
          case True then obtain a u where au:"t = insert a u" "a\<notin>u" apply(drule_tac card_eq_SucD) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1075
          show ?P proof(cases "u={}")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1076
            case True hence "x=a" using t(4)[unfolded au] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1077
            show ?P unfolding `x=a` apply(rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI)
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
  1078
              using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"])
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1079
          next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1080
            case False obtain ux vx b where obt:"ux\<ge>0" "vx\<ge>0" "ux + vx = 1" "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1081
              using t(4)[unfolded au convex_hull_insert[OF False]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1082
            have *:"1 - vx = ux" using obt(3) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1083
            show ?P apply(rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=vx in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1084
              using obt and t(1-3) unfolding au and * using card_insert_disjoint[OF _ au(2)]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1085
              by(auto intro!: exI[where x=u])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1086
          qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1087
        qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1088
      qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1089
      thus ?thesis using compact_convex_combinations[OF assms Suc] by simp 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1090
    qed
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36341
diff changeset
  1091
  qed
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1092
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1093
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1094
lemma finite_imp_compact_convex_hull:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1095
  fixes s :: "('a::euclidean_space) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1096
  shows "finite s \<Longrightarrow> compact(convex hull s)"
36071
c8ae8e56d42e tuned many proofs a bit
nipkow
parents: 35577
diff changeset
  1097
by (metis compact_convex_hull finite_imp_compact)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1098
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1099
subsection {* Extremal points of a simplex are some vertices. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1100
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1101
lemma dist_increases_online:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1102
  fixes a b d :: "'a::real_inner"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1103
  assumes "d \<noteq> 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1104
  shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1105
proof(cases "inner a d - inner b d > 0")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1106
  case True hence "0 < inner d d + (inner a d * 2 - inner b d * 2)" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1107
    apply(rule_tac add_pos_pos) using assms by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1108
  thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1109
    by (simp add: algebra_simps inner_commute)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1110
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1111
  case False hence "0 < inner d d + (inner b d * 2 - inner a d * 2)" 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1112
    apply(rule_tac add_pos_nonneg) using assms by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1113
  thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1114
    by (simp add: algebra_simps inner_commute)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1115
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1116
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1117
lemma norm_increases_online:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1118
  fixes d :: "'a::real_inner"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1119
  shows "d \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1120
  using dist_increases_online[of d a 0] unfolding dist_norm by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1121
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1122
lemma simplex_furthest_lt:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1123
  fixes s::"'a::real_inner set" assumes "finite s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1124
  shows "\<forall>x \<in> (convex hull s).  x \<notin> s \<longrightarrow> (\<exists>y\<in>(convex hull s). norm(x - a) < norm(y - a))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1125
proof(induct_tac rule: finite_induct[of s])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1126
  fix x s assume as:"finite s" "x\<notin>s" "\<forall>x\<in>convex hull s. x \<notin> s \<longrightarrow> (\<exists>y\<in>convex hull s. norm (x - a) < norm (y - a))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1127
  show "\<forall>xa\<in>convex hull insert x s. xa \<notin> insert x s \<longrightarrow> (\<exists>y\<in>convex hull insert x s. norm (xa - a) < norm (y - a))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1128
  proof(rule,rule,cases "s = {}")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1129
    case False fix y assume y:"y \<in> convex hull insert x s" "y \<notin> insert x s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1130
    obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "y = u *\<^sub>R x + v *\<^sub>R b"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1131
      using y(1)[unfolded convex_hull_insert[OF False]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1132
    show "\<exists>z\<in>convex hull insert x s. norm (y - a) < norm (z - a)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1133
    proof(cases "y\<in>convex hull s")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1134
      case True then obtain z where "z\<in>convex hull s" "norm (y - a) < norm (z - a)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1135
        using as(3)[THEN bspec[where x=y]] and y(2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1136
      thus ?thesis apply(rule_tac x=z in bexI) unfolding convex_hull_insert[OF False] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1137
    next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1138
      case False show ?thesis  using obt(3) proof(cases "u=0", case_tac[!] "v=0")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1139
        assume "u=0" "v\<noteq>0" hence "y = b" using obt by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1140
        thus ?thesis using False and obt(4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1141
      next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1142
        assume "u\<noteq>0" "v=0" hence "y = x" using obt by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1143
        thus ?thesis using y(2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1144
      next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1145
        assume "u\<noteq>0" "v\<noteq>0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1146
        then obtain w where w:"w>0" "w<u" "w<v" using real_lbound_gt_zero[of u v] and obt(1,2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1147
        have "x\<noteq>b" proof(rule ccontr) 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1148
          assume "\<not> x\<noteq>b" hence "y=b" unfolding obt(5)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1149
            using obt(3) by(auto simp add: scaleR_left_distrib[THEN sym])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1150
          thus False using obt(4) and False by simp qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1151
        hence *:"w *\<^sub>R (x - b) \<noteq> 0" using w(1) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1152
        show ?thesis using dist_increases_online[OF *, of a y]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1153
        proof(erule_tac disjE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1154
          assume "dist a y < dist a (y + w *\<^sub>R (x - b))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1155
          hence "norm (y - a) < norm ((u + w) *\<^sub>R x + (v - w) *\<^sub>R b - a)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1156
            unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1157
          moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \<in> convex hull insert x s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1158
            unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1159
            apply(rule_tac x="u + w" in exI) apply rule defer 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1160
            apply(rule_tac x="v - w" in exI) using `u\<ge>0` and w and obt(3,4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1161
          ultimately show ?thesis by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1162
        next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1163
          assume "dist a y < dist a (y - w *\<^sub>R (x - b))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1164
          hence "norm (y - a) < norm ((u - w) *\<^sub>R x + (v + w) *\<^sub>R b - a)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1165
            unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1166
          moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \<in> convex hull insert x s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1167
            unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1168
            apply(rule_tac x="u - w" in exI) apply rule defer 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1169
            apply(rule_tac x="v + w" in exI) using `u\<ge>0` and w and obt(3,4) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1170
          ultimately show ?thesis by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1171
        qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1172
      qed auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1173
    qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1174
  qed auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1175
qed (auto simp add: assms)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1176
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1177
lemma simplex_furthest_le:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1178
  fixes s :: "('a::euclidean_space) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1179
  assumes "finite s" "s \<noteq> {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1180
  shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x - a) \<le> norm(y - a)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1181
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1182
  have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1183
  then obtain x where x:"x\<in>convex hull s" "\<forall>y\<in>convex hull s. norm (y - a) \<le> norm (x - a)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1184
    using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1185
    unfolding dist_commute[of a] unfolding dist_norm by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1186
  thus ?thesis proof(cases "x\<in>s")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1187
    case False then obtain y where "y\<in>convex hull s" "norm (x - a) < norm (y - a)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1188
      using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1189
    thus ?thesis using x(2)[THEN bspec[where x=y]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1190
  qed auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1191
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1192
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1193
lemma simplex_furthest_le_exists:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1194
  fixes s :: "('a::euclidean_space) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1195
  shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1196
  using simplex_furthest_le[of s] by (cases "s={}")auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1197
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1198
lemma simplex_extremal_le:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1199
  fixes s :: "('a::euclidean_space) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1200
  assumes "finite s" "s \<noteq> {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1201
  shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x - y) \<le> norm(u - v)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1202
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1203
  have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1204
  then obtain u v where obt:"u\<in>convex hull s" "v\<in>convex hull s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1205
    "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull s. norm (x - y) \<le> norm (u - v)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1206
    using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1207
  thus ?thesis proof(cases "u\<notin>s \<or> v\<notin>s", erule_tac disjE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1208
    assume "u\<notin>s" then obtain y where "y\<in>convex hull s" "norm (u - v) < norm (y - v)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1209
      using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1210
    thus ?thesis using obt(3)[THEN bspec[where x=y], THEN bspec[where x=v]] and obt(2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1211
  next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1212
    assume "v\<notin>s" then obtain y where "y\<in>convex hull s" "norm (v - u) < norm (y - u)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1213
      using simplex_furthest_lt[OF assms(1), THEN bspec[where x=v]] and obt(2) by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1214
    thus ?thesis using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1215
      by (auto simp add: norm_minus_commute)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1216
  qed auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1217
qed 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1218
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1219
lemma simplex_extremal_le_exists:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1220
  fixes s :: "('a::euclidean_space) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1221
  shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1222
  \<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x - y) \<le> norm(u - v))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1223
  using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1224
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1225
subsection {* Closest point of a convex set is unique, with a continuous projection. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1226
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1227
definition
36337
87b6c83d7ed7 generalize constant closest_point
huffman
parents: 36071
diff changeset
  1228
  closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a" where
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1229
 "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1230
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1231
lemma closest_point_exists:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1232
  assumes "closed s" "s \<noteq> {}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1233
  shows  "closest_point s a \<in> s" "\<forall>y\<in>s. dist a (closest_point s a) \<le> dist a y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1234
  unfolding closest_point_def apply(rule_tac[!] someI2_ex) 
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1235
  using distance_attains_inf[OF assms(1,2), of a] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1236
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1237
lemma closest_point_in_set:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1238
  "closed s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> (closest_point s a) \<in> s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1239
  by(meson closest_point_exists)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1240
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1241
lemma closest_point_le:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1242
  "closed s \<Longrightarrow> x \<in> s \<Longrightarrow> dist a (closest_point s a) \<le> dist a x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1243
  using closest_point_exists[of s] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1244
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1245
lemma closest_point_self:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1246
  assumes "x \<in> s"  shows "closest_point s x = x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1247
  unfolding closest_point_def apply(rule some1_equality, rule ex1I[of _ x])