Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Analysis/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 115 kB

Quelle Convex.thy Sprache: 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"  "HOL-Library.FuncSet"
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"
  by (simp add: assms convex_def)

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")
  by (metis convex_def diff_eq_eq diff_ge_0_iff_ge)

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 a: "(\ i \ S. a i) = 1" "\i. i \ S \ a i \ 0"
    and C: "\i. i \ S \ y i \ C"
  shows "(\ j \ S. a j *\<^sub>R y j) \ C"
  using \<open>finite S\<close> a C
proof (induction arbitrary: a set: finite)
  case empty
  then show ?case by simp
next
  case (insert i S)
  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 insert show ?thesis
      by (simp add: sum_nonneg_eq_0_iff)
  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 insert
      by (simp add: insert.IH flip: sum_divide_distrib)
    with \<open>convex C\<close> insert \<open>0 \<le> sum a S\<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 (simp add: convex_def)
    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 \
    (\<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> (sum u {1..k} = 1)
      \<longrightarrow> sum (\<lambda>i. u i *\<^sub>R x i) {1..k} \<in> S)"
  (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    by (metis (full_types) atLeastAtMost_iff convex_sum finite_atLeastAtMost)
  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 S: "(\j \ {1..2}. ?u j *\<^sub>R ?x j) \ S"
      using sum.If_cases[of "{(1 :: nat) .. 2}" "\x. x = 1" "\x. \" "\x. 1 - \"]
      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
    with sum.atLeast_Suc_atMost
    have "(\j \ {1..2}. ?u j *\<^sub>R ?x j) = \ *\<^sub>R x + (1 - \) *\<^sub>R y"
      by (smt (verit, best) Suc_1 Suc_eq_plus1 add_0 le_add1)
    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"
    by (simp add: convex_sum subsetD)
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
        by (simp add: "**")
    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 \ convex S \
    (\<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)"

definition\<^marker>\<open>tag important\<close> concave_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
  where "concave_on S f \ convex_on S (\x. - f x)"

lemma convex_on_iff_concave: "convex_on S f = concave_on S (\x. - f x)"
  by (simp add: concave_on_def)

lemma concave_on_iff:
  "concave_on S f \ convex S \
    (\<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) \<ge> u * f x + v * f y)"
  by (auto simp: concave_on_def convex_on_def algebra_simps)

lemma concave_onD:
  assumes "concave_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) \<ge> (1 - t) * f x + t * f y"
  using assms by (auto simp: concave_on_iff)

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"
    and "convex A"
  shows "convex_on A f"
  unfolding convex_on_def
  by (smt (verit, del_insts) assms mult_cancel_right1 mult_eq_0_iff scaleR_collapse scaleR_eq_0_iff)

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_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"
    and "convex A"
  shows "convex_on A f"
  by (smt (verit, best) add.commute assms convex_onI distrib_left linorder_cases mult.commute mult_cancel_left2 scaleR_collapse)

lemma concave_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) \<ge> (1 - t) * f x + t * f y"
    and "convex A"
  shows "concave_on A f"
  by (smt (verit) assms concave_on_def convex_on_linorderI mult_minus_right)

lemma convex_on_imp_convex: "convex_on A f \ convex A"
  by (auto simp: convex_on_def)

lemma concave_on_imp_convex: "concave_on A f \ convex A"
  by (simp add: concave_on_def convex_on_imp_convex)

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 S\ \ convex_on S f"
  by (simp add: convex_on_def subset_iff)

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)
  }
  with assms show ?thesis
    unfolding convex_on_def by auto
qed

lemma convex_on_ident: "convex_on S (\x. x) \ convex S"
  by (simp add: convex_on_def)

lemma concave_on_ident: "concave_on S (\x. x) \ convex S"
  by (simp add: concave_on_iff)

lemma convex_on_const: "convex_on S (\x. a) \ convex S"
  by (simp add: convex_on_def flip: distrib_right)

