# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1707233350 0
# Node ID 7822b55b26ce2ba640bc985c62cfc273d1deb664
# Parent  163b554af747a650da03082d57e8e5b1d845507d
Correct the definition of a convex function, and updated the proofs

diff -r 163b554af747 -r 7822b55b26ce src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Mon Feb 05 22:03:43 2024 +0100
+++ b/src/HOL/Analysis/Convex.thy	Tue Feb 06 15:29:10 2024 +0000
@@ -302,20 +302,21 @@
 subsection \<open>Convex Functions on a Set\<close>
 
 definition\<^marker>\<open>tag important\<close> convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
-  where "convex_on S f \<longleftrightarrow>
+  where "convex_on S f \<longleftrightarrow> convex S \<and>
     (\<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>
+  "concave_on S f \<longleftrightarrow> convex S \<and>
     (\<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"
+    and "convex A"
   shows "convex_on A f"
   unfolding convex_on_def
   by (smt (verit, del_insts) assms mult_cancel_right1 mult_eq_0_iff scaleR_collapse scaleR_eq_0_iff)
@@ -324,6 +325,7 @@
   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) \<le> (1 - t) * f x + t * f y"
+    and "convex A"
   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)
 
@@ -333,14 +335,20 @@
     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_imp_convex: "convex_on A f \<Longrightarrow> convex A"
+  by (auto simp: convex_on_def)
+
+lemma concave_on_imp_convex: "concave_on A f \<Longrightarrow> convex A"
+  by (simp add: concave_on_def convex_on_imp_convex)
+
 lemma convex_onD_Icc:
   assumes "convex_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) \<le> (1 - t) * f x + t * f y"
   using assms(2) by (intro convex_onD [OF assms(1)]) simp_all
 
-lemma convex_on_subset: "convex_on t f \<Longrightarrow> S \<subseteq> t \<Longrightarrow> convex_on S f"
-  unfolding convex_on_def by auto
+lemma convex_on_subset: "\<lbrakk>convex_on T f; S \<subseteq> T; convex S\<rbrakk> \<Longrightarrow> convex_on S f"
+  by (simp add: convex_on_def subset_iff)
 
 lemma convex_on_add [intro]:
   assumes "convex_on S f"
@@ -359,7 +367,7 @@
     then have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)"
       by (simp add: field_simps)
   }
-  then show ?thesis
+  with assms show ?thesis
     unfolding convex_on_def by auto
 qed
 
@@ -396,8 +404,10 @@
 
 lemma convex_on_dist [intro]:
   fixes S :: "'a::real_normed_vector set"
+  assumes "convex S"
   shows "convex_on S (\<lambda>x. dist a x)"
-proof (clarsimp simp: convex_on_def dist_norm)
+unfolding convex_on_def dist_norm
+proof (intro conjI strip)
   fix x y
   assume "x \<in> S" "y \<in> S"
   fix u v :: real
@@ -410,7 +420,7 @@
     by (auto simp: algebra_simps)
   then show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
     by (smt (verit, best) \<open>0 \<le> u\<close> \<open>0 \<le> v\<close> norm_scaleR norm_triangle_ineq)
-qed
+qed (use assms in auto)
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic operations on sets preserve convexity\<close>
@@ -568,7 +578,7 @@
 
 lemma convex_on_alt:
   fixes C :: "'a::real_vector set"
