# HG changeset patch
# User paulson
# Date 1636363886 0
# Node ID 25f5f1fa31bb7a9a1e4b8da3d65ee0c15670dad3
# Parent  58ae06d382ee5a1867d402550dbc69d2d1275c27# Parent  64b3d8d9bd105ee4bd2fe070e6a78fc07dc4ac8c
merged

diff -r 58ae06d382ee -r 25f5f1fa31bb src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Sun Nov 07 23:35:11 2021 +0100
+++ b/src/HOL/Analysis/Convex.thy	Mon Nov 08 09:31:26 2021 +0000
@@ -344,6 +344,14 @@
   where "convex_on S f \<longleftrightarrow>
     (\<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) \<le> u * f x + v * f y)"
 
+definition\<^marker>\<open>tag important\<close> concave_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+  where "concave_on S f \<equiv> convex_on S (\<lambda>x. - f x)"
+
+lemma concave_on_iff:
+  "concave_on S f \<longleftrightarrow>
+    (\<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 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"
@@ -865,35 +873,44 @@
   assumes conv: "convex C"
     and f': "\<And>x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
     and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
-    and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
+    and 0: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
   shows "convex_on C f"
-  using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function
+  using f''_imp_f'[OF conv f' f'' 0] assms pos_convex_function
   by fastforce
 
+lemma f''_le0_imp_concave:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "convex C"
+    and "\<And>x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
+    and "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
+    and "\<And>x. x \<in> C \<Longrightarrow> f'' x \<le> 0"
+  shows "concave_on C f"
+  unfolding concave_on_def
+  by (rule assms f''_ge0_imp_convex derivative_eq_intros | simp)+
+
+lemma log_concave:
+  fixes b :: real
+  assumes "b > 1"
+  shows "concave_on {0<..} (\<lambda> x. log b x)"
+  using assms
+  by (intro f''_le0_imp_concave derivative_eq_intros | simp)+
+
+lemma ln_concave: "concave_on {0<..} ln"
+  unfolding log_ln by (simp add: log_concave)
+
 lemma minus_log_convex:
   fixes b :: real
   assumes "b > 1"
   shows "convex_on {0 <..} (\<lambda> x. - log b x)"
