# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1707306754 0
# Node ID a521c241e946b28f52717a2d646fc15d0da04bdf
# Parent  7822b55b26ce2ba640bc985c62cfc273d1deb664
Further lemmas concerning complexity and measures

diff -r 7822b55b26ce -r a521c241e946 src/HOL/Analysis/Convex.thy
--- 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]:
diff -r 7822b55b26ce -r a521c241e946 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- 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>
 
diff -r 7822b55b26ce -r a521c241e946 src/HOL/Analysis/Sigma_Algebra.thy
--- 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"
diff -r 7822b55b26ce -r a521c241e946 src/HOL/Analysis/Starlike.thy
--- 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" .
diff -r 7822b55b26ce -r a521c241e946 src/HOL/Probability/Conditional_Expectation.thy
--- 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