-  shows "convex_on C f \<longleftrightarrow>
+  shows "convex_on C f \<longleftrightarrow> convex C \<and>
          (\<forall>x \<in> C. \<forall>y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1 \<longrightarrow>
           f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
   by (smt (verit) convex_on_def)
@@ -765,6 +775,11 @@
     and "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f' x \<le> f' y"
   shows "convex_on A f"
 proof (rule convex_on_linorderI)
+  show "convex A"
+    using \<open>connected A\<close> convex_real_interval interval_cases
+    by (smt (verit, ccfv_SIG) connectedD_interval convex_UNIV convex_empty)
+      \<comment> \<open>the equivalence of "connected" and "convex" for real intervals is proved later\<close>
+next
   fix t x y :: real
   assume t: "t > 0" "t < 1"
   assume xy: "x \<in> A" "y \<in> A" "x < y"
@@ -810,7 +825,7 @@
 
 lemma convex_on_inverse:
   fixes A :: "real set"
-  assumes "A \<subseteq> {0<..}"
+  assumes "A \<subseteq> {0<..}" "convex A"
   shows "convex_on A inverse"
 proof -
   have "convex_on {0::real<..} inverse"
@@ -2307,15 +2322,13 @@
 lemma mem_epigraph: "(x, y) \<in> epigraph S f \<longleftrightarrow> x \<in> S \<and> f x \<le> y"
   unfolding epigraph_def by auto
 
-lemma convex_epigraph: "convex (epigraph S f) \<longleftrightarrow> convex_on S f \<and> convex S"
+lemma convex_epigraph: "convex (epigraph S f) \<longleftrightarrow> convex_on S f"
 proof safe
   assume L: "convex (epigraph S f)"
   then show "convex_on S f"
-    by (auto simp: convex_def convex_on_def epigraph_def)
-  show "convex S"
-    using L by (fastforce simp: convex_def convex_on_def epigraph_def)
+    by (fastforce simp: convex_def convex_on_def epigraph_def)
 next
-  assume "convex_on S f" "convex S"
+  assume "convex_on S f"
   then show "convex (epigraph S f)"
     unfolding convex_def convex_on_def epigraph_def
     apply safe
@@ -2324,16 +2337,15 @@
     done
 qed
 
-lemma convex_epigraphI: "convex_on S f \<Longrightarrow> convex S \<Longrightarrow> convex (epigraph S f)"
+lemma convex_epigraphI: "convex_on S f \<Longrightarrow> convex (epigraph S f)"
   unfolding convex_epigraph by auto
 
-lemma convex_epigraph_convex: "convex S \<Longrightarrow> convex_on S f \<longleftrightarrow> convex(epigraph S f)"
+lemma convex_epigraph_convex: "convex_on S f \<longleftrightarrow> convex(epigraph S f)"
   by (simp add: convex_epigraph)
 
 
 subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Use this to derive general bound property of convex function\<close>
 
-
 lemma convex_on:
   assumes "convex S"
   shows "convex_on S f \<longleftrightarrow>
@@ -2360,7 +2372,7 @@
 next
   assume "\<forall>k u x. ?rhs k u x"
   then show ?lhs
-  unfolding convex_epigraph_convex[OF assms] convex epigraph_def Ball_def mem_Collect_eq fst_sum snd_sum
+  unfolding convex_epigraph_convex convex epigraph_def Ball_def mem_Collect_eq fst_sum snd_sum
   using assms[unfolded convex] apply clarsimp
   apply (rule_tac y="\<Sum>i = 1..k. u i * f (fst (x i))" in order_trans)
   by (auto simp add: mult_left_mono intro: sum_mono)
diff -r 163b554af747 -r 7822b55b26ce src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Feb 05 22:03:43 2024 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Feb 06 15:29:10 2024 +0000
@@ -10,8 +10,7 @@
 
 theory Convex_Euclidean_Space
 imports
-  Convex
-  Topology_Euclidean_Space
+  Convex Topology_Euclidean_Space Line_Segment
 begin
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets and Functions\<close>
@@ -1959,7 +1958,7 @@
 lemma convex_on_bounded_continuous:
   fixes S :: "('a::real_normed_vector) set"
   assumes "open S"
-    and "convex_on S f"
+    and f: "convex_on S f"
     and "\<forall>x\<in>S. \<bar>f x\<bar> \<le> b"
   shows "continuous_on S f"
 proof -
@@ -2002,9 +2001,8 @@
             unfolding t_def using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
             by (auto simp:field_simps)
           have "f y - f x \<le> (f w - f x) / t"
-            using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w]
-            using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> S\<close> \<open>w \<in> S\<close>
-            by (auto simp:field_simps)
+            using convex_onD [OF f, of "(t - 1)/t" w x] \<open>0 < t\<close> \<open>2 < t\<close> \<open>x \<in> S\<close> \<open>w \<in> S\<close>
+            by (simp add: w field_simps)
           also have "... < e"
             using B(2)[OF \<open>w\<in>S\<close>] and B(2)[OF \<open>x\<in>S\<close>] 2 \<open>t > 0\<close> by (auto simp: field_simps)
           finally have th1: "f y - f x < e" .
@@ -2030,9 +2028,8 @@
             using \<open>t > 0\<close>
             by (auto simp:field_simps)
           have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
-            using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
-            using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> S\<close> \<open>w \<in> S\<close>
-            by (auto simp:field_simps)
+            using convex_onD [OF f, of "t / (1+t)" w y] \<open>0 < t\<close> \<open>2 < t\<close> \<open>y \<in> S\<close> \<open>w \<in> S\<close>
+            by (simp add: w field_simps)
           also have "\<dots> = (f w + t * f y) / (1 + t)"
             using \<open>t > 0\<close> by (simp add: add_divide_distrib) 
           also have "\<dots> < e + f y"
@@ -2051,8 +2048,8 @@
 
 lemma convex_bounds_lemma:
   fixes x :: "'a::real_normed_vector"
-  assumes "convex_on (cball x e) f"
-    and "\<forall>y \<in> cball x e. f y \<le> b" and y: "y \<in> cball x e"
+  assumes f: "convex_on (cball x e) f"
+    and b: "\<And>y. y \<in> cball x e \<Longrightarrow> f y \<le> b" and y: "y \<in> cball x e"
   shows "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
 proof (cases "0 \<le> e")
   case True
@@ -2064,9 +2061,8 @@
   have "(1 / 2) *\<^sub>R y + (1 / 2) *\<^sub>R z = x"
     unfolding z_def by (auto simp: algebra_simps)
   then show "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
