(* Title: HOL/Library/Convex.thy

Author: Armin Heller, TU Muenchen

Author: Johannes Hoelzl, TU Muenchen

*)

header {* Convexity in real vector spaces *}

theory Convex

imports Product_Vector

begin

subsection {* Convexity. *}

definition convex :: "'a::real_vector set => bool"

where "convex s <-> (∀x∈s. ∀y∈s. ∀u≥0. ∀v≥0. u + v = 1 --> u *⇩_{R}x + v *⇩_{R}y ∈ s)"

lemma convexI:

assumes "!!x y u v. x ∈ s ==> y ∈ s ==> 0 ≤ u ==> 0 ≤ v ==> u + v = 1 ==> u *⇩_{R}x + v *⇩_{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 *⇩_{R}x + v *⇩_{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) *⇩_{R}x + u *⇩_{R}y) ∈ s)"

(is "_ <-> ?alt")

proof

assume alt[rule_format]: ?alt

{ 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 *⇩_{R}x + v *⇩_{R}y ∈ s" using alt[OF mem] by auto }

then show "convex s" unfolding convex_def by auto

qed (auto simp: convex_def)

lemma mem_convex:

assumes "convex s" "a ∈ s" "b ∈ s" "0 ≤ u" "u ≤ 1"

shows "((1 - u) *⇩_{R}a + u *⇩_{R}b) ∈ s"

using assms unfolding convex_alt by auto

lemma convex_empty[intro]: "convex {}"

unfolding convex_def by simp

lemma convex_singleton[intro]: "convex {a}"

unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric])

lemma convex_UNIV[intro]: "convex UNIV"

unfolding convex_def by auto

lemma convex_Inter: "(∀s∈f. convex s) ==> convex(\<Inter> 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∈A. convex (B i) ==> convex (\<Inter>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_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_real_interval:

fixes a b :: "real"

shows "convex {a..}" and "convex {..b}"

and "convex {a<..}" and "convex {..<b}"

and "convex {a..b}" and "convex {a<..b}"

and "convex {a..<b}" and "convex {a<..<b}"

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 "{..<b} = {x. inner 1 x < b}" by auto

then show 4: "convex {..<b}" 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..<b} = {a..} ∩ {..<b}" by auto

then show "convex {a..<b}" by (simp only: convex_Int 1 4)

have "{a<..<b} = {a<..} ∩ {..<b}" by auto

then show "convex {a<..<b}" by (simp only: convex_Int 3 4)

qed

subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}

lemma convex_setsum:

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 *⇩_{R}y j) ∈ C"

using assms

proof (induct s arbitrary:a rule: finite_induct)

case empty

then show ?case by auto

next

case (insert i s) note asms = this