lemma concave_on_const: "concave_on S (\x. a) \ convex S"
  by (simp add: concave_on_iff flip: distrib_right)

lemma convex_on_diff:
  assumes "convex_on S f" and "concave_on S g"
  shows "convex_on S (\x. f x - g x)"
  using assms concave_on_def convex_on_add by fastforce

lemma concave_on_diff:
  assumes "concave_on S f"
    and "convex_on S g"
  shows "concave_on S (\x. f x - g x)"
  using convex_on_diff assms concave_on_def by fastforce

lemma concave_on_add:
  assumes "concave_on S f"
    and "concave_on S g"
  shows "concave_on S (\x. f x + g x)"
  using assms convex_on_iff_concave concave_on_diff concave_on_def by fastforce

lemma convex_on_mul:
  fixes S::"real set"
  assumes "convex_on S f" "convex_on S g"
  assumes "mono_on S f" "mono_on S g"
  assumes fty: "f \ S \ {0..}" and gty: "g \ S \ {0..}"
  shows "convex_on S (\x. f x*g x)"
proof (intro convex_on_linorderI)
  show "convex S"
    using assms convex_on_imp_convex by auto
  fix t::real and x y
  assume t: "0 < t" "t < 1" and xy: "x \ S" "y \ S" "x
  have *: "t*(1-t) * f x * g y + t*(1-t) * f y * g x \ t*(1-t) * f x * g x + t*(1-t) * f y * g y"
    using t \<open>mono_on S f\<close> \<open>mono_on S g\<close> xy
    by (smt (verit, ccfv_SIG) left_diff_distrib mono_onD mult_left_less_imp_less zero_le_mult_iff)
  have inS: "(1-t)*x + t*y \ S"
    using t xy \<open>convex S\<close> by (simp add: convex_alt)
  then have "f ((1-t)*x + t*y) * g ((1-t)*x + t*y) \ ((1-t) * f x + t * f y)*g ((1-t)*x + t*y)"
    using convex_onD [OF \<open>convex_on S f\<close>, of t x y] t xy fty gty
    by (intro mult_mono add_nonneg_nonneg) (auto simp: Pi_iff zero_le_mult_iff)
  also have "\ \ ((1-t) * f x + t * f y) * ((1-t)*g x + t*g y)"
    using convex_onD [OF \<open>convex_on S g\<close>, of t x y] t xy fty gty inS
    by (intro mult_mono add_nonneg_nonneg) (auto simp: Pi_iff zero_le_mult_iff)
  also have "\ \ (1-t) * (f x*g x) + t * (f y*g y)"
    using * by (simp add: algebra_simps)
  finally show "f ((1-t) *\<^sub>R x + t *\<^sub>R y) * g ((1-t) *\<^sub>R x + t *\<^sub>R y) \ (1-t)*(f x*g x) + t*(f y*g y)"
    by simp
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_on_cdiv [intro]:
  fixes c :: real
  assumes "0 \ c" and "convex_on S f"
  shows "convex_on S (\x. f x / c)"
  unfolding divide_inverse
  using convex_on_cmul [of "inverse c" S f] by (simp add: mult.commute assms)

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"
  assumes "convex S"
  shows "convex_on S (\x. dist a x)"
unfolding convex_on_def dist_norm
proof (intro conjI strip)
  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"
    by (metis \<open>u + v = 1\<close> scaleR_left.add scaleR_one)
  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)
  then show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \ u * norm (a - x) + v * norm (a - y)"
    by (smt (verit, best) \<open>0 \<le> u\<close> \<open>0 \<le> v\<close> norm_scaleR norm_triangle_ineq)
qed (use assms in auto)

lemma concave_on_mul:
  fixes S::"real set"
  assumes f: "concave_on S f" and g: "concave_on S g"
  assumes "mono_on S f" "antimono_on S g"
  assumes fty: "f \ S \ {0..}" and gty: "g \ S \ {0..}"
  shows "concave_on S (\x. f x * g x)"