-    using assms(1)[unfolded convex_on_def,rule_format, OF y z, of "1/2" "1/2"]
-    using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z]
-    by (auto simp:field_simps)
+    using convex_onD [OF f, of "1/2" y z] b[OF y] b y z
+    by (fastforce simp add: field_simps)
 next
   case False
   have "dist x y < 0"
@@ -2082,23 +2078,22 @@
   by auto
 
 lemma convex_on_continuous:
-  assumes "open (s::('a::euclidean_space) set)" "convex_on s f"
-  shows "continuous_on s f"
-  unfolding continuous_on_eq_continuous_at[OF assms(1)]
+  fixes S :: "'a::euclidean_space set"
+  assumes "open S" "convex_on S f"
+  shows "continuous_on S f"
+  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
 proof
   note dimge1 = DIM_positive[where 'a='a]
   fix x
-  assume "x \<in> s"
-  then obtain e where e: "cball x e \<subseteq> s" "e > 0"
+  assume "x \<in> S"
+  then obtain e where e: "cball x e \<subseteq> S" "e > 0"
     using assms(1) unfolding open_contains_cball by auto
   define d where "d = e / real DIM('a)"
   have "0 < d"
     unfolding d_def using \<open>e > 0\<close> dimge1 by auto
   let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
   obtain c
-    where c: "finite c"
-    and c1: "convex hull c \<subseteq> cball x e"
-    and c2: "cball x d \<subseteq> convex hull c"
+    where c: "finite c" and c1: "convex hull c \<subseteq> cball x e" and c2: "cball x d \<subseteq> convex hull c"
   proof
     define c where "c = (\<Sum>i\<in>Basis. (\<lambda>a. a *\<^sub>R i) ` {x\<bullet>i - d, x\<bullet>i + d})"
     show "finite c"
@@ -2145,9 +2140,11 @@
     using \<open>convex_on (convex hull c) f\<close> c2 convex_on_subset by blast
   then have "\<And>y. y\<in>cball x d \<Longrightarrow> \<bar>f y\<bar> \<le> k + 2 * \<bar>f x\<bar>"
     by (rule convex_bounds_lemma) (use c2 k in blast)
-  then have "continuous_on (ball x d) f"
-    by (meson Elementary_Metric_Spaces.open_ball ball_subset_cball conv convex_on_bounded_continuous 
-              convex_on_subset mem_ball_imp_mem_cball)
+  moreover have "convex_on (ball x d) f"
+    using conv convex_on_subset by fastforce
+  ultimately
+  have "continuous_on (ball x d) f"
+    by (metis convex_on_bounded_continuous Elementary_Metric_Spaces.open_ball mem_ball_imp_mem_cball)
   then show "continuous (at x) f"
     unfolding continuous_on_eq_continuous_at[OF open_ball]
     using \<open>d > 0\<close> by auto
diff -r 163b554af747 -r 7822b55b26ce src/HOL/Analysis/Line_Segment.thy
--- a/src/HOL/Analysis/Line_Segment.thy	Mon Feb 05 22:03:43 2024 +0100
+++ b/src/HOL/Analysis/Line_Segment.thy	Tue Feb 06 15:29:10 2024 +0000
@@ -109,10 +109,7 @@
   fix u v :: real
   assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
   have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
-    using uv yz
-    using convex_on_dist [of "ball x e" x, unfolded convex_on_def,
-      THEN bspec[where x=y], THEN bspec[where x=z]]
-    by auto
+    using uv yz by (meson UNIV_I convex_def convex_on_def convex_on_dist)
   then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
     using convex_bound_lt[OF yz uv] by auto
 qed
@@ -127,10 +124,7 @@
     fix u v :: real
     assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
     have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
-      using uv yz
-      using convex_on_dist [of "cball x e" x, unfolded convex_on_def,
-        THEN bspec[where x=y], THEN bspec[where x=z]]
-      by auto
+      using uv yz by (meson UNIV_I convex_def convex_on_def convex_on_dist)
     then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
       using convex_bound_le[OF yz uv] by auto
   }
diff -r 163b554af747 -r 7822b55b26ce src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Feb 05 22:03:43 2024 +0100
+++ b/src/HOL/Fun.thy	Tue Feb 06 15:29:10 2024 +0000
@@ -1024,7 +1024,6 @@
     using mono_f[THEN monotone_onD] by simp
 qed
 
-
 subsubsection \<open>Specializations For @{class ord} Type Class And More\<close>
 
 context ord begin
@@ -1158,6 +1157,20 @@
   qed
 qed
 
+lemma mono_on_ident: "mono_on S (\<lambda>x. x)"
+  by (simp add: monotone_on_def)
+
+lemma strict_mono_on_ident: "strict_mono_on S (\<lambda>x. x)"
+  by (simp add: monotone_on_def)
+
+lemma mono_on_const:
+  fixes a :: "'b::order" shows "mono_on S (\<lambda>x. a)"
+  by (simp add: mono_on_def)
+
+lemma antimono_on_const:
+  fixes a :: "'b::order" shows "antimono_on S (\<lambda>x. a)"
+  by (simp add: monotone_on_def)
+
 end
 
 context linorder begin