{ assume "a i = 1"

then have "(∑ j ∈ s. a j) = 0"

using asms by auto

then have "!!j. j ∈ s ==> a j = 0"

using setsum_nonneg_0[where 'b=real] asms by fastforce

then have ?case using asms by auto }

moreover

{ assume asm: "a i ≠ 1"

from asms have yai: "y i ∈ C" "a i ≥ 0" by auto

have fis: "finite (insert i s)" using asms by auto

then have ai1: "a i ≤ 1" using setsum_nonneg_leq_bound[of "insert i s" a 1] asms by simp

then have "a i < 1" using asm by auto

then have i0: "1 - a i > 0" by auto

let ?a = "λj. a j / (1 - a i)"

{ fix j assume "j ∈ s"

then have "?a j ≥ 0"

using i0 asms divide_nonneg_pos

by fastforce

} note a_nonneg = this

have "(∑ j ∈ insert i s. a j) = 1" using asms by auto

then have "(∑ j ∈ s. a j) = 1 - a i" using setsum.insert asms 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 setsum_divide_distrib by simp

with asms have "(∑j∈s. ?a j *⇩_{R}y j) ∈ C" using a_nonneg by fastforce

then have "a i *⇩_{R}y i + (1 - a i) *⇩_{R}(∑ j ∈ s. ?a j *⇩_{R}y j) ∈ C"

using asms yai ai1 by (auto intro: convexD)

then have "a i *⇩_{R}y i + (∑ j ∈ s. (1 - a i) *⇩_{R}(?a j *⇩_{R}y j)) ∈ C"

using scaleR_right.setsum[of "(1 - a i)" "λ j. ?a j *⇩_{R}y j" s] by auto

then have "a i *⇩_{R}y i + (∑ j ∈ s. a j *⇩_{R}y j) ∈ C" using i0 by auto

then have ?case using setsum.insert asms by auto

}

ultimately show ?case by auto

qed

lemma convex:

"convex s <-> (∀(k::nat) u x. (∀i. 1≤i ∧ i≤k --> 0 ≤ u i ∧ x i ∈s) ∧ (setsum u {1..k} = 1)

--> setsum (λi. u i *⇩_{R}x i) {1..k} ∈ 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"

"setsum u {1..k} = 1"

from this convex_setsum[of "{1 .. k}" s]

show "(∑j∈{1 .. k}. u j *⇩_{R}x j) ∈ s" by auto

next

assume asm: "∀k u x. (∀ i :: nat. 1 ≤ i ∧ i ≤ k --> 0 ≤ u i ∧ x i ∈ s) ∧ setsum u {1..k} = 1

--> (∑i = 1..k. u i *⇩_{R}(x i :: 'a)) ∈ s"

{ fix μ :: 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 "setsum ?u {1 .. 2} = 1"

using setsum_cases[of "{(1 :: nat) .. 2}" "λ x. x = 1" "λ x. μ" "λ x. 1 - μ"]

by auto

with asm[rule_format, of "2" ?u ?x] have s: "(∑j ∈ {1..2}. ?u j *⇩_{R}?x j) ∈ s"

using mu xy by auto

have grarr: "(∑j ∈ {Suc (Suc 0)..2}. ?u j *⇩_{R}?x j) = (1 - μ) *⇩_{R}y"

using setsum_head_Suc[of "Suc (Suc 0)" 2 "λ j. (1 - μ) *⇩_{R}y"] by auto

from setsum_head_Suc[of "Suc 0" 2 "λ j. ?u j *⇩_{R}?x j", simplified this]

have "(∑j ∈ {1..2}. ?u j *⇩_{R}?x j) = μ *⇩_{R}x + (1 - μ) *⇩_{R}y" by auto

then have "(1 - μ) *⇩_{R}y + μ *⇩_{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 <->

(∀t u. finite t ∧ t ⊆ s ∧ (∀x∈t. 0 ≤ u x) ∧ setsum u t = 1 --> setsum (λx. u x *⇩_{R}x) t ∈ s)"

proof safe

fix t

fix u :: "'a => real"

assume "convex s" "finite t"

"t ⊆ s" "∀x∈t. 0 ≤ u x" "setsum u t = 1"

then show "(∑x∈t. u x *⇩_{R}x) ∈ s"

using convex_setsum[of t s u "λ x. x"] by auto

next

assume asm0: "∀t. ∀ u. finite t ∧ t ⊆ s ∧ (∀x∈t. 0 ≤ u x)

∧ setsum u t = 1 --> (∑x∈t. u x *⇩_{R}x) ∈ s"

show "convex s"

unfolding convex_alt

proof safe

fix x y

fix μ :: real

assume asm: "x ∈ s" "y ∈ s" "0 ≤ μ" "μ ≤ 1"

{ assume "x ≠ y"

then have "(1 - μ) *⇩_{R}x + μ *⇩_{R}y ∈ s"

using asm0[rule_format, of "{x, y}" "λ z. if z = x then 1 - μ else μ"]

asm by auto }

moreover

{ assume "x = y"

then have "(1 - μ) *⇩_{R}x + μ *⇩_{R}y ∈ s"

using asm0[rule_format, of "{x, y}" "λ z. 1"]

asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) }

ultimately show "(1 - μ) *⇩_{R}x + μ *⇩_{R}y ∈ s" by blast

qed

qed

lemma convex_finite:

assumes "finite s"

shows "convex s <-> (∀u. (∀x∈s. 0 ≤ u x) ∧ setsum u s = 1

--> setsum (λx. u x *⇩_{R}x) s ∈ s)"

unfolding convex_explicit

proof safe

fix t u

assume sum: "∀u. (∀x∈s. 0 ≤ u x) ∧ setsum u s = 1 --> (∑x∈s. u x *⇩_{R}x) ∈ s"

and as: "finite t" "t ⊆ s" "∀x∈t. 0 ≤ u x" "setsum u t = (1::real)"

have *: "s ∩ t = t" using as(2) by auto

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

show "(∑x∈t. u x *⇩_{R}x) ∈ s"

using sum[THEN spec[where x="λx. if x∈t then u x else 0"]] as *

by (auto simp: assms setsum_cases if_distrib if_distrib_arg)

qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)

definition convex_on :: "'a::real_vector set => ('a => real) => bool"

where "convex_on s f <->

(∀x∈s. ∀y∈s. ∀u≥0. ∀v≥0. u + v = 1 --> f (u *⇩_{R}x + v *⇩_{R}y) ≤ u * f x + v * f y)"

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" "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 *⇩_{R}x + v *⇩_{R}y) + g (u *⇩_{R}x + v *⇩_{R}y) ≤ (u * f x + v * f y) + (u * g x + v * g y)"