proof (intro concave_on_linorderI)
  show "convex S"
    using concave_on_imp_convex f by blast
  fix t::real and x y
  assume t: "0 < t" "t < 1" and xy: "x \ S" "y \ S" "x
  have inS: "(1-t)*x + t*y \ S"
    using t xy \<open>convex S\<close> by (simp add: convex_alt)
  have "f x * g y + f y * g x \ f x * g x + f y * g y"
    using \<open>mono_on S f\<close> \<open>antimono_on S g\<close>
    unfolding monotone_on_def by (smt (verit, best) left_diff_distrib mult_left_mono xy)
  with t have *: "t*(1-t) * f x * g y + t*(1-t) * f y * g x \ t*(1-t) * f x * g x + t*(1-t) * f y * g y"
    by (smt (verit, ccfv_SIG) distrib_left mult_left_mono diff_ge_0_iff_ge mult.assoc)
  have "(1 - t) * (f x * g x) + t * (f y * g y) \ ((1-t) * f x + t * f y) * ((1-t) * g x + t * g y)"
    using * by (simp add: algebra_simps)
  also have "\ \ ((1-t) * f x + t * f y)*g ((1-t)*x + t*y)"
    using concave_onD [OF \<open>concave_on S g\<close>, of t x y] t xy fty gty inS
    by (intro mult_mono add_nonneg_nonneg) (auto simp: Pi_iff zero_le_mult_iff)
  also have "\ \ f ((1-t)*x + t*y) * g ((1-t)*x + t*y)"
    using concave_onD [OF \<open>concave_on S f\<close>, of t x y] t xy fty gty inS
    by (intro mult_mono add_nonneg_nonneg) (auto simp: Pi_iff zero_le_mult_iff)
  finally show "(1 - t) * (f x * g x) + t * (f y * g y)
           \<le> f ((1 - t) *\<^sub>R x + t *\<^sub>R y) * g ((1 - t) *\<^sub>R x + t *\<^sub>R y)"
    by simp
qed

lemma concave_on_cmul [intro]:
  fixes c :: real
  assumes "0 \ c" and "concave_on S f"
  shows "concave_on S (\x. c * f x)"
  using assms convex_on_cmul [of c S "\x. - f x"]
  by (auto simp: concave_on_def)

lemma concave_on_cdiv [intro]:
  fixes c :: real
  assumes "0 \ c" and "concave_on S f"
  shows "concave_on S (\x. f x / c)"
  unfolding divide_inverse
  using concave_on_cmul [of "inverse c" S f] by (simp add: mult.commute assms)

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)"
  by (simp add: assms convex_linear_image)

lemma convex_scaled:
  assumes "convex S"
  shows "convex ((\x. x *\<^sub>R c) ` S)"
  by (simp add: assms convex_linear_image)

lemma convex_negations:
  assumes "convex S"
  shows "convex ((\x. - x) ` S)"
  by (simp add: assms convex_linear_image module_hom_uminus)

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"
  using convex_sums [OF convex_singleton [of a] that]
  by (simp add: UNION_singleton_eq_range)

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 "(\ 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 show ?case
    by auto
next
  case (insert i S)
  then have yai: "y i \ C" "a i \ 0"
    by auto
  with insert 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 add: convex_on_def)
  show ?case
  proof (cases "a i = 1")
    case True
    with insert have "(\ j \ S. a j) = 0"
      by auto
    with insert show ?thesis
      by (simp add: sum_nonneg_eq_0_iff)
  next
    case False
    then have ai1: "a i < 1"
      using sum_nonneg_leq_bound[of "insert i S" a] insert by force
    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 \<open>convex_on C f\<close> by (simp add: convex_on_def)
    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)"
      by (simp add: add.commute insert.hyps)
    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 ai1 by (smt (verit) asum conv real_scaleR_def yai)
    also have "\ \ (1 - a i) * (\ j \ S. ?a j * f (y j)) + a i * f (y i)"
      using asum_le i0 by fastforce
    also have "\ = (\ j \ S. a j * f (y j)) + a i * f (y i)"
      using i0 by (auto simp: sum_distrib_left)
    finally show ?thesis
      using insert by auto
  qed
