# HG changeset patch
# User paulson
# Date 1677846127 0
# Node ID fd9422c110ed0565a3718bdd815c48ec511fe8a5
# Parent  8a28ab58d155e20b46bc55dab0c3e0b9ff0f5a9b# Parent  9d431c939a7fff11ebafd032827f832caf47d4f2
merged

diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Convex.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -2369,9 +2369,6 @@
     using hull_inc u by fastforce
 qed
 
-lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> (\<Sum>Basis) \<bullet> i = 1"
-  by (simp add: inner_sum_left sum.If_cases inner_Basis)
-
 lemma convex_set_plus:
   assumes "convex S" and "convex T" shows "convex (S + T)"
 proof -
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -895,6 +895,17 @@
     by (rule bounded_subset)
 qed
 
+lemma continuous_on_compact_bound:
+  assumes "compact A" "continuous_on A f"
+  obtains B where "B \<ge> 0" "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B"
+proof -
+  have "compact (f ` A)" by (metis assms compact_continuous_image)
+  then obtain B where "\<forall>x\<in>A. norm (f x) \<le> B"
+    by (auto dest!: compact_imp_bounded simp: bounded_iff)
+  hence "max B 0 \<ge> 0" and "\<forall>x\<in>A. norm (f x) \<le> max B 0" by auto
+  thus ?thesis using that by blast
+qed
+
 lemma closure_Int_ball_not_empty:
   assumes "S \<subseteq> closure T" "x \<in> S" "r > 0"
   shows "T \<inter> ball x r \<noteq> {}"
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -53,6 +53,9 @@
 lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
   unfolding sgn_div_norm by (simp add: scaleR_one)
 
+lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> inner (\<Sum>Basis) i = 1"
+  by (simp add: inner_sum_left sum.If_cases inner_Basis)
+
 lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
 proof
   assume "0 \<in> Basis" thus "False"
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -12,8 +12,7 @@
 
 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
   \<Longrightarrow> norm(y-x) \<le> e"
-  using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
-  by (simp add: add_diff_add)
+  by (smt (verit, ccfv_SIG) norm_diff_triangle_ineq)
 
 lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
   by auto
@@ -2326,11 +2325,9 @@
 qed
 
 lemma has_integral_spike_eq:
-  assumes "negligible S"
-    and gf: "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+  assumes "negligible S" and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
   shows "(f has_integral y) T \<longleftrightarrow> (g has_integral y) T"
-    using has_integral_spike [OF \<open>negligible S\<close>] gf
-    by metis
+  by (metis assms has_integral_spike)
 
 lemma integrable_spike:
   assumes "f integrable_on T" "negligible S" "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
@@ -4878,13 +4875,22 @@
 
 lemma integrable_on_superset:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on S"
-    and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0"
-    and "S \<subseteq> t"
+  assumes "f integrable_on S" and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0" and "S \<subseteq> t"
   shows "f integrable_on t"
-  using assms
-  unfolding integrable_on_def
-  by (auto intro:has_integral_on_superset)
+  by (meson assms has_integral_on_superset integrable_integral integrable_on_def)
+
+lemma integral_subset_negligible:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+  assumes "S \<subseteq> T" "negligible (T - S)"
+  shows   "integral S f = integral T f"
+proof -
+  have "integral T f = integral T (\<lambda>x. if x \<in> S then f x else 0)"
+    by (rule integral_spike[of "T - S"]) (use assms in auto)
+  also have "\<dots> = integral (S \<inter> T) f"
+    by (subst integral_restrict_Int) auto
+  also have "S \<inter> T = S" using assms by auto
+  finally show ?thesis ..
+qed
 
 lemma integral_restrict_UNIV:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -840,6 +840,76 @@
     by (metis assms continuous_on_compose continuous_on_swap swap_cbox_Pair)
 qed
 
