--- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Feb 19 08:23:23 2024 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Feb 19 14:12:20 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"
--- 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>
--- a/src/HOL/Groups_Big.thy Mon Feb 19 08:23:23 2024 +0100
+++ b/src/HOL/Groups_Big.thy Mon Feb 19 14:12:20 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
--- a/src/HOL/Transcendental.thy Mon Feb 19 08:23:23 2024 +0100
+++ b/src/HOL/Transcendental.thy Mon Feb 19 14:12:20 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"