qed

lemma concave_on_sum:
  fixes a :: "'a \ real"
    and y :: "'a \ 'b::real_vector"
    and f :: "'b \ real"
  assumes "finite S" "S \ {}"
    and "concave_on C f"
    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))"
proof -
  have "(uminus \ f) (\i\S. a i *\<^sub>R y i) \ (\i\S. a i * (uminus \ f) (y i))"
  proof (intro convex_on_sum)
    show "convex_on C (uminus \ f)"
      by (simp add: assms convex_on_iff_concave)
  qed (use assms in auto)
  then show ?thesis
    by (simp add: sum_negf o_def)
qed

lemma convex_on_alt:
  fixes C :: "'a::real_vector set"
  shows "convex_on C f \ convex C \
         (\<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)"
  by (smt (verit) convex_on_def)

lemma convex_on_slope_le:
  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 "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" and 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
    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
    from z1 have "f x - f y = (x - y) * f' z1"
      by (simp add: field_simps)
    then have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3"
      using le(1) z3(3) 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
    with cool' have "f' y - (f x - f y) / (x - y) \<ge> 0"
      using z1 by auto
    then have res: "f' y * (x - y) \ f x - f y"
      by (meson diff_ge_0_iff_ge le(1) neg_divide_le_eq)
    have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2"
      using le(1) z1(3) z2(3) 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
    with z1 assms have "(z1 - x) * f'' z2 \ 0"
      by auto
    then show "f y - f x \ f' x * (y - x)" "f' y * (x - y) \ f x - f y"
      using that(3) z1(3) res cool by auto
  qed
  then show ?thesis
    using x y by fastforce
qed

