# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1711030779 0
# Node ID ca004ccf2352c6702e2f40513209d7346f09f946
# Parent  67d28b35c5d8e25cf6d7ab2929b9d0fdc6dc1941
New material from a variety of sources (including AFP)

diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -891,10 +891,9 @@
   let ?\<mu> = "measure lebesgue"
   have "x \<in> cbox (vec (- real (nat \<lceil>norm x\<rceil>))) (vec (real (nat \<lceil>norm x\<rceil>)))" for x :: "real^'n::_"
     apply (simp add: mem_box_cart)
-    by (smt (verit, best) Finite_Cartesian_Product.norm_nth_le nat_ceiling_le_eq 
-        real_nat_ceiling_ge real_norm_def)
+    by (smt (verit, best) component_le_norm_cart le_of_int_ceiling)
   then have Seq: "S = (\<Union>n. ?I n)"
-    by auto
+    by blast
   have fIn: "f ` ?I n \<in> lmeasurable"
        and mfIn: "?\<mu> (f ` ?I n) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" (is ?MN) for n
   proof -
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -387,6 +387,11 @@
 lemma analytic_on_open: "open S \<Longrightarrow> f analytic_on S \<longleftrightarrow> f holomorphic_on S"
   by (meson analytic_imp_holomorphic analytic_on_def holomorphic_on_subset openE)
 
+lemma constant_on_imp_analytic_on:
+  assumes "f constant_on A" "open A"
+  shows "f analytic_on A"
+  by (simp add: analytic_on_open assms constant_on_imp_holomorphic_on)
+
 lemma analytic_on_imp_differentiable_at:
   "f analytic_on S \<Longrightarrow> x \<in> S \<Longrightarrow> f field_differentiable (at x)"
   using analytic_on_def holomorphic_on_imp_differentiable_at by auto
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Analysis/Convex.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -315,6 +315,12 @@
     (\<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 concave_onD:
+  assumes "concave_on A f"
+  shows "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
+    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<ge> (1 - t) * f x + t * f y"
+  using assms by (auto simp: concave_on_iff)
+
 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"
@@ -323,6 +329,12 @@
   unfolding convex_on_def
   by (smt (verit, del_insts) assms mult_cancel_right1 mult_eq_0_iff scaleR_collapse scaleR_eq_0_iff)
 
+lemma convex_onD:
+  assumes "convex_on A f"
+  shows "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 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"
+  using assms by (auto simp: convex_on_def)
+
 lemma convex_on_linorderI [intro?]:
   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>
@@ -331,11 +343,13 @@
   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)
 
-lemma convex_onD:
-  assumes "convex_on A f"
-  shows "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 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"
-  using assms by (auto simp: convex_on_def)
+lemma concave_on_linorderI [intro?]:
+  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) \<ge> (1 - t) * f x + t * f y"
+    and "convex A"
+  shows "concave_on A f"
+  by (smt (verit) assms concave_on_def convex_on_linorderI mult_minus_right)
 
 lemma convex_on_imp_convex: "convex_on A f \<Longrightarrow> convex A"
   by (auto simp: convex_on_def)
@@ -407,27 +421,21 @@
   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)"
+  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
+    using assms convex_on_imp_convex by auto
   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)  
+  assume t: "0 < t" "t < 1" and xy: "x \<in> S" "y \<in> S" "x<y"
+  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 \<open>mono_on S f\<close> \<open>mono_on S g\<close> xy
+    by (smt (verit, ccfv_SIG) left_diff_distrib mono_onD mult_left_less_imp_less zero_le_mult_iff)
   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)"
+  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)"
+  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)"
@@ -494,6 +502,50 @@
     by (smt (verit, best) \<open>0 \<le> u\<close> \<open>0 \<le> v\<close> norm_scaleR norm_triangle_ineq)
 qed (use assms in auto)
 
+lemma concave_on_mul:
+  fixes S::"real set"
+  assumes f: "concave_on S f" and g: "concave_on S g"
+  assumes "mono_on S f" "antimono_on S g"
+  assumes fty: "f \<in> S \<rightarrow> {0..}" and gty: "g \<in> S \<rightarrow> {0..}"
+  shows "concave_on S (\<lambda>x. f x * g x)"
+proof (intro concave_on_linorderI)
+  show "convex S"
+    using concave_on_imp_convex f by blast
+  fix t::real and x y
+  assume t: "0 < t" "t < 1" and xy: "x \<in> S" "y \<in> S" "x<y"
+  have inS: "(1-t)*x + t*y \<in> S"
+    using t xy \<open>convex S\<close> by (simp add: convex_alt)
+  have "f x * g y + f y * g x \<ge> f x * g x + f y * g y"
+    using \<open>mono_on S f\<close> \<open>antimono_on S g\<close>
+    unfolding monotone_on_def by (smt (verit, best) left_diff_distrib mult_left_mono xy)
+  with t have *: "t*(1-t) * f x * g y + t*(1-t) * f y * g x \<ge> t*(1-t) * f x * g x + t*(1-t) * f y * g y"
+    by (smt (verit, ccfv_SIG) distrib_left mult_left_mono diff_ge_0_iff_ge mult.assoc)
+  have "(1 - t) * (f x * g x) + t * (f y * g y) \<le> ((1-t) * f x + t * f y) * ((1-t) * g x + t * g y)"
+    using * by (simp add: algebra_simps)
+  also have "\<dots> \<le> ((1-t) * f x + t * f y)*g ((1-t)*x + t*y)"
+    using concave_onD [OF \<open>concave_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> f ((1-t)*x + t*y) * g ((1-t)*x + t*y)"
+    using concave_onD [OF \<open>concave_on S f\<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)
+  finally show "(1 - t) * (f x * g x) + t * (f y * g y)
+           \<le> f ((1 - t) *\<^sub>R x + t *\<^sub>R y) * g ((1 - t) *\<^sub>R x + t *\<^sub>R y)" 
+    by simp
+qed
+
+lemma concave_on_cmul [intro]:
+  fixes c :: real
+  assumes "0 \<le> c" and "concave_on S f"
+  shows "concave_on S (\<lambda>x. c * f x)"
+  using assms convex_on_cmul [of c S "\<lambda>x. - f x"]
+  by (auto simp: concave_on_def)
+
+lemma concave_on_cdiv [intro]:
+  fixes c :: real
+  assumes "0 \<le> c" and "concave_on S f"
+  shows "concave_on S (\<lambda>x. f x / c)"
+  unfolding divide_inverse
+  using concave_on_cmul [of "inverse c" S f] by (simp add: mult.commute assms)
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic operations on sets preserve convexity\<close>
 
@@ -1041,6 +1093,66 @@
   finally show ?thesis .
 qed (use assms in auto)
 
+lemma concave_onD_Icc:
+  assumes "concave_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) \<ge> (1 - t) * f x + t * f y"
+  using assms(2) by (intro concave_onD [OF assms(1)]) simp_all
+
+lemma concave_onD_Icc':
+  assumes "concave_on {x..y} f" "c \<in> {x..y}"
+  defines "d \<equiv> y - x"
+  shows "f c \<ge> (f y - f x) / d * (c - x) + f x"
+proof -
+  have "- f c \<le> (f x - f y) / d * (c - x) - f x"
+    using assms convex_onD_Icc' [of x y "\<lambda>x. - f x" c]
+    by (simp add: concave_on_def)
+  then show ?thesis
+    by (smt (verit, best) divide_minus_left mult_minus_left)
+qed
+
+lemma concave_onD_Icc'':
+  assumes "concave_on {x..y} f" "c \<in> {x..y}"
+  defines "d \<equiv> y - x"
+  shows "f c \<ge> (f x - f y) / d * (y - c) + f y"
+proof -
+  have "- f c \<le> (f y - f x) / d * (y - c) - f y"
+    using assms convex_onD_Icc'' [of x y "\<lambda>x. - f x" c]
+    by (simp add: concave_on_def)
+  then show ?thesis
+    by (smt (verit, best) divide_minus_left mult_minus_left)
+qed
+
+lemma convex_on_le_max:
+  fixes a::real
+  assumes "convex_on {x..y} f" and a: "a \<in> {x..y}"
+  shows "f a \<le> max (f x) (f y)"
+proof -
+  have *: "(f y - f x) * (a - x) \<le> (f y - f x) * (y - x)" if "f x \<le> f y"
+    using a that by (intro mult_left_mono) auto
+  have "f a \<le> (f y - f x) / (y - x) * (a - x) + f x" 
+    using assms convex_onD_Icc' by blast
+  also have "\<dots> \<le> max (f x) (f y)"
+    using a *
+    by (simp add: divide_le_0_iff mult_le_0_iff zero_le_mult_iff max_def add.commute mult.commute scaling_mono)
+  finally show ?thesis .
+qed
+
+lemma concave_on_ge_min:
+  fixes a::real
+  assumes "concave_on {x..y} f" and a: "a \<in> {x..y}"
+  shows "f a \<ge> min (f x) (f y)"
+proof -
+  have *: "(f y - f x) * (a - x) \<ge> (f y - f x) * (y - x)" if "f x \<ge> f y"
+    using a that by (intro mult_left_mono_neg) auto
+  have "min (f x) (f y) \<le> (f y - f x) / (y - x) * (a - x) + f x"
+    using a * apply (simp add: zero_le_divide_iff mult_le_0_iff zero_le_mult_iff min_def)
+    by (smt (verit, best) nonzero_eq_divide_eq pos_divide_le_eq)
+  also have "\<dots> \<le> f a"
+    using assms concave_onD_Icc' by blast
+  finally show ?thesis .
+qed
+
 subsection \<open>Some inequalities: Applications of convexity\<close>
 
 lemma Youngs_inequality_0:
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -2014,15 +2014,7 @@
       using assms by (intro finite_not_islimpt_in_compact) auto
   qed auto
   also have "(\<Union>n. cball 0 (real n)) = (UNIV :: 'a set)"
-  proof safe
-    fix z :: 'a
-    have "norm z \<ge> 0"
-      by simp
-    hence "real (nat \<lceil>norm z\<rceil>) \<ge> norm z"
-      by linarith
-    thus "z \<in> (\<Union>n. cball 0 (real n))"
-      by auto
-  qed auto
+    by (force simp: real_arch_simple)
   hence "(\<Union>n. cball 0 (real n) \<inter> X) = X"
     by blast
   finally show "countable X" .
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Archimedean_Field.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -647,6 +647,11 @@
 lemma of_nat_ceiling: "of_nat (nat \<lceil>r\<rceil>) \<ge> r"
   by (cases "r\<ge>0") auto
 
+lemma of_nat_int_floor [simp]: "x\<ge>0 \<Longrightarrow> of_nat (nat\<lfloor>x\<rfloor>) = of_int \<lfloor>x\<rfloor>"
+  by auto
+
+lemma of_nat_int_ceiling [simp]: "x\<ge>0 \<Longrightarrow> of_nat (nat \<lceil>x\<rceil>) = of_int \<lceil>x\<rceil>"
+  by auto
 
 subsection \<open>Frac Function\<close>
 
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -1822,6 +1822,9 @@
     by (simp add: zorder_def P_def)
 qed
 
+lemma zorder_uminus [simp]: "zorder (\<lambda>z. -f z) z = zorder f z"
+  using zorder_cmult[of "-1" f] by simp
+
 lemma zorder_nonzero_div_power:
   assumes sz: "open S" "z \<in> S" "f holomorphic_on S" "f z \<noteq> 0" and "n > 0"
   shows  "zorder (\<lambda>w. f w / (w - z) ^ n) z = - n"
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Complex_Analysis/Laurent_Convergence.thy
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -2541,4 +2541,44 @@
   "(\<lambda>z. tan (c * z)) has_laurent_expansion fps_to_fls (fps_tan c)"
   by (intro has_laurent_expansion_fps has_fps_expansion_tan)
 
+subsection \<open>More Laurent expansions\<close>
+
+lemma has_laurent_expansion_frequently_zero_iff:
+  assumes "(\<lambda>w. f (z + w)) has_laurent_expansion F"
+  shows   "frequently (\<lambda>z. f z = 0) (at z) \<longleftrightarrow> F = 0"
+  using assms by (simp add: frequently_def has_laurent_expansion_eventually_nonzero_iff)
+
+lemma has_laurent_expansion_eventually_zero_iff:
+  assumes "(\<lambda>w. f (z + w)) has_laurent_expansion F"
+  shows   "eventually (\<lambda>z. f z = 0) (at z) \<longleftrightarrow> F = 0"
+  using assms
+  by (metis has_laurent_expansion_frequently_zero_iff has_laurent_expansion_isolated 
+            has_laurent_expansion_not_essential laurent_expansion_def 
+            not_essential_frequently_0_imp_eventually_0 not_essential_has_laurent_expansion)
+
+lemma has_laurent_expansion_frequently_nonzero_iff:
+  assumes "(\<lambda>w. f (z + w)) has_laurent_expansion F"
+  shows   "frequently (\<lambda>z. f z \<noteq> 0) (at z) \<longleftrightarrow> F \<noteq> 0"
+  using assms by (metis has_laurent_expansion_eventually_zero_iff not_eventually)
+
+lemma has_laurent_expansion_sum_list [laurent_expansion_intros]:
+  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x has_laurent_expansion F x"
+  shows   "(\<lambda>y. \<Sum>x\<leftarrow>xs. f x y) has_laurent_expansion (\<Sum>x\<leftarrow>xs. F x)"
+  using assms by (induction xs) (auto intro!: laurent_expansion_intros)
+
+lemma has_laurent_expansion_prod_list [laurent_expansion_intros]:
+  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x has_laurent_expansion F x"
+  shows   "(\<lambda>y. \<Prod>x\<leftarrow>xs. f x y) has_laurent_expansion (\<Prod>x\<leftarrow>xs. F x)"
+  using assms by (induction xs) (auto intro!: laurent_expansion_intros)
+
+lemma has_laurent_expansion_sum_mset [laurent_expansion_intros]:
+  assumes "\<And>x. x \<in># I \<Longrightarrow> f x has_laurent_expansion F x"
+  shows   "(\<lambda>y. \<Sum>x\<in>#I. f x y) has_laurent_expansion (\<Sum>x\<in>#I. F x)"
+  using assms by (induction I) (auto intro!: laurent_expansion_intros)
+
+lemma has_laurent_expansion_prod_mset [laurent_expansion_intros]:
+  assumes "\<And>x. x \<in># I \<Longrightarrow> f x has_laurent_expansion F x"
+  shows   "(\<lambda>y. \<Prod>x\<in>#I. f x y) has_laurent_expansion (\<Prod>x\<in>#I. F x)"
+  using assms by (induction I) (auto intro!: laurent_expansion_intros)
+
 end
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Complex_Analysis/Meromorphic.thy
--- a/src/HOL/Complex_Analysis/Meromorphic.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -4,62 +4,6 @@
   "HOL-Analysis.Sparse_In"
 begin
 
-(*TODO: move to topological space? *)
-lemma eventually_nhds_conv_at:
-  "eventually P (nhds x) \<longleftrightarrow> eventually P (at x) \<and> P x"
-  unfolding eventually_at_topological eventually_nhds by fast
-
-(*TODO: to Complex_Singularities? *)
-lemma zorder_uminus [simp]: "zorder (\<lambda>z. -f z) z = zorder f z"
-  using zorder_cmult[of "-1" f] by (simp del: zorder_cmult)
-
-lemma constant_on_imp_analytic_on:
-  assumes "f constant_on A" "open A"
-  shows "f analytic_on A"
-  by (simp add: analytic_on_open assms
-      constant_on_imp_holomorphic_on)
-
-(*TODO: could be moved to Laurent_Convergence*)
-subsection \<open>More Laurent expansions\<close>
-
-lemma has_laurent_expansion_frequently_zero_iff:
-  assumes "(\<lambda>w. f (z + w)) has_laurent_expansion F"
-  shows   "frequently (\<lambda>z. f z = 0) (at z) \<longleftrightarrow> F = 0"
-  using assms by (simp add: frequently_def has_laurent_expansion_eventually_nonzero_iff)
-
-lemma has_laurent_expansion_eventually_zero_iff:
-  assumes "(\<lambda>w. f (z + w)) has_laurent_expansion F"
-  shows   "eventually (\<lambda>z. f z = 0) (at z) \<longleftrightarrow> F = 0"
-  using assms
-  by (metis has_laurent_expansion_frequently_zero_iff has_laurent_expansion_isolated 
-            has_laurent_expansion_not_essential laurent_expansion_def 
-            not_essential_frequently_0_imp_eventually_0 not_essential_has_laurent_expansion)
-
-lemma has_laurent_expansion_frequently_nonzero_iff:
-  assumes "(\<lambda>w. f (z + w)) has_laurent_expansion F"
-  shows   "frequently (\<lambda>z. f z \<noteq> 0) (at z) \<longleftrightarrow> F \<noteq> 0"
-  using assms by (metis has_laurent_expansion_eventually_zero_iff not_eventually)
-
-lemma has_laurent_expansion_sum_list [laurent_expansion_intros]:
-  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x has_laurent_expansion F x"
-  shows   "(\<lambda>y. \<Sum>x\<leftarrow>xs. f x y) has_laurent_expansion (\<Sum>x\<leftarrow>xs. F x)"
-  using assms by (induction xs) (auto intro!: laurent_expansion_intros)
-
-lemma has_laurent_expansion_prod_list [laurent_expansion_intros]:
-  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x has_laurent_expansion F x"
-  shows   "(\<lambda>y. \<Prod>x\<leftarrow>xs. f x y) has_laurent_expansion (\<Prod>x\<leftarrow>xs. F x)"
-  using assms by (induction xs) (auto intro!: laurent_expansion_intros)
-
-lemma has_laurent_expansion_sum_mset [laurent_expansion_intros]:
-  assumes "\<And>x. x \<in># I \<Longrightarrow> f x has_laurent_expansion F x"
-  shows   "(\<lambda>y. \<Sum>x\<in>#I. f x y) has_laurent_expansion (\<Sum>x\<in>#I. F x)"
-  using assms by (induction I) (auto intro!: laurent_expansion_intros)
-
-lemma has_laurent_expansion_prod_mset [laurent_expansion_intros]:
-  assumes "\<And>x. x \<in># I \<Longrightarrow> f x has_laurent_expansion F x"
-  shows   "(\<lambda>y. \<Prod>x\<in>#I. f x y) has_laurent_expansion (\<Prod>x\<in>#I. F x)"
-  using assms by (induction I) (auto intro!: laurent_expansion_intros)
-
 subsection \<open>Remove singular points\<close>
 
 definition remove_sings :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Groups_Big.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -742,6 +742,22 @@
   "(\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i) \<Longrightarrow> (\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   by (induct K rule: infinite_finite_induct) (use add_mono in auto)
 
+lemma (in ordered_cancel_comm_monoid_add) sum_strict_mono_strong:
+  assumes "finite A" "a \<in> A" "f a < g a"
+    and "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+  shows "sum f A < sum g A"
+proof -
+  have "sum f A = f a + sum f (A-{a})"
+    by (simp add: assms sum.remove)
+  also have "\<dots> \<le> f a + sum g (A-{a})"
+    using assms by (meson DiffD1 add_left_mono sum_mono)
+  also have "\<dots> < g a + sum g (A-{a})"
+    using assms add_less_le_mono by blast
+  also have "\<dots> = sum g A"
+    using assms by (intro sum.remove [symmetric])
+  finally show ?thesis .
+qed
+
 lemma (in strict_ordered_comm_monoid_add) sum_strict_mono:
   assumes "finite A" "A \<noteq> {}"
     and "\<And>x. x \<in> A \<Longrightarrow> f x < g x"
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -15,13 +15,7 @@
 lemma prob_spaceI[Pure.intro!]:
   assumes *: "emeasure M (space M) = 1"
   shows "prob_space M"
-proof -
-  interpret finite_measure M
-  proof
-    show "emeasure M (space M) \<noteq> \<infinity>" using * by simp
-  qed
-  show "prob_space M" by standard fact
-qed
+  by (simp add: assms finite_measureI prob_space_axioms.intro prob_space_def)
 
 lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M"
   unfolding prob_space_def finite_measure_def by simp
@@ -54,7 +48,7 @@
 qed
 
 lemma (in prob_space) prob_space: "prob (space M) = 1"
-  using emeasure_space_1 unfolding measure_def by (simp add: one_ennreal.rep_eq)
+  by (simp add: emeasure_space_1 measure_eq_emeasure_eq_ennreal)
 
 lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1"
   using bounded_measure[of A] by (simp add: prob_space)
@@ -237,6 +231,20 @@
   finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
 qed
 
+lemma (in prob_space) finite_borel_measurable_integrable:
+  assumes "f\<in> borel_measurable M"
+  and "finite (f`(space M))"
+  shows "integrable M f"
+proof -
+  have "simple_function M f" using assms by (simp add: simple_function_borel_measurable)
+  moreover have "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" by simp
+  ultimately have "Bochner_Integration.simple_bochner_integrable M f"
+    using Bochner_Integration.simple_bochner_integrable.simps by blast
+  hence "has_bochner_integral M f (Bochner_Integration.simple_bochner_integral M f)"
+    using has_bochner_integral_simple_bochner_integrable by auto
+  thus ?thesis using integrable.simps by auto
+qed
+
 subsection  \<open>Introduce binder for probability\<close>
 
 syntax
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -1482,6 +1482,9 @@
   then show "linear f" by (intro linearI) auto
 qed
 
+lemma linear_of_real [simp]: "linear of_real"
+  by (simp add: linear_iff scaleR_conv_of_real)
+
 lemmas linear_scaleR_left = linear_scale_left
 lemmas linear_imp_scaleR = linear_imp_scale
 
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -535,6 +535,10 @@
   "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"
   by (simp add: eventually_nhds eventually_at_filter)
 
+lemma eventually_nhds_conv_at:
+  "eventually P (nhds x) \<longleftrightarrow> eventually P (at x) \<and> P x"
+  unfolding eventually_at_topological eventually_nhds by fast
+
 lemma eventually_at_in_open:
   assumes "open A" "x \<in> A"
   shows   "eventually (\<lambda>y. y \<in> A - {x}) (at x)"
diff -r 67d28b35c5d8 -r ca004ccf2352 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Mar 20 21:12:49 2024 +0100
+++ b/src/HOL/Transcendental.thy	Thu Mar 21 14:19:39 2024 +0000
@@ -1760,6 +1760,9 @@
   for x :: real
   by (simp add: linorder_not_less [symmetric])
 
+lemma ln_mono: "\<And>x::real. \<lbrakk>x \<le> y; 0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y"
+  using ln_le_cancel_iff by presburger
+
 lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
   for x :: real
   by (simp add: order_eq_iff)