Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Convex.thy Sprache: Isabelle

Original von: Isabelle^©

(* Title:      HOL/Analysis/Convex.thy
   Author:     L C Paulson, University of Cambridge
   Author:     Robert Himmelmann, TU Muenchen
   Author:     Bogdan Grechuk, University of Edinburgh
   Author:     Armin Heller, TU Muenchen
   Author:     Johannes Hoelzl, TU Muenchen
*)

section \<open>Convex Sets and Functions\<close>

theory Convex
imports
  Affine
  "HOL-Library.Set_Algebras"
begin

subsection \<open>Convex Sets\<close>

definition\<^marker>\<open>tag important\<close> convex :: "'a::real_vector set \<Rightarrow> bool"
  where "convex s \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)"

lemma convexI:
  assumes "\x y u v. x \ s \ y \ s \ 0 \ u \ 0 \ v \ u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s"
  shows "convex s"
  using assms unfolding convex_def by fast

lemma convexD:
  assumes "convex s" and "x \ s" and "y \ s" and "0 \ u" and "0 \ v" and "u + v = 1"
  shows "u *\<^sub>R x + v *\<^sub>R y \ s"
  using assms unfolding convex_def by fast

lemma convex_alt: "convex s \ (\x\s. \y\s. \u. 0 \ u \ u \ 1 \ ((1 - u) *\<^sub>R x + u *\<^sub>R y) \ s)"
  (is "_ \ ?alt")
proof
  show "convex s" if alt: ?alt
  proof -
    {
      fix x y and u v :: real
      assume mem: "x \ s" "y \ s"
      assume "0 \ u" "0 \ v"
      moreover
      assume "u + v = 1"
      then have "u = 1 - v" by auto
      ultimately have "u *\<^sub>R x + v *\<^sub>R y \ s"
        using alt [rule_format, OF mem] by auto
    }
    then show ?thesis
      unfolding convex_def by auto
  qed
  show ?alt if "convex s"
    using that by (auto simp: convex_def)
qed

lemma convexD_alt:
  assumes "convex s" "a \ s" "b \ s" "0 \ u" "u \ 1"
  shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \ s"
  using assms unfolding convex_alt by auto

lemma mem_convex_alt:
  assumes "convex S" "x \ S" "y \ S" "u \ 0" "v \ 0" "u + v > 0"
  shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) \ S"
  using assms
  by (simp add: convex_def zero_le_divide_iff add_divide_distrib [symmetric])

lemma convex_empty[intro,simp]: "convex {}"
  unfolding convex_def by simp

lemma convex_singleton[intro,simp]: "convex {a}"
  unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric])

lemma convex_UNIV[intro,simp]: "convex UNIV"
  unfolding convex_def by auto

lemma convex_Inter: "(\s. s\f \ convex s) \ convex(\f)"
  unfolding convex_def by auto

lemma convex_Int: "convex s \ convex t \ convex (s \ t)"
  unfolding convex_def by auto

lemma convex_INT: "(\i. i \ A \ convex (B i)) \ convex (\i\A. B i)"
  unfolding convex_def by auto

lemma convex_Times: "convex s \ convex t \ convex (s \ t)"
  unfolding convex_def by auto

lemma convex_halfspace_le: "convex {x. inner a x \ b}"
  unfolding convex_def
  by (auto simp: inner_add intro!: convex_bound_le)

lemma convex_halfspace_ge: "convex {x. inner a x \ b}"
proof -
  have *: "{x. inner a x \ b} = {x. inner (-a) x \ -b}"
    by auto
  show ?thesis
    unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
qed

lemma convex_halfspace_abs_le: "convex {x. \inner a x\ \ b}"
proof -
  have *: "{x. \inner a x\ \ b} = {x. inner a x \ b} \ {x. -b \ inner a x}"
    by auto
  show ?thesis
    unfolding * by (simp add: convex_Int convex_halfspace_ge convex_halfspace_le)
qed

lemma convex_hyperplane: "convex {x. inner a x = b}"
proof -
  have *: "{x. inner a x = b} = {x. inner a x \ b} \ {x. inner a x \ b}"
    by auto
  show ?thesis using convex_halfspace_le convex_halfspace_ge
    by (auto intro!: convex_Int simp: *)
qed

lemma convex_halfspace_lt: "convex {x. inner a x < b}"
  unfolding convex_def
  by (auto simp: convex_bound_lt inner_add)

lemma convex_halfspace_gt: "convex {x. inner a x > b}"
  using convex_halfspace_lt[of "-a" "-b"] by auto

lemma convex_halfspace_Re_ge: "convex {x. Re x \ b}"
  using convex_halfspace_ge[of b "1::complex"] by simp

lemma convex_halfspace_Re_le: "convex {x. Re x \ b}"
  using convex_halfspace_le[of "1::complex" b] by simp

lemma convex_halfspace_Im_ge: "convex {x. Im x \ b}"
  using convex_halfspace_ge[of b \<i>] by simp

lemma convex_halfspace_Im_le: "convex {x. Im x \ b}"
  using convex_halfspace_le[of \<i> b] by simp

lemma convex_halfspace_Re_gt: "convex {x. Re x > b}"
  using convex_halfspace_gt[of b "1::complex"] by simp

lemma convex_halfspace_Re_lt: "convex {x. Re x < b}"
  using convex_halfspace_lt[of "1::complex" b] by simp

lemma convex_halfspace_Im_gt: "convex {x. Im x > b}"
  using convex_halfspace_gt[of b \<i>] by simp

lemma convex_halfspace_Im_lt: "convex {x. Im x < b}"
  using convex_halfspace_lt[of \<i> b] by simp

lemma convex_real_interval [iff]:
  fixes a b :: "real"
  shows "convex {a..}" and "convex {..b}"
    and "convex {a<..}" and "convex {..
    and "convex {a..b}" and "convex {a<..b}"
    and "convex {a.. and "convex {a<..
proof -
  have "{a..} = {x. a \ inner 1 x}"
    by auto
  then show 1: "convex {a..}"
    by (simp only: convex_halfspace_ge)
  have "{..b} = {x. inner 1 x \ b}"
    by auto
  then show 2: "convex {..b}"
    by (simp only: convex_halfspace_le)
  have "{a<..} = {x. a < inner 1 x}"
    by auto
  then show 3: "convex {a<..}"
    by (simp only: convex_halfspace_gt)
  have "{..
    by auto
  then show 4: "convex {..
    by (simp only: convex_halfspace_lt)
  have "{a..b} = {a..} \ {..b}"
    by auto
  then show "convex {a..b}"
    by (simp only: convex_Int 1 2)
  have "{a<..b} = {a<..} \ {..b}"
    by auto
  then show "convex {a<..b}"
    by (simp only: convex_Int 3 2)
  have "{a.. {..
    by auto
  then show "convex {a..
    by (simp only: convex_Int 1 4)
  have "{a<.. {..
    by auto
  then show "convex {a<..
    by (simp only: convex_Int 3 4)
qed

lemma convex_Reals: "convex \"
  by (simp add: convex_def scaleR_conv_of_real)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Explicit expressions for convexity in terms of arbitrary sums\<close>

lemma convex_sum:
  fixes C :: "'a::real_vector set"
  assumes "finite S"
    and "convex C"
    and "(\ i \ S. a i) = 1"
  assumes "\i. i \ S \ a i \ 0"
    and "\i. i \ S \ y i \ C"
  shows "(\ j \ S. a j *\<^sub>R y j) \ C"
  using assms(1,3,4,5)
proof (induct arbitrary: a set: finite)
  case empty
  then show ?case by simp
next
  case (insert i S) note IH = this(3)
  have "a i + sum a S = 1"
    and "0 \ a i"
    and "\j\S. 0 \ a j"
    and "y i \ C"
    and "\j\S. y j \ C"
    using insert.hyps(1,2) insert.prems by simp_all
  then have "0 \ sum a S"
    by (simp add: sum_nonneg)
  have "a i *\<^sub>R y i + (\j\S. a j *\<^sub>R y j) \ C"
  proof (cases "sum a S = 0")
    case True
    with \<open>a i + sum a S = 1\<close> have "a i = 1"
      by simp
    from sum_nonneg_0 [OF \<open>finite S\<close> _ True] \<open>\<forall>j\<in>S. 0 \<le> a j\<close> have "\<forall>j\<in>S. a j = 0"
      by simp
    show ?thesis using \<open>a i = 1\<close> and \<open>\<forall>j\<in>S. a j = 0\<close> and \<open>y i \<in> C\<close>
      by simp
  next
    case False
    with \<open>0 \<le> sum a S\<close> have "0 < sum a S"
      by simp
    then have "(\j\S. (a j / sum a S) *\<^sub>R y j) \ C"
      using \<open>\<forall>j\<in>S. 0 \<le> a j\<close> and \<open>\<forall>j\<in>S. y j \<in> C\<close>
      by (simp add: IH sum_divide_distrib [symmetric])
    from \<open>convex C\<close> and \<open>y i \<in> C\<close> and this and \<open>0 \<le> a i\<close>
      and \<open>0 \<le> sum a S\<close> and \<open>a i + sum a S = 1\<close>
    have "a i *\<^sub>R y i + sum a S *\<^sub>R (\j\S. (a j / sum a S) *\<^sub>R y j) \ C"
      by (rule convexD)
    then show ?thesis
      by (simp add: scaleR_sum_right False)
  qed
  then show ?case using \<open>finite S\<close> and \<open>i \<notin> S\<close>
    by simp
qed

lemma convex:
  "convex S \ (\(k::nat) u x. (\i. 1\i \ i\k \ 0 \ u i \ x i \S) \ (sum u {1..k} = 1)
      \<longrightarrow> sum (\<lambda>i. u i *\<^sub>R x i) {1..k} \<in> S)"
