# HG changeset patch
# User paulson
# Date 1708351949 0
# Node ID 1d0cb3f003d409f740e74b785b28175dd268f2b0
# Parent  a3e7a323780f6b3cc3b3da8455e85e7d7fcdb694# Parent  f471e1715fc4c5656bed7c854a89eadd1e4f25c0
merged

diff -r a3e7a323780f -r 1d0cb3f003d4 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Feb 19 14:31:26 2024 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Feb 19 14:12:29 2024 +0000
@@ -2379,8 +2379,7 @@
   by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
 
 lemma powr_times_real:
-    "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
-           \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
+    "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk> \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
   by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
 
 lemma Re_powr_le: "r \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> Re (r powr z) \<le> Re r powr Re z"
@@ -2392,6 +2391,12 @@
   shows Reals_powr [simp]: "w powr z \<in> \<real>" and nonneg_Reals_powr [simp]: "w powr z \<in> \<real>\<^sub>\<ge>\<^sub>0"
   using assms by (auto simp: nonneg_Reals_def Reals_def powr_of_real)
 
+lemma exp_powr_complex:
+  fixes x::complex 
+  assumes "-pi < Im(x)" "Im(x) \<le> pi"
+  shows "exp x powr y = exp (x*y)"
+  using assms by (simp add: powr_def mult.commute)
+
 lemma powr_neg_real_complex:
   fixes w::complex
   shows "(- of_real x) powr w = (-1) powr (of_real (sgn x) * w) * of_real x powr w"
diff -r a3e7a323780f -r 1d0cb3f003d4 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Mon Feb 19 14:31:26 2024 +0100
+++ b/src/HOL/Analysis/Convex.thy	Mon Feb 19 14:12:29 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>
 
diff -r a3e7a323780f -r 1d0cb3f003d4 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Feb 19 14:31:26 2024 +0100
+++ b/src/HOL/Groups_Big.thy	Mon Feb 19 14:12:29 2024 +0000
@@ -1596,10 +1596,10 @@
 context linordered_semidom
 begin
 
-lemma prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
+lemma prod_nonneg: "(\<And>a. a\<in>A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
   by (induct A rule: infinite_finite_induct) simp_all
 
-lemma prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
+lemma prod_pos: "(\<And>a. a\<in>A \<Longrightarrow> 0 < f a) \<Longrightarrow> 0 < prod f A"
   by (induct A rule: infinite_finite_induct) simp_all
 
 lemma prod_mono:
@@ -1738,14 +1738,13 @@
   case empty
   then show ?case by auto
 next
-  case (insert x F)
-  from insertI1 have "0 \<le> g (f x)" by (rule insert)
-  hence 1: "sum g (f ` F) \<le> g (f x) + sum g (f ` F)" using add_increasing by blast
-  have 2: "sum g (f ` F) \<le> sum (g \<circ> f) F" using insert by blast
-  have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp
-  also have "\<dots> \<le> g (f x) + sum g (f ` F)" by (simp add: 1 insert sum.insert_if)
-  also from 2 have "\<dots> \<le> g (f x) + sum (g \<circ> f) F" by (rule add_left_mono)
-  also from insert(1, 2) have "\<dots> = sum (g \<circ> f) (insert x F)" by (simp add: sum.insert_if)
+  case (insert i I)
+  hence *: "sum g (f ` I) \<le> g (f i) + sum g (f ` I)" 
+           "sum g (f ` I) \<le> sum (g \<circ> f) I" using add_increasing by blast+
+  have "sum g (f ` insert i I) = sum g (insert (f i) (f ` I))" by simp
+  also have "\<dots> \<le> g (f i) + sum g (f ` I)" by (simp add: * insert sum.insert_if)
+  also from * have "\<dots> \<le> g (f i) + sum (g \<circ> f) I" by (intro add_left_mono)
+  also from insert have "\<dots> = sum (g \<circ> f) (insert i I)" by (simp add: sum.insert_if)
   finally show ?case .
 qed
 
diff -r a3e7a323780f -r 1d0cb3f003d4 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Feb 19 14:31:26 2024 +0100
+++ b/src/HOL/Transcendental.thy	Mon Feb 19 14:12:29 2024 +0000
@@ -2450,6 +2450,10 @@
   shows "continuous_on s (\<lambda>x. log (f x) (g x))"
   using assms unfolding continuous_on_def by (fast intro: tendsto_log)
 