using assms unfolding convex_on_def by (auto simp add: add_mono)

then have "f (u *⇩_{R}x + v *⇩_{R}y) + g (u *⇩_{R}x + v *⇩_{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]:

assumes "0 ≤ (c::real)" "convex_on s f"

shows "convex_on s (λx. c * f x)"

proof-

have *: "!!u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)"

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" "x∈s" "y ∈ s" "0 ≤ u" "0 ≤ v" "u + v = 1"

shows "f (u *⇩_{R}x + v *⇩_{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 add: mult_left_mono add_mono)

also have "… = max (f x) (f y)" using assms(6) unfolding distrib[symmetric] by auto

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 add: convex_on_def dist_norm)

fix x y

assume "x∈s" "y∈s"

fix u v :: real

assume "0 ≤ u" "0 ≤ v" "u + v = 1"

have "a = u *⇩_{R}a + v *⇩_{R}a"

unfolding scaleR_left_distrib[symmetric] and `u+v=1` by simp

then have *: "a - (u *⇩_{R}x + v *⇩_{R}y) = (u *⇩_{R}(a - x)) + (v *⇩_{R}(a - y))"

by (auto simp add: algebra_simps)

show "norm (a - (u *⇩_{R}x + v *⇩_{R}y)) ≤ u * norm (a - x) + v * norm (a - y)"

unfolding * using norm_triangle_ineq[of "u *⇩_{R}(a - x)" "v *⇩_{R}(a - y)"]

using `0 ≤ u` `0 ≤ v` by auto

qed

subsection {* Arithmetic operations on sets preserve convexity. *}

lemma convex_linear_image:

assumes "linear f" and "convex s" shows "convex (f ` s)"

proof -

interpret f: linear f by fact

from `convex s` 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 `convex s` show "convex (f -` s)"

by (simp add: convex_def f.add f.scaleR)

qed

lemma convex_scaling:

assumes "convex s" shows "convex ((λx. c *⇩_{R}x) ` s)"

proof -

have "linear (λx. c *⇩_{R}x)" by (simp add: linearI scaleR_add_right)

then show ?thesis using `convex s` 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 `convex s` by (rule convex_linear_image)

qed

lemma convex_sums:

assumes "convex s" and "convex t"