proof safe
  fix k :: nat
  fix u :: "nat \ real"
  fix x
  assume "convex S"
    "\i. 1 \ i \ i \ k \ 0 \ u i \ x i \ S"
    "sum u {1..k} = 1"
  with convex_sum[of "{1 .. k}" S] show "(\j\{1 .. k}. u j *\<^sub>R x j) \ S"
    by auto
next
  assume *: "\k u x. (\ i :: nat. 1 \ i \ i \ k \ 0 \ u i \ x i \ S) \ sum u {1..k} = 1
    \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R (x i :: 'a)) \<in> S"
  {
    fix \<mu> :: real
    fix x y :: 'a
    assume xy: "x \ S" "y \ S"
    assume mu: "\ \ 0" "\ \ 1"
    let ?u = "\i. if (i :: nat) = 1 then \ else 1 - \"
    let ?x = "\i. if (i :: nat) = 1 then x else y"
    have "{1 :: nat .. 2} \ - {x. x = 1} = {2}"
      by auto
    then have card: "card ({1 :: nat .. 2} \ - {x. x = 1}) = 1"
      by simp
    then have "sum ?u {1 .. 2} = 1"
      using sum.If_cases[of "{(1 :: nat) .. 2}" "\ x. x = 1" "\ x. \" "\ x. 1 - \"]
      by auto
    with *[rule_format, of "2" ?u ?x] have S: "(\j \ {1..2}. ?u j *\<^sub>R ?x j) \ S"
      using mu xy by auto
    have grarr: "(\j \ {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \) *\<^sub>R y"
      using sum.atLeast_Suc_atMost[of "Suc (Suc 0)" 2 "\ j. (1 - \) *\<^sub>R y"] by auto
    from sum.atLeast_Suc_atMost[of "Suc 0" 2 "\ j. ?u j *\<^sub>R ?x j", simplified this]
    have "(\j \ {1..2}. ?u j *\<^sub>R ?x j) = \ *\<^sub>R x + (1 - \) *\<^sub>R y"
      by auto
    then have "(1 - \) *\<^sub>R y + \ *\<^sub>R x \ S"
      using S by (auto simp: add.commute)
  }
  then show "convex S"
    unfolding convex_alt by auto
qed

lemma convex_explicit:
  fixes S :: "'a::real_vector set"
  shows "convex S \
    (\<forall>t u. finite t \<and> t \<subseteq> S \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> sum u t = 1 \<longrightarrow> sum (\<lambda>x. u x *\<^sub>R x) t \<in> S)"
proof safe
  fix t
  fix u :: "'a \ real"
  assume "convex S"
    and "finite t"
    and "t \ S" "\x\t. 0 \ u x" "sum u t = 1"
  then show "(\x\t. u x *\<^sub>R x) \ S"
    using convex_sum[of t S u "\ x. x"] by auto
next
  assume *: "\t. \ u. finite t \ t \ S \ (\x\t. 0 \ u x) \
    sum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> S"
  show "convex S"
    unfolding convex_alt
  proof safe
    fix x y
    fix \<mu> :: real
    assume **: "x \ S" "y \ S" "0 \ \" "\ \ 1"
    show "(1 - \) *\<^sub>R x + \ *\<^sub>R y \ S"
    proof (cases "x = y")
      case False
      then show ?thesis
        using *[rule_format, of "{x, y}" "\ z. if z = x then 1 - \ else \"] **
        by auto
    next
      case True
      then show ?thesis
        using *[rule_format, of "{x, y}" "\ z. 1"] **
        by (auto simp: field_simps real_vector.scale_left_diff_distrib)
    qed
  qed
qed

lemma convex_finite:
  assumes "finite S"
  shows "convex S \ (\u. (\x\S. 0 \ u x) \ sum u S = 1 \ sum (\x. u x *\<^sub>R x) S \ S)"
       (is "?lhs = ?rhs")
proof
  { have if_distrib_arg: "\P f g x. (if P then f else g) x = (if P then f x else g x)"
      by simp
    fix T :: "'a set" and u :: "'a \ real"
    assume sum: "\u. (\x\S. 0 \ u x) \ sum u S = 1 \ (\x\S. u x *\<^sub>R x) \ S"
    assume *: "\x\T. 0 \ u x" "sum u T = 1"
    assume "T \ S"
    then have "S \ T = T" by auto
    with sum[THEN spec[where x="\x. if x\T then u x else 0"]] * have "(\x\T. u x *\<^sub>R x) \ S"
      by (auto simp: assms sum.If_cases if_distrib if_distrib_arg) }
  moreover assume ?rhs
  ultimately show ?lhs
    unfolding convex_explicit by auto
qed (auto simp: convex_explicit assms)

subsection \<open>Convex Functions on a Set\<close>

definition\<^marker>\<open>tag important\<close> convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
  where "convex_on S f \
    (\<forall>x\<in>S. \<forall>y\<in>S. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"

lemma convex_onI [intro?]:
  assumes "\t x y. t > 0 \ t < 1 \ x \ A \ y \ A \
    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
  shows "convex_on A f"
  unfolding convex_on_def
proof clarify
  fix x y
  fix u v :: real
  assume A: "x \ A" "y \ A" "u \ 0" "v \ 0" "u + v = 1"
  from A(5) have [simp]: "v = 1 - u"
    by (simp add: algebra_simps)
  from A(1-4) show "f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y"
    using assms[of u y x]
    by (cases "u = 0 \ u = 1") (auto simp: algebra_simps)
qed

lemma convex_on_linorderI [intro?]:
  fixes A :: "('a::{linorder,real_vector}) set"
  assumes "\t x y. t > 0 \ t < 1 \ x \ A \ y \ A \ x < y \
    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
  shows "convex_on A f"
proof
  fix x y
  fix t :: real
  assume A: "x \ A" "y \ A" "t > 0" "t < 1"
  with assms [of t x y] assms [of "1 - t" y x]
  show "f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \ (1 - t) * f x + t * f y"
    by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
qed

lemma convex_onD:
  assumes "convex_on A f"
  shows "\t x y. t \ 0 \ t \ 1 \ x \ A \ y \ A \
    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
  using assms by (auto simp: convex_on_def)

lemma convex_onD_Icc:
  assumes "convex_on {x..y} f" "x \ (y :: _ :: {real_vector,preorder})"
  shows "\t. t \ 0 \ t \ 1 \
    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
  using assms(2) by (intro convex_onD [OF assms(1)]) simp_all

lemma convex_on_subset: "convex_on t f \ S \ t \ convex_on S f"
  unfolding convex_on_def by auto

lemma convex_on_add [intro]:
  assumes "convex_on S f"
    and "convex_on S g"
  shows "convex_on S (\x. f x + g x)"
proof -
  {
    fix x y
    assume "x \ S" "y \ S"
    moreover
    fix u v :: real
    assume "0 \ u" "0 \ v" "u + v = 1"
    ultimately
    have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \ (u * f x + v * f y) + (u * g x + v * g y)"
      using assms unfolding convex_on_def by (auto simp: add_mono)
    then have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \ u * (f x + g x) + v * (f y + g y)"
      by (simp add: field_simps)
  }
  then show ?thesis
    unfolding convex_on_def by auto
qed

lemma convex_on_cmul [intro]:
  fixes c :: real
  assumes "0 \ c"
    and "convex_on S f"
  shows "convex_on S (\x. c * f x)"
proof -
  have *: "u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)"
    for u c fx v fy :: real
    by (simp add: field_simps)
  show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)]
    unfolding convex_on_def and * by auto
qed

lemma convex_lower:
  assumes "convex_on S f"
    and "x \ S"
    and "y \ S"
    and "0 \ u"
    and "0 \ v"
    and "u + v = 1"
  shows "f (u *\<^sub>R x + v *\<^sub>R y) \ max (f x) (f y)"
proof -
  let ?m = "max (f x) (f y)"
  have "u * f x + v * f y \ u * max (f x) (f y) + v * max (f x) (f y)"
    using assms(4,5) by (auto simp: mult_left_mono add_mono)
  also have "\ = max (f x) (f y)"
    using assms(6) by (simp add: distrib_right [symmetric])
  finally show ?thesis
    using assms unfolding convex_on_def by fastforce
qed

lemma convex_on_dist [intro]:
  fixes S :: "'a::real_normed_vector set"
  shows "convex_on S (\x. dist a x)"
proof (auto simp: convex_on_def dist_norm)
  fix x y
  assume "x \ S" "y \ S"
  fix u v :: real
  assume "0 \ u"
  assume "0 \ v"
  assume "u + v = 1"
  have "a = u *\<^sub>R a + v *\<^sub>R a"
    unfolding scaleR_left_distrib[symmetric] and \<open>u + v = 1\<close> by simp
  then have *: "a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
    by (auto simp: algebra_simps)
  show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \ u * norm (a - x) + v * norm (a - y)"
    unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"]
    using \<open>0 \<le> u\<close> \<open>0 \<le> v\<close> by auto
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic operations on sets preserve convexity\<close>

lemma convex_linear_image:
  assumes "linear f"
    and "convex S"
  shows "convex (f ` S)"
proof -
  interpret f: linear f by fact
  from \<open>convex S\<close> show "convex (f ` S)"
    by (simp add: convex_def f.scaleR [symmetric] f.add [symmetric])
qed

lemma convex_linear_vimage:
  assumes "linear f"
    and "convex S"
  shows "convex (f -` S)"
proof -
  interpret f: linear f by fact
  from \<open>convex S\<close> show "convex (f -` S)"
    by (simp add: convex_def f.add f.scaleR)
qed

lemma convex_scaling:
  assumes "convex S"
  shows "convex ((\x. c *\<^sub>R x) ` S)"
proof -
  have "linear (\x. c *\<^sub>R x)"
    by (simp add: linearI scaleR_add_right)
  then show ?thesis
    using \<open>convex S\<close> by (rule convex_linear_image)
qed

lemma convex_scaled:
  assumes "convex S"
  shows "convex ((\x. x *\<^sub>R c) ` S)"
proof -
  have "linear (\x. x *\<^sub>R c)"
    by (simp add: linearI scaleR_add_left)
  then show ?thesis
    using \<open>convex S\<close> by (rule convex_linear_image)
qed

lemma convex_negations:
  assumes "convex S"
  shows "convex ((\x. - x) ` S)"
proof -
  have "linear (\x. - x)"
    by (simp add: linearI)
  then show ?thesis
    using \<open>convex S\<close> by (rule convex_linear_image)
qed

lemma convex_sums:
  assumes "convex S"
    and "convex T"
  shows "convex (\x\ S. \y \ T. {x + y})"
proof -
  have "linear (\(x, y). x + y)"
    by (auto intro: linearI simp: scaleR_add_right)
  with assms have "convex ((\(x, y). x + y) ` (S \ T))"
    by (intro convex_linear_image convex_Times)
  also have "((\(x, y). x + y) ` (S \ T)) = (\x\ S. \y \ T. {x + y})"
    by auto
  finally show ?thesis .
qed

lemma convex_differences:
  assumes "convex S" "convex T"
  shows "convex (\x\ S. \y \ T. {x - y})"
proof -
  have "{x - y| x y. x \ S \ y \ T} = {x + y |x y. x \ S \ y \ uminus ` T}"
    by (auto simp: diff_conv_add_uminus simp del: add_uminus_conv_diff)
  then show ?thesis
    using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto
qed

lemma convex_translation:
  "convex ((+) a ` S)" if "convex S"
proof -
  have "(\ x\ {a}. \y \ S. {x + y}) = (+) a ` S"
    by auto
  then show ?thesis
    using convex_sums [OF convex_singleton [of a] that] by auto
qed

lemma convex_translation_subtract:
  "convex ((\b. b - a) ` S)" if "convex S"
  using convex_translation [of S "- a"] that by (simp cong: image_cong_simp)

lemma convex_affinity:
  assumes "convex S"
  shows "convex ((\x. a + c *\<^sub>R x) ` S)"
proof -
  have "(\x. a + c *\<^sub>R x) ` S = (+) a ` (*\<^sub>R) c ` S"
    by auto
  then show ?thesis
    using convex_translation[OF convex_scaling[OF assms], of a c] by auto
qed

lemma convex_on_sum:
  fixes a :: "'a \ real"
    and y :: "'a \ 'b::real_vector"
    and f :: "'b \ real"
  assumes "finite s" "s \ {}"
    and "convex_on C f"
    and "convex C"
    and "(\ i \ s. a i) = 1"
    and "\i. i \ s \ a i \ 0"
    and "\i. i \ s \ y i \ C"
  shows "f (\ i \ s. a i *\<^sub>R y i) \ (\ i \ s. a i * f (y i))"
  using assms
proof (induct s arbitrary: a rule: finite_ne_induct)
  case (singleton i)
  then have ai: "a i = 1"
    by auto
  then show ?case
    by auto
next
  case (insert i s)
  then have "convex_on C f"
    by simp
  from this[unfolded convex_on_def, rule_format]
  have conv: "\x y \. x \ C \ y \ C \ 0 \ \ \ \ \ 1 \
      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
    by simp
  show ?case
  proof (cases "a i = 1")
    case True
    then have "(\ j \ s. a j) = 0"
      using insert by auto
    then have "\j. j \ s \ a j = 0"
      using insert by (fastforce simp: sum_nonneg_eq_0_iff)
    then show ?thesis
      using insert by auto
  next
    case False
    from insert have yai: "y i \ C" "a i \ 0"
      by auto
    have fis: "finite (insert i s)"
      using insert by auto
    then have ai1: "a i \ 1"
      using sum_nonneg_leq_bound[of "insert i s" a] insert by simp
    then have "a i < 1"
      using False by auto
    then have i0: "1 - a i > 0"
      by auto
    let ?a = "\j. a j / (1 - a i)"
    have a_nonneg: "?a j \ 0" if "j \ s" for j
      using i0 insert that by fastforce
    have "(\ j \ insert i s. a j) = 1"
      using insert by auto
    then have "(\ j \ s. a j) = 1 - a i"
      using sum.insert insert by fastforce
    then have "(\ j \ s. a j) / (1 - a i) = 1"
      using i0 by auto
    then have a1: "(\ j \ s. ?a j) = 1"
      unfolding sum_divide_distrib by simp
    have "convex C" using insert by auto
    then have asum: "(\ j \ s. ?a j *\<^sub>R y j) \ C"
      using insert convex_sum [OF \<open>finite s\<close> \<open>convex C\<close> a1 a_nonneg] by auto
    have asum_le: "f (\ j \ s. ?a j *\<^sub>R y j) \ (\ j \ s. ?a j * f (y j))"
      using a_nonneg a1 insert by blast
    have "f (\ j \ insert i s. a j *\<^sub>R y j) = f ((\ j \ s. a j *\<^sub>R y j) + a i *\<^sub>R y i)"
      using sum.insert[of s i "\ j. a j *\<^sub>R y j", OF \finite s\ \i \ s\] insert
      by (auto simp only: add.commute)
    also have "\ = f (((1 - a i) * inverse (1 - a i)) *\<^sub>R (\ j \ s. a j *\<^sub>R y j) + a i *\<^sub>R y i)"
      using i0 by auto
    also have "\ = f ((1 - a i) *\<^sub>R (\ j \ s. (a j * inverse (1 - a i)) *\<^sub>R y j) + a i *\<^sub>R y i)"
      using scaleR_right.sum[of "inverse (1 - a i)" "\ j. a j *\<^sub>R y j" s, symmetric]
      by (auto simp: algebra_simps)
    also have "\ = f ((1 - a i) *\<^sub>R (\ j \ s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)"
      by (auto simp: divide_inverse)
    also have "\ \ (1 - a i) *\<^sub>R f ((\ j \ s. ?a j *\<^sub>R y j)) + a i * f (y i)"
      using conv[of "y i" "(\ j \ s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1]
      by (auto simp: add.commute)
    also have "\ \ (1 - a i) * (\ j \ s. ?a j * f (y j)) + a i * f (y i)"
      using add_right_mono [OF mult_left_mono [of _ _ "1 - a i",
            OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"]
      by simp
    also have "\ = (\ j \ s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
      unfolding sum_distrib_left[of "1 - a i" "\ j. ?a j * f (y j)"]
      using i0 by auto
    also have "\ = (\ j \ s. a j * f (y j)) + a i * f (y i)"
      using i0 by auto
    also have "\ = (\ j \ insert i s. a j * f (y j))"
      using insert by auto
    finally show ?thesis
      by simp
  qed
qed

lemma convex_on_alt:
  fixes C :: "'a::real_vector set"
  shows "convex_on C f \
    (\<forall>x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1 \<longrightarrow>
      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
proof safe
  fix x y
  fix \<mu> :: real
  assume *: "convex_on C f" "x \ C" "y \ C" "0 \ \" "\ \ 1"
  from this[unfolded convex_on_def, rule_format]
  have "0 \ u \ 0 \ v \ u + v = 1 \ f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y" for u v
    by auto
  from this [of "\" "1 - \", simplified] *
  show "f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y"
    by auto
next
  assume *: "\x\C. \y\C. \\. 0 \ \ \ \ \ 1 \
    f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
  {
    fix x y
    fix u v :: real
    assume **: "x \ C" "y \ C" "u \ 0" "v \ 0" "u + v = 1"
    then have[simp]: "1 - u = v" by auto
    from *[rule_format, of x y u]
    have "f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y"
      using ** by auto
  }
  then show "convex_on C f"
    unfolding convex_on_def by auto
qed

lemma convex_on_diff:
  fixes f :: "real \ real"
  assumes f: "convex_on I f"
    and I: "x \ I" "y \ I"
    and t: "x < t" "t < y"
  shows "(f x - f t) / (x - t) \ (f x - f y) / (x - y)"
    and "(f x - f y) / (x - y) \ (f t - f y) / (t - y)"
proof -
  define a where "a \ (t - y) / (x - y)"
  with t have "0 \ a" "0 \ 1 - a"
    by (auto simp: field_simps)
  with f \<open>x \<in> I\<close> \<open>y \<in> I\<close> have cvx: "f (a * x + (1 - a) * y) \<le> a * f x + (1 - a) * f y"
    by (auto simp: convex_on_def)
  have "a * x + (1 - a) * y = a * (x - y) + y"
    by (simp add: field_simps)
  also have "\ = t"
    unfolding a_def using \<open>x < t\<close> \<open>t < y\<close> by simp
  finally have "f t \ a * f x + (1 - a) * f y"
    using cvx by simp
  also have "\ = a * (f x - f y) + f y"
    by (simp add: field_simps)
  finally have "f t - f y \ a * (f x - f y)"
    by simp
  with t show "(f x - f t) / (x - t) \ (f x - f y) / (x - y)"
    by (simp add: le_divide_eq divide_le_eq field_simps a_def)
  with t show "(f x - f y) / (x - y) \ (f t - f y) / (t - y)"
    by (simp add: le_divide_eq divide_le_eq field_simps)
qed

lemma pos_convex_function:
  fixes f :: "real \ real"
  assumes "convex C"
    and leq: "\x y. x \ C \ y \ C \ f' x * (y - x) \ f y - f x"
  shows "convex_on C f"
  unfolding convex_on_alt
  using assms
proof safe
  fix x y \<mu> :: real
  let ?x = "\ *\<^sub>R x + (1 - \) *\<^sub>R y"
  assume *: "convex C" "x \ C" "y \ C" "\ \ 0" "\ \ 1"
  then have "1 - \ \ 0" by auto
  then have xpos: "?x \ C"
    using * unfolding convex_alt by fastforce
  have geq: "\ * (f x - f ?x) + (1 - \) * (f y - f ?x) \
      \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
    using add_mono [OF mult_left_mono [OF leq [OF xpos *(2)] \<open>\<mu> \<ge> 0\<close>]
        mult_left_mono [OF leq [OF xpos *(3)] \<open>1 - \<mu> \<ge> 0\<close>]]
    by auto
  then have "\ * f x + (1 - \) * f y - f ?x \ 0"
    by (auto simp: field_simps)
  then show "f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y"
    by auto
qed

lemma atMostAtLeast_subset_convex:
  fixes C :: "real set"
  assumes "convex C"
    and "x \ C" "y \ C" "x < y"
  shows "{x .. y} \ C"
proof safe
  fix z assume z: "z \ {x .. y}"
  have less: "z \ C" if *: "x < z" "z < y"
  proof -
    let ?\<mu> = "(y - z) / (y - x)"
    have "0 \ ?\" "?\ \ 1"
      using assms * by (auto simp: field_simps)
    then have comb: "?\ * x + (1 - ?\) * y \ C"
      using assms iffD1[OF convex_alt, rule_format, of C y x ?\<mu>]
      by (simp add: algebra_simps)
    have "?\ * x + (1 - ?\) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
      by (auto simp: field_simps)
    also have "\ = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
      using assms by (simp only: add_divide_distrib) (auto simp: field_simps)
    also have "\ = z"
      using assms by (auto simp: field_simps)
    finally show ?thesis
      using comb by auto
  qed
  show "z \ C"
    using z less assms by (auto simp: le_less)
qed

lemma f''_imp_f':
  fixes f :: "real \ real"
  assumes "convex C"
    and f': "\x. x \ C \ DERIV f x :> (f' x)"
    and f'': "\x. x \ C \ DERIV f' x :> (f'' x)"
    and pos: "\x. x \ C \ f'' x \ 0"
    and x: "x \ C"
    and y: "y \ C"
  shows "f' x * (y - x) \ f y - f x"
  using assms
proof -
  have less_imp: "f y - f x \ f' x * (y - x)" "f' y * (x - y) \ f x - f y"
    if *: "x \ C" "y \ C" "y > x" for x y :: real
  proof -
    from * have ge: "y - x > 0" "y - x \ 0"
      by auto
    from * have le: "x - y < 0" "x - y \ 0"
      by auto
    then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1"
      using subsetD[OF atMostAtLeast_subset_convex[OF \<open>convex C\<close> \<open>x \<in> C\<close> \<open>y \<in> C\<close> \<open>x < y\<close>],
          THEN f', THEN MVT2[OF \x < y\, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
      by auto
    then have "z1 \ C"
      using atMostAtLeast_subset_convex \<open>convex C\<close> \<open>x \<in> C\<close> \<open>y \<in> C\<close> \<open>x < y\<close>
      by fastforce
    from z1 have z1': "f x - f y = (x - y) * f' z1"
      by (simp add: field_simps)
    obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
      using subsetD[OF atMostAtLeast_subset_convex[OF \<open>convex C\<close> \<open>x \<in> C\<close> \<open>z1 \<in> C\<close> \<open>x < z1\<close>],
          THEN f'', THEN MVT2[OF \<open>x < z1\<close>, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
      by auto
    obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3"
      using subsetD[OF atMostAtLeast_subset_convex[OF \<open>convex C\<close> \<open>z1 \<in> C\<close> \<open>y \<in> C\<close> \<open>z1 < y\<close>],
          THEN f'', THEN MVT2[OF \<open>z1 < y\<close>, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
      by auto
    have "f' y - (f x - f y) / (x - y) = f' y - f' z1"
      using * z1' by auto
    also have "\ = (y - z1) * f'' z3"
      using z3 by auto
    finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3"
      by simp
    have A': "y - z1 \ 0"
      using z1 by auto
    have "z3 \ C"
      using z3 * atMostAtLeast_subset_convex \<open>convex C\<close> \<open>x \<in> C\<close> \<open>z1 \<in> C\<close> \<open>x < z1\<close>
      by fastforce
    then have B': "f'' z3 \ 0"
      using assms by auto
    from A' B' have "(y - z1) * f'' z3 \ 0"
      by auto
    from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0"
      by auto
    from mult_right_mono_neg[OF this le(2)]
    have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \ 0 * (x - y)"
      by (simp add: algebra_simps)
    then have "f' y * (x - y) - (f x - f y) \ 0"
      using le by auto
    then have res: "f' y * (x - y) \ f x - f y"
      by auto
    have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
      using * z1 by auto
    also have "\ = (z1 - x) * f'' z2"
      using z2 by auto
    finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2"
      by simp
    have A: "z1 - x \ 0"
      using z1 by auto
    have "z2 \ C"
      using z2 z1 * atMostAtLeast_subset_convex \<open>convex C\<close> \<open>z1 \<in> C\<close> \<open>y \<in> C\<close> \<open>z1 < y\<close>
      by fastforce
    then have B: "f'' z2 \ 0"
      using assms by auto
    from A B have "(z1 - x) * f'' z2 \ 0"
      by auto
    with cool have "(f y - f x) / (y - x) - f' x \ 0"
      by auto
    from mult_right_mono[OF this ge(2)]
    have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \ 0 * (y - x)"
      by (simp add: algebra_simps)
    then have "f y - f x - f' x * (y - x) \ 0"
      using ge by auto
    then show "f y - f x \ f' x * (y - x)" "f' y * (x - y) \ f x - f y"
      using res by auto
  qed
  show ?thesis
  proof (cases "x = y")
    case True
    with x y show ?thesis by auto
  next
    case False
    with less_imp x y show ?thesis
      by (auto simp: neq_iff)
  qed
qed

lemma f''_ge0_imp_convex:
  fixes f :: "real \ real"
  assumes conv: "convex C"
    and f': "\x. x \ C \ DERIV f x :> (f' x)"
    and f'': "\x. x \ C \ DERIV f' x :> (f'' x)"
    and pos: "\x. x \ C \ f'' x \ 0"
  shows "convex_on C f"
  using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function
  by fastforce

lemma minus_log_convex:
  fixes b :: real
  assumes "b > 1"
  shows "convex_on {0 <..} (\ x. - log b x)"
proof -
  have "\z. z > 0 \ DERIV (log b) z :> 1 / (ln b * z)"
    using DERIV_log by auto
  then have f': "\z. z > 0 \ DERIV (\ z. - log b z) z :> - 1 / (ln b * z)"
    by (auto simp: DERIV_minus)
  have "\z::real. z > 0 \ DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
    using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
  from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
  have "\z::real. z > 0 \
    DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
    by auto
  then have f''0: "\z::real. z > 0 \
    DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
    unfolding inverse_eq_divide by (auto simp: mult.assoc)
  have f''_ge0: "\z::real. z > 0 \ 1 / (ln b * z * z) \ 0"
    using \<open>b > 1\<close> by (auto intro!: less_imp_le)
  from f''_ge0_imp_convex[OF convex_real_interval(3), unfolded greaterThan_iff, OF f' f''0 f''_ge0]
  show ?thesis
    by auto
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Convexity of real functions\<close>

lemma convex_on_realI:
  assumes "connected A"
    and "\x. x \ A \ (f has_real_derivative f' x) (at x)"
    and "\x y. x \ A \ y \ A \ x \ y \ f' x \ f' y"
  shows "convex_on A f"
proof (rule convex_on_linorderI)
  fix t x y :: real
  assume t: "t > 0" "t < 1"
  assume xy: "x \ A" "y \ A" "x < y"
  define z where "z = (1 - t) * x + t * y"
  with \<open>connected A\<close> and xy have ivl: "{x..y} \<subseteq> A"
    using connected_contains_Icc by blast

  from xy t have xz: "z > x"
    by (simp add: z_def algebra_simps)
  have "y - z = (1 - t) * (y - x)"
    by (simp add: z_def algebra_simps)
  also from xy t have "\ > 0"
    by (intro mult_pos_pos) simp_all
  finally have yz: "z < y"
    by simp

  from assms xz yz ivl t have "\\. \ > x \ \ < z \ f z - f x = (z - x) * f' \"
    by (intro MVT2) (auto intro!: assms(2))
  then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)"
    by auto
  from assms xz yz ivl t have "\\. \ > z \ \ < y \ f y - f z = (y - z) * f' \"
    by (intro MVT2) (auto intro!: assms(2))
  then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)"
    by auto

  from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" ..
  also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A"
    by auto
  with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>"
    by (intro assms(3)) auto
  also from \<xi>(3) have "f' \<xi> = (f z - f x) / (z - x)" .
  finally have "(f y - f z) * (z - x) \ (f z - f x) * (y - z)"
    using xz yz by (simp add: field_simps)
  also have "z - x = t * (y - x)"
    by (simp add: z_def algebra_simps)
  also have "y - z = (1 - t) * (y - x)"
    by (simp add: z_def algebra_simps)
  finally have "(f y - f z) * t \ (f z - f x) * (1 - t)"
    using xy by simp
  then show "(1 - t) * f x + t * f y \ f ((1 - t) *\<^sub>R x + t *\<^sub>R y)"
    by (simp add: z_def algebra_simps)
qed

lemma convex_on_inverse:
  assumes "A \ {0<..}"
  shows "convex_on A (inverse :: real \ real)"
proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "\x. -inverse (x^2)"])
  fix u v :: real
  assume "u \ {0<..}" "v \ {0<..}" "u \ v"
  with assms show "-inverse (u^2) \ -inverse (v^2)"
    by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all)
qed (insert assms, auto intro!: derivative_eq_intros simp: field_split_simps power2_eq_square)

lemma convex_onD_Icc':
  assumes "convex_on {x..y} f" "c \ {x..y}"
  defines "d \ y - x"
  shows "f c \ (f y - f x) / d * (c - x) + f x"
proof (cases x y rule: linorder_cases)
  case less
  then have d: "d > 0"
    by (simp add: d_def)
  from assms(2) less have A: "0 \ (c - x) / d" "(c - x) / d \ 1"
    by (simp_all add: d_def field_split_simps)
  have "f c = f (x + (c - x) * 1)"
    by simp
  also from less have "1 = ((y - x) / d)"
    by (simp add: d_def)
  also from d have "x + (c - x) * \ = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y"
    by (simp add: field_simps)
  also have "f \ \ (1 - (c - x) / d) * f x + (c - x) / d * f y"
    using assms less by (intro convex_onD_Icc) simp_all
  also from d have "\ = (f y - f x) / d * (c - x) + f x"
    by (simp add: field_simps)
  finally show ?thesis .
qed (insert assms(2), simp_all)

lemma convex_onD_Icc'':
  assumes "convex_on {x..y} f" "c \ {x..y}"
  defines "d \ y - x"
  shows "f c \ (f x - f y) / d * (y - c) + f y"
proof (cases x y rule: linorder_cases)
  case less
  then have d: "d > 0"
    by (simp add: d_def)
  from assms(2) less have A: "0 \ (y - c) / d" "(y - c) / d \ 1"
    by (simp_all add: d_def field_split_simps)
  have "f c = f (y - (y - c) * 1)"
    by simp
  also from less have "1 = ((y - x) / d)"
    by (simp add: d_def)
  also from d have "y - (y - c) * \ = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y"
    by (simp add: field_simps)
  also have "f \ \ (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y"
    using assms less by (intro convex_onD_Icc) (simp_all add: field_simps)
  also from d have "\ = (f x - f y) / d * (y - c) + f y"
    by (simp add: field_simps)
  finally show ?thesis .
qed (insert assms(2), simp_all)

lemma convex_translation_eq [simp]:
  "convex ((+) a ` s) \ convex s"
  by (metis convex_translation translation_galois)

lemma convex_translation_subtract_eq [simp]:
  "convex ((\b. b - a) ` s) \ convex s"
  using convex_translation_eq [of "- a"] by (simp cong: image_cong_simp)

lemma convex_linear_image_eq [simp]:
    fixes f :: "'a::real_vector \ 'b::real_vector"
    shows "\linear f; inj f\ \ convex (f ` s) \ convex s"
    by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq)

lemma fst_snd_linear: "linear (\(x,y). x + y)"
  unfolding linear_iff by (simp add: algebra_simps)

lemma vector_choose_size:
  assumes "0 \ c"
  obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c"
proof -
  obtain a::'a where "a \ 0"
    using UNIV_not_singleton UNIV_eq_I set_zero singletonI by fastforce
  then show ?thesis
    by (rule_tac x="scaleR (c / norm a) a" in that) (simp add: assms)
qed

lemma vector_choose_dist:
  assumes "0 \ c"
  obtains y :: "'a::{real_normed_vector, perfect_space}" where "dist x y = c"
by (metis add_diff_cancel_left' assms dist_commute dist_norm vector_choose_size)

lemma sum_delta'':
  fixes s::"'a::real_vector set"
  assumes "finite s"
  shows "(\x\s. (if y = x then f x else 0) *\<^sub>R x) = (if y\s then (f y) *\<^sub>R y else 0)"
proof -
  have *: "\x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)"
    by auto
  show ?thesis
    unfolding * using sum.delta[OF assms, of y "\x. f x *\<^sub>R x"] by auto
qed

lemma dist_triangle_eq:
  fixes x y z :: "'a::real_inner"
  shows "dist x z = dist x y + dist y z \
    norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
proof -
  have *: "x - y + (y - z) = x - z" by auto
  show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
    by (auto simp:norm_minus_commute)
qed

subsection \<open>Cones\<close>

definition\<^marker>\<open>tag important\<close> cone :: "'a::real_vector set \<Rightarrow> bool"
  where "cone s \ (\x\s. \c\0. c *\<^sub>R x \ s)"

lemma cone_empty[intro, simp]: "cone {}"
  unfolding cone_def by auto

lemma cone_univ[intro, simp]: "cone UNIV"
  unfolding cone_def by auto

lemma cone_Inter[intro]: "\s\f. cone s \ cone (\f)"
  unfolding cone_def by auto

lemma subspace_imp_cone: "subspace S \ cone S"
  by (simp add: cone_def subspace_scale)

subsubsection \<open>Conic hull\<close>

lemma cone_cone_hull: "cone (cone hull S)"
  unfolding hull_def by auto

lemma cone_hull_eq: "cone hull S = S \ cone S"
  by (metis cone_cone_hull hull_same)

lemma mem_cone:
  assumes "cone S" "x \ S" "c \ 0"
  shows "c *\<^sub>R x \ S"
  using assms cone_def[of S] by auto

lemma cone_contains_0:
  assumes "cone S"
  shows "S \ {} \ 0 \ S"
  using assms mem_cone by fastforce

lemma cone_0: "cone {0}"
  unfolding cone_def by auto

lemma cone_Union[intro]: "(\s\f. cone s) \ cone (\f)"
  unfolding cone_def by blast

lemma cone_iff:
  assumes "S \ {}"
  shows "cone S \ 0 \ S \ (\c. c > 0 \ ((*\<^sub>R) c) ` S = S)"
proof -
  {
    assume "cone S"
    {
      fix c :: real
      assume "c > 0"
      {
        fix x
        assume "x \ S"
        then have "x \ ((*\<^sub>R) c) ` S"
          unfolding image_def
          using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"]
            exI[of "(\t. t \ S \ x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
          by auto
      }
      moreover
      {
        fix x
        assume "x \ ((*\<^sub>R) c) ` S"
        then have "x \ S"
          using \<open>0 < c\<close> \<open>cone S\<close> mem_cone by fastforce
      }
      ultimately have "((*\<^sub>R) c) ` S = S" by blast
    }
    then have "0 \ S \ (\c. c > 0 \ ((*\<^sub>R) c) ` S = S)"
      using \<open>cone S\<close> cone_contains_0[of S] assms by auto
  }
  moreover
  {
    assume a: "0 \ S \ (\c. c > 0 \ ((*\<^sub>R) c) ` S = S)"
    {
      fix x
      assume "x \ S"
      fix c1 :: real
      assume "c1 \ 0"
      then have "c1 = 0 \ c1 > 0" by auto
      then have "c1 *\<^sub>R x \ S" using a \x \ S\ by auto
    }
    then have "cone S" unfolding cone_def by auto
  }
  ultimately show ?thesis by blast
qed

lemma cone_hull_empty: "cone hull {} = {}"
  by (metis cone_empty cone_hull_eq)

lemma cone_hull_empty_iff: "S = {} \ cone hull S = {}"
  by (metis bot_least cone_hull_empty hull_subset xtrans(5))

lemma cone_hull_contains_0: "S \ {} \ 0 \ cone hull S"
  using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S]
  by auto

lemma mem_cone_hull:
  assumes "x \ S" "c \ 0"
  shows "c *\<^sub>R x \ cone hull S"
  by (metis assms cone_cone_hull hull_inc mem_cone)

proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \ 0 \ x \ S}"
  (is "?lhs = ?rhs")
proof -
  {
    fix x
    assume "x \ ?rhs"
    then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \ 0" "xx \ S"
      by auto
    fix c :: real
    assume c: "c \ 0"
    then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx"
      using x by (simp add: algebra_simps)
    moreover
    have "c * cx \ 0" using c x by auto
    ultimately
    have "c *\<^sub>R x \ ?rhs" using x by auto
  }
  then have "cone ?rhs"
    unfolding cone_def by auto
  then have "?rhs \ Collect cone"
    unfolding mem_Collect_eq by auto
  {
    fix x
    assume "x \ S"
    then have "1 *\<^sub>R x \ ?rhs"
      using zero_le_one by blast
    then have "x \ ?rhs" by auto
  }
  then have "S \ ?rhs" by auto
  then have "?lhs \ ?rhs"
    using \<open>?rhs \<in> Collect cone\<close> hull_minimal[of S "?rhs" "cone"] by auto
  moreover
  {
    fix x
    assume "x \ ?rhs"
    then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \ 0" "xx \ S"
      by auto
    then have "xx \ cone hull S"
      using hull_subset[of S] by auto
    then have "x \ ?lhs"
      using x cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
  }
  ultimately show ?thesis by auto
qed

lemma convex_cone:
  "convex s \ cone s \ (\x\s. \y\s. (x + y) \ s) \ (\x\s. \c\0. (c *\<^sub>R x) \ s)"
  (is "?lhs = ?rhs")
proof -
  {
    fix x y
    assume "x\s" "y\s" and ?lhs
    then have "2 *\<^sub>R x \s" "2 *\<^sub>R y \ s"
      unfolding cone_def by auto
    then have "x + y \ s"
      using \<open>?lhs\<close>[unfolded convex_def, THEN conjunct1]
      apply (erule_tac x="2*\<^sub>R x" in ballE)
      apply (erule_tac x="2*\<^sub>R y" in ballE)
      apply (erule_tac x="1/2" in allE, simp)
      apply (erule_tac x="1/2" in allE, auto)
      done
  }
  then show ?thesis
    unfolding convex_def cone_def by blast
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Connectedness of convex sets\<close>

lemma convex_connected:
  fixes S :: "'a::real_normed_vector set"
  assumes "convex S"
  shows "connected S"
proof (rule connectedI)
  fix A B
  assume "open A" "open B" "A \ B \ S = {}" "S \ A \ B"
  moreover
  assume "A \ S \ {}" "B \ S \ {}"
  then obtain a b where a: "a \ A" "a \ S" and b: "b \ B" "b \ S" by auto
  define f where [abs_def]: "f u = u *\<^sub>R a + (1 - u) *\<^sub>R b" for u
  then have "continuous_on {0 .. 1} f"
    by (auto intro!: continuous_intros)
  then have "connected (f ` {0 .. 1})"
    by (auto intro!: connected_continuous_image)
  note connectedD[OF this, of A B]
  moreover have "a \ A \ f ` {0 .. 1}"
    using a by (auto intro!: image_eqI[of _ _ 1] simp: f_def)
  moreover have "b \ B \ f ` {0 .. 1}"
    using b by (auto intro!: image_eqI[of _ _ 0] simp: f_def)
  moreover have "f ` {0 .. 1} \ S"
    using \<open>convex S\<close> a b unfolding convex_def f_def by auto
  ultimately show False by auto
qed

corollary%unimportant connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
by (simp add: convex_connected)

lemma convex_prod:
  assumes "\i. i \ Basis \ convex {x. P i x}"
  shows "convex {x. \i\Basis. P i (x\i)}"
  using assms unfolding convex_def
  by (auto simp: inner_add_left)

lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\i\Basis. 0 \ x\i)}"
by (rule convex_prod) (simp flip: atLeast_def)

subsection \<open>Convex hull\<close>

lemma convex_convex_hull [iff]: "convex (convex hull s)"
  unfolding hull_def
  using convex_Inter[of "{t. convex t \ s \ t}"]
  by auto

lemma convex_hull_subset:
    "s \ convex hull t \ convex hull s \ convex hull t"
  by (simp add: subset_hull)

lemma convex_hull_eq: "convex hull s = s \ convex s"
  by (metis convex_convex_hull hull_same)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Convex hull is "preserved" by a linear function\<close>

lemma convex_hull_linear_image:
  assumes f: "linear f"
  shows "f ` (convex hull s) = convex hull (f ` s)"
proof
  show "convex hull (f ` s) \ f ` (convex hull s)"
    by (intro hull_minimal image_mono hull_subset convex_linear_image assms convex_convex_hull)
  show "f ` (convex hull s) \ convex hull (f ` s)"
  proof (unfold image_subset_iff_subset_vimage, rule hull_minimal)
    show "s \ f -` (convex hull (f ` s))"
      by (fast intro: hull_inc)
    show "convex (f -` (convex hull (f ` s)))"
      by (intro convex_linear_vimage [OF f] convex_convex_hull)
  qed
qed

lemma in_convex_hull_linear_image:
  assumes "linear f"
    and "x \ convex hull s"
  shows "f x \ convex hull (f ` s)"
  using convex_hull_linear_image[OF assms(1)] assms(2) by auto

lemma convex_hull_Times:
  "convex hull (s \ t) = (convex hull s) \ (convex hull t)"
proof
  show "convex hull (s \ t) \ (convex hull s) \ (convex hull t)"
    by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull)
  have "(x, y) \ convex hull (s \ t)" if x: "x \ convex hull s" and y: "y \ convex hull t" for x y
  proof (rule hull_induct [OF x], rule hull_induct [OF y])
    fix x y assume "x \ s" and "y \ t"
    then show "(x, y) \ convex hull (s \ t)"
      by (simp add: hull_inc)
  next
    fix x let ?S = "((\y. (0, y)) -` (\p. (- x, 0) + p) ` (convex hull s \ t))"
    have "convex ?S"
      by (intro convex_linear_vimage convex_translation convex_convex_hull,
        simp add: linear_iff)
    also have "?S = {y. (x, y) \ convex hull (s \ t)}"
      by (auto simp: image_def Bex_def)
    finally show "convex {y. (x, y) \ convex hull (s \ t)}" .
  next
    show "convex {x. (x, y) \ convex hull s \ t}"
    proof -
      fix y let ?S = "((\x. (x, 0)) -` (\p. (0, - y) + p) ` (convex hull s \ t))"
      have "convex ?S"
      by (intro convex_linear_vimage convex_translation convex_convex_hull,
        simp add: linear_iff)
      also have "?S = {x. (x, y) \ convex hull (s \ t)}"
        by (auto simp: image_def Bex_def)
      finally show "convex {x. (x, y) \ convex hull (s \ t)}" .
    qed
  qed
  then show "(convex hull s) \ (convex hull t) \ convex hull (s \ t)"
    unfolding subset_eq split_paired_Ball_Sigma by blast
