src/HOL/Library/Convex_Euclidean_Space.thy
author himmelma
Thu, 28 May 2009 15:42:44 +0200
changeset 31279 4ae81233cf69
parent 31278 60a53b5af39c
child 31281 b4d4dbc5b04f
child 31285 0a3f9ee4117c
permissions -rw-r--r--
Corrected error in Convex_Euclidean_Space
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31276
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
     1
(* Title:      Convex
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
     2
   ID:         $Id: 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
     3
   Author:     Robert Himmelmann, TU Muenchen*)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
     4
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
     5
header {* Convex sets, functions and related things. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
     6
31278
60a53b5af39c Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
himmelma
parents: 31276
diff changeset
     7
theory Convex_Euclidean_Space
31276
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
     8
  imports Topology_Euclidean_Space
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
     9
begin
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    10
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    11
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    12
(* ------------------------------------------------------------------------- *)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    13
(* To be moved elsewhere                                                     *)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    14
(* ------------------------------------------------------------------------- *)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    15
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    16
declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    17
declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    18
declare dot_ladd[simp] dot_radd[simp] dot_lsub[simp] dot_rsub[simp]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    19
declare dot_lmult[simp] dot_rmult[simp] dot_lneg[simp] dot_rneg[simp]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    20
declare UNIV_1[simp]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    21
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    22
term "(x::real^'n \<Rightarrow> real) 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    23
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    24
lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    25
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    26
lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_less_eq_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    27
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    28
lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    29
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    30
lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    31
  uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    32
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    33
lemma dest_vec1_simps[simp]: fixes a::"real^1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    34
  shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    35
  "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    36
  by(auto simp add:vector_component_simps all_1 Cart_eq)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    37
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    38
definition 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    39
  "is_interval_new (s::((real^'n::finite) set)) \<longleftrightarrow>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    40
  (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i)))  \<longrightarrow> x \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    41
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    42
lemma is_interval_interval_new: "is_interval_new {a .. b}" (is ?th1) "is_interval_new {a<..<b}" (is ?th2) proof - 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    43
  have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    44
  show ?th1 ?th2  unfolding is_interval_new_def mem_interval Ball_def atLeastAtMost_iff
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    45
    by(meson real_le_trans le_less_trans less_le_trans *)+ qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    46
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    47
lemma nequals0I:"x\<in>A \<Longrightarrow> A \<noteq> {}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    48
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    49
lemma norm_not_0:"(x::real^'n::finite)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    50
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    51
lemma vector_unminus_smult[simp]: "(-1::real) *s x = -x" unfolding pth_3[symmetric] by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    52
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    53
lemma setsum_delta_notmem: assumes "x\<notin>s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    54
  shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    55
        "setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    56
        "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    57
        "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    58
  apply(rule_tac [!] setsum_cong2) using assms by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    59
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    60
lemma setsum_diff1'':assumes "finite A" "a \<in> A"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    61
  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)" unfolding setsum_diff1'[OF assms] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    62
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    63
lemma setsum_delta'': fixes s::"(real^'n) set" assumes "finite s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    64
  shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *s x) = (if y\<in>s then (f y) *s y else 0)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    65
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    66
  have *:"\<And>x y. (if y = x then f x else (0::real)) *s x = (if x=y then (f x) *s x else 0)" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    67
  show ?thesis unfolding * using setsum_delta[OF assms, of y "\<lambda>x. f x *s x"] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    68
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    69
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    70
lemma not_disjointI:"x\<in>A \<Longrightarrow> x\<in>B \<Longrightarrow> A \<inter> B \<noteq> {}" by blast
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    71
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    72
lemma if_smult:"(if P then x else (y::real)) *s v = (if P then x *s v else y *s v)" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    73
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    74
lemma ex_bij_betw_nat_finite_1:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    75
  assumes "finite M"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    76
  shows "\<exists>h. bij_betw h {1 .. card M} M"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    77
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    78
  obtain h where h:"bij_betw h {0..<card M} M" using ex_bij_betw_nat_finite[OF assms] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    79
  let ?h = "h \<circ> (\<lambda>i. i - 1)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    80
  have *:"(\<lambda>i. i - 1) ` {1..card M} = {0..<card M}" apply auto  unfolding image_iff apply(rule_tac x="Suc x" in bexI) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    81
  hence "?h ` {1..card M} = h ` {0..<card M}" unfolding image_compose by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    82
  hence "?h ` {1..card M} = M" unfolding image_compose using h unfolding * unfolding bij_betw_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    83
  moreover
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    84
  have "inj_on (\<lambda>i. i - Suc 0) {Suc 0..card M}" unfolding inj_on_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    85
  hence "inj_on ?h {1..card M}" apply(rule_tac comp_inj_on) unfolding * using h[unfolded bij_betw_def] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    86
  ultimately show ?thesis apply(rule_tac x="h \<circ> (\<lambda>i. i - 1)" in exI) unfolding o_def and bij_betw_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    87
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    88
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    89
lemma finite_subset_image:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    90
  assumes "B \<subseteq> f ` A" "finite B"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    91
  shows "\<exists>C\<subseteq>A. finite C \<and> B = f ` C"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    92
proof- from assms(1) have "\<forall>x\<in>B. \<exists>y\<in>A. x = f y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    93
  then obtain c where "\<forall>x\<in>B. c x \<in> A \<and> x = f (c x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    94
    using bchoice[of B "\<lambda>x y. y\<in>A \<and> x = f y"] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    95
  thus ?thesis apply(rule_tac x="c ` B" in exI) using assms(2) by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    96
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    97
lemma inj_on_image_eq_iff: assumes "inj_on f (A \<union> B)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    98
  shows "f ` A = f ` B \<longleftrightarrow> A = B"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
    99
  using assms by(blast dest: inj_onD)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   100
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   101
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   102
lemma mem_interval_1: fixes x :: "real^1" shows
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   103
 "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   104
 "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   105
by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def all_1)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   106
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   107
lemma image_smult_interval:"(\<lambda>x. m *s (x::real^'n::finite)) ` {a..b} =
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   108
  (if {a..b} = {} then {} else if 0 \<le> m then {m *s a..m *s b} else {m *s b..m *s a})"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   109
  using image_affinity_interval[of m 0 a b] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   110
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   111
lemma dest_vec1_inverval:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   112
  "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   113
  "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   114
  "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   115
  "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   116
  apply(rule_tac [!] equalityI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   117
  unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   118
  apply(rule_tac [!] allI)apply(rule_tac [!] impI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   119
  apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   120
  apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   121
  by (auto simp add: vector_less_def vector_less_eq_def all_1 dest_vec1_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   122
    vec1_dest_vec1[unfolded dest_vec1_def One_nat_def])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   123
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   124
lemma dest_vec1_setsum: assumes "finite S"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   125
  shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   126
  using dest_vec1_sum[OF assms] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   127
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   128
lemma dist_triangle_eq:"dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *s (y - z) = norm (y - z) *s (x - y)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   129
proof- have *:"x - y + (y - z) = x - z" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   130
  show ?thesis unfolding dist_def norm_triangle_eq[of "x - y" "y - z", unfolded *] 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   131
    by(auto simp add:norm_minus_commute) qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   132
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   133
lemma norm_eqI:"x = y \<Longrightarrow> norm x = norm y" by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   134
lemma norm_minus_eqI:"(x::real^'n::finite) = - y \<Longrightarrow> norm x = norm y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   135
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   136
lemma Min_grI: assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a" shows "x < Min A"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   137
  unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   138
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   139
lemma dimindex_ge_1:"CARD(_::finite) \<ge> 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   140
  using one_le_card_finite by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   141
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   142
lemma real_dimindex_ge_1:"real (CARD('n::finite)) \<ge> 1" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   143
  by(metis dimindex_ge_1 linorder_not_less real_eq_of_nat real_le_trans real_of_nat_1 real_of_nat_le_iff) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   144
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   145
lemma real_dimindex_gt_0:"real (CARD('n::finite)) > 0" apply(rule less_le_trans[OF _ real_dimindex_ge_1]) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   146
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   147
subsection {* Affine set and affine hull.*}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   148
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   149
definition "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v::real. u + v = 1 \<longrightarrow> (u *s x + v *s y) \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   150
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   151
lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *s x + u *s y \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   152
proof- have *:"\<And>u v ::real. u + v = 1 \<longleftrightarrow> v = 1 - u" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   153
  { fix x y assume "x\<in>s" "y\<in>s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   154
    hence "(\<forall>u v::real. u + v = 1 \<longrightarrow> u *s x + v *s y \<in> s) \<longleftrightarrow> (\<forall>u::real. (1 - u) *s x + u *s y \<in> s)" apply auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   155
      apply(erule_tac[!] x="1 - u" in allE) unfolding * by auto  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   156
  thus ?thesis unfolding affine_def by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   157
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   158
lemma affine_empty[intro]: "affine {}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   159
  unfolding affine_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   160
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   161
lemma affine_sing[intro]: "affine {x}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   162
  unfolding affine_alt by (auto simp add: vector_sadd_rdistrib[THEN sym]) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   163
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   164
lemma affine_UNIV[intro]: "affine UNIV"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   165
  unfolding affine_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   166
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   167
lemma affine_Inter: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter> f)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   168
  unfolding affine_def by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   169
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   170
lemma affine_Int: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   171
  unfolding affine_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   172
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   173
lemma affine_affine_hull: "affine(affine hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   174
  unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   175
  unfolding mem_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   176
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   177
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   178
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   179
  { fix f assume "f \<subseteq> affine"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   180
    hence "affine (\<Inter>f)" using affine_Inter[of f] unfolding subset_eq mem_def by auto  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   181
  thus ?thesis using hull_eq[unfolded mem_def, of affine s] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   182
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   183
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   184
lemma setsum_restrict_set'': assumes "finite A"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   185
  shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   186
  unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] ..
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   187
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   188
subsection {* Some explicit formulations (from Lars Schewe). *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   189
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   190
lemma affine: fixes V::"(real^'n) set"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   191
  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) *s x)) s \<in> V)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   192
unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   193
defer apply(rule, rule, rule, rule, rule) proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   194
  fix x y u v assume as:"x \<in> V" "y \<in> V" "u + v = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   195
    "\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *s x) \<in> V"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   196
  thus "u *s x + v *s y \<in> V" apply(cases "x=y")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   197
    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) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   198
    by(auto simp add: vector_sadd_rdistrib[THEN sym])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   199
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   200
  fix s u assume as:"\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *s x + v *s y \<in> V"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   201
    "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   202
  def n \<equiv> "card s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   203
  have "card s = 0 \<or> card s = 1 \<or> card s = 2 \<or> card s > 2" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   204
  thus "(\<Sum>x\<in>s. u x *s x) \<in> V" proof(auto simp only: disjE)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   205
    assume "card s = 2" hence "card s = Suc (Suc 0)" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   206
    then obtain a b where "s = {a, b}" unfolding card_Suc_eq by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   207
    thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   208
      by(auto simp add: setsum_clauses(2))
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   209
  next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   210
      case (Suc n) fix s::"(real^'n) set" and u::"real^'n\<Rightarrow> real"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   211
      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 *s x + v *s y \<in> V; finite s;
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   212
               s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n \<equiv> card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *s x) \<in> V" and
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   213
	as:"Suc n \<equiv> card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *s x + v *s y \<in> V"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   214
           "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   215
      have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   216
	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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   217
	thus False using as(7) and `card s > 2` by (metis Numeral1_eq1_nat less_0_number_of less_int_code(15)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   218
	  less_nat_number_of not_less_iff_gr_or_eq of_nat_1 of_nat_eq_iff pos2 rel_simps(4)) qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   219
      then obtain x where x:"x\<in>s" "u x \<noteq> 1" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   220
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   221
      have c:"card (s - {x}) = card s - 1" apply(rule card_Diff_singleton) using `x\<in>s` as(4) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   222
      have *:"s = insert x (s - {x})" "finite (s - {x})" using `x\<in>s` and as(4) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   223
      have **:"setsum u (s - {x}) = 1 - u x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   224
	using setsum_clauses(2)[OF *(2), of u x, unfolded *(1)[THEN sym] as(7)] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   225
      have ***:"inverse (1 - u x) * setsum u (s - {x}) = 1" unfolding ** using `u x \<noteq> 1` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   226
      have "(\<Sum>xa\<in>s - {x}. (inverse (1 - u x) * u xa) *s xa) \<in> V" proof(cases "card (s - {x}) > 2")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   227
	case True hence "s - {x} \<noteq> {}" "card (s - {x}) = n" unfolding c and as(1)[symmetric] proof(rule_tac ccontr) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   228
	  assume "\<not> s - {x} \<noteq> {}" hence "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   229
	  thus False using True by auto qed auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   230
	thus ?thesis apply(rule_tac IA[of "s - {x}" "\<lambda>y. (inverse (1 - u x) * u y)"])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   231
	unfolding setsum_right_distrib[THEN sym] using as and *** and True by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   232
      next case False hence "card (s - {x}) = Suc (Suc 0)" using as(2) and c by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   233
	then obtain a b where "(s - {x}) = {a, b}" "a\<noteq>b" unfolding card_Suc_eq by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   234
	thus ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   235
	  using *** *(2) and `s \<subseteq> V` unfolding setsum_right_distrib by(auto simp add: setsum_clauses(2)) qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   236
      thus "(\<Sum>x\<in>s. u x *s x) \<in> V" unfolding vector_smult_assoc[THEN sym] and setsum_cmul
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   237
 	 apply(subst *) unfolding setsum_clauses(2)[OF *(2)]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   238
	 using as(3)[THEN bspec[where x=x], THEN bspec[where x="(inverse (1 - u x)) *s (\<Sum>xa\<in>s - {x}. u xa *s xa)"], 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   239
	 THEN spec[where x="u x"], THEN spec[where x="1 - u x"]] and rev_subsetD[OF `x\<in>s` `s\<subseteq>V`] and `u x \<noteq> 1` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   240
    qed auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   241
  next assume "card s = 1" then obtain a where "s={a}" by(auto simp add: card_Suc_eq)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   242
    thus ?thesis using as(4,5) by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   243
  qed(insert `s\<noteq>{}` `finite s`, auto)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   244
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   245
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   246
lemma affine_hull_explicit:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   247
  "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) *s v) s = y}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   248
  apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   249
  apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   250
  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 *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   251
    apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   252
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   253
  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 *s v) = x" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   254
  thus "x \<in> t" using as(2)[unfolded affine, THEN spec[where x=s], THEN spec[where x=u]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   255
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   256
  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 *s v) = y}" unfolding affine_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   257
    apply(rule,rule,rule,rule,rule) unfolding mem_Collect_eq proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   258
    fix u v ::real assume uv:"u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   259
    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 *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   260
    then obtain sx ux where x:"finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "setsum ux sx = 1" "(\<Sum>v\<in>sx. ux v *s v) = x" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   261
    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 *s v) = y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   262
    then obtain sy uy where y:"finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "setsum uy sy = 1" "(\<Sum>v\<in>sy. uy v *s v) = y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   263
    have xy:"finite (sx \<union> sy)" using x(1) y(1) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   264
    have **:"(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   265
    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 *s v) = u *s x + v *s y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   266
      apply(rule_tac x="sx \<union> sy" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   267
      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)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   268
      unfolding vector_sadd_rdistrib setsum_addf if_smult vector_smult_lzero  ** setsum_restrict_set[OF xy, THEN sym]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   269
      unfolding vector_smult_assoc[THEN sym] setsum_cmul and setsum_right_distrib[THEN sym]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   270
      unfolding x y using x(1-3) y(1-3) uv by simp qed qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   271
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   272
lemma affine_hull_finite:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   273
  assumes "finite s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   274
  shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *s v) s = y}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   275
  unfolding affine_hull_explicit and expand_set_eq and mem_Collect_eq apply (rule,rule)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   276
  apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   277
  fix x u assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   278
  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 *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   279
    apply(rule_tac x=s in exI, rule_tac x=u in exI) using assms by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   280
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   281
  fix x t u assume "t \<subseteq> s" hence *:"s \<inter> t = t" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   282
  assume "finite t" "\<not> (\<forall>x. (x \<in> t) = (x \<in> {}))" "setsum u t = 1" "(\<Sum>v\<in>t. u v *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   283
  thus "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *s v) = x" apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   284
    unfolding if_smult vector_smult_lzero and setsum_restrict_set[OF assms, THEN sym] and * by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   285
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   286
subsection {* Stepping theorems and hence small special cases. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   287
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   288
lemma affine_hull_empty[simp]: "affine hull {} = {}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   289
  apply(rule hull_unique) unfolding mem_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   290
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   291
lemma affine_hull_finite_step:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   292
  shows "(\<exists>u::real^'n=>real. setsum u {} = w \<and> setsum (\<lambda>x. u x *s x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   293
  "finite s \<Longrightarrow> (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *s x) (insert a s) = y) \<longleftrightarrow>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   294
                (\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *s x) s = y - v *s a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   295
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   296
  show ?th1 by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   297
  assume ?as 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   298
  { assume ?lhs
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   299
    then obtain u where u:"setsum u (insert a s) = w \<and> (\<Sum>x\<in>insert a s. u x *s x) = y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   300
    have ?rhs proof(cases "a\<in>s")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   301
      case True hence *:"insert a s = s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   302
      show ?thesis using u[unfolded *] apply(rule_tac x=0 in exI) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   303
    next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   304
      case False thus ?thesis apply(rule_tac x="u a" in exI) using u and `?as` by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   305
    qed  } moreover
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   306
  { assume ?rhs
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   307
    then obtain v u where vu:"setsum u s = w - v"  "(\<Sum>x\<in>s. u x *s x) = y - v *s a" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   308
    have *:"\<And>x M. (if x = a then v else M) *s x = (if x = a then v *s x else M *s x)" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   309
    have ?lhs proof(cases "a\<in>s")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   310
      case True thus ?thesis
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   311
	apply(rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   312
	unfolding setsum_clauses(2)[OF `?as`]  apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   313
	unfolding vector_sadd_rdistrib and setsum_addf 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   314
	unfolding vu and * and pth_4(1)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   315
	by (auto simp add: setsum_delta[OF `?as`])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   316
    next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   317
      case False 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   318
      hence **:"\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   319
               "\<And>x. x \<in> s \<Longrightarrow> u x *s x = (if x = a then v *s x else u x *s x)" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   320
      from False show ?thesis
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   321
	apply(rule_tac x="\<lambda>x. if x=a then v else u x" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   322
	unfolding setsum_clauses(2)[OF `?as`] and * using vu
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   323
	using setsum_cong2[of s "\<lambda>x. u x *s x" "\<lambda>x. if x = a then v *s x else u x *s x", OF **(2)]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   324
	using setsum_cong2[of s u "\<lambda>x. if x = a then v else u x", OF **(1)] by auto  
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   325
    qed }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   326
  ultimately show "?lhs = ?rhs" by blast
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   327
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   328
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   329
lemma affine_hull_2: "affine hull {a,b::real^'n} = {u *s a + v *s b| u v. (u + v = 1)}" (is "?lhs = ?rhs")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   330
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   331
  have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   332
         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real^'n)" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   333
  have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *s v) = y}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   334
    using affine_hull_finite[of "{a,b}"] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   335
  also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *s b = y - v *s a}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   336
    by(simp add: affine_hull_finite_step(2)[of "{b}" a]) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   337
  also have "\<dots> = ?rhs" unfolding * by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   338
  finally show ?thesis by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   339
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   340
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   341
lemma affine_hull_3: "affine hull {a,b,c::real^'n} = { u *s a + v *s b + w *s c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   342
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   343
  have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   344
         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real^'n)" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   345
  show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   346
    unfolding * apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   347
    apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   348
    apply(rule_tac x=u in exI) by(auto intro!: exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   349
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   350
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   351
subsection {* Some relations between affine hull and subspaces. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   352
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   353
lemma affine_hull_insert_subset_span:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   354
  "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   355
  unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   356
  apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   357
  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 *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   358
  have "(\<lambda>x. x - a) ` (t - {a}) \<subseteq> {x - a |x. x \<in> s}" using as(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   359
  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 *s v) = v)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   360
    apply(rule_tac x="x - a" in exI) apply rule defer apply(rule_tac x="(\<lambda>x. x - a) ` (t - {a})" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   361
    apply(rule_tac x="\<lambda>x. u (x + a)" in exI) using as(1)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   362
    apply(simp add: setsum_reindex[unfolded inj_on_def] setsum_subtractf setsum_diff1 setsum_vmul[THEN sym])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   363
    unfolding as by simp_all qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   364
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   365
lemma affine_hull_insert_span:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   366
  assumes "a \<notin> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   367
  shows "affine hull (insert a s) =
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   368
            {a + v | v . v \<in> span {x - a | x.  x \<in> s}}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   369
  apply(rule, rule affine_hull_insert_subset_span) unfolding subset_eq Ball_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   370
  unfolding affine_hull_explicit and mem_Collect_eq proof(rule,rule,erule exE,erule conjE)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   371
  fix y v assume "y = a + v" "v \<in> span {x - a |x. x \<in> s}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   372
  then obtain t u where obt:"finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *s v) = y" unfolding span_explicit by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   373
  def f \<equiv> "(\<lambda>x. x + a) ` t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   374
  have f:"finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v - a) *s (v - a)) = y - a" unfolding f_def using obt 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   375
    by(auto simp add: setsum_reindex[unfolded inj_on_def])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   376
  have *:"f \<inter> {a} = {}" "f \<inter> - {a} = f" using f(2) assms by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   377
  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 *s v) = y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   378
    apply(rule_tac x="insert a f" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   379
    apply(rule_tac x="\<lambda>x. if x=a then 1 - setsum (\<lambda>x. u (x - a)) f else u (x - a)" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   380
    using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   381
    unfolding setsum_cases[OF f(1), of "{a}", unfolded singleton_iff] and *
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   382
    by (auto simp add: setsum_subtractf setsum_vmul field_simps) qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   383
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   384
lemma affine_hull_span:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   385
  assumes "a \<in> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   386
  shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   387
  using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   388
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   389
subsection {* Convexity. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   390
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   391
definition "convex (s::(real^'n) set) \<longleftrightarrow>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   392
        (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. (u + v = 1) \<longrightarrow> (u *s x + v *s y) \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   393
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   394
lemma convex_alt: "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> ((1 - u) *s x + u *s y) \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   395
proof- have *:"\<And>u v::real. u + v = 1 \<longleftrightarrow> u = 1 - v" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   396
  show ?thesis unfolding convex_def apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   397
    apply(erule_tac x=x in ballE) apply(erule_tac x=y in ballE) apply(erule_tac x="1 - u" in allE)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   398
    by (auto simp add: *) qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   399
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   400
lemma mem_convex:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   401
  assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   402
  shows "((1 - u) *s a + u *s b) \<in> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   403
  using assms unfolding convex_alt by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   404
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   405
lemma convex_empty[intro]: "convex {}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   406
  unfolding convex_def by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   407
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   408
lemma convex_singleton[intro]: "convex {a}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   409
  unfolding convex_def by (auto simp add:vector_sadd_rdistrib[THEN sym])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   410
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   411
lemma convex_UNIV[intro]: "convex UNIV"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   412
  unfolding convex_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   413
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   414
lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   415
  unfolding convex_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   416
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   417
lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   418
  unfolding convex_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   419
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   420
lemma convex_halfspace_le: "convex {x. a \<bullet> x \<le> b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   421
  unfolding convex_def apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   422
  unfolding dot_radd dot_rmult by (metis real_convex_bound_le) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   423
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   424
lemma convex_halfspace_ge: "convex {x. a \<bullet> x \<ge> b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   425
proof- have *:"{x. a \<bullet> x \<ge> b} = {x. -a \<bullet> x \<le> -b}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   426
  show ?thesis apply(unfold *) using convex_halfspace_le[of "-a" "-b"] by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   427
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   428
lemma convex_hyperplane: "convex {x. a \<bullet> x = b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   429
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   430
  have *:"{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   431
  show ?thesis unfolding * apply(rule convex_Int)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   432
    using convex_halfspace_le convex_halfspace_ge by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   433
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   434
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   435
lemma convex_halfspace_lt: "convex {x. a \<bullet> x < b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   436
  unfolding convex_def by(auto simp add: real_convex_bound_lt dot_radd dot_rmult)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   437
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   438
lemma convex_halfspace_gt: "convex {x. a \<bullet> x > b}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   439
   using convex_halfspace_lt[of "-a" "-b"] by(auto simp add: dot_lneg neg_less_iff_less)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   440
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   441
lemma convex_positive_orthant: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   442
  unfolding convex_def apply auto apply(erule_tac x=i in allE)+
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   443
  apply(rule add_nonneg_nonneg) by(auto simp add: mult_nonneg_nonneg)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   444
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   445
subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   446
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   447
lemma convex: "convex s \<longleftrightarrow>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   448
  (\<forall>(k::nat) u x. (\<forall>i. 1\<le>i \<and> i\<le>k \<longrightarrow> 0 \<le> u i \<and> x i \<in>s) \<and> (setsum u {1..k} = 1)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   449
           \<longrightarrow> setsum (\<lambda>i. u i *s x i) {1..k} \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   450
  unfolding convex_def apply rule apply(rule allI)+ defer apply(rule ballI)+ apply(rule allI)+ proof(rule,rule,rule,rule)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   451
  fix x y u v assume as:"\<forall>(k::nat) u x. (\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow> (\<Sum>i = 1..k. u i *s x i) \<in> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   452
    "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   453
  show "u *s x + v *s y \<in> s" using as(1)[THEN spec[where x=2], THEN spec[where x="\<lambda>n. if n=1 then u else v"], THEN spec[where x="\<lambda>n. if n=1 then x else y"]] and as(2-)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   454
    by (auto simp add: setsum_head_Suc) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   455
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   456
  fix k u x assume as:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *s x + v *s y \<in> s" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   457
  show "(\<forall>i::nat. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow> (\<Sum>i = 1..k. u i *s x i) \<in> s" apply(rule,erule conjE) proof(induct k arbitrary: u)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   458
  case (Suc k) show ?case proof(cases "u (Suc k) = 1")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   459
    case True hence "(\<Sum>i = Suc 0..k. u i *s x i) = 0" apply(rule_tac setsum_0') apply(rule ccontr) unfolding ball_simps apply(erule bexE) proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   460
      fix i assume i:"i \<in> {Suc 0..k}" "u i *s x i \<noteq> 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   461
      hence ui:"u i \<noteq> 0" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   462
      hence "setsum (\<lambda>k. if k=i then u i else 0) {1 .. k} \<le> setsum u {1 .. k}" apply(rule_tac setsum_mono) using Suc(2) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   463
      hence "setsum u {1 .. k} \<ge> u i" using i(1) by(auto simp add: setsum_delta) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   464
      hence "setsum u {1 .. k} > 0"  using ui apply(rule_tac less_le_trans[of _ "u i"]) using Suc(2)[THEN spec[where x=i]] and i(1) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   465
      thus False using Suc(3) unfolding setsum_cl_ivl_Suc and True by simp qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   466
    thus ?thesis unfolding setsum_cl_ivl_Suc using True and Suc(2) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   467
  next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   468
    have *:"setsum u {1..k} = 1 - u (Suc k)" using Suc(3)[unfolded setsum_cl_ivl_Suc] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   469
    have **:"u (Suc k) \<le> 1" apply(rule ccontr) unfolding not_le using Suc(3) using setsum_nonneg[of "{1..k}" u] using Suc(2) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   470
    have ***:"\<And>i k. (u i / (1 - u (Suc k))) *s x i = (inverse (1 - u (Suc k))) *s (u i *s x i)" unfolding real_divide_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   471
    case False hence nn:"1 - u (Suc k) \<noteq> 0" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   472
    have "(\<Sum>i = 1..k. (u i / (1 - u (Suc k))) *s x i) \<in> s" apply(rule Suc(1)) unfolding setsum_divide_distrib[THEN sym] and *
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   473
      apply(rule_tac allI) apply(rule,rule) apply(rule divide_nonneg_pos) using nn Suc(2) ** by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   474
    hence "(1 - u (Suc k)) *s (\<Sum>i = 1..k. (u i / (1 - u (Suc k))) *s x i) + u (Suc k) *s x (Suc k) \<in> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   475
      apply(rule as[THEN bspec, THEN bspec, THEN spec, THEN mp, THEN spec, THEN mp, THEN mp]) using Suc(2)[THEN spec[where x="Suc k"]] and ** by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   476
    thus ?thesis unfolding setsum_cl_ivl_Suc and *** and setsum_cmul using nn by auto qed qed auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   477
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   478
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   479
lemma convex_explicit: "convex (s::(real^'n) set) \<longleftrightarrow>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   480
  (\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> setsum (\<lambda>x. u x *s x) t \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   481
  unfolding convex_def apply(rule,rule,rule) apply(subst imp_conjL,rule) defer apply(rule,rule,rule,rule,rule,rule,rule) proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   482
  fix x y u v assume as:"\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *s x) \<in> s" "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   483
  show "u *s x + v *s y \<in> s" proof(cases "x=y")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   484
    case True show ?thesis unfolding True and vector_sadd_rdistrib[THEN sym] using as(3,6) by auto next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   485
    case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>z. if z=x then u else v"]] and as(2-) by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   486
next 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   487
  fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *s x + v *s y \<in> s" "finite (t::(real^'n) set)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   488
  (*"finite t" "t \<subseteq> s" "\<forall>x\<in>t. (0::real) \<le> u x" "setsum u t = 1"*)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   489
  from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *s x) \<in> s" apply(induct_tac t rule:finite_induct)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   490
    prefer 3 apply (rule,rule) apply(erule conjE)+ proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   491
    fix x f u assume ind:"\<forall>u. f \<subseteq> s \<and> (\<forall>x\<in>f. 0 \<le> u x) \<and> setsum u f = 1 \<longrightarrow> (\<Sum>x\<in>f. u x *s x) \<in> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   492
    assume as:"finite f" "x \<notin> f" "insert x f \<subseteq> s" "\<forall>x\<in>insert x f. 0 \<le> u x" "setsum u (insert x f) = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   493
    show "(\<Sum>x\<in>insert x f. u x *s x) \<in> s" proof(cases "u x = 1")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   494
      case True hence "setsum (\<lambda>x. u x *s x) f = 0" apply(rule_tac setsum_0') apply(rule ccontr) unfolding ball_simps apply(erule bexE) proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   495
	fix y assume y:"y \<in> f" "u y *s y \<noteq> 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   496
	hence uy:"u y \<noteq> 0" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   497
	hence "setsum (\<lambda>k. if k=y then u y else 0) f \<le> setsum u f" apply(rule_tac setsum_mono) using as(4) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   498
	hence "setsum u f \<ge> u y" using y(1) and as(1) by(auto simp add: setsum_delta) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   499
	hence "setsum u f > 0" using uy apply(rule_tac less_le_trans[of _ "u y"]) using as(4) and y(1) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   500
	thus False using as(2,5) unfolding setsum_clauses(2)[OF as(1)] and True by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   501
      thus ?thesis unfolding setsum_clauses(2)[OF as(1)] using as(2,3) unfolding True by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   502
    next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   503
      have *:"setsum u f = setsum u (insert x f) - u x" using as(2) unfolding setsum_clauses(2)[OF as(1)] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   504
      have **:"u x \<le> 1" apply(rule ccontr) unfolding not_le using as(5)[unfolded setsum_clauses(2)[OF as(1)]] and as(2)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   505
	using setsum_nonneg[of f u] and as(4) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   506
      case False hence "inverse (1 - u x) *s (\<Sum>x\<in>f. u x *s x) \<in> s" unfolding setsum_cmul[THEN sym] and vector_smult_assoc
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   507
	apply(rule_tac ind[THEN spec, THEN mp]) apply rule defer apply rule apply rule apply(rule mult_nonneg_nonneg)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   508
	unfolding setsum_right_distrib[THEN sym] and * using as and ** by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   509
      hence "u x *s x + (1 - u x) *s ((inverse (1 - u x)) *s setsum (\<lambda>x. u x *s x) f) \<in>s" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   510
	apply(rule_tac asm(1)[THEN bspec, THEN bspec, THEN spec, THEN mp, THEN spec, THEN mp, THEN mp]) using as and ** False by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   511
      thus ?thesis unfolding setsum_clauses(2)[OF as(1)] using as(2) and False by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   512
  qed auto thus "t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *s x) \<in> s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   513
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   514
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   515
lemma convex_finite: assumes "finite s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   516
  shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   517
                      \<longrightarrow> setsum (\<lambda>x. u x *s x) s \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   518
  unfolding convex_explicit apply(rule, rule, rule) defer apply(rule,rule,rule)apply(erule conjE)+ proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   519
  fix t u assume as:"\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *s x) \<in> s" " finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   520
  have *:"s \<inter> t = t" using as(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   521
  show "(\<Sum>x\<in>t. u x *s x) \<in> s" using as(1)[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   522
    unfolding if_smult and setsum_cases[OF assms] and * using as(2-) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   523
qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   524
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   525
subsection {* Cones. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   526
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   527
definition "cone (s::(real^'n) set) \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *s x) \<in> s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   528
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   529
lemma cone_empty[intro, simp]: "cone {}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   530
  unfolding cone_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   531
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   532
lemma cone_univ[intro, simp]: "cone UNIV"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   533
  unfolding cone_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   534
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   535
lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   536
  unfolding cone_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   537
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   538
subsection {* Conic hull. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   539
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   540
lemma cone_cone_hull: "cone (cone hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   541
  unfolding hull_def using cone_Inter[of "{t \<in> conic. s \<subseteq> t}"] 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   542
  by (auto simp add: mem_def)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   543
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   544
lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   545
  apply(rule hull_eq[unfolded mem_def])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   546
  using cone_Inter unfolding subset_eq by (auto simp add: mem_def)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   547
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   548
subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   549
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   550
definition "affine_dependent (s::(real^'n) set) \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   551
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   552
lemma affine_dependent_explicit:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   553
  "affine_dependent p \<longleftrightarrow>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   554
    (\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   555
    (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *s v) s = 0)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   556
  unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq apply(rule)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   557
  apply(erule bexE,erule exE,erule exE) apply(erule conjE)+ defer apply(erule exE,erule exE) apply(erule conjE)+ apply(erule bexE)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   558
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   559
  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 *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   560
  have "x\<notin>s" using as(1,4) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   561
  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 *s v) = 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   562
    apply(rule_tac x="insert x s" in exI, rule_tac x="\<lambda>v. if v = x then - 1 else u v" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   563
    unfolding if_smult and setsum_clauses(2)[OF as(2)] and setsum_delta_notmem[OF `x\<notin>s`] and as using as by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   564
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   565
  fix s u v assume as:"finite s" "s \<subseteq> p" "setsum u s = 0" "(\<Sum>v\<in>s. u v *s v) = 0" "v \<in> s" "u v \<noteq> 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   566
  have "s \<noteq> {v}" using as(3,6) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   567
  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 *s v) = x" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   568
    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)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   569
    unfolding vector_smult_assoc[THEN sym] and setsum_cmul unfolding setsum_right_distrib[THEN sym] and setsum_diff1''[OF as(1,5)] using as by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   570
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   571
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   572
lemma affine_dependent_explicit_finite:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   573
  assumes "finite (s::(real^'n) set)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   574
  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 *s v) s = 0)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   575
  (is "?lhs = ?rhs")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   576
proof
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   577
  have *:"\<And>vt u v. (if vt then u v else 0) *s v = (if vt then (u v) *s v else (0::real^'n))" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   578
  assume ?lhs
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   579
  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 *s v) = 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   580
    unfolding affine_dependent_explicit by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   581
  thus ?rhs apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   582
    apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   583
    unfolding Int_absorb2[OF `t\<subseteq>s`, unfolded Int_commute] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   584
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   585
  assume ?rhs
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   586
  then obtain u v where "setsum u s = 0"  "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *s v) = 0" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   587
  thus ?lhs unfolding affine_dependent_explicit using assms by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   588
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   589
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   590
subsection {* A general lemma. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   591
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   592
lemma convex_connected:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   593
  assumes "convex s" shows "connected s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   594
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   595
  { fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   596
    assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   597
    then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   598
    hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   599
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   600
    { fix x e::real assume as:"0 \<le> x" "x \<le> 1" "0 < e"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   601
      { fix y have *:"(1 - x) *s x1 + x *s x2 - ((1 - y) *s x1 + y *s x2) = (y - x) *s x1 - (y - x) *s x2"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   602
	  by(simp add: ring_simps vector_sadd_rdistrib vector_sub_rdistrib)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   603
	assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   604
	hence "norm ((1 - x) *s x1 + x *s x2 - ((1 - y) *s x1 + y *s x2)) < e"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   605
	  unfolding * and vector_ssub_ldistrib[THEN sym] and norm_mul 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   606
	  unfolding less_divide_eq using n by auto  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   607
      hence "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *s x1 + x *s x2 - ((1 - y) *s x1 + y *s x2)) < e"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   608
	apply(rule_tac x="e / norm (x1 - x2)" in exI) using as
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   609
	apply auto unfolding zero_less_divide_iff using n by simp  }  note * = this
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   610
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   611
    have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e2"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   612
      apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_sym)+
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   613
      using * apply(simp add: dist_def)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   614
      using as(1,2)[unfolded open_def] apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   615
      using as(1,2)[unfolded open_def] apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   616
      using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   617
      using as(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   618
    then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *s x1 + x *s x2 \<notin> e1"  "(1 - x) *s x1 + x *s x2 \<notin> e2" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   619
    hence False using as(4) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   620
      using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   621
      using x1(2) x2(2) by auto  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   622
  thus ?thesis unfolding connected_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   623
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   624
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   625
subsection {* One rather trivial consequence. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   626
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   627
lemma connected_UNIV: "connected UNIV"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   628
  by(simp add: convex_connected convex_UNIV)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   629
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   630
subsection {* Convex functions into the reals. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   631
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   632
definition "convex_on s (f::real^'n \<Rightarrow> real) = 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   633
  (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *s x + v *s y) \<le> u * f x + v * f y)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   634
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   635
lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   636
  unfolding convex_on_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   637
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   638
lemma convex_add:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   639
  assumes "convex_on s f" "convex_on s g"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   640
  shows "convex_on s (\<lambda>x. f x + g x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   641
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   642
  { fix x y assume "x\<in>s" "y\<in>s" moreover
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   643
    fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   644
    ultimately have "f (u *s x + v *s y) + g (u *s x + v *s y) \<le> (u * f x + v * f y) + (u * g x + v * g y)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   645
      using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   646
      using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   647
      apply - apply(rule add_mono) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   648
    hence "f (u *s x + v *s y) + g (u *s x + v *s y) \<le> u * (f x + g x) + v * (f y + g y)" by (simp add: ring_simps)  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   649
  thus ?thesis unfolding convex_on_def by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   650
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   651
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   652
lemma convex_cmul: 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   653
  assumes "0 \<le> (c::real)" "convex_on s f"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   654
  shows "convex_on s (\<lambda>x. c * f x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   655
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   656
  have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: ring_simps)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   657
  show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   658
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   659
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   660
lemma convex_lower:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   661
  assumes "convex_on s f"  "x\<in>s"  "y \<in> s"  "0 \<le> u"  "0 \<le> v"  "u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   662
  shows "f (u *s x + v *s y) \<le> max (f x) (f y)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   663
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   664
  let ?m = "max (f x) (f y)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   665
  have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)" apply(rule add_mono) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   666
    using assms(4,5) by(auto simp add: mult_mono1)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   667
  also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   668
  finally show ?thesis using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   669
    using assms(2-6) by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   670
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   671
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   672
lemma convex_local_global_minimum:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   673
  assumes "0<e" "convex_on s f" "ball x e \<subseteq> s" "\<forall>y\<in>ball x e. f x \<le> f y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   674
  shows "\<forall>y\<in>s. f x \<le> f y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   675
proof(rule ccontr)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   676
  have "x\<in>s" using assms(1,3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   677
  assume "\<not> (\<forall>y\<in>s. f x \<le> f y)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   678
  then obtain y where "y\<in>s" and y:"f x > f y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   679
  hence xy:"0 < dist x y" by (auto simp add: dist_nz[THEN sym])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   680
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   681
  then obtain u where "0 < u" "u \<le> 1" and u:"u < e / dist x y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   682
    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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   683
  hence "f ((1-u) *s x + u *s y) \<le> (1-u) * f x + u * f y" using `x\<in>s` `y\<in>s`
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   684
    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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   685
  moreover
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   686
  have *:"x - ((1 - u) *s x + u *s y) = u *s (x - y)" by (simp add: vector_ssub_ldistrib vector_sub_rdistrib)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   687
  have "(1 - u) *s x + u *s y \<in> ball x e" unfolding mem_ball dist_def unfolding * and norm_mul and abs_of_pos[OF `0<u`] unfolding dist_def[THEN sym]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   688
    using u unfolding pos_less_divide_eq[OF xy] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   689
  hence "f x \<le> f ((1 - u) *s x + u *s y)" using assms(4) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   690
  ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   691
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   692
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   693
lemma convex_distance: "convex_on s (\<lambda>x. dist a x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   694
proof(auto simp add: convex_on_def dist_def)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   695
  fix x y assume "x\<in>s" "y\<in>s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   696
  fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   697
  have "a = u *s a + v *s a" unfolding vector_sadd_rdistrib[THEN sym] and `u+v=1` by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   698
  hence *:"a - (u *s x + v *s y) = (u *s (a - x)) + (v *s (a - y))" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   699
  show "norm (a - (u *s x + v *s y)) \<le> u * norm (a - x) + v * norm (a - y)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   700
    unfolding * using norm_triangle_ineq[of "u *s (a - x)" "v *s (a - y)"] unfolding norm_mul
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   701
    using `0 \<le> u` `0 \<le> v` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   702
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   703
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   704
subsection {* Arithmetic operations on sets preserve convexity. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   705
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   706
lemma convex_scaling: "convex s \<Longrightarrow> convex ((\<lambda>x. c *s x) ` s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   707
  unfolding convex_def and image_iff apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   708
  apply (rule_tac x="u *s x+v *s y" in bexI) by (auto simp add: field_simps)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   709
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   710
lemma convex_negations: "convex s \<Longrightarrow> convex ((\<lambda>x. -x)` s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   711
  unfolding convex_def and image_iff apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   712
  apply (rule_tac x="u *s x+v *s y" in bexI) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   713
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   714
lemma convex_sums:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   715
  assumes "convex s" "convex t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   716
  shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   717
proof(auto simp add: convex_def image_iff)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   718
  fix xa xb ya yb assume xy:"xa\<in>s" "xb\<in>s" "ya\<in>t" "yb\<in>t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   719
  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   720
  show "\<exists>x y. u *s xa + u *s ya + (v *s xb + v *s yb) = x + y \<and> x \<in> s \<and> y \<in> t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   721
    apply(rule_tac x="u *s xa + v *s xb" in exI) apply(rule_tac x="u *s ya + v *s yb" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   722
    using assms(1)[unfolded convex_def, THEN bspec[where x=xa], THEN bspec[where x=xb]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   723
    using assms(2)[unfolded convex_def, THEN bspec[where x=ya], THEN bspec[where x=yb]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   724
    using uv xy by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   725
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   726
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   727
lemma convex_differences: 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   728
  assumes "convex s" "convex t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   729
  shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   730
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   731
  have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}" unfolding image_iff apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   732
    apply(rule_tac x=xa in exI) apply(rule_tac x="-y" in exI) apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   733
    apply(rule_tac x=xa in exI) apply(rule_tac x=xb in exI) by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   734
  thus ?thesis using convex_sums[OF assms(1)  convex_negations[OF assms(2)]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   735
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   736
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   737
lemma convex_translation: assumes "convex s" shows "convex ((\<lambda>x. a + x) ` s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   738
proof- have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   739
  thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   740
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   741
lemma convex_affinity: assumes "convex (s::(real^'n) set)" shows "convex ((\<lambda>x. a + c *s x) ` s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   742
proof- have "(\<lambda>x. a + c *s x) ` s = op + a ` op *s c ` s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   743
  thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   744
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   745
lemma convex_linear_image: assumes c:"convex s" and l:"linear f" shows "convex(f ` s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   746
proof(auto simp add: convex_def)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   747
  fix x y assume xy:"x \<in> s" "y \<in> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   748
  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   749
  show "u *s f x + v *s f y \<in> f ` s" unfolding image_iff
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   750
    apply(rule_tac x="u *s x + v *s y" in bexI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   751
    unfolding linear_add[OF l] linear_cmul[OF l] 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   752
    using c[unfolded convex_def] xy uv by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   753
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   754
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   755
subsection {* Balls, being convex, are connected. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   756
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   757
lemma convex_ball: "convex (ball x e)" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   758
proof(auto simp add: convex_def)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   759
  fix y z assume yz:"dist x y < e" "dist x z < e"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   760
  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   761
  have "dist x (u *s y + v *s z) \<le> u * dist x y + v * dist x z" using uv yz
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   762
    using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   763
  thus "dist x (u *s y + v *s z) < e" using real_convex_bound_lt[OF yz uv] by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   764
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   765
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   766
lemma convex_cball: "convex(cball x e)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   767
proof(auto simp add: convex_def Ball_def mem_cball)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   768
  fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   769
  fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   770
  have "dist x (u *s y + v *s z) \<le> u * dist x y + v * dist x z" using uv yz
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   771
    using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   772
  thus "dist x (u *s y + v *s z) \<le> e" using real_convex_bound_le[OF yz uv] by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   773
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   774
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   775
lemma connected_ball: "connected(ball x e)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   776
  using convex_connected convex_ball by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   777
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   778
lemma connected_cball: "connected(cball x e)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   779
  using convex_connected convex_cball by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   780
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   781
subsection {* Convex hull. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   782
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   783
lemma convex_convex_hull: "convex(convex hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   784
  unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   785
  unfolding mem_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   786
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   787
lemma convex_hull_eq: "(convex hull s = s) \<longleftrightarrow> convex s" apply(rule hull_eq[unfolded mem_def])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   788
  using convex_Inter[unfolded Ball_def mem_def] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   789
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   790
lemma bounded_convex_hull: assumes "bounded s" shows "bounded(convex hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   791
proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   792
  show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   793
    unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   794
    unfolding subset_eq mem_cball dist_def using B by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   795
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   796
lemma finite_imp_bounded_convex_hull:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   797
  "finite s \<Longrightarrow> bounded(convex hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   798
  using bounded_convex_hull finite_imp_bounded by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   799
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   800
subsection {* Stepping theorems for convex hulls of finite sets. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   801
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   802
lemma convex_hull_empty[simp]: "convex hull {} = {}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   803
  apply(rule hull_unique) unfolding mem_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   804
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   805
lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   806
  apply(rule hull_unique) unfolding mem_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   807
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   808
lemma convex_hull_insert:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   809
  assumes "s \<noteq> {}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   810
  shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   811
                                    b \<in> (convex hull s) \<and> (x = u *s a + v *s b)}" (is "?xyz = ?hull")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   812
 apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   813
 fix x assume x:"x = a \<or> x \<in> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   814
 thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   815
   apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   816
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   817
  fix x assume "x\<in>?hull"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   818
  then obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *s a + v *s b" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   819
  have "a\<in>convex hull insert a s" "b\<in>convex hull insert a s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   820
    using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   821
  thus "x\<in> convex hull insert a s" unfolding obt(5) using convex_convex_hull[of "insert a s", unfolded convex_def]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   822
    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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   823
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   824
  show "convex ?hull" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   825
    fix x y u v assume as:"(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   826
    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 *s a + v1 *s b1" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   827
    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 *s a + v2 *s b2" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   828
    have *:"\<And>x s1 s2. x - s1 *s x - s2 *s x = ((1::real) - (s1 + s2)) *s x" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   829
    have "\<exists>b \<in> convex hull s. u *s x + v *s y = (u * u1) *s a + (v * u2) *s a + (b - (u * u1) *s b - (v * u2) *s b)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   830
    proof(cases "u * v1 + v * v2 = 0")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   831
      have *:"\<And>x s1 s2. x - s1 *s x - s2 *s x = ((1::real) - (s1 + s2)) *s x" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   832
      case True hence **:"u * v1 = 0" "v * v2 = 0" apply- apply(rule_tac [!] ccontr)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   833
	using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   834
      hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   835
      thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: **) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   836
    next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   837
      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)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   838
      also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   839
      also have "\<dots> = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   840
      case False have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2" apply -
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   841
	apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   842
	using as(1,2) obt1(1,2) obt2(1,2) by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   843
      thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   844
	apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *s b1 + ((v * v2) / (u * v1 + v * v2)) *s b2" in bexI) defer
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   845
	apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   846
	unfolding add_divide_distrib[THEN sym] and real_0_le_divide_iff by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   847
    qed note * = this
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   848
    have u1:"u1 \<le> 1" apply(rule ccontr) unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   849
    have u2:"u2 \<le> 1" apply(rule ccontr) unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   850
    have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   851
      apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   852
    also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   853
    finally 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   854
    show "u *s x + v *s y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   855
      apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   856
      using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add:field_simps)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   857
  qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   858
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   859
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   860
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   861
subsection {* Explicit expression for convex hull. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   862
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   863
lemma convex_hull_indexed:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   864
  "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   865
                            (setsum u {1..k} = 1) \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   866
                            (setsum (\<lambda>i. u i *s x i) {1..k} = y)}" (is "?xyz = ?hull")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   867
  apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   868
  apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   869
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   870
  fix x assume "x\<in>s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   871
  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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   872
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   873
  fix t assume as:"s \<subseteq> t" "convex t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   874
  show "?hull \<subseteq> t" apply(rule) unfolding mem_Collect_eq apply(erule exE | erule conjE)+ proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   875
    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 *s y i) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   876
    show "x\<in>t" unfolding assm(3)[THEN sym] apply(rule as(2)[unfolded convex, rule_format])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   877
      using assm(1,2) as(1) by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   878
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   879
  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"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   880
  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 *s x1 i) = x" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   881
  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 *s x2 i) = y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   882
  have *:"\<And>P x1 x2 s1 s2 i.(if P i then s1 else s2) *s (if P i then x1 else x2) = (if P i then s1 *s x1 else s2 *s x2)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   883
    "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   884
    prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   885
  have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto  
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   886
  show "u *s x + v *s y \<in> ?hull" apply(rule)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   887
    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)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   888
    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)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   889
    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   890
    unfolding vector_smult_assoc[THEN sym] setsum_cmul setsum_right_distrib[THEN sym] proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   891
    fix i assume i:"i \<in> {1..k1+k2}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   892
    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"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   893
    proof(cases "i\<in>{1..k1}")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   894
      case True thus ?thesis using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   895
    next def j \<equiv> "i - k1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   896
      case False with i have "j \<in> {1..k2}" unfolding j_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   897
      thus ?thesis unfolding j_def[symmetric] using False
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   898
	using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   899
  qed(auto simp add: not_le x(2,3) y(2,3) uv(3))
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   900
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   901
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   902
lemma convex_hull_finite:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   903
  assumes "finite (s::(real^'n)set)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   904
  shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   905
         setsum u s = 1 \<and> setsum (\<lambda>x. u x *s x) s = y}" (is "?HULL = ?set")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   906
proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   907
  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 *s x) = x" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   908
    apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   909
    unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   910
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   911
  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   912
  fix ux assume ux:"\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   913
  fix uy assume uy:"\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   914
  { fix x assume "x\<in>s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   915
    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)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   916
      by (auto, metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   917
  moreover have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   918
    unfolding setsum_addf and setsum_right_distrib[THEN sym] and ux(2) uy(2) using uv(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   919
  moreover have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *s x) = u *s (\<Sum>x\<in>s. ux x *s x) + v *s (\<Sum>x\<in>s. uy x *s x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   920
    unfolding vector_sadd_rdistrib and setsum_addf and vector_smult_assoc[THEN sym] and setsum_cmul by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   921
  ultimately show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and> (\<Sum>x\<in>s. uc x *s x) = u *s (\<Sum>x\<in>s. ux x *s x) + v *s (\<Sum>x\<in>s. uy x *s x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   922
    apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   923
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   924
  fix t assume t:"s \<subseteq> t" "convex t" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   925
  fix u assume u:"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   926
  thus "(\<Sum>x\<in>s. u x *s x) \<in> t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   927
    using assms and t(1) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   928
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   929
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   930
subsection {* Another formulation from Lars Schewe. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   931
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   932
lemma convex_hull_explicit:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   933
  "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   934
             (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *s v) s = y}" (is "?lhs = ?rhs")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   935
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   936
  { fix x assume "x\<in>?lhs"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   937
    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 *s y i) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   938
      unfolding convex_hull_indexed by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   939
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   940
    have fin:"finite {1..k}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   941
    have fin':"\<And>v. finite {i \<in> {1..k}. y i = v}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   942
    { fix j assume "j\<in>{1..k}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   943
      hence "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   944
	using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   945
	apply(rule setsum_nonneg) using obt(1) by auto } 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   946
    moreover
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   947
    have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1"  
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   948
      unfolding setsum_image_gen[OF fin, THEN sym] using obt(2) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   949
    moreover have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v} *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   950
      using setsum_image_gen[OF fin, of "\<lambda>i. u i *s y i" y, THEN sym]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   951
      unfolding setsum_vmul[OF fin']  using obt(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   952
    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 *s v) = x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   953
      apply(rule_tac x="y ` {1..k}" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   954
      apply(rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   955
    hence "x\<in>?rhs" by auto  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   956
  moreover
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   957
  { fix y assume "y\<in>?rhs"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   958
    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 *s v) = y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   959
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   960
    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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   961
    
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   962
    { fix i::nat assume "i\<in>{1..card s}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   963
      hence "f i \<in> s"  apply(subst f(2)[THEN sym]) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   964
      hence "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   965
    moreover have *:"finite {1..card s}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   966
    { fix y assume "y\<in>s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   967
      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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   968
      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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   969
      hence "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   970
      hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y" "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *s f x) = u y *s y" by auto   }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   971
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   972
    hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *s f i) = y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   973
      unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *s f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f] 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   974
      unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *s f x)" "\<lambda>v. u v *s v"]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   975
      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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   976
    
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   977
    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 *s x i) = y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   978
      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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   979
    hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   980
  ultimately show ?thesis unfolding expand_set_eq by blast
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   981
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   982
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   983
subsection {* A stepping theorem for that expansion. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   984
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   985
lemma convex_hull_finite_step:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   986
  assumes "finite (s::(real^'n) set)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   987
  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 *s x) (insert a s) = y)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   988
     \<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 *s x) s = y - v *s a)" (is "?lhs = ?rhs")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   989
proof(rule, case_tac[!] "a\<in>s")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   990
  assume "a\<in>s" hence *:"insert a s = s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   991
  assume ?lhs thus ?rhs unfolding * apply(rule_tac x=0 in exI) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   992
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   993
  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 *s x) = y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   994
  assume "a\<notin>s" thus ?rhs apply(rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   995
    apply(rule_tac x=u in exI) using u[unfolded setsum_clauses(2)[OF assms]] and `a\<notin>s` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   996
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   997
  assume "a\<in>s" hence *:"insert a s = s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   998
  have fin:"finite (insert a s)" using assms by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
   999
  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 *s x) = y - v *s a" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1000
  show ?lhs apply(rule_tac x="\<lambda>x. (if a = x then v else 0) + u x" in exI) unfolding vector_sadd_rdistrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1001
    unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\<in>s` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1002
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1003
  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 *s x) = y - v *s a" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1004
  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) *s x) = (\<Sum>x\<in>s. u x *s x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1005
    apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\<notin>s` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1006
  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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1007
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1008
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1009
subsection {* Hence some special cases. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1010
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1011
lemma convex_hull_2:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1012
  "convex hull {a,b} = {u *s a + v *s b | u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1013
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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1014
show ?thesis apply(simp add: convex_hull_finite) unfolding convex_hull_finite_step[OF **, of a 1, unfolded * conj_assoc]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1015
  apply auto apply(rule_tac x=v in exI) apply(rule_tac x="1 - v" in exI) apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1016
  apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\<lambda>x. v" in exI) by simp qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1017
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1018
lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *s (b - a) | u.  0 \<le> u \<and> u \<le> 1}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1019
  unfolding convex_hull_2 unfolding Collect_def 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1020
proof(rule ext) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1021
  fix x show "(\<exists>v u. x = v *s a + u *s b \<and> 0 \<le> v \<and> 0 \<le> u \<and> v + u = 1) = (\<exists>u. x = a + u *s (b - a) \<and> 0 \<le> u \<and> u \<le> 1)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1022
    unfolding * apply auto apply(rule_tac[!] x=u in exI) by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1023
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1024
lemma convex_hull_3:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1025
  "convex hull {a::real^'n,b,c} = { u *s a + v *s b + w *s c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1026
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1027
  have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1028
  have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1029
         "\<And>x y z ::real^'n. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: ring_simps)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1030
  show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1031
    unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1032
    apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1033
    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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1034
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1035
lemma convex_hull_3_alt:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1036
  "convex hull {a,b,c} = {a + u *s (b - a) + v *s (c - a) | u v.  0 \<le> u \<and> 0 \<le> v \<and> u + v \<le> 1}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1037
proof- have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1038
  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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1039
    apply(rule_tac x=u in exI) apply(rule_tac x=v in exI) by simp qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1040
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1041
subsection {* Relations among closure notions and corresponding hulls. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1042
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1043
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1044
  unfolding subspace_def affine_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1045
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1046
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1047
  unfolding affine_def convex_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1048
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1049
lemma subspace_imp_convex: "subspace s \<Longrightarrow> convex s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1050
  using subspace_imp_affine affine_imp_convex by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1051
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1052
lemma affine_hull_subset_span: "(affine hull s) \<subseteq> (span s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1053
  unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1054
  using subspace_imp_affine  by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1055
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1056
lemma convex_hull_subset_span: "(convex hull s) \<subseteq> (span s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1057
  unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1058
  using subspace_imp_convex by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1059
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1060
lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1061
  unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1062
  using affine_imp_convex by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1063
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1064
lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1065
  unfolding affine_dependent_def dependent_def 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1066
  using affine_hull_subset_span by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1067
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1068
lemma dependent_imp_affine_dependent:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1069
  assumes "dependent {x - a| x . x \<in> s}" "a \<notin> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1070
  shows "affine_dependent (insert a s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1071
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1072
  from assms(1)[unfolded dependent_explicit] obtain S u v 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1073
    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 *s v) = 0" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1074
  def t \<equiv> "(\<lambda>x. x + a) ` S"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1075
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1076
  have inj:"inj_on (\<lambda>x. x + a) S" unfolding inj_on_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1077
  have "0\<notin>S" using obt(2) assms(2) unfolding subset_eq by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1078
  have fin:"finite t" and  "t\<subseteq>s" unfolding t_def using obt(1,2) by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1079
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1080
  hence "finite (insert a t)" and "insert a t \<subseteq> insert a s" by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1081
  moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x)) = (\<Sum>x\<in>t. Q x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1082
    apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1083
  have "(\<Sum>x\<in>insert a t. if x = a then - (\<Sum>x\<in>t. u (x - a)) else u (x - a)) = 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1084
    unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` apply auto unfolding * by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1085
  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"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1086
    apply(rule_tac x="v + a" in bexI) using obt(3,4) and `0\<notin>S` unfolding t_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1087
  moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *s x) = (\<Sum>x\<in>t. Q x *s x)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1088
    apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1089
  have "(\<Sum>x\<in>t. u (x - a)) *s a = (\<Sum>v\<in>t. u (v - a) *s v)" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1090
    unfolding setsum_vmul[OF fin(1)] unfolding t_def and setsum_reindex[OF inj] and o_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1091
    using obt(5) by (auto simp add: setsum_addf)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1092
  hence "(\<Sum>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) *s v) = 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1093
    unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` by (auto simp add: *  vector_smult_lneg) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1094
  ultimately show ?thesis unfolding affine_dependent_explicit
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1095
    apply(rule_tac x="insert a t" in exI) by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1096
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1097
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1098
lemma convex_cone:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1099
  "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 *s x) \<in> s)" (is "?lhs = ?rhs")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1100
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1101
  { fix x y assume "x\<in>s" "y\<in>s" and ?lhs
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1102
    hence "2 *s x \<in>s" "2 *s y \<in> s" unfolding cone_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1103
    hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1104
      apply(erule_tac x="2*s x" in ballE) apply(erule_tac x="2*s y" in ballE)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1105
      apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1106
  thus ?thesis unfolding convex_def cone_def by blast
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1107
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1108
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1109
lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1110
  assumes "finite s" "card s \<ge> CARD('n) + 2"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1111
  shows "affine_dependent s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1112
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1113
  have "s\<noteq>{}" using assms by auto then obtain a where "a\<in>s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1114
  have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1115
  have "card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding * 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1116
    apply(rule card_image) unfolding inj_on_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1117
  also have "\<dots> > CARD('n)" using assms(2)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1118
    unfolding card_Diff_singleton[OF assms(1) `a\<in>s`] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1119
  finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1120
    apply(rule dependent_imp_affine_dependent)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1121
    apply(rule dependent_biggerset) by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1122
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1123
lemma affine_dependent_biggerset_general:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1124
  assumes "finite (s::(real^'n::finite) set)" "card s \<ge> dim s + 2"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1125
  shows "affine_dependent s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1126
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1127
  from assms(2) have "s \<noteq> {}" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1128
  then obtain a where "a\<in>s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1129
  have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1130
  have **:"card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding * 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1131
    apply(rule card_image) unfolding inj_on_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1132
  have "dim {x - a |x. x \<in> s - {a}} \<le> dim s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1133
    apply(rule subset_le_dim) unfolding subset_eq
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1134
    using `a\<in>s` by (auto simp add:span_superset span_sub)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1135
  also have "\<dots> < dim s + 1" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1136
  also have "\<dots> \<le> card (s - {a})" using assms
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1137
    using card_Diff_singleton[OF assms(1) `a\<in>s`] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1138
  finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1139
    apply(rule dependent_imp_affine_dependent) apply(rule dependent_biggerset_general) unfolding ** by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1140
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1141
subsection {* Caratheodory's theorem. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1142
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1143
lemma convex_hull_caratheodory: fixes p::"(real^'n::finite) set"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1144
  shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> CARD('n) + 1 \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1145
  (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *s v) s = y}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1146
  unfolding convex_hull_explicit expand_set_eq mem_Collect_eq
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1147
proof(rule,rule)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1148
  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 *s v) = y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1149
  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 *s v) = y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1150
  then obtain N where "?P N" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1151
  hence "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n" apply(rule_tac ex_least_nat_le) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1152
  then obtain n where "?P n" and smallest:"\<forall>k<n. \<not> ?P k" by blast
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1153
  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 *s v) = y" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1154
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1155
  have "card s \<le> CARD('n) + 1" proof(rule ccontr, simp only: not_le)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1156
    assume "CARD('n) + 1 < card s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1157
    hence "affine_dependent s" using affine_dependent_biggerset[OF obt(1)] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1158
    then obtain w v where wv:"setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *s v) = 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1159
      using affine_dependent_explicit_finite[OF obt(1)] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1160
    def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"  def t \<equiv> "Min i"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1161
    have "\<exists>x\<in>s. w x < 0" proof(rule ccontr, simp add: not_less)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1162
      assume as:"\<forall>x\<in>s. 0 \<le> w x"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1163
      hence "setsum w (s - {v}) \<ge> 0" apply(rule_tac setsum_nonneg) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1164
      hence "setsum w s > 0" unfolding setsum_diff1'[OF obt(1) `v\<in>s`]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1165
	using as[THEN bspec[where x=v]] and `v\<in>s` using `w v \<noteq> 0` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1166
      thus False using wv(1) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1167
    qed hence "i\<noteq>{}" unfolding i_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1168
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1169
    hence "t \<ge> 0" using Min_ge_iff[of i 0 ] and obt(1) unfolding t_def i_def
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1170
      using obt(4)[unfolded le_less] apply auto unfolding divide_le_0_iff by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1171
    have t:"\<forall>v\<in>s. u v + t * w v \<ge> 0" proof
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1172
      fix v assume "v\<in>s" hence v:"0\<le>u v" using obt(4)[THEN bspec[where x=v]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1173
      show"0 \<le> u v + t * w v" proof(cases "w v < 0")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1174
	case False thus ?thesis apply(rule_tac add_nonneg_nonneg) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1175
	  using v apply simp apply(rule mult_nonneg_nonneg) using `t\<ge>0` by auto next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1176
	case True hence "t \<le> u v / (- w v)" using `v\<in>s`
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1177
	  unfolding t_def i_def apply(rule_tac Min_le) using obt(1) by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1178
	thus ?thesis unfolding real_0_le_add_iff
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1179
	  using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[THEN sym]]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1180
      qed qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1181
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1182
    obtain a where "a\<in>s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1183
      using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1184
    hence a:"a\<in>s" "u a + t * w a = 0" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1185
    have *:"\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'a::ring)" unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1186
    have "(\<Sum>v\<in>s. u v + t * w v) = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1187
      unfolding setsum_addf wv(1) setsum_right_distrib[THEN sym] obt(5) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1188
    moreover have "(\<Sum>v\<in>s. u v *s v + (t * w v) *s v) - (u a *s a + (t * w a) *s a) = y" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1189
      unfolding setsum_addf obt(6) vector_smult_assoc[THEN sym] setsum_cmul wv(4)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1190
      by (metis diff_0_right a(2) pth_5 pth_8 pth_d vector_mul_eq_0)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1191
    ultimately have "?P (n - 1)" apply(rule_tac x="(s - {a})" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1192
      apply(rule_tac x="\<lambda>v. u v + t * w v" in exI) using obt(1-3) and t and a by (auto simp add: *)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1193
    thus False using smallest[THEN spec[where x="n - 1"]] by auto qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1194
  thus "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> CARD('n) + 1
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1195
    \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *s v) = y" using obt by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1196
qed auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1197
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1198
lemma caratheodory:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1199
 "convex hull p = {x::real^'n::finite. \<exists>s. finite s \<and> s \<subseteq> p \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1200
      card s \<le> CARD('n) + 1 \<and> x \<in> convex hull s}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1201
  unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1202
  fix x assume "x \<in> convex hull p"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1203
  then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> CARD('n) + 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1204
     "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *s v) = x"unfolding convex_hull_caratheodory by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1205
  thus "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> CARD('n) + 1 \<and> x \<in> convex hull s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1206
    apply(rule_tac x=s in exI) using hull_subset[of s convex]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1207
  using convex_convex_hull[unfolded convex_explicit, of s, THEN spec[where x=s], THEN spec[where x=u]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1208
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1209
  fix x assume "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> CARD('n) + 1 \<and> x \<in> convex hull s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1210
  then obtain s where "finite s" "s \<subseteq> p" "card s \<le> CARD('n) + 1" "x \<in> convex hull s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1211
  thus "x \<in> convex hull p" using hull_mono[OF `s\<subseteq>p`] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1212
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1213
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1214
subsection {* Openness and compactness are preserved by convex hull operation. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1215
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1216
lemma open_convex_hull:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1217
  assumes "open s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1218
  shows "open(convex hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1219
  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1220
proof(rule, rule) fix a
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1221
  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 *s v) = a"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1222
  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 *s v) = a" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1223
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1224
  from assms[unfolded open_contains_cball] obtain b where b:"\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1225
    using bchoice[of s "\<lambda>x e. e>0 \<and> cball x e \<subseteq> s"] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1226
  have "b ` t\<noteq>{}" unfolding i_def using obt by auto  def i \<equiv> "b ` t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1227
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1228
  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 *s v) = y}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1229
    apply(rule_tac x="Min i" in exI) unfolding subset_eq apply rule defer apply rule unfolding mem_Collect_eq
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1230
  proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1231
    show "0 < Min i" unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] `b \` t\<noteq>{}`]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1232
      using b apply simp apply rule apply(erule_tac x=x in ballE) using `t\<subseteq>s` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1233
  next  fix y assume "y \<in> cball a (Min i)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1234
    hence y:"norm (a - y) \<le> Min i" unfolding dist_def[THEN sym] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1235
    { fix x assume "x\<in>t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1236
      hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1237
      hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1238
      moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1239
      ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by auto }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1240
    moreover
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1241
    have *:"inj_on (\<lambda>v. v + (y - a)) t" unfolding inj_on_def by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1242
    have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1243
      unfolding setsum_reindex[OF *] o_def using obt(4) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1244
    moreover have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a)) *s v) = y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1245
      unfolding setsum_reindex[OF *] o_def using obt(4,5)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1246
      by (simp add: setsum_addf setsum_subtractf setsum_vmul[OF obt(1), THEN sym]) 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1247
    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 *s v) = y"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1248
      apply(rule_tac x="(\<lambda>v. v + (y - a)) ` t" in exI) apply(rule_tac x="\<lambda>v. u (v - (y - a))" in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1249
      using obt(1, 3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1250
  qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1251
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1252
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1253
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1254
lemma compact_convex_combinations:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1255
  assumes "compact s" "compact t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1256
  shows "compact { (1 - u) *s x + u *s y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1257
proof-
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1258
  let ?X = "{ pastecart u w | u w. u \<in> {vec1 0 .. vec1 1} \<and> w \<in> { pastecart x y |x y. x \<in> s \<and> y \<in> t} }"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1259
  let ?h = "(\<lambda>z. (1 - dest_vec1(fstcart z)) *s fstcart(sndcart z) + dest_vec1(fstcart z) *s sndcart(sndcart z))"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1260
  have *:"{ (1 - u) *s x + u *s y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t} = ?h ` ?X"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1261
    apply(rule set_ext) unfolding image_iff mem_Collect_eq unfolding mem_interval_1 vec1_dest_vec1
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1262
    apply rule apply auto apply(rule_tac x="pastecart (vec1 u) (pastecart xa y)" in exI) apply simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1263
    apply(rule_tac x="vec1 u" in exI) apply(rule_tac x="pastecart xa y" in exI) by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1264
  { fix u::"real^1" fix x y assume as:"0 \<le> dest_vec1 u" "dest_vec1 u \<le> 1" "x \<in> s" "y \<in> t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1265
    hence "continuous (at (pastecart u (pastecart x y)))
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1266
           (\<lambda>z. fstcart (sndcart z) - dest_vec1 (fstcart z) *s fstcart (sndcart z) +
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1267
                dest_vec1 (fstcart z) *s sndcart (sndcart z))"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1268
      apply (auto intro!: continuous_add continuous_sub continuous_mul simp add: o_def vec1_dest_vec1)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1269
      using linear_continuous_at linear_fstcart linear_sndcart linear_sndcart
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1270
      using linear_compose[unfolded o_def] by auto }
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1271
  hence "continuous_on {pastecart u w |u w. u \<in> {vec1 0..vec1 1} \<and> w \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}}
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1272
     (\<lambda>z. (1 - dest_vec1 (fstcart z)) *s fstcart (sndcart z) + dest_vec1 (fstcart z) *s sndcart (sndcart z))"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1273
    apply(rule_tac continuous_at_imp_continuous_on) unfolding mem_Collect_eq
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1274
    unfolding mem_interval_1 vec1_dest_vec1 by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1275
 thus ?thesis unfolding * apply(rule compact_continuous_image)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1276
    defer apply(rule compact_pastecart) defer apply(rule compact_pastecart)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1277
    using compact_interval assms by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1278
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1279
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1280
lemma compact_convex_hull: fixes s::"(real^'n::finite) set"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1281
  assumes "compact s"  shows "compact(convex hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1282
proof(cases "s={}")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1283
  case True thus ?thesis using compact_empty by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1284
next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1285
  case False then obtain w where "w\<in>s" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1286
  show ?thesis unfolding caratheodory[of s]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1287
  proof(induct "CARD('n) + 1")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1288
    have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1289
      using compact_empty by (auto simp add: convex_hull_empty)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1290
    case 0 thus ?case unfolding * by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1291
  next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1292
    case (Suc n)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1293
    show ?case proof(cases "n=0")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1294
      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"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1295
	unfolding expand_set_eq and mem_Collect_eq proof(rule, rule)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1296
	fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1297
	then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1298
	show "x\<in>s" proof(cases "card t = 0")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1299
	  case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by(simp add: convex_hull_empty)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1300
	next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1301
	  case False hence "card t = Suc 0" using t(3) `n=0` by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1302
	  then obtain a where "t = {a}" unfolding card_Suc_eq by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1303
	  thus ?thesis using t(2,4) by (simp add: convex_hull_singleton)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1304
	qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1305
      next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1306
	fix x assume "x\<in>s"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1307
	thus "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1308
	  apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1309
      qed thus ?thesis using assms by simp
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1310
    next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1311
      case False have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} =
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1312
	{ (1 - u) *s x + u *s y | x y u. 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1313
	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}}"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1314
	unfolding expand_set_eq and mem_Collect_eq proof(rule,rule)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1315
	fix x assume "\<exists>u v c. x = (1 - c) *s u + c *s v \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1316
          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)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1317
	then obtain u v c t where obt:"x = (1 - c) *s u + c *s v"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1318
          "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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1319
	moreover have "(1 - c) *s u + c *s v \<in> convex hull insert u t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1320
	  apply(rule mem_convex) using obt(2) and convex_convex_hull and hull_subset[of "insert u t" convex]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1321
	  using obt(7) and hull_mono[of t "insert u t"] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1322
	ultimately show "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1323
	  apply(rule_tac x="insert u t" in exI) by (auto simp add: card_insert_if)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1324
      next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1325
	fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1326
	then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1327
	let ?P = "\<exists>u v c. x = (1 - c) *s u + c *s v \<and>
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1328
          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)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1329
	show ?P proof(cases "card t = Suc n")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1330
	  case False hence "card t \<le> n" using t(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1331
	  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
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1332
	    by(auto intro!: exI[where x=t])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1333
	next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1334
	  case True then obtain a u where au:"t = insert a u" "a\<notin>u" apply(drule_tac card_eq_SucD) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1335
	  show ?P proof(cases "u={}")
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1336
	    case True hence "x=a" using t(4)[unfolded au] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1337
	    show ?P unfolding `x=a` apply(rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1338
	      using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"] simp add: convex_hull_singleton)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1339
	  next
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1340
	    case False obtain ux vx b where obt:"ux\<ge>0" "vx\<ge>0" "ux + vx = 1" "b \<in> convex hull u" "x = ux *s a + vx *s b"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1341
	      using t(4)[unfolded au convex_hull_insert[OF False]] by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1342
	    have *:"1 - vx = ux" using obt(3) by auto
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1343
	    show ?P apply(rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=vx in exI)
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1344
	      using obt and t(1-3) unfolding au and * using card_insert_disjoint[OF _ au(2)]
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1345
	      by(auto intro!: exI[where x=u])
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1346
	  qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1347
	qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1348
      qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1349
      thus ?thesis using compact_convex_combinations[OF assms Suc] by simp 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1350
    qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1351
  qed 
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1352
qed
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1353
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1354
lemma finite_imp_compact_convex_hull:
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1355
 "finite s \<Longrightarrow> compact(convex hull s)"
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1356
  apply(drule finite_imp_compact, drule compact_convex_hull) by assumption
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1357
f6427bc40421 Added Convex_Euclidean_Space.thy
himmelma
parents:
diff changeset
  1358
subsection {* Extremal points of a simplex are some vertices. *}
f6427bc40421 Added Convex_Euclidean_Space.thy
hi