shows "convex {x + y| x y. x ∈ s ∧ y ∈ t}"

proof -

have "linear (λ(x, y). x + y)"

by (auto intro: linearI simp add: 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 + y| x y. x ∈ s ∧ y ∈ t}"

by auto

finally show ?thesis .

qed

lemma convex_differences:

assumes "convex s" "convex t"

shows "convex {x - y| x y. x ∈ s ∧ y ∈ t}"

proof -

have "{x - y| x y. x ∈ s ∧ y ∈ t} = {x + y |x y. x ∈ s ∧ y ∈ uminus ` t}"

unfolding diff_def by auto

then show ?thesis

using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto

qed

lemma convex_translation:

assumes "convex s"

shows "convex ((λx. a + x) ` s)"

proof -

have "{a + y |y. y ∈ s} = (λx. a + x) ` s" by auto

then show ?thesis

using convex_sums[OF convex_singleton[of a] assms] by auto

qed

lemma convex_affinity:

assumes "convex s"

shows "convex ((λx. a + c *⇩_{R}x) ` s)"

proof -

have "(λx. a + c *⇩_{R}x) ` s = op + a ` op *⇩_{R}c ` s" by auto

then show ?thesis

using convex_translation[OF convex_scaling[OF assms], of a c] by auto

qed

lemma pos_is_convex: "convex {0 :: real <..}"

unfolding convex_alt

proof safe

fix y x μ :: real

assume asms: "y > 0" "x > 0" "μ ≥ 0" "μ ≤ 1"

{ assume "μ = 0"

then have "μ *⇩_{R}x + (1 - μ) *⇩_{R}y = y" by simp

then have "μ *⇩_{R}x + (1 - μ) *⇩_{R}y > 0" using asms by simp }

moreover

{ assume "μ = 1"

then have "μ *⇩_{R}x + (1 - μ) *⇩_{R}y > 0" using asms by simp }

moreover

{ assume "μ ≠ 1" "μ ≠ 0"

then have "μ > 0" "(1 - μ) > 0" using asms by auto

then have "μ *⇩_{R}x + (1 - μ) *⇩_{R}y > 0" using asms

by (auto simp add: add_pos_pos mult_pos_pos) }

ultimately show "(1 - μ) *⇩_{R}y + μ *⇩_{R}x > 0" using assms by fastforce

qed