qed

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Stepping theorems for convex hulls of finite sets\<close>

lemma convex_hull_empty[simp]: "convex hull {} = {}"
  by (rule hull_unique) auto

lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
  by (rule hull_unique) auto

lemma convex_hull_insert:
  fixes S :: "'a::real_vector set"
  assumes "S \ {}"
  shows "convex hull (insert a S) =
         {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull S) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}"
  (is "_ = ?hull")
proof (intro equalityI hull_minimal subsetI)
  fix x
  assume "x \ insert a S"
  then have "\u\0. \v\0. u + v = 1 \ (\b. b \ convex hull S \ x = u *\<^sub>R a + v *\<^sub>R b)"
  unfolding insert_iff
  proof
    assume "x = a"
    then show ?thesis
      by (rule_tac x=1 in exI) (use assms hull_subset in fastforce)
  next
    assume "x \ S"
    with hull_subset[of S convex] show ?thesis
      by force
  qed
  then show "x \ ?hull"
    by simp
next
  fix x
  assume "x \ ?hull"
  then obtain u v b where obt: "u\0" "v\0" "u + v = 1" "b \ convex hull S" "x = u *\<^sub>R a + v *\<^sub>R b"
    by auto
  have "a \ convex hull insert a S" "b \ convex hull insert a S"
    using hull_mono[of S "insert a S" convex] hull_mono[of "{a}" "insert a S" convex] and obt(4)
    by auto
  then show "x \ convex hull insert a S"
    unfolding obt(5) using obt(1-3)
    by (rule convexD [OF convex_convex_hull])