-proof -
-  have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)"
-    using DERIV_log by auto
-  then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
-    by (auto simp: DERIV_minus)
-  have "\<And>z::real. z > 0 \<Longrightarrow> 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 "\<And>z::real. z > 0 \<Longrightarrow>
-    DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
-    by auto
-  then have f''0: "\<And>z::real. z > 0 \<Longrightarrow>
-    DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
-    unfolding inverse_eq_divide by (auto simp: mult.assoc)
-  have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
-    using \<open>b > 1\<close> by (auto intro!: less_imp_le)
-  from f''_ge0_imp_convex[OF convex_real_interval(3), unfolded greaterThan_iff, OF f' f''0 f''_ge0]
-  show ?thesis
-    by auto
-qed
+  using assms concave_on_def log_concave by blast
+
+lemma powr_convex: 
+  assumes "p \<ge> 1" shows "convex_on {0<..} (\<lambda>x. x powr p)"
+  using assms
+  by (intro f''_ge0_imp_convex derivative_eq_intros | simp)+
+
+lemma exp_convex: "convex_on UNIV exp"
+  by (intro f''_ge0_imp_convex derivative_eq_intros | simp)+
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Convexity of real functions\<close>
@@ -1003,6 +1020,63 @@
   finally show ?thesis .
 qed (insert assms(2), simp_all)
 
+subsection \<open>Some inequalities\<close>
+
+lemma Youngs_inequality_0:
+  fixes a::real
+  assumes "0 \<le> \<alpha>" "0 \<le> \<beta>" "\<alpha>+\<beta> = 1" "a>0" "b>0"
+  shows "a powr \<alpha> * b powr \<beta> \<le> \<alpha>*a + \<beta>*b"
+proof -
+  have "\<alpha> * ln a + \<beta> * ln b \<le> ln (\<alpha> * a + \<beta> * b)"
+    using assms ln_concave by (simp add: concave_on_iff)
+  moreover have "0 < \<alpha> * a + \<beta> * b"
+    using assms by (smt (verit) mult_pos_pos split_mult_pos_le)
+  ultimately show ?thesis
+    using assms by (simp add: powr_def mult_exp_exp flip: ln_ge_iff)
+qed
+
+lemma Youngs_inequality:
+  fixes p::real
+  assumes "p>1" "q>1" "1/p + 1/q = 1" "a\<ge>0" "b\<ge>0"
+  shows "a * b \<le> a powr p / p + b powr q / q"
+proof (cases "a=0 \<or> b=0")
+  case False
+  then show ?thesis 
+  using Youngs_inequality_0 [of "1/p" "1/q" "a powr p" "b powr q"] assms
+  by (simp add: powr_powr)
+qed (use assms in auto)
+
+lemma Cauchy_Schwarz_ineq_sum:
+  fixes a :: "'a \<Rightarrow> 'b::linordered_field"
+  shows "(\<Sum>i\<in>I. a i * b i)\<^sup>2 \<le> (\<Sum>i\<in>I. (a i)\<^sup>2) * (\<Sum>i\<in>I. (b i)\<^sup>2)"
+proof (cases "(\<Sum>i\<in>I. (b i)\<^sup>2) > 0")
+  case False
+  then consider "\<And>i. i\<in>I \<Longrightarrow> b i = 0" | "infinite I"
+    by (metis (mono_tags, lifting) sum_pos2 zero_le_power2 zero_less_power2)
+  thus ?thesis
+    by fastforce
+next
+  case True
+  define r where "r \<equiv> (\<Sum>i\<in>I. a i * b i) / (\<Sum>i\<in>I. (b i)\<^sup>2)"
+  with True have *: "(\<Sum>i\<in>I. a i * b i) = r * (\<Sum>i\<in>I. (b i)\<^sup>2)"
+    by simp
+  have "0 \<le> (\<Sum>i\<in>I. (a i - r * b i)\<^sup>2)"
+    by (meson sum_nonneg zero_le_power2)
+  also have "... = (\<Sum>i\<in>I. (a i)\<^sup>2) - 2 * r * (\<Sum>i\<in>I. a i * b i) + r\<^sup>2 * (\<Sum>i\<in>I. (b i)\<^sup>2)"
+    by (simp add: algebra_simps power2_eq_square sum_distrib_left flip: sum.distrib)
+  also have "\<dots> = (\<Sum>i\<in>I. (a i)\<^sup>2) - (\<Sum>i\<in>I. a i * b i) * r"
+    by (simp add: * power2_eq_square)
+  also have "\<dots> = (\<Sum>i\<in>I. (a i)\<^sup>2) - ((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2)"
+    by (simp add: r_def power2_eq_square)
+  finally have "0 \<le> (\<Sum>i\<in>I. (a i)\<^sup>2) - ((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2)" .
+  hence "((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2) \<le> (\<Sum>i\<in>I. (a i)\<^sup>2)"
+    by (simp add: le_diff_eq)
+  thus "((\<Sum>i\<in>I. a i * b i))\<^sup>2 \<le> (\<Sum>i\<in>I. (a i)\<^sup>2) * (\<Sum>i\<in>I. (b i)\<^sup>2)"
+    by (simp add: pos_divide_le_eq True)
+qed
+
+subsection \<open>Misc related lemmas\<close>
+
 lemma convex_translation_eq [simp]:
   "convex ((+) a ` s) \<longleftrightarrow> convex s"
   by (metis convex_translation translation_galois)
@@ -1016,9 +1090,6 @@
     shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> convex (f ` s) \<longleftrightarrow> convex s"
     by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq)
 
-lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
-  unfolding linear_iff by (simp add: algebra_simps)
-
 lemma vector_choose_size:
   assumes "0 \<le> c"
   obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c"
@@ -1045,18 +1116,6 @@
     unfolding * using sum.delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto
 qed
 
-lemma dist_triangle_eq:
-  fixes x y z :: "'a::real_inner"
-  shows "dist x z = dist x y + dist y z \<longleftrightarrow>
-    norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
-proof -
-  have *: "x - y + (y - z) = x - z" by auto
-  show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
-    by (auto simp:norm_minus_commute)
-qed
-
-
-
 
 subsection \<open>Cones\<close>
 
diff -r 58ae06d382ee -r 25f5f1fa31bb src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Nov 07 23:35:11 2021 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Nov 08 09:31:26 2021 +0000
@@ -1143,6 +1143,15 @@
   finally show ?thesis .
 qed
 
+lemma dist_triangle_eq:
+  fixes x y z :: "'a::real_inner"
+  shows "dist x z = dist x y + dist y z \<longleftrightarrow>
+    norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
+proof -
+  have *: "x - y + (y - z) = x - z" by auto
+  show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
+    by (auto simp:norm_minus_commute)
+qed
 
 subsection \<open>Collinearity\<close>
 
diff -r 58ae06d382ee -r 25f5f1fa31bb src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sun Nov 07 23:35:11 2021 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Mon Nov 08 09:31:26 2021 +0000
@@ -2398,6 +2398,9 @@
   by (intro closure_bounded_linear_image_subset bounded_linear_add
     bounded_linear_fst bounded_linear_snd)
 
+lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
+  unfolding linear_iff by (simp add: algebra_simps)
+
 lemma rel_interior_sum:
   fixes S T :: "'n::euclidean_space set"
   assumes "convex S"