--- a/src/HOL/Analysis/Convex.thy Tue Feb 06 15:29:10 2024 +0000
+++ b/src/HOL/Analysis/Convex.thy Wed Feb 07 11:52:34 2024 +0000
@@ -10,8 +10,7 @@
theory Convex
imports
- Affine
- "HOL-Library.Set_Algebras"
+ Affine "HOL-Library.Set_Algebras" "HOL-Library.FuncSet"
begin
subsection \<open>Convex Sets\<close>
@@ -308,6 +307,9 @@
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 convex_on_iff_concave: "convex_on S f = concave_on S (\<lambda>x. - f x)"
+ by (simp add: concave_on_def)
+
lemma concave_on_iff:
"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)"
@@ -371,6 +373,69 @@
unfolding convex_on_def by auto
qed
+lemma convex_on_ident: "convex_on S (\<lambda>x. x) \<longleftrightarrow> convex S"
+ by (simp add: convex_on_def)
+
+lemma concave_on_ident: "concave_on S (\<lambda>x. x) \<longleftrightarrow> convex S"
+ by (simp add: concave_on_iff)
+
+lemma convex_on_const: "convex_on S (\<lambda>x. a) \<longleftrightarrow> convex S"
+ by (simp add: convex_on_def flip: distrib_right)
+
+lemma concave_on_const: "concave_on S (\<lambda>x. a) \<longleftrightarrow> convex S"
+ by (simp add: concave_on_iff flip: distrib_right)
+
+lemma convex_on_diff:
+ assumes "convex_on S f" and "concave_on S g"
+ shows "convex_on S (\<lambda>x. f x - g x)"
+ using assms concave_on_def convex_on_add by fastforce
+
+lemma concave_on_diff:
+ assumes "concave_on S f"
+ and "convex_on S g"
+ shows "concave_on S (\<lambda>x. f x - g x)"
+ using convex_on_diff assms concave_on_def by fastforce
+
+lemma concave_on_add:
+ assumes "concave_on S f"
+ and "concave_on S g"
+ shows "concave_on S (\<lambda>x. f x + g x)"
+ using assms convex_on_iff_concave concave_on_diff concave_on_def by fastforce
+
+lemma convex_on_mul:
+ fixes S::"real set"
+ assumes "convex_on S f" "convex_on S g"
+ assumes "mono_on S f" "mono_on S g"
+ assumes fty: "f \<in> S \<rightarrow> {0..}" and gty: "g \<in> S \<rightarrow> {0..}"
+ shows "convex_on S (\<lambda>x. f x * g x)"
+proof (intro convex_on_linorderI)
+ show "convex S"
+ using \<open>convex_on S f\<close> convex_on_imp_convex by blast
+ fix t::real and x y
+ assume t: "0 < t" "t < 1" and xy: "x \<in> S" "y \<in> S"
+ have "f x*g y + f y*g x \<le> f x*g x + f y*g y"
+ using \<open>mono_on S f\<close> \<open>mono_on S g\<close>
+ by (smt (verit, ccfv_SIG) mono_onD mult_right_mono right_diff_distrib' xy)
+ then have "(1-t) * f x * g y + (1-t) * f y * g x \<le> (1-t) * f x * g x + (1-t) * f y * g y"
+ using t
+ by (metis (mono_tags, opaque_lifting) mult.assoc diff_gt_0_iff_gt distrib_left mult_le_cancel_left_pos)
+ then have *: "t*(1-t) * f x * g y + t*(1-t) * f y * g x \<le> t*(1-t) * f x * g x + t*(1-t) * f y * g y"
+ using t
+ by (metis (mono_tags, opaque_lifting) mult.assoc distrib_left mult_le_cancel_left_pos)
+ have inS: "(1-t)*x + t*y \<in> S"
+ using t xy \<open>convex S\<close> by (simp add: convex_alt)
+ then have "f ((1-t)*x + t*y) * g ((1-t)*x + t*y) \<le> ((1-t)*f x + t*f y)*g ((1-t)*x + t*y)"
+ using convex_onD [OF \<open>convex_on S f\<close>, of t x y] t xy fty gty
+ by (intro mult_mono add_nonneg_nonneg) (auto simp: Pi_iff zero_le_mult_iff)
+ also have "\<dots> \<le> ((1-t)*f x + t*f y) * ((1-t)*g x + t*g y)"
+ using convex_onD [OF \<open>convex_on S g\<close>, of t x y] t xy fty gty inS
+ by (intro mult_mono add_nonneg_nonneg) (auto simp: Pi_iff zero_le_mult_iff)
+ also have "\<dots> \<le> (1-t) * (f x*g x) + t * (f y*g y)"
+ using * by (simp add: algebra_simps)
+ finally show "f ((1-t) *\<^sub>R x + t *\<^sub>R y) * g ((1-t) *\<^sub>R x + t *\<^sub>R y) \<le> (1-t)*(f x*g x) + t*(f y*g y)"
+ by simp
+qed
+
lemma convex_on_cmul [intro]:
fixes c :: real
assumes "0 \<le> c"
@@ -384,6 +449,13 @@
unfolding convex_on_def and * by auto
qed
+lemma convex_on_cdiv [intro]:
+ fixes c :: real
+ assumes "0 \<le> c" and "convex_on S f"
+ shows "convex_on S (\<lambda>x. f x / c)"
+ unfolding divide_inverse
+ using convex_on_cmul [of "inverse c" S f] by (simp add: mult.commute assms)
+
lemma convex_lower:
assumes "convex_on S f"
and "x \<in> S"
@@ -583,7 +655,7 @@
f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
by (smt (verit) convex_on_def)
-lemma convex_on_diff:
+lemma convex_on_slope_le:
fixes f :: "real \<Rightarrow> real"
assumes f: "convex_on I f"
and I: "x \<in> I" "y \<in> I"
@@ -742,6 +814,33 @@
unfolding concave_on_def
by (rule assms f''_ge0_imp_convex derivative_eq_intros | simp)+
+lemma convex_power_even:
+ assumes "even n"
+ shows "convex_on (UNIV::real set) (\<lambda>x. x^n)"
+proof (intro f''_ge0_imp_convex)
+ show "((\<lambda>x. x ^ n) has_real_derivative of_nat n * x^(n-1)) (at x)" for x
+ by (rule derivative_eq_intros | simp)+
+ show "((\<lambda>x. of_nat n * x^(n-1)) has_real_derivative of_nat n * of_nat (n-1) * x^(n-2)) (at x)" for x
+ by (rule derivative_eq_intros | simp add: eval_nat_numeral)+
+ show "\<And>x. 0 \<le> real n * real (n - 1) * x ^ (n - 2)"
+ using assms by (auto simp: zero_le_mult_iff zero_le_even_power)
+qed auto
+
+lemma convex_power_odd:
+ assumes "odd n"
+ shows "convex_on {0::real..} (\<lambda>x. x^n)"
+proof (intro f''_ge0_imp_convex)
+ show "((\<lambda>x. x ^ n) has_real_derivative of_nat n * x^(n-1)) (at x)" for x
+ by (rule derivative_eq_intros | simp)+
+ show "((\<lambda>x. of_nat n * x^(n-1)) has_real_derivative of_nat n * of_nat (n-1) * x^(n-2)) (at x)" for x
+ by (rule derivative_eq_intros | simp add: eval_nat_numeral)+
+ show "\<And>x. x \<in> {0::real..} \<Longrightarrow> 0 \<le> real n * real (n - 1) * x ^ (n - 2)"
+ using assms by (auto simp: zero_le_mult_iff zero_le_even_power)
+qed auto
+
+lemma convex_power2: "convex_on (UNIV::real set) power2"
+ by (simp add: convex_power_even)
+
lemma log_concave:
fixes b :: real
assumes "b > 1"
@@ -888,7 +987,7 @@
finally show ?thesis .
qed (use assms in auto)
-subsection \<open>Some inequalities\<close>
+subsection \<open>Some inequalities: Applications of convexity\<close>
lemma Youngs_inequality_0:
fixes a::real
@@ -939,6 +1038,20 @@
by (simp add: pos_divide_le_eq True)
qed
+lemma sum_squared_le_sum_of_squares:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes "\<And>i. i\<in>I \<Longrightarrow> f i \<ge> 0" "finite I" "I \<noteq> {}"
+ shows "(\<Sum>i\<in>I. f i)\<^sup>2 \<le> (\<Sum>y\<in>I. (f y)\<^sup>2) * card I"
+proof (cases "finite I \<and> I \<noteq> {}")
+ case True
+ have "(\<Sum>i\<in>I. f i / real (card I))\<^sup>2 \<le> (\<Sum>i\<in>I. (f i)\<^sup>2 / real (card I))"
+ using assms convex_on_sum [OF _ _ convex_power2, where a = "\<lambda>x. 1 / real(card I)" and S=I]
+ by simp
+ then show ?thesis
+ using assms
+ by (simp add: divide_simps power2_eq_square split: if_split_asm flip: sum_divide_distrib)
+qed auto
+
subsection \<open>Misc related lemmas\<close>
lemma convex_translation_eq [simp]:
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Tue Feb 06 15:29:10 2024 +0000
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Feb 07 11:52:34 2024 +0000
@@ -2472,6 +2472,15 @@
"finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)"
by (subst emeasure_point_measure) (auto dest: finite_subset intro!: sum.mono_neutral_left simp: less_le)
+lemma emeasure_point_measure_finite_if:
+ "finite A \<Longrightarrow> emeasure (point_measure A f) X = (if X \<subseteq> A then \<Sum>a\<in>X. f a else 0)"
+ by (simp add: emeasure_point_measure_finite emeasure_notin_sets sets_point_measure)
+
+lemma measure_point_measure_finite_if:
+ assumes "finite A" and "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+ shows "measure (point_measure A f) X = (if X \<subseteq> A then \<Sum>a\<in>X. f a else 0)"
+ by (simp add: Sigma_Algebra.measure_def assms emeasure_point_measure_finite_if subset_eq sum_nonneg)
+
lemma emeasure_point_measure_finite2:
"X \<subseteq> A \<Longrightarrow> finite X \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)"
by (subst emeasure_point_measure)
@@ -2607,10 +2616,18 @@
by (simp add: emeasure_point_measure_finite uniform_count_measure_def divide_inverse ennreal_mult
ennreal_of_nat_eq_real_of_nat)
+lemma emeasure_uniform_count_measure_if:
+ "finite A \<Longrightarrow> emeasure (uniform_count_measure A) X = (if X \<subseteq> A then card X / card A else 0)"
+ by (simp add: emeasure_notin_sets emeasure_uniform_count_measure sets_uniform_count_measure)
+
lemma measure_uniform_count_measure:
"finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> measure (uniform_count_measure A) X = card X / card A"
by (simp add: emeasure_point_measure_finite uniform_count_measure_def measure_def enn2real_mult)
+lemma measure_uniform_count_measure_if:
+ "finite A \<Longrightarrow> measure (uniform_count_measure A) X = (if X \<subseteq> A then card X / card A else 0)"
+ by (simp add: measure_uniform_count_measure measure_notin_sets sets_uniform_count_measure)
+
lemma space_uniform_count_measure_empty_iff [simp]:
"space (uniform_count_measure X) = {} \<longleftrightarrow> X = {}"
by(simp add: space_uniform_count_measure)
@@ -2618,7 +2635,7 @@
lemma sets_uniform_count_measure_eq_UNIV [simp]:
"sets (uniform_count_measure UNIV) = UNIV \<longleftrightarrow> True"
"UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True"
-by(simp_all add: sets_uniform_count_measure)
+ by(simp_all add: sets_uniform_count_measure)
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Scaled measure\<close>
--- a/src/HOL/Analysis/Sigma_Algebra.thy Tue Feb 06 15:29:10 2024 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Wed Feb 07 11:52:34 2024 +0000
@@ -497,6 +497,9 @@
lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
by (erule sigma_sets.induct, auto)
+lemma sigma_sets_finite: "\<lbrakk>x \<in> sigma_sets \<Omega> (Pow \<Omega>); finite \<Omega>\<rbrakk> \<Longrightarrow> finite x"
+ by (meson finite_subset order.refl sigma_sets_into_sp)
+
lemma sigma_algebra_sigma_sets:
"a \<subseteq> Pow \<Omega> \<Longrightarrow> sigma_algebra \<Omega> (sigma_sets \<Omega> a)"
by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp
@@ -1585,6 +1588,11 @@
by (auto simp add: measure_of_def intro!: arg_cong[where f=Abs_measure])
qed
+lemma measure_space_Pow_eq:
+ assumes "\<And>X. X \<in> Pow \<Omega> \<Longrightarrow> \<mu> X = \<mu>' X"
+ shows "measure_space \<Omega> (Pow \<Omega>) \<mu> = measure_space \<Omega> (Pow \<Omega>) \<mu>'"
+ by (smt (verit, best) assms measure_space_eq sigma_algebra.sigma_sets_eq sigma_algebra_Pow subset_eq)
+
lemma
shows space_measure_of_conv: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
and sets_measure_of_conv:
@@ -1926,6 +1934,10 @@
"f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
unfolding measurable_def by simp
+lemma finite_count_space: "finite \<Omega> \<Longrightarrow> count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) card"
+ unfolding count_space_def
+ by (smt (verit, best) PowD Pow_top count_space_def finite_subset measure_of_eq sets_count_space sets_measure_of)
+
lemma measurable_compose_countable':
assumes f: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f i x) \<in> measurable M N"
and g: "g \<in> measurable M (count_space I)" and I: "countable I"
--- a/src/HOL/Analysis/Starlike.thy Tue Feb 06 15:29:10 2024 +0000
+++ b/src/HOL/Analysis/Starlike.thy Wed Feb 07 11:52:34 2024 +0000
@@ -2782,11 +2782,11 @@
using \<open>t \<in> I\<close> \<open>x < t\<close> by auto
show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
using \<open>convex_on I f\<close> \<open>x \<in> I\<close> \<open>y \<in> I\<close> \<open>x < t\<close> \<open>t < y\<close>
- by (rule convex_on_diff)
+ by (rule convex_on_slope_le)
next
fix y
assume "y \<in> ?F x"
- with order_trans[OF convex_on_diff[OF \<open>convex_on I f\<close> \<open>K \<in> I\<close> _ \<open>K < x\<close> _]]
+ with order_trans[OF convex_on_slope_le[OF \<open>convex_on I f\<close> \<open>K \<in> I\<close> _ \<open>K < x\<close> _]]
show "(f K - f x) / (K - x) \<le> y" by auto
qed
then show ?thesis
@@ -2809,7 +2809,7 @@
also
fix z
assume "z \<in> ?F x"
- with order_trans[OF convex_on_diff[OF \<open>convex_on I f\<close> \<open>y \<in> I\<close> _ \<open>y < x\<close>]]
+ with order_trans[OF convex_on_slope_le[OF \<open>convex_on I f\<close> \<open>y \<in> I\<close> _ \<open>y < x\<close>]]
have "(f y - f x) / (y - x) \<le> z"
by auto
finally show "(f x - f y) / (x - y) \<le> z" .
--- a/src/HOL/Probability/Conditional_Expectation.thy Tue Feb 06 15:29:10 2024 +0000
+++ b/src/HOL/Probability/Conditional_Expectation.thy Wed Feb 07 11:52:34 2024 +0000
@@ -1145,9 +1145,9 @@
unfolding phi_def proof (rule cInf_greatest, auto)
fix t assume "t \<in> I" "y < t"
have "(q x - q y) / (x - y) \<le> (q x - q t) / (x - t)"
- apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
+ apply (rule convex_on_slope_le[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
also have "... \<le> (q y - q t) / (y - t)"
- apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
+ apply (rule convex_on_slope_le[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
finally show "(q x - q y) / (x - y) \<le> (q y - q t) / (y - t)" by simp
next
obtain e where "0 < e" "ball y e \<subseteq> I" using \<open>open I\<close> \<open>y \<in> I\<close> openE by blast