next
  show "convex ?hull"
  proof (rule convexI)
    fix x y u v
    assume as: "(0::real) \ u" "0 \ v" "u + v = 1" and x: "x \ ?hull" and y: "y \ ?hull"
    from x obtain u1 v1 b1 where
      obt1: "u1\0" "v1\0" "u1 + v1 = 1" "b1 \ convex hull S" and xeq: "x = u1 *\<^sub>R a + v1 *\<^sub>R b1"
      by auto
    from y obtain u2 v2 b2 where
      obt2: "u2\0" "v2\0" "u2 + v2 = 1" "b2 \ convex hull S" and yeq: "y = u2 *\<^sub>R a + v2 *\<^sub>R b2"
      by auto
    have *: "\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
      by (auto simp: algebra_simps)
    have "\b \ convex hull S. u *\<^sub>R x + v *\<^sub>R y =
      (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
    proof (cases "u * v1 + v * v2 = 0")
      case True
      have *: "\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
        by (auto simp: algebra_simps)
      have eq0: "u * v1 = 0" "v * v2 = 0"
        using True mult_nonneg_nonneg[OF \<open>u\<ge>0\<close> \<open>v1\<ge>0\<close>] mult_nonneg_nonneg[OF \<open>v\<ge>0\<close> \<open>v2\<ge>0\<close>]
        by arith+
      then have "u * u1 + v * u2 = 1"
        using as(3) obt1(3) obt2(3) by auto
      then show ?thesis
        using "*" eq0 as obt1(4) xeq yeq by auto
    next
      case False
      have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)"
        using as(3) obt1(3) obt2(3) by (auto simp: field_simps)
      also have "\ = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)"
        using as(3) obt1(3) obt2(3) by (auto simp: field_simps)
      also have "\ = u * v1 + v * v2"
        by simp
      finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
      let ?b = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2"
      have zeroes: "0 \ u * v1 + v * v2" "0 \ u * v1" "0 \ u * v1 + v * v2" "0 \ v * v2"
        using as(1,2) obt1(1,2) obt2(1,2) by auto
      show ?thesis
      proof
        show "u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (?b - (u * u1) *\<^sub>R ?b - (v * u2) *\<^sub>R ?b)"
          unfolding xeq yeq * **
          using False by (auto simp: scaleR_left_distrib scaleR_right_distrib)
        show "?b \ convex hull S"
          using False zeroes obt1(4) obt2(4)
          by (auto simp: convexD [OF convex_convex_hull] scaleR_left_distrib scaleR_right_distrib  add_divide_distrib[symmetric]  zero_le_divide_iff)
      qed
    qed
    then obtain b where b: "b \ convex hull S"
       "u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" ..

    have u1: "u1 \ 1"
      unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
    have u2: "u2 \ 1"
      unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
    have "u1 * u + u2 * v \ max u1 u2 * u + max u1 u2 * v"
    proof (rule add_mono)
      show "u1 * u \ max u1 u2 * u" "u2 * v \ max u1 u2 * v"
        by (simp_all add: as mult_right_mono)
    qed
    also have "\ \ 1"
      unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
    finally have le1: "u1 * u + u2 * v \ 1" .
    show "u *\<^sub>R x + v *\<^sub>R y \ ?hull"
    proof (intro CollectI exI conjI)
      show "0 \ u * u1 + v * u2"
        by (simp add: as(1) as(2) obt1(1) obt2(1))
      show "0 \ 1 - u * u1 - v * u2"
        by (simp add: le1 diff_diff_add mult.commute)
    qed (use b in \<open>auto simp: algebra_simps\<close>)
  qed