+lemma open_contains_cbox:
+  fixes x :: "'a :: euclidean_space"
+  assumes "open A" "x \<in> A"
+  obtains a b where "cbox a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+proof -
+  from assms obtain R where R: "R > 0" "ball x R \<subseteq> A"
+    by (auto simp: open_contains_ball)
+  define r :: real where "r = R / (2 * sqrt DIM('a))"
+  from \<open>R > 0\<close> have [simp]: "r > 0" by (auto simp: r_def)
+  define d :: 'a where "d = r *\<^sub>R Topology_Euclidean_Space.One"
+  have "cbox (x - d) (x + d) \<subseteq> A"
+  proof safe
+    fix y assume y: "y \<in> cbox (x - d) (x + d)"
+    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
+      by (subst euclidean_dist_l2) (auto simp: L2_set_def)
+    also from y have "sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2) \<le> sqrt (\<Sum>i\<in>(Basis::'a set). r\<^sup>2)"
+      by (intro real_sqrt_le_mono sum_mono power_mono)
+         (auto simp: dist_norm d_def cbox_def algebra_simps)
+    also have "\<dots> = sqrt (DIM('a) * r\<^sup>2)" by simp
+    also have "DIM('a) * r\<^sup>2 = (R / 2) ^ 2"
+      by (simp add: r_def power_divide)
+    also have "sqrt \<dots> = R / 2"
+      using \<open>R > 0\<close> by simp
+    also from \<open>R > 0\<close> have "\<dots> < R" by simp
+    finally have "y \<in> ball x R" by simp
+    with R show "y \<in> A" by blast
+  qed
+  thus ?thesis
+    using that[of "x - d" "x + d"] by (auto simp: algebra_simps d_def box_def)
+qed
+
+lemma open_contains_box:
+  fixes x :: "'a :: euclidean_space"
+  assumes "open A" "x \<in> A"
+  obtains a b where "box a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+  by (meson assms box_subset_cbox dual_order.trans open_contains_cbox)
+
+lemma inner_image_box:
+  assumes "(i :: 'a :: euclidean_space) \<in> Basis"
+  assumes "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+  shows   "(\<lambda>x. x \<bullet> i) ` box a b = {a \<bullet> i<..<b \<bullet> i}"
+proof safe
+  fix x assume x: "x \<in> {a \<bullet> i<..<b \<bullet> i}"
+  let ?y = "(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j)"
+  from x assms have "?y \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` box a b"
+    by (intro imageI) (auto simp: box_def algebra_simps)
+  also have "?y \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i))"
+    by (simp add: inner_sum_left)
+  also have "\<dots> = (\<Sum>j\<in>Basis. if i = j then x else 0)"
+    by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
+  also have "\<dots> = x" using assms by simp
+  finally show "x \<in> (\<lambda>x. x \<bullet> i) ` box a b"  .
+qed (insert assms, auto simp: box_def)
+
+lemma inner_image_cbox:
+  assumes "(i :: 'a :: euclidean_space) \<in> Basis"
+  assumes "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
+  shows   "(\<lambda>x. x \<bullet> i) ` cbox a b = {a \<bullet> i..b \<bullet> i}"
+proof safe
+  fix x assume x: "x \<in> {a \<bullet> i..b \<bullet> i}"
+  let ?y = "(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j)"
+  from x assms have "?y \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` cbox a b"
+    by (intro imageI) (auto simp: cbox_def)
+  also have "?y \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i))"
+    by (simp add: inner_sum_left)
+  also have "\<dots> = (\<Sum>j\<in>Basis. if i = j then x else 0)"
+    by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
+  also have "\<dots> = x" using assms by simp
+  finally show "x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b"  .
+qed (insert assms, auto simp: cbox_def)
 
 subsection \<open>General Intervals\<close>
 
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Archimedean_Field.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -417,33 +417,7 @@
 
 lemma floor_divide_of_nat_eq: "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)"
   for m n :: nat
-proof (cases "n = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0"
-    by (auto intro: floor_unique)
-  have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)"
-    by simp
-  also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
-    using False by (simp only: of_nat_add) (simp add: field_simps)
-  finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
-    by simp
-  then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
-    using False by (simp only:) simp
-  then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>"
-    by simp
-  then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\<rfloor>"
-    by (simp add: ac_simps)
-  moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))"
-    by simp
-  ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> =
-      \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
-    by (simp only: floor_add_int)
-  with * show ?thesis
-    by simp
-qed
+    by (metis floor_divide_of_int_eq of_int_of_nat_eq unique_euclidean_semiring_with_nat_class.of_nat_div)
 
 lemma floor_divide_lower:
   fixes q :: "'a::floor_ceiling"
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Complex_Analysis/Contour_Integration.thy
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -23,7 +23,7 @@
 subsection\<open>Definition\<close>
 
 text\<open>