lemma f''_ge0_imp_convex:
  fixes f :: "real \ real"
  assumes "convex C"
    and "\x. x \ C \ DERIV f x :> (f' x)"
    and "\x. x \ C \ DERIV f' x :> (f'' x)"
    and "\x. x \ C \ f'' x \ 0"
  shows "convex_on C f"
  by (metis assms f''_imp_f' pos_convex_function)

lemma f''_le0_imp_concave:
  fixes f :: "real \ real"
  assumes "convex C"
    and "\x. x \ C \ DERIV f x :> (f' x)"
    and "\x. x \ C \ DERIV f' x :> (f'' x)"
    and "\x. x \ C \ f'' x \ 0"
  shows "concave_on C f"
  unfolding concave_on_def
  by (rule assms f''_ge0_imp_convex derivative_eq_intros | simp)+

lemma convex_power_even:
  assumes "even n"
  shows "convex_on (UNIV::real set) (\x. x^n)"
proof (intro f''_ge0_imp_convex)
  show "((\x. x ^ n) has_real_derivative of_nat n * x^(n-1)) (at x)" for x
    by (rule derivative_eq_intros | simp)+
  show "((\x. of_nat n * x^(n-1)) has_real_derivative of_nat n * of_nat (n-1) * x^(n-2)) (at x)" for x
    by (rule derivative_eq_intros | simp add: eval_nat_numeral)+
  show "\x. 0 \ real n * real (n - 1) * x ^ (n - 2)"
    using assms by (auto simp: zero_le_mult_iff zero_le_even_power)
qed auto

lemma convex_power_odd:
  assumes "odd n"
  shows "convex_on {0::real..} (\x. x^n)"
proof (intro f''_ge0_imp_convex)
  show "((\x. x ^ n) has_real_derivative of_nat n * x^(n-1)) (at x)" for x
    by (rule derivative_eq_intros | simp)+
  show "((\x. of_nat n * x^(n-1)) has_real_derivative of_nat n * of_nat (n-1) * x^(n-2)) (at x)" for x
    by (rule derivative_eq_intros | simp add: eval_nat_numeral)+
  show "\x. x \ {0::real..} \ 0 \ real n * real (n - 1) * x ^ (n - 2)"
    using assms by (auto simp: zero_le_mult_iff zero_le_even_power)
qed auto

lemma convex_power2: "convex_on (UNIV::real set) power2"
  by (simp add: convex_power_even)

lemma log_concave:
  fixes b :: real
  assumes "b > 1"
  shows "concave_on {0<..} (\ x. log b x)"
  using assms
  by (intro f''_le0_imp_concave derivative_eq_intros | simp)+

lemma ln_concave: "concave_on {0<..} ln"
  unfolding log_ln by (simp add: log_concave)

lemma minus_log_convex:
  fixes b :: real
  assumes "b > 1"
  shows "convex_on {0 <..} (\ x. - log b x)"
  using assms concave_on_def log_concave by blast

lemma powr_convex:
  assumes "p \ 1" shows "convex_on {0<..} (\x. x powr p)"
  using assms
  by (intro f''_ge0_imp_convex derivative_eq_intros | simp)+

lemma exp_convex: "convex_on UNIV exp"
  by (intro f''_ge0_imp_convex derivative_eq_intros | simp)+

text \<open>The AM-GM inequality: the arithmetic mean exceeds the geometric mean.\<close>
lemma arith_geom_mean:
  fixes x :: "'a \ real"
  assumes "finite S" "S \ {}"
    and x: "\i. i \ S \ x i \ 0"
  shows "(\i \ S. x i / card S) \ (\i \ S. x i) powr (1 / card S)"
proof (cases "\i\S. x i = 0")
  case True
  then have "(\i \ S. x i) = 0"
    by (simp add: \<open>finite S\<close>)
  moreover have "(\i \ S. x i / card S) \ 0"
    by (simp add: sum_nonneg x)
  ultimately show ?thesis
    by simp
next
  case False
  have "ln (\i \ S. (1 / card S) *\<^sub>R x i) \ (\i \ S. (1 / card S) * ln (x i))"
  proof (intro concave_on_sum)
    show "concave_on {0<..} ln"
      by (simp add: ln_concave)
    show "\i. i\S \ x i \ {0<..}"
      using False x by fastforce
  qed (use assms False in auto)
  moreover have "(\i \ S. (1 / card S) *\<^sub>R x i) > 0"
    using False assms by (simp add: card_gt_0_iff less_eq_real_def sum_pos)
  ultimately have "(\i \ S. (1 / card S) *\<^sub>R x i) \ exp (\i \ S. (1 / card S) * ln (x i))"
    using ln_ge_iff by blast
  then have "(\i \ S. x i / card S) \ exp (\i \ S. ln (x i) / card S)"
    by (simp add: divide_simps)
  then show ?thesis
    using assms False
    by (smt (verit, ccfv_SIG) divide_inverse exp_ln exp_powr_real exp_sum inverse_eq_divide prod.cong prod_powr_distrib)
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)
  show "convex A"
    using \<open>connected A\<close> convex_real_interval interval_cases
    by (smt (verit, ccfv_SIG) connectedD_interval convex_UNIV convex_empty)
      \<comment> \<open>the equivalence of "connected" and "convex" for real intervals is proved later\<close>
next
  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:
  fixes A :: "real set"
  assumes "A \ {0<..}" "convex A"
  shows "convex_on A inverse"
proof -
  have "convex_on {0::real<..} inverse"
  proof (intro convex_on_realI)
    fix u v :: real
    assume "u \ {0<..}" "v \ {0<..}" "u \ v"
    with assms show "-inverse (u^2) \ -inverse (v^2)"
      by simp
  next
    show "\x. x \ {0<..} \ (inverse has_real_derivative - inverse (x\<^sup>2)) (at x)"
      by (rule derivative_eq_intros | simp add: power2_eq_square)+
  qed auto
  then show ?thesis
    using assms convex_on_subset by blast