lemma convex_on_setsum:

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 *⇩_{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) note asms = this

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 (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y"

by simp

{ assume "a i = 1"

then have "(∑ j ∈ s. a j) = 0"

using asms by auto

then have "!!j. j ∈ s ==> a j = 0"

using setsum_nonneg_0[where 'b=real] asms by fastforce

then have ?case using asms by auto }

moreover

{ assume asm: "a i ≠ 1"

from asms have yai: "y i ∈ C" "a i ≥ 0" by auto

have fis: "finite (insert i s)" using asms by auto

then have ai1: "a i ≤ 1" using setsum_nonneg_leq_bound[of "insert i s" a] asms by simp

then have "a i < 1" using asm by auto

then have i0: "1 - a i > 0" by auto

let ?a = "λj. a j / (1 - a i)"

{ fix j assume "j ∈ s"

then have "?a j ≥ 0"

using i0 asms divide_nonneg_pos

by fastforce }

note a_nonneg = this

have "(∑ j ∈ insert i s. a j) = 1" using asms by auto

then have "(∑ j ∈ s. a j) = 1 - a i" using setsum.insert asms 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 setsum_divide_distrib by simp

have "convex C" using asms by auto

then have asum: "(∑ j ∈ s. ?a j *⇩_{R}y j) ∈ C"

using asms convex_setsum[OF `finite s`

`convex C` a1 a_nonneg] by auto

have asum_le: "f (∑ j ∈ s. ?a j *⇩_{R}y j) ≤ (∑ j ∈ s. ?a j * f (y j))"

using a_nonneg a1 asms by blast

have "f (∑ j ∈ insert i s. a j *⇩_{R}y j) = f ((∑ j ∈ s. a j *⇩_{R}y j) + a i *⇩_{R}y i)"

using setsum.insert[of s i "λ j. a j *⇩_{R}y j", OF `finite s` `i ∉ s`] asms

by (auto simp only:add_commute)

also have "… = f (((1 - a i) * inverse (1 - a i)) *⇩_{R}(∑ j ∈ s. a j *⇩_{R}y j) + a i *⇩_{R}y i)"

using i0 by auto

also have "… = f ((1 - a i) *⇩_{R}(∑ j ∈ s. (a j * inverse (1 - a i)) *⇩_{R}y j) + a i *⇩_{R}y i)"

using scaleR_right.setsum[of "inverse (1 - a i)" "λ j. a j *⇩_{R}y j" s, symmetric]

by (auto simp:algebra_simps)

also have "… = f ((1 - a i) *⇩_{R}(∑ j ∈ s. ?a j *⇩_{R}y j) + a i *⇩_{R}y i)"

by (auto simp: divide_inverse)

also have "… ≤ (1 - a i) *⇩_{R}f ((∑ j ∈ s. ?a j *⇩_{R}y j)) + a i * f (y i)"

using conv[of "y i" "(∑ j ∈ s. ?a j *⇩_{R}y j)" "a i", OF yai(1) asum yai(2) ai1]

by (auto simp add: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 setsum_right_distrib[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 asms by auto

finally have "f (∑ j ∈ insert i s. a j *⇩_{R}y j) ≤ (∑ j ∈ insert i s. a j * f (y j))"

by simp }

ultimately show ?case by auto

qed

lemma convex_on_alt:

fixes C :: "'a::real_vector set"

assumes "convex C"

shows "convex_on C f =

(∀ x ∈ C. ∀ y ∈ C. ∀ μ :: real. μ ≥ 0 ∧ μ ≤ 1

--> f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y)"

proof safe

fix x y

fix μ :: real

assume asms: "convex_on C f" "x ∈ C" "y ∈ C" "0 ≤ μ" "μ ≤ 1"

from this[unfolded convex_on_def, rule_format]

have "!!u v. [|0 ≤ u; 0 ≤ v; u + v = 1|] ==> f (u *⇩_{R}x + v *⇩_{R}y) ≤ u * f x + v * f y" by auto

from this[of "μ" "1 - μ", simplified] asms

show "f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y" by auto

next

assume asm: "∀x∈C. ∀y∈C. ∀μ. 0 ≤ μ ∧ μ ≤ 1 --> f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y"

{ fix x y

fix u v :: real

assume lasm: "x ∈ C" "y ∈ C" "u ≥ 0" "v ≥ 0" "u + v = 1"

then have[simp]: "1 - u = v" by auto

from asm[rule_format, of x y u]

have "f (u *⇩_{R}x + v *⇩_{R}y) ≤ u * f x + v * f y" using lasm 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)"

"(f x - f y) / (x - y) ≤ (f t - f y) / (t - y)"

proof -

def a ≡ "(t - y) / (x - y)"

with t have "0 ≤ a" "0 ≤ 1 - a" by (auto simp: field_simps)

with f `x ∈ I` `y ∈ I` have cvx: "f (a * x + (1 - a) * y) ≤ 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 `x < t` `t < y` 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[OF assms(1)]

using assms

proof safe

fix x y μ :: real

let ?x = "μ *⇩_{R}x + (1 - μ) *⇩_{R}y"

assume asm: "convex C" "x ∈ C" "y ∈ C" "μ ≥ 0" "μ ≤ 1"

then have "1 - μ ≥ 0" by auto

then have xpos: "?x ∈ C" using asm unfolding convex_alt by fastforce

have geq: "μ * (f x - f ?x) + (1 - μ) * (f y - f ?x)

≥ μ * f' ?x * (x - ?x) + (1 - μ) * f' ?x * (y - ?x)"

using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `μ ≥ 0`]

mult_left_mono[OF leq[OF xpos asm(3)] `1 - μ ≥ 0`]] by auto

then have "μ * f x + (1 - μ) * f y - f ?x ≥ 0"

by (auto simp add: field_simps)

then show "f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y"

using convex_on_alt 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 zasm: "z ∈ {x .. y}"

{ assume asm: "x < z" "z < y"

let ?μ = "(y - z) / (y - x)"

have "0 ≤ ?μ" "?μ ≤ 1" using assms asm by (auto simp add: field_simps)

then have comb: "?μ * x + (1 - ?μ) * y ∈ C"

using assms iffD1[OF convex_alt, rule_format, of C y x ?μ]

by (simp add: algebra_simps)

have "?μ * x + (1 - ?μ) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"

by (auto simp add: field_simps)

also have "… = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"

using assms unfolding add_divide_distrib by (auto simp: field_simps)

also have "… = z"

using assms by (auto simp: field_simps)

finally have "z ∈ C"

using comb by auto }

note less = this

show "z ∈ C" using zasm less assms

unfolding atLeastAtMost_iff le_less by auto

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 ∈ C" "y ∈ C"

shows "f' x * (y - x) ≤ f y - f x"

using assms

proof -

{ fix x y :: real

assume asm: "x ∈ C" "y ∈ C" "y > x"

then have ge: "y - x > 0" "y - x ≥ 0" by auto

from asm 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 `convex C` `x ∈ C` `y ∈ C` `x < y`],

THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]]