qed

lemma convex_hull_insert_alt:
   "convex hull (insert a S) =
     (if S = {} then {a}
      else {(1 - u) *\<^sub>R a + u *\<^sub>R x |x u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> convex hull S})"
  apply (auto simp: convex_hull_insert)
  using diff_eq_eq apply fastforce
  using diff_add_cancel diff_ge_0_iff_ge by blast

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Explicit expression for convex hull\<close>

proposition convex_hull_indexed:
  fixes S :: "'a::real_vector set"
  shows "convex hull S =
    {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
                (sum u {1..k} = 1) \<and> (\<Sum>i = 1..k. u i *\<^sub>R x i) = y}"
    (is "?xyz = ?hull")
proof (rule hull_unique [OF _ convexI])
  show "S \ ?hull"
    by (clarsimp, rule_tac x=1 in exI, rule_tac x="\x. 1" in exI, auto)
next
  fix T
  assume "S \ T" "convex T"
  then show "?hull \ T"
    by (blast intro: convex_sum)
next
  fix x y u v
  assume uv: "0 \ u" "0 \ v" "u + v = (1::real)"
  assume xy: "x \ ?hull" "y \ ?hull"
  from xy obtain k1 u1 x1 where
    x [rule_format]: "\i\{1::nat..k1}. 0\u1 i \ x1 i \ S"
                      "sum u1 {Suc 0..k1} = 1" "(\i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
    by auto
  from xy obtain k2 u2 x2 where
    y [rule_format]: "\i\{1::nat..k2}. 0\u2 i \ x2 i \ S"
                     "sum u2 {Suc 0..k2} = 1" "(\i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
    by auto
  have *: "\P (x::'a) y s t i. (if P i then s else t) *\<^sub>R (if P i then x else y) = (if P i then s *\<^sub>R x else t *\<^sub>R y)"
          "{1..k1 + k2} \ {1..k1} = {1..k1}" "{1..k1 + k2} \ - {1..k1} = (\i. i + k1) ` {1..k2}"
    by auto
  have inj: "inj_on (\i. i + k1) {1..k2}"
    unfolding inj_on_def by auto
  let ?uu = "\i. if i \ {1..k1} then u * u1 i else v * u2 (i - k1)"
  let ?xx = "\i. if i \ {1..k1} then x1 i else x2 (i - k1)"
  show "u *\<^sub>R x + v *\<^sub>R y \ ?hull"
  proof (intro CollectI exI conjI ballI)
    show "0 \ ?uu i" "?xx i \ S" if "i \ {1..k1+k2}" for i
      using that by (auto simp add: le_diff_conv uv(1) x(1) uv(2) y(1))
    show "(\i = 1..k1 + k2. ?uu i) = 1" "(\i = 1..k1 + k2. ?uu i *\<^sub>R ?xx i) = u *\<^sub>R x + v *\<^sub>R y"
      unfolding * sum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]]
        sum.reindex[OF inj] Collect_mem_eq o_def
      unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_distrib_left[symmetric]
      by (simp_all add: sum_distrib_left[symmetric]  x(2,3) y(2,3) uv(3))
  qed
