--- 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)
--- 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
--- 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
}
--- 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