qed

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 (use assms in auto)

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 (use assms in auto)

lemma concave_onD_Icc:
  assumes "concave_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) \<ge> (1 - t) * f x + t * f y"
  using assms(2) by (intro concave_onD [OF assms(1)]) simp_all

lemma concave_onD_Icc':
  assumes "concave_on {x..y} f" "c \ {x..y}"
  defines "d \ y - x"
  shows "f c \ (f y - f x) / d * (c - x) + f x"
proof -
  have "- f c \ (f x - f y) / d * (c - x) - f x"
    using assms convex_onD_Icc' [of x y "\x. - f x" c]
    by (simp add: concave_on_def)
  then show ?thesis
    by (smt (verit, best) divide_minus_left mult_minus_left)
qed

lemma concave_onD_Icc'':
  assumes "concave_on {x..y} f" "c \ {x..y}"
  defines "d \ y - x"
  shows "f c \ (f x - f y) / d * (y - c) + f y"
proof -
  have "- f c \ (f y - f x) / d * (y - c) - f y"
    using assms convex_onD_Icc'' [of x y "\x. - f x" c]
    by (simp add: concave_on_def)
  then show ?thesis
    by (smt (verit, best) divide_minus_left mult_minus_left)
qed

lemma convex_on_le_max:
  fixes a::real
  assumes "convex_on {x..y} f" and a: "a \ {x..y}"
  shows "f a \ max (f x) (f y)"
proof -
  have *: "(f y - f x) * (a - x) \ (f y - f x) * (y - x)" if "f x \ f y"
    using a that by (intro mult_left_mono) auto
  have "f a \ (f y - f x) / (y - x) * (a - x) + f x"
    using assms convex_onD_Icc' by blast
  also have "\ \ max (f x) (f y)"
    using a *
    by (simp add: divide_le_0_iff mult_le_0_iff zero_le_mult_iff max_def add.commute mult.commute scaling_mono)
  finally show ?thesis .
qed

lemma concave_on_ge_min:
  fixes a::real
  assumes "concave_on {x..y} f" and a: "a \ {x..y}"
  shows "f a \ min (f x) (f y)"
proof -
  have *: "(f y - f x) * (a - x) \ (f y - f x) * (y - x)" if "f x \ f y"
    using a that by (intro mult_left_mono_neg) auto
  have "min (f x) (f y) \ (f y - f x) / (y - x) * (a - x) + f x"
    using a * apply (simp add: zero_le_divide_iff mult_le_0_iff zero_le_mult_iff min_def)
    by (smt (verit, best) nonzero_eq_divide_eq pos_divide_le_eq)
  also have "\ \ f a"
    using assms concave_onD_Icc' by blast
  finally show ?thesis .
qed

subsection \<open>Convexity of the generalised binomial\<close>

lemma mono_on_mul:
  fixes f::"'a::ord \ 'b::ordered_semiring"
  assumes "mono_on S f" "mono_on S g"
  assumes fty: "f \ S \ {0..}" and gty: "g \ S \ {0..}"
  shows "mono_on S (\x. f x * g x)"
  using assms by (auto simp: Pi_iff monotone_on_def intro!: mult_mono)

lemma mono_on_prod:
  fixes f::"'i \ 'a::ord \ 'b::linordered_idom"
  assumes "\i. i \ I \ mono_on S (f i)"
  assumes "\i. i \ I \ f i \ S \ {0..}"
  shows "mono_on S (\x. prod (\i. f i x) I)"
  using assms
  by (induction I rule: infinite_finite_induct)
     (auto simp: mono_on_const Pi_iff prod_nonneg mono_on_mul mono_onI)

lemma convex_gchoose_aux: "convex_on {k-1..} (\a. prod (\i. a - of_nat i) {0..
proof (induction k)
  case 0
  then show ?case
    by (simp add: convex_on_def)