qed

lemma convex_hull_finite:
  fixes S :: "'a::real_vector set"
  assumes "finite S"
  shows "convex hull S = {y. \u. (\x\S. 0 \ u x) \ sum u S = 1 \ sum (\x. u x *\<^sub>R x) S = y}"
  (is "?HULL = _")
proof (rule hull_unique [OF _ convexI]; clarify)
  fix x
  assume "x \ S"
  then show "\u. (\x\S. 0 \ u x) \ sum u S = 1 \ (\x\S. u x *\<^sub>R x) = x"
    by (rule_tac x="\y. if x=y then 1 else 0" in exI) (auto simp: sum.delta'[OF assms] sum_delta''[OF assms])
next
  fix u v :: real
  assume uv: "0 \ u" "0 \ v" "u + v = 1"
  fix ux assume ux [rule_format]: "\x\S. 0 \ ux x" "sum ux S = (1::real)"
  fix uy assume uy [rule_format]: "\x\S. 0 \ uy x" "sum uy S = (1::real)"
  have "0 \ u * ux x + v * uy x" if "x\S" for x
    by (simp add: that uv ux(1) uy(1))
  moreover
  have "(\x\S. u * ux x + v * uy x) = 1"
    unfolding sum.distrib and sum_distrib_left[symmetric] ux(2) uy(2)
    using uv(3) by auto
  moreover
  have "(\x\S. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\S. ux x *\<^sub>R x) + v *\<^sub>R (\x\S. uy x *\<^sub>R x)"
    unfolding scaleR_left_distrib sum.distrib scaleR_scaleR[symmetric] scaleR_right.sum [symmetric]
    by auto
  ultimately
  show "\uc. (\x\S. 0 \ uc x) \ sum uc S = 1 \
             (\<Sum>x\<in>S. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>S. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>S. uy x *\<^sub>R x)"
    by (rule_tac x="\x. u * ux x + v * uy x" in exI, auto)
qed (use assms in \<open>auto simp: convex_explicit\<close>)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Another formulation\<close>

text "Formalized by Lars Schewe."

lemma convex_hull_explicit:
  fixes p :: "'a::real_vector set"
  shows "convex hull p =
    {y. \<exists>S u. finite S \<and> S \<subseteq> p \<and> (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
  (is "?lhs = ?rhs")
proof -
  {
    fix x
    assume "x\?lhs"
    then obtain k u y where
        obt: "\i\{1::nat..k}. 0 \ u i \ y i \ p" "sum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x"
      unfolding convex_hull_indexed by auto

    have fin: "finite {1..k}" by auto
    have fin': "\v. finite {i \ {1..k}. y i = v}" by auto
    {
      fix j
      assume "j\{1..k}"
      then have "y j \ p \ 0 \ sum u {i. Suc 0 \ i \ i \ k \ y i = y j}"
        using obt(1)[THEN bspec[where x=j]] and obt(2)
        by (metis (no_types, lifting) One_nat_def atLeastAtMost_iff mem_Collect_eq obt(1) sum_nonneg)
    }
    moreover
    have "(\v\y ` {1..k}. sum u {i \ {1..k}. y i = v}) = 1"
      unfolding sum.image_gen[OF fin, symmetric] using obt(2) by auto
    moreover have "(\v\y ` {1..k}. sum u {i \ {1..k}. y i = v} *\<^sub>R v) = x"
      using sum.image_gen[OF fin, of "\i. u i *\<^sub>R y i" y, symmetric]
      unfolding scaleR_left.sum using obt(3) by auto
    ultimately
    have "\S u. finite S \ S \ p \ (\x\S. 0 \ u x) \ sum u S = 1 \ (\v\S. u v *\<^sub>R v) = x"
      apply (rule_tac x="y ` {1..k}" in exI)
      apply (rule_tac x="\v. sum u {i\{1..k}. y i = v}" in exI, auto)
      done
    then have "x\?rhs" by auto
  }
  moreover
  {
    fix y
    assume "y\?rhs"
    then obtain S u where
      obt: "finite S" "S \ p" "\x\S. 0 \ u x" "sum u S = 1" "(\v\S. u v *\<^sub>R v) = y"
      by auto

    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
    {
      fix i :: nat
      assume "i\{1..card S}"
      then have "f i \ S"
        using f(2) by blast
      then have "0 \ u (f i)" "f i \ p" using obt(2,3) by auto
    }
    moreover have *: "finite {1..card S}" by auto
    {
      fix y
      assume "y\S"
      then obtain i where "i\{1..card S}" "f i = y"
        using f using image_iff[of y f "{1..card S}"]
        by auto
      then have "{x. Suc 0 \ x \ x \ card S \ f x = y} = {i}"
        using f(1) inj_onD by fastforce
      then have "card {x. Suc 0 \ x \ x \ card S \ f x = y} = 1" by auto
      then have "(\x\{x \ {1..card S}. f x = y}. u (f x)) = u y"
          "(\x\{x \ {1..card S}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
        by (auto simp: sum_constant_scaleR)
    }
    then have "(\x = 1..card S. u (f x)) = 1" "(\i = 1..card S. u (f i) *\<^sub>R f i) = y"
      unfolding sum.image_gen[OF *(1), of "\x. u (f x) *\<^sub>R f x" f]
        and sum.image_gen[OF *(1), of "\x. u (f x)" f]
      unfolding f
      using sum.cong [of S S "\y. (\x\{x \ {1..card S}. f x = y}. u (f x) *\<^sub>R f x)" "\v. u v *\<^sub>R v"]
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.54 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.