-  This definition is for complex numbers only, and does not generalise to 
+  This definition is for complex numbers only, and does not generalise to
   line integrals in a vector field
 \<close>
 
@@ -92,6 +92,47 @@
       (\<lambda>t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}"
   by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def)
 
+lemma has_contour_integral_mirror_iff:
+  assumes "valid_path g"
+  shows   "(f has_contour_integral I) (-g) \<longleftrightarrow> ((\<lambda>x. -f (- x)) has_contour_integral I) g"
+proof -
+  from assms have "g piecewise_differentiable_on {0..1}"
+    by (auto simp: valid_path_def piecewise_C1_imp_differentiable)
+  then obtain S where "finite S" and S: "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g differentiable at x within {0..1}"
+     unfolding piecewise_differentiable_on_def by blast
+  have S': "g differentiable at x" if "x \<in> {0..1} - ({0, 1} \<union> S)" for x
+  proof -
+    from that have "x \<in> interior {0..1}" by auto
+    with S[of x] that show ?thesis by (auto simp: at_within_interior[of _ "{0..1}"])
+  qed
+
+  have "(f has_contour_integral I) (-g) \<longleftrightarrow>
+          ((\<lambda>x. f (- g x) * vector_derivative (-g) (at x)) has_integral I) {0..1}"
+    by (simp add: has_contour_integral)
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. -f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}"
+    by (intro has_integral_spike_finite_eq[of "S \<union> {0, 1}"])
+       (insert \<open>finite S\<close> S', auto simp: o_def fun_Compl_def)
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. -f (-x)) has_contour_integral I) g"
+    by (simp add: has_contour_integral)
+  finally show ?thesis .
+qed
+
+lemma contour_integral_on_mirror_iff:
+  assumes "valid_path g"
+  shows   "f contour_integrable_on (-g) \<longleftrightarrow> (\<lambda>x. -f (- x)) contour_integrable_on g"
+  by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff assms)
+
+lemma contour_integral_mirror:
+  assumes "valid_path g"
+  shows   "contour_integral (-g) f = contour_integral g (\<lambda>x. -f (- x))"
+proof (cases "f contour_integrable_on (-g)")
+  case True with contour_integral_unique assms show ?thesis 
+    by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff)
+next
+  case False then show ?thesis
+    by (simp add: assms contour_integral_on_mirror_iff not_integrable_contour_integral)
+qed
+
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path\<close>
 
 lemma has_contour_integral_reversepath:
@@ -170,12 +211,12 @@
           has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]]
     by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac)
   have g1: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
-            2 *\<^sub>R vector_derivative g1 (at (z*2))" 
+            2 *\<^sub>R vector_derivative g1 (at (z*2))"
       if "0 \<le> z" "z*2 < 1" "z*2 \<notin> s1" for z
   proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
     show "0 < \<bar>z - 1/2\<bar>"
       using that by auto
-    have "((*) 2 has_vector_derivative 2) (at z)" 
+    have "((*) 2 has_vector_derivative 2) (at z)"
       by (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
     moreover have "(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))"
       using s1 that by (auto simp: algebra_simps vector_derivative_works)
@@ -185,7 +226,7 @@
   qed (use that in \<open>simp_all add: dist_real_def abs_if split: if_split_asm\<close>)
 
   have g2: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
-            2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" 
+            2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))"
            if "1 < z*2" "z \<le> 1" "z*2 - 1 \<notin> s2" for z
   proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
     show "0 < \<bar>z - 1/2\<bar>"
@@ -234,7 +275,7 @@
   then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
     by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
   have g1: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) =
-            2 *\<^sub>R vector_derivative g1 (at z)" 
+            2 *\<^sub>R vector_derivative g1 (at z)"
     if "0 < z" "z < 1" "z \<notin> s1" for z
   proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
     show "0 < \<bar>(z - 1)/2\<bar>"
@@ -261,14 +302,14 @@
     where s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x"
     using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
   have "(\<lambda>x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}"
-    using assms integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2"] 
+    using assms integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2"]
                 integrable_on_subcbox [where a="1/2" and b=1]
     by (fastforce simp: contour_integrable_on image_affinity_atLeastAtMost_diff)
   then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2)))
                 integrable_on {0..1}"
     by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
   have g2: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
-            2 *\<^sub>R vector_derivative g2 (at z)" 
+            2 *\<^sub>R vector_derivative g2 (at z)"
         if "0 < z" "z < 1" "z \<notin> s2" for z
   proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
     show "0 < \<bar>z/2\<bar>"
@@ -600,6 +641,22 @@
   unfolding contour_integral_integral using assms
   by (intro integral_cong) (auto simp: path_image_def)
 
+lemma contour_integral_spike_finite_simple_path:
+  assumes "finite A" "simple_path g" "g = g'" "\<And>x. x \<in> path_image g - A \<Longrightarrow> f x = f' x"
+  shows   "contour_integral g f = contour_integral g' f'"
+  unfolding contour_integral_integral
+proof (rule integral_spike)
+  have "finite (g -` A \<inter> {0<..<1})" using \<open>simple_path g\<close> \<open>finite A\<close>
+    by (intro finite_vimage_IntI simple_path_inj_on) auto
+  hence "finite ({0, 1} \<union> g -` A \<inter> {0<..<1})" by auto
+  thus "negligible ({0, 1} \<union> g -` A \<inter> {0<..<1})" by (rule negligible_finite)
+next
+  fix x assume "x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1})"
+  hence "g x \<in> path_image g - A" by (auto simp: path_image_def)
+  from assms(4)[OF this] and assms(3)
+    show "f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)" by simp
+  qed
+
 
 text \<open>Contour integral along a segment on the real axis\<close>
 
@@ -619,7 +676,7 @@
   also have "(\<lambda>x. f (a + b * of_real x - a * of_real x)) =
                (\<lambda>x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))"
     using \<open>a \<noteq> b\<close> by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real)
-  also have "(\<dots> has_integral I /\<^sub>R (Re b - Re a)) {0..1} \<longleftrightarrow> 
+  also have "(\<dots> has_integral I /\<^sub>R (Re b - Re a)) {0..1} \<longleftrightarrow>
                ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms
     by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps)
   also have "\<dots> \<longleftrightarrow> (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def
@@ -846,8 +903,7 @@
     "\<lbrakk>f contour_integrable_on (linepath a b);
       0 \<le> B; \<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
      \<Longrightarrow> norm(contour_integral (linepath a b) f) \<le> B*norm(b - a)"
-  using has_contour_integral_bound_linepath [of f]
-  by (auto simp: has_contour_integral_integral)
+  by (meson has_contour_integral_bound_linepath has_contour_integral_integral)
 
 lemma contour_integral_0 [simp]: "contour_integral g (\<lambda>x. 0) = 0"
   by (simp add: contour_integral_unique has_contour_integral_0)
@@ -900,6 +956,10 @@
    unfolding contour_integrable_on_def
    by (metis has_contour_integral_sum)
 
+lemma contour_integrable_neg_iff:
+  "(\<lambda>x. -f x) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+  using contour_integrable_neg[of f g] contour_integrable_neg[of "\<lambda>x. -f x" g] by auto
+
 lemma contour_integrable_lmul_iff:
     "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
   using contour_integrable_lmul[of f g c] contour_integrable_lmul[of "\<lambda>x. c * f x" g "inverse c"]
