diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Analysis/Convex.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -315,6 +315,12 @@
     (\<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 "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
+    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 "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
     f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
@@ -323,6 +329,12 @@
   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 "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
+    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 "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x < y \<Longrightarrow>
@@ -331,11 +343,13 @@
   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 convex_onD:
-  assumes "convex_on A f"
-  shows "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
-    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 concave_on_linorderI [intro?]:
+  fixes A :: "('a::{linorder,real_vector}) set"
+  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x < y \<Longrightarrow>
+    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 \<Longrightarrow> convex A"
   by (auto simp: convex_on_def)
@@ -407,27 +421,21 @@
   assumes "convex_on S f" "convex_on S g"
   assumes "mono_on S f" "mono_on S g"
   assumes fty: "f \<in> S \<rightarrow> {0..}" and gty: "g \<in> S \<rightarrow> {0..}"
-  shows "convex_on S (\<lambda>x. f x * g x)"
+  shows "convex_on S (\<lambda>x. f x*g x)"
 proof (intro convex_on_linorderI)
   show "convex S"
-    using \<open>convex_on S f\<close> convex_on_imp_convex by blast
+    using assms convex_on_imp_convex by auto
   fix t::real and x y
-  assume t: "0 < t" "t < 1" and xy: "x \<in> S" "y \<in> S"
-  have "f x*g y + f y*g x \<le> f x*g x + f y*g y"
-    using \<open>mono_on S f\<close> \<open>mono_on S g\<close>
-    by (smt (verit, ccfv_SIG) mono_onD mult_right_mono right_diff_distrib' xy)
-  then have "(1-t) * f x * g y + (1-t) * f y * g x \<le> (1-t) * f x * g x + (1-t) * f y * g y"
-    using t
-    by (metis (mono_tags, opaque_lifting) mult.assoc diff_gt_0_iff_gt distrib_left mult_le_cancel_left_pos)
-  then have *: "t*(1-t) * f x * g y + t*(1-t) * f y * g x \<le> t*(1-t) * f x * g x + t*(1-t) * f y * g y"
-    using t
-    by (metis (mono_tags, opaque_lifting) mult.assoc distrib_left mult_le_cancel_left_pos)  
+  assume t: "0 < t" "t < 1" and xy: "x \<in> S" "y \<in> S" "x<y"
+  have *: "t*(1-t) * f x * g y + t*(1-t) * f y * g x \<le> 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 \<in> 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) \<le> ((1-t)*f x + t*f y)*g ((1-t)*x + t*y)"
+  then have "f ((1-t)*x + t*y) * g ((1-t)*x + t*y) \<le> ((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 "\<dots> \<le> ((1-t)*f x + t*f y) * ((1-t)*g x + t*g y)"
+  also have "\<dots> \<le> ((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 "\<dots> \<le> (1-t) * (f x*g x) + t * (f y*g y)"
@@ -494,6 +502,50 @@
     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 \<in> S \<rightarrow> {0..}" and gty: "g \<in> S \<rightarrow> {0..}"
+  shows "concave_on S (\<lambda>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 \<in> S" "y \<in> S" "x<y"
+  have inS: "(1-t)*x + t*y \<in> S"
+    using t xy \<open>convex S\<close> by (simp add: convex_alt)
+  have "f x * g y + f y * g x \<ge> 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 \<ge> 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) \<le> ((1-t) * f x + t * f y) * ((1-t) * g x + t * g y)"
+    using * by (simp add: algebra_simps)
+  also have "\<dots> \<le> ((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 "\<dots> \<le> 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 \<le> c" and "concave_on S f"
+  shows "concave_on S (\<lambda>x. c * f x)"
+  using assms convex_on_cmul [of c S "\<lambda>x. - f x"]
+  by (auto simp: concave_on_def)
+
+lemma concave_on_cdiv [intro]:
+  fixes c :: real
+  assumes "0 \<le> c" and "concave_on S f"
+  shows "concave_on S (\<lambda>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>
 
@@ -1041,6 +1093,66 @@
   finally show ?thesis .
 qed (use assms in auto)
 
+lemma concave_onD_Icc:
+  assumes "concave_on {x..y} f" "x \<le> (y :: _ :: {real_vector,preorder})"
+  shows "\<And>t. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow>
+    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 \<in> {x..y}"
+  defines "d \<equiv> y - x"
+  shows "f c \<ge> (f y - f x) / d * (c - x) + f x"
+proof -
+  have "- f c \<le> (f x - f y) / d * (c - x) - f x"
+    using assms convex_onD_Icc' [of x y "\<lambda>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 \<in> {x..y}"
+  defines "d \<equiv> y - x"
+  shows "f c \<ge> (f x - f y) / d * (y - c) + f y"
+proof -
+  have "- f c \<le> (f y - f x) / d * (y - c) - f y"
+    using assms convex_onD_Icc'' [of x y "\<lambda>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 \<in> {x..y}"
+  shows "f a \<le> max (f x) (f y)"
+proof -
+  have *: "(f y - f x) * (a - x) \<le> (f y - f x) * (y - x)" if "f x \<le> f y"
+    using a that by (intro mult_left_mono) auto
+  have "f a \<le> (f y - f x) / (y - x) * (a - x) + f x" 
+    using assms convex_onD_Icc' by blast
+  also have "\<dots> \<le> 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 \<in> {x..y}"
+  shows "f a \<ge> min (f x) (f y)"
+proof -
+  have *: "(f y - f x) * (a - x) \<ge> (f y - f x) * (y - x)" if "f x \<ge> f y"
+    using a that by (intro mult_left_mono_neg) auto
+  have "min (f x) (f y) \<le> (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 "\<dots> \<le> f a"
+    using assms concave_onD_Icc' by blast
+  finally show ?thesis .
+qed
+
 subsection \<open>Some inequalities: Applications of convexity\<close>
 
 lemma Youngs_inequality_0: