--- 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 -
--- 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
--- 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:
--- 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" .
--- 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>
--- 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"
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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)"
--- 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)