@@ -952,8 +1012,8 @@
     then have "\<And>x. ((k - x) / k) *\<^sub>R a + (x / k) *\<^sub>R c = (1 - x) *\<^sub>R a + x *\<^sub>R b"
       using False by (simp add: c' algebra_simps)
     then have "((\<lambda>x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral i) {0..k}"
-      using k has_integral_affinity01 [OF *, of "inverse k" "0"] 
-      by (force dest: has_integral_cmul [where c = "inverse k"] 
+      using k has_integral_affinity01 [OF *, of "inverse k" "0"]
+      by (force dest: has_integral_cmul [where c = "inverse k"]
               simp add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost c)
   } note fi = this
   { assume *: "((\<lambda>x. f ((1 - x) *\<^sub>R c + x *\<^sub>R b) * (b - c)) has_integral j) {0..1}"
@@ -1148,9 +1208,9 @@
 
 lemma reversepath_part_circlepath[simp]:
     "reversepath (part_circlepath z r s t) = part_circlepath z r t s"
-  unfolding part_circlepath_def reversepath_def linepath_def 
+  unfolding part_circlepath_def reversepath_def linepath_def
   by (auto simp:algebra_simps)
-    
+
 lemma has_vector_derivative_part_circlepath [derivative_intros]:
     "((part_circlepath z r s t) has_vector_derivative
       (\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
@@ -1209,7 +1269,7 @@
 lemma path_image_part_circlepath':
   "path_image (part_circlepath z r s t) = (\<lambda>x. z + r * cis x) ` closed_segment s t"
 proof -
-  have "path_image (part_circlepath z r s t) = 
+  have "path_image (part_circlepath z r s t) =
           (\<lambda>x. z + r * exp(\<i> * of_real x)) ` linepath s t ` {0..1}"
     by (simp add: image_image path_image_def part_circlepath_def)
   also have "linepath s t ` {0..1} = closed_segment s t"
@@ -1283,7 +1343,7 @@
        (simp_all add: cis_conv_exp)
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (c + r * exp (\<i> * linepath (of_real a) (of_real b) x)) *
                        r * \<i> * exp (\<i> * linepath (of_real a) (of_real b) x) *
-                       vector_derivative (linepath (of_real a) (of_real b)) 
+                       vector_derivative (linepath (of_real a) (of_real b))
                          (at x within {0..1})) has_integral I) {0..1}"
     by (intro has_integral_cong, subst vector_derivative_linepath_within)
        (auto simp: part_circlepath_def cis_conv_exp of_real_linepath [symmetric])
@@ -1299,7 +1359,7 @@
   assumes "a < b"
   shows "f contour_integrable_on (part_circlepath c r a b) \<longleftrightarrow>
            (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
-  using assms by (auto simp: contour_integrable_on_def integrable_on_def 
+  using assms by (auto simp: contour_integrable_on_def integrable_on_def
                              has_contour_integral_part_circlepath_iff)
 
 lemma contour_integral_part_circlepath_eq:
@@ -1308,14 +1368,14 @@
            integral {a..b} (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t)"
 proof (cases "f contour_integrable_on part_circlepath c r a b")
   case True
-  hence "(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}" 
+  hence "(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
     using assms by (simp add: contour_integrable_part_circlepath_iff)
   with True show ?thesis
     using has_contour_integral_part_circlepath_iff[OF assms]
           contour_integral_unique has_integral_integrable_integral by blast
 next
   case False
-  hence "\<not>(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}" 
+  hence "\<not>(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
     using assms by (simp add: contour_integrable_part_circlepath_iff)
   with False show ?thesis
     by (simp add: not_integrable_contour_integral not_integrable_integral)
@@ -1323,10 +1383,10 @@
 
 lemma contour_integral_part_circlepath_reverse:
   "contour_integral (part_circlepath c r a b) f = -contour_integral (part_circlepath c r b a) f"
-  by (subst reversepath_part_circlepath [symmetric], subst contour_integral_reversepath) simp_all
+  by (metis contour_integral_reversepath reversepath_part_circlepath valid_path_part_circlepath)
 
 lemma contour_integral_part_circlepath_reverse':
-  "b < a \<Longrightarrow> contour_integral (part_circlepath c r a b) f = 
+  "b < a \<Longrightarrow> contour_integral (part_circlepath c r a b) f =
                -contour_integral (part_circlepath c r b a) f"
   by (rule contour_integral_part_circlepath_reverse)
 
@@ -1382,7 +1442,7 @@
     proof -
       let ?w = "(y - z)/of_real r / exp(\<i> * of_real s)"
       have fin: "finite (of_real -` {z. cmod z \<le> 1 \<and> exp (\<i> * complex_of_real (t - s) * z) = ?w})"
-        using \<open>s < t\<close> 
+        using \<open>s < t\<close>
         by (intro finite_vimageI [OF finite_bounded_log2]) (auto simp: inj_of_real)
       show ?thesis
         unfolding part_circlepath_def linepath_def vimage_def
@@ -1396,13 +1456,20 @@
                        vector_derivative (part_circlepath z r s t) (at x)) has_integral i)  {0..1}"
       by (rule has_integral_spike [OF negligible_finite [OF fin01]])  (use fi has_contour_integral in auto)
     have *: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1; part_circlepath z r s t x \<notin> k\<rbrakk> \<Longrightarrow> cmod (f (part_circlepath z r s t x)) \<le> B"
-      by (auto intro!: B [unfolded path_image_def image_def, simplified])
+      by (auto intro!: B [unfolded path_image_def image_def])
     show ?thesis
       apply (rule has_integral_bound [where 'a=real, simplified, OF _ **, simplified])
       using assms le * "2" \<open>r > 0\<close> by (auto simp add: norm_mult vector_derivative_part_circlepath)
   qed
 qed
 
+corollary contour_integral_bound_part_circlepath_strong:
+  assumes "f contour_integrable_on part_circlepath z r s t"
+      and "finite k" and "0 \<le> B" "0 < r" "s \<le> t"
+      and "\<And>x. x \<in> path_image(part_circlepath z r s t) - k \<Longrightarrow> norm(f x) \<le> B"
+    shows "cmod (contour_integral (part_circlepath z r s t) f) \<le> B * r * (t - s)"
+  using assms has_contour_integral_bound_part_circlepath_strong has_contour_integral_integral by blast
+
 lemma has_contour_integral_bound_part_circlepath:
       "\<lbrakk>(f has_contour_integral i) (part_circlepath z r s t);
         0 \<le> B; 0 < r; s \<le> t;
@@ -1414,9 +1481,8 @@
      "continuous_on (path_image (part_circlepath z r s t)) f
       \<Longrightarrow> f contour_integrable_on (part_circlepath z r s t)"
   unfolding contour_integrable_on has_contour_integral_def vector_derivative_part_circlepath path_image_def
-  apply (rule integrable_continuous_real)
-  apply (fast intro: path_part_circlepath [unfolded path_def] continuous_intros continuous_on_compose2 [where g=f, OF _ _ order_refl])
-  done
+  by (best intro: integrable_continuous_real path_part_circlepath [unfolded path_def] continuous_intros 
+      continuous_on_compose2 [where g=f, OF _ _ order_refl])
 
 lemma simple_path_part_circlepath:
     "simple_path(part_circlepath z r s t) \<longleftrightarrow> (r \<noteq> 0 \<and> s \<noteq> t \<and> \<bar>s - t\<bar> \<le> 2*pi)"
@@ -1686,7 +1752,7 @@
       then show ?thesis
         by (simp add: left_diff_distrib [symmetric] norm_mult)
     qed
-    have le_e: "\<And>x. \<lbrakk>\<forall>xa\<in>{0..1}. 2 * cmod (f x (\<gamma> xa) - l (\<gamma> xa)) < e / B'; f x contour_integrable_on \<gamma>\<rbrakk>
+    have le_e: "\<And>x. \<lbrakk>\<forall>u\<in>{0..1}. 2 * cmod (f x (\<gamma> u) - l (\<gamma> u)) < e / B'; f x contour_integrable_on \<gamma>\<rbrakk>
          \<Longrightarrow> cmod (integral {0..1}
                     (\<lambda>u. f x (\<gamma> u) * vector_derivative \<gamma> (at u) - l (\<gamma> u) * vector_derivative \<gamma> (at u))) < e"
       apply (rule le_less_trans [OF integral_norm_bound_integral ie])
@@ -1711,4 +1777,4 @@
           "((\<lambda>n. contour_integral (circlepath z r) (f n)) \<longlongrightarrow> contour_integral (circlepath z r) l) F"
   using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)
 
-end
\ No newline at end of file
+end
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -1499,6 +1499,21 @@
   shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
   using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
 
+lemma le_imp_bigo_real:
+  assumes "c \<ge> 0" "eventually (\<lambda>x. f x \<le> c * (g x :: real)) F" "eventually (\<lambda>x. 0 \<le> f x) F"
+  shows   "f \<in> O[F](g)"
+proof -
+  have "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
+    using assms(2,3)
+  proof eventually_elim
+    case (elim x)
+    have "norm (f x) \<le> c * g x" using elim by simp
+    also have "\<dots> \<le> c * norm (g x)" by (intro mult_left_mono assms) auto
+    finally show ?case .
+  qed
+  thus ?thesis by (intro bigoI[of _ c]) auto
+qed
+
 context landau_symbol
 begin
 
@@ -2052,6 +2067,17 @@
   shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
   using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
 
+lemma asymp_equivD_strong:
+  assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<noteq> 0 \<or> g x \<noteq> 0) F"
+  shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
+proof -
+  from assms(1) have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
+    by (rule asymp_equivD)
+  also have "?this \<longleftrightarrow> ?thesis"
+    by (intro filterlim_cong eventually_mono[OF assms(2)]) auto
+  finally show ?thesis .
+qed
+
 lemma asymp_equiv_compose [asymp_equiv_intros]:
   assumes "f \<sim>[G] g" "filterlim h G F"
   shows   "f \<circ> h \<sim>[F] g \<circ> h"
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Real.thy
--- a/src/HOL/Real.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Real.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -1067,11 +1067,7 @@
   by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq)
 
 lemma real_of_nat_div3: "real n / real x - real (n div x) \<le> 1" for n x :: nat
