diff -r 65223730d7e1 -r f471e1715fc4 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Mon Feb 19 08:23:23 2024 +0100
+++ b/src/HOL/Analysis/Convex.thy	Mon Feb 19 14:12:20 2024 +0000
@@ -583,7 +583,6 @@
     and f :: "'b \<Rightarrow> real"
   assumes "finite S" "S \<noteq> {}"
     and "convex_on C f"
-    and "convex C"
     and "(\<Sum> i \<in> S. a i) = 1"
     and "\<And>i. i \<in> S \<Longrightarrow> a i \<ge> 0"
     and "\<And>i. i \<in> S \<Longrightarrow> y i \<in> C"
@@ -624,6 +623,8 @@
       using i0 by auto
     then have a1: "(\<Sum> j \<in> 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: "(\<Sum> j \<in> S. ?a j *\<^sub>R y j) \<in> C"
       using insert convex_sum [OF \<open>finite S\<close> \<open>convex C\<close> a1 a_nonneg] by auto
     have asum_le: "f (\<Sum> j \<in> S. ?a j *\<^sub>R y j) \<le> (\<Sum> j \<in> S. ?a j * f (y j))"
@@ -648,6 +649,26 @@
   qed
 qed
 
+lemma concave_on_sum:
+  fixes a :: "'a \<Rightarrow> real"
+    and y :: "'a \<Rightarrow> 'b::real_vector"
+    and f :: "'b \<Rightarrow> real"
+  assumes "finite S" "S \<noteq> {}"
+    and "concave_on C f" 
+    and "(\<Sum>i \<in> S. a i) = 1"
+    and "\<And>i. i \<in> S \<Longrightarrow> a i \<ge> 0"
+    and "\<And>i. i \<in> S \<Longrightarrow> y i \<in> C"
+  shows "f (\<Sum>i \<in> S. a i *\<^sub>R y i) \<ge> (\<Sum>i \<in> S. a i * f (y i))"
+proof -
+  have "(uminus \<circ> f) (\<Sum>i\<in>S. a i *\<^sub>R y i) \<le> (\<Sum>i\<in>S. a i * (uminus \<circ> f) (y i))"
+  proof (intro convex_on_sum)
+    show "convex_on C (uminus \<circ> 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 \<longleftrightarrow> convex C \<and>
@@ -865,6 +886,39 @@
 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 \<Rightarrow> real"
+  assumes "finite S" "S \<noteq> {}"
+    and x: "\<And>i. i \<in> S \<Longrightarrow> x i \<ge> 0"
+  shows "(\<Sum>i \<in> S. x i / card S) \<ge> (\<Prod>i \<in> S. x i) powr (1 / card S)"
+proof (cases "\<exists>i\<in>S. x i = 0")
+  case True
+  then have "(\<Prod>i \<in> S. x i) = 0"
+    by (simp add: \<open>finite S\<close>)
+  moreover have "(\<Sum>i \<in> S. x i / card S) \<ge> 0"
+    by (simp add: sum_nonneg x)
+  ultimately show ?thesis
+    by simp
+next
+  case False
+  have "ln (\<Sum>i \<in> S. (1 / card S) *\<^sub>R x i) \<ge> (\<Sum>i \<in> S. (1 / card S) * ln (x i))"
+  proof (intro concave_on_sum)
+    show "concave_on {0<..} ln"
+      by (simp add: ln_concave)
+    show "\<And>i. i\<in>S \<Longrightarrow> x i \<in> {0<..}"
+      using False x by fastforce
+  qed (use assms False in auto)
+  moreover have "(\<Sum>i \<in> 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 "(\<Sum>i \<in> S. (1 / card S) *\<^sub>R x i) \<ge> exp (\<Sum>i \<in> S. (1 / card S) * ln (x i))"
+    using ln_ge_iff by blast
+  then have "(\<Sum>i \<in> S. x i / card S) \<ge> exp (\<Sum>i \<in> 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>