next
  case (Suc k)
  have "convex_on {real k..} (\a. (\i = 0..
  proof (intro convex_on_mul convex_on_diff)
    show "convex_on {real k..} (\x. \i = 0..
      using Suc convex_on_subset by fastforce
    show "mono_on {real k..} (\x. \i = 0..
      by (force simp: monotone_on_def intro!: prod_mono)
  next
    show "(\x. \i = 0.. {real k..} \ {0..}"
      by (auto intro!: prod_nonneg)
  qed (auto simp: convex_on_ident concave_on_const mono_onI)
  then show ?case
    by simp
qed

lemma convex_gchoose: "convex_on {k-1..} (\x. x gchoose k)"
  by (simp add: gbinomial_prod_rev convex_on_cdiv convex_gchoose_aux)

subsection \<open>Some inequalities: Applications of convexity\<close>

lemma Youngs_inequality_0:
  fixes a::real
  assumes "0 \ \" "0 \ \" "\+\ = 1" "a>0" "b>0"
  shows "a powr \ * b powr \ \ \*a + \*b"
proof -
  have "\ * ln a + \ * ln b \ ln (\ * a + \ * b)"
    using assms ln_concave by (simp add: concave_on_iff)
  moreover have "0 < \ * a + \ * b"
    using assms by (smt (verit) mult_pos_pos split_mult_pos_le)
  ultimately show ?thesis
    using assms by (simp add: powr_def mult_exp_exp flip: ln_ge_iff)
qed

lemma Youngs_inequality:
  fixes p::real
  assumes "p>1" "q>1" "1/p + 1/q = 1" "a\0" "b\0"
  shows "a * b \ a powr p / p + b powr q / q"
proof (cases "a=0 \ b=0")
  case False
  then show ?thesis
  using Youngs_inequality_0 [of "1/p" "1/q" "a powr p" "b powr q"] assms
  by (simp add: powr_powr)
qed (use assms in auto)

lemma Cauchy_Schwarz_ineq_sum:
  fixes a :: "'a \ 'b::linordered_field"
  shows "(\i\I. a i * b i)\<^sup>2 \ (\i\I. (a i)\<^sup>2) * (\i\I. (b i)\<^sup>2)"
proof (cases "(\i\I. (b i)\<^sup>2) > 0")
  case False
  then consider "\i. i\I \ b i = 0" | "infinite I"
    by (metis (mono_tags, lifting) sum_pos2 zero_le_power2 zero_less_power2)
  thus ?thesis
    by fastforce
next
  case True
  define r where "r \ (\i\I. a i * b i) / (\i\I. (b i)\<^sup>2)"
  have "0 \ (\i\I. (a i - r * b i)\<^sup>2)"
    by (simp add: sum_nonneg)
  also have "... = (\i\I. (a i)\<^sup>2) - 2 * r * (\i\I. a i * b i) + r\<^sup>2 * (\i\I. (b i)\<^sup>2)"
    by (simp add: algebra_simps power2_eq_square sum_distrib_left flip: sum.distrib)
  also have "\ = (\i\I. (a i)\<^sup>2) - ((\i\I. a i * b i))\<^sup>2 / (\i\I. (b i)\<^sup>2)"
    by (simp add: r_def power2_eq_square)
  finally have "0 \ (\i\I. (a i)\<^sup>2) - ((\i\I. a i * b i))\<^sup>2 / (\i\I. (b i)\<^sup>2)" .
  hence "((\i\I. a i * b i))\<^sup>2 / (\i\I. (b i)\<^sup>2) \ (\i\I. (a i)\<^sup>2)"
    by (simp add: le_diff_eq)
  thus "((\i\I. a i * b i))\<^sup>2 \ (\i\I. (a i)\<^sup>2) * (\i\I. (b i)\<^sup>2)"
    by (simp add: pos_divide_le_eq True)
qed

text \<open>The inequality between the arithmetic mean and the root mean square\<close>
lemma sum_squared_le_sum_of_squares:
  fixes f :: "'a \ real"
  shows "(\i\I. f i)\<^sup>2 \ (\y\I. (f y)\<^sup>2) * card I"
proof (cases "finite I \ I \ {}")
  case True
  then have "(\i\I. f i / of_nat (card I))\<^sup>2 \ (\i\I. (f i)\<^sup>2 / of_nat (card I))"
    using convex_on_sum [OF _ _ convex_power2, where a = "\x. 1 / of_nat(card I)" and S=I]
    by simp
  with True show ?thesis
    by (simp add: divide_simps power2_eq_square split: if_split_asm flip: sum_divide_distrib)
qed auto

lemma sum_squared_le_sum_of_squares_2:
  "(x+y)/2 \ sqrt ((x\<^sup>2 + y\<^sup>2) / 2)"
proof -
  have "(x + y)\<^sup>2 / 2^2 \ (x\<^sup>2 + y\<^sup>2) / 2"
    using sum_squared_le_sum_of_squares [of "\b. if b then x else y" UNIV]
    by (simp add: UNIV_bool add.commute)
  then show ?thesis
    by (metis power_divide real_le_rsqrt)
qed

subsection \<open>Misc related lemmas\<close>

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 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
  show ?thesis
  proof
    show "norm (scaleR (c / norm a) a) = c"
      by (simp add: \<open>a \<noteq> 0\<close> assms)
  qed
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

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)" (is "_ = ?rhs")
proof
  assume "cone S"
  {
    fix c :: real
    assume "c > 0"
    have "x \ ((*\<^sub>R) c) ` S" if "x \ S" for x
        using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"] that
          exI[of "(\t. t \ S \ x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
        by auto
    then have "((*\<^sub>R) c) ` S = S"
        using \<open>0 < c\<close> \<open>cone S\<close> mem_cone by fastforce
  }
  then show "0 \ S \ (\c. c > 0 \ ((*\<^sub>R) c) ` S = S)"
    using \<open>cone S\<close> cone_contains_0[of S] assms by auto
next
  show "?rhs \ cone S"
    by (metis Convex.cone_def imageI order_neq_le_trans scaleR_zero_left)
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 cone_hull_empty hull_subset subset_empty)

lemma cone_hull_contains_0: "S \ {} \ 0 \ cone hull S"
  by (metis cone_cone_hull cone_contains_0 cone_hull_empty_iff)

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
  have "?rhs \ Collect cone"
    using Convex.cone_def by fastforce
  moreover have "S \ ?rhs"
    by (smt (verit) mem_Collect_eq scaleR_one subsetI)
  ultimately show "?lhs \ ?rhs"
    using hull_minimal by blast
qed (use mem_cone_hull in auto)

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" "convex S"
      unfolding cone_def by auto
    then have "x + y \ S"
      using convexD [OF \<open>convex S\<close>, of "2*\<^sub>R x" "2*\<^sub>R y"]
      by (smt (verit, ccfv_threshold) field_sum_of_halves scaleR_2 scaleR_half_double)
  }
  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 by (auto simp: inner_add_left convex_def)

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)"
  by (metis (mono_tags) convex_Inter hull_def mem_Collect_eq)

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)"
    by (meson convex_convex_hull convex_linear_vimage f hull_minimal hull_subset image_subset_iff_subset_vimage)
qed

lemma in_convex_hull_linear_image:
  assumes "linear f" "x \ convex hull S"
  shows "f x \ convex hull (f ` S)"
  using assms convex_hull_linear_image image_eqI by blast

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 (simp add: hull_same)

lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
  by (simp add: hull_same)

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 show "x \ ?hull"
  unfolding insert_iff
  proof
    assume "x = a"
    then show ?thesis
      by (smt (verit, del_insts) add.right_neutral assms ex_in_conv hull_inc mem_Collect_eq scaleR_one scaleR_zero_left)
  next
    assume "x \ S"
    with hull_subset show ?thesis
      by force
  qed
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
--> --------------------

--> maximum size reached

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

quality96%

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.