by auto

then have "z1 ∈ C" using atMostAtLeast_subset_convex

`convex C` `x ∈ C` `y ∈ C` `x < y` 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 `convex C` `x ∈ C` `z1 ∈ C` `x < z1`],

THEN f'', THEN MVT2[OF `x < z1`, 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 `convex C` `z1 ∈ C` `y ∈ C` `z1 < y`],

THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1

by auto

have "f' y - (f x - f y) / (x - y) = f' y - f' z1"

using asm 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 asm atMostAtLeast_subset_convex

`convex C` `x ∈ C` `z1 ∈ C` `x < z1` by fastforce

then have B': "f'' z3 ≥ 0" using assms by auto

from A' B' have "(y - z1) * f'' z3 ≥ 0" using mult_nonneg_nonneg by auto

from cool' this have "f' y - (f x - f y) / (x - y) ≥ 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 asm 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 asm atMostAtLeast_subset_convex

`convex C` `z1 ∈ C` `y ∈ C` `z1 < y` by fastforce

then have B: "f'' z2 ≥ 0" using assms by auto

from A B have "(z1 - x) * f'' z2 ≥ 0" using mult_nonneg_nonneg by auto

from cool this 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 have "f y - f x ≥ f' x * (y - x)" "f' y * (x - y) ≤ f x - f y"

using res by auto } note less_imp = this

{ fix x y :: real

assume "x ∈ C" "y ∈ C" "x ≠ y"

then have"f y - f x ≥ f' x * (y - x)"

unfolding neq_iff using less_imp by auto } note neq_imp = this

moreover

{ fix x y :: real

assume asm: "x ∈ C" "y ∈ C" "x = y"

then have "f y - f x ≥ f' x * (y - x)" by auto }

ultimately show ?thesis using assms by blast

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 (λ 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 (λ z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"

unfolding inverse_eq_divide by (auto simp add: mult_assoc)

have f''_ge0: "!!z :: real. z > 0 ==> 1 / (ln b * z * z) ≥ 0"

using `b > 1` by (auto intro!:less_imp_le simp add: divide_pos_pos[of 1] mult_pos_pos)

from f''_ge0_imp_convex[OF pos_is_convex,

unfolded greaterThan_iff, OF f' f''0 f''_ge0]

show ?thesis by auto

qed

end