+lemma exp_powr_real:
+  fixes x::real shows "exp x powr y = exp (x*y)"
+  by (simp add: powr_def)
+
 lemma powr_one_eq_one [simp]: "1 powr a = 1"
   by (simp add: powr_def)
 
@@ -2469,6 +2473,13 @@
   for a x y :: real
   by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
 
+lemma prod_powr_distrib:
+  fixes  x :: "'a \<Rightarrow> real"
+  assumes "\<And>i. i\<in>I \<Longrightarrow> x i \<ge> 0"
+  shows "(prod x I) powr r = (\<Prod>i\<in>I. x i powr r)"
+  using assms
+  by (induction I rule: infinite_finite_induct) (auto simp add: powr_mult prod_nonneg)
+
 lemma powr_ge_pzero [simp]: "0 \<le> x powr y"
   for x y :: real
   by (simp add: powr_def)
@@ -2546,6 +2557,14 @@
   shows   "x powr real_of_int n = power_int x n"
   by (metis assms exp_ln_iff exp_power_int nless_le power_int_eq_0_iff powr_def)
 
+lemma exp_minus_ge: 
+  fixes x::real shows "1 - x \<le> exp (-x)"
+  by (smt (verit) exp_ge_add_one_self)
+
+lemma exp_minus_greater: 
+  fixes x::real shows "1 - x < exp (-x) \<longleftrightarrow> x \<noteq> 0"
+  by (smt (verit) exp_minus_ge exp_eq_one_iff exp_gt_zero ln_eq_minus_one ln_exp)
+
 lemma log_ln: "ln x = log (exp(1)) x"
   by (simp add: log_def)
 
@@ -2945,6 +2964,17 @@
   for x :: real
   using less_eq_real_def powr_less_mono2 that by auto
 
+lemma powr01_less_one: 
+  fixes a::real 
+  assumes "0 < a" "a < 1"  
+  shows "a powr e < 1 \<longleftrightarrow> e>0"
+proof
+  show "a powr e < 1 \<Longrightarrow> e>0"
+    using assms not_less_iff_gr_or_eq powr_less_mono2_neg by fastforce
+  show "e>0 \<Longrightarrow> a powr e < 1"
+    by (metis assms less_eq_real_def powr_less_mono2 powr_one_eq_one)
+qed
+
 lemma powr_le1: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr a \<le> 1"
   for x :: real
   using powr_mono2 by fastforce
@@ -2973,6 +3003,9 @@
 lemma powr_half_sqrt: "0 \<le> x \<Longrightarrow> x powr (1/2) = sqrt x"
   by (simp add: powr_def root_powr_inverse sqrt_def)
 
+lemma powr_half_sqrt_powr: "0 \<le> x \<Longrightarrow> x powr (a/2) = sqrt(x powr a)"
+  by (metis divide_inverse mult.left_neutral powr_ge_pzero powr_half_sqrt powr_powr)
+
 lemma square_powr_half [simp]:
   fixes x::real shows "x\<^sup>2 powr (1/2) = \<bar>x\<bar>"
   by (simp add: powr_half_sqrt)
@@ -3108,6 +3141,23 @@
     by (rule has_derivative_transform_within[OF _ \<open>d > 0\<close> \<open>x \<in> X\<close>]) (auto simp: powr_def dest: pos')
 qed
 
+lemma has_derivative_const_powr [derivative_intros]:
+  assumes "\<And>x. (f has_derivative f') (at x)" "a \<noteq> (0::real)"
+  shows "((\<lambda>x. a powr (f x)) has_derivative (\<lambda>y. f' y * ln a * a powr (f x))) (at x)"
+  using assms
+  apply (simp add: powr_def)
+  apply (rule assms derivative_eq_intros refl)+
+  done
+
+lemma has_real_derivative_const_powr [derivative_intros]:
+  assumes "\<And>x. (f has_real_derivative f' x) (at x)"
+    "a \<noteq> (0::real)"
+  shows "((\<lambda>x. a powr (f x)) has_real_derivative (f' x * ln a * a powr (f x))) (at x)"
+  using assms
+  apply (simp add: powr_def)
+  apply (rule assms derivative_eq_intros refl | simp)+
+  done
+
 lemma DERIV_powr:
   fixes r :: real
   assumes g: "DERIV g x :> m"