-proof (cases "x = 0")
-  case False
-  then show ?thesis
-    by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int)
-qed auto
+  by (metis of_int_of_nat_eq real_of_int_div3 of_nat_div)
 
 lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat
   using real_of_nat_div2 [of n x] by simp
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Series.thy
--- a/src/HOL/Series.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Series.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -1023,6 +1023,17 @@
   for f :: "nat \<Rightarrow> real"
   by (fold real_norm_def) (rule summable_norm)
 
+lemma norm_suminf_le:
+  assumes "\<And>n. norm (f n :: 'a :: banach) \<le> g n" "summable g"
+  shows   "norm (suminf f) \<le> suminf g"
+proof -
+  have *: "summable (\<lambda>n. norm (f n))" 
+    using assms summable_norm_comparison_test by blast
+  hence "norm (suminf f) \<le> (\<Sum>n. norm (f n))" by (intro summable_norm) auto
+  also have "\<dots> \<le> suminf g" by (intro suminf_le * assms allI)
+  finally show ?thesis .
+qed
+
 lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a::{comm_ring_1,topological_space})"
 proof -
   have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)"
@@ -1054,12 +1065,7 @@
 qed
 
 lemma summable_0_powser: "summable (\<lambda>n. f n * 0 ^ n :: 'a::real_normed_div_algebra)"
-proof -
-  have A: "(\<lambda>n. f n * 0 ^ n) = (\<lambda>n. if n = 0 then f n else 0)"
-    by (intro ext) auto
-  then show ?thesis
-    by (subst A) simp_all
-qed
+  by simp
 
 lemma summable_powser_split_head:
   "summable (\<lambda>n. f (Suc n) * z ^ n :: 'a::real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)"
diff -r 8a28ab58d155 -r fd9422c110ed src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Transcendental.thy	Fri Mar 03 12:22:07 2023 +0000
@@ -2492,6 +2492,9 @@
       for a x :: "'a::{ln,real_normed_field}"
   by (simp add: divide_inverse powr_minus)
 
+lemma powr_sum: "x \<noteq> 0 \<Longrightarrow> finite A \<Longrightarrow> x powr sum f A = (\<Prod>y\<in>A. x powr f y)"
+  by (simp add: powr_def exp_sum sum_distrib_right)
+
 lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
   for a b c :: real
   by (simp add: powr_minus_divide)