--- a/src/HOL/Analysis/FPS_Convergence.thy Thu Apr 03 21:08:36 2025 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Fri Apr 04 16:37:58 2025 +0100
@@ -10,7 +10,9 @@
theory FPS_Convergence
imports
Generalised_Binomial_Theorem
- "HOL-Computational_Algebra.Formal_Power_Series"
+ "HOL-Computational_Algebra.Formal_Power_Series"
+ "HOL-Computational_Algebra.Polynomial_FPS"
+
begin
text \<open>
@@ -593,6 +595,52 @@
that is available.
\<close>
+subsection \<open>FPS of a polynomial\<close>
+
+lemma fps_conv_radius_fps_of_poly [simp]:
+ fixes p :: "'a :: {banach, real_normed_div_algebra} poly"
+ shows "fps_conv_radius (fps_of_poly p) = \<infinity>"
+proof -
+ have "conv_radius (poly.coeff p) = conv_radius (\<lambda>_. 0 :: 'a)"
+ using MOST_coeff_eq_0 unfolding cofinite_eq_sequentially by (rule conv_radius_cong')
+ also have "\<dots> = \<infinity>"
+ by simp
+ finally show ?thesis
+ by (simp add: fps_conv_radius_def)
+qed
+
+lemma eval_fps_power:
+ fixes F :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
+ assumes z: "norm z < fps_conv_radius F"
+ shows "eval_fps (F ^ n) z = eval_fps F z ^ n"
+proof (induction n)
+ case 0
+ thus ?case
+ by (auto simp: eval_fps_mult)
+next
+ case (Suc n)
+ have "eval_fps (F ^ Suc n) z = eval_fps (F * F ^ n) z"
+ by simp
+ also from z have "\<dots> = eval_fps F z * eval_fps (F ^ n) z"
+ by (subst eval_fps_mult) (auto intro!: less_le_trans[OF _ fps_conv_radius_power])
+ finally show ?case
+ using Suc.IH by simp
+qed
+
+lemma eval_fps_of_poly [simp]: "eval_fps (fps_of_poly p) z = poly p z"
+proof -
+ have "(\<lambda>n. poly.coeff p n * z ^ n) sums poly p z"
+ unfolding poly_altdef by (rule sums_finite) (auto simp: coeff_eq_0)
+ moreover have "(\<lambda>n. poly.coeff p n * z ^ n) sums eval_fps (fps_of_poly p) z"
+ using sums_eval_fps[of z "fps_of_poly p"] by simp
+ ultimately show ?thesis
+ using sums_unique2 by blast
+qed
+
+lemma poly_holomorphic_on [holomorphic_intros]:
+ assumes [holomorphic_intros]: "f holomorphic_on A"
+ shows "(\<lambda>z. poly p (f z)) holomorphic_on A"
+ unfolding poly_altdef by (intro holomorphic_intros)
subsection \<open>Power series expansions of analytic functions\<close>
--- a/src/HOL/Analysis/Path_Connected.thy Thu Apr 03 21:08:36 2025 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Apr 04 16:37:58 2025 +0100
@@ -1266,6 +1266,46 @@
lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0"
by (simp add: linepath_def)
+lemma
+ assumes "x \<in> closed_segment y z"
+ shows in_closed_segment_imp_Re_in_closed_segment: "Re x \<in> closed_segment (Re y) (Re z)" (is ?th1)
+ and in_closed_segment_imp_Im_in_closed_segment: "Im x \<in> closed_segment (Im y) (Im z)" (is ?th2)
+proof -
+ from assms obtain t where t: "t \<in> {0..1}" "x = linepath y z t"
+ by (metis imageE linepath_image_01)
+ have "Re x = linepath (Re y) (Re z) t" "Im x = linepath (Im y) (Im z) t"
+ by (simp_all add: t Re_linepath' Im_linepath')
+ with t(1) show ?th1 ?th2
+ using linepath_in_path[of t "Re y" "Re z"] linepath_in_path[of t "Im y" "Im z"] by simp_all
+qed
+
+lemma linepath_in_open_segment: "t \<in> {0<..<1} \<Longrightarrow> x \<noteq> y \<Longrightarrow> linepath x y t \<in> open_segment x y"
+ unfolding greaterThanLessThan_iff by (metis in_segment(2) linepath_def)
+
+lemma in_open_segment_imp_Re_in_open_segment:
+ assumes "x \<in> open_segment y z" "Re y \<noteq> Re z"
+ shows "Re x \<in> open_segment (Re y) (Re z)"
+proof -
+ from assms obtain t where t: "t \<in> {0<..<1}" "x = linepath y z t"
+ by (metis greaterThanLessThan_iff in_segment(2) linepath_def)
+ have "Re x = linepath (Re y) (Re z) t"
+ by (simp_all add: t Re_linepath')
+ with t(1) show ?thesis
+ using linepath_in_open_segment[of t "Re y" "Re z"] assms by auto
+qed
+
+lemma in_open_segment_imp_Im_in_open_segment:
+ assumes "x \<in> open_segment y z" "Im y \<noteq> Im z"
+ shows "Im x \<in> open_segment (Im y) (Im z)"
+proof -
+ from assms obtain t where t: "t \<in> {0<..<1}" "x = linepath y z t"
+ by (metis greaterThanLessThan_iff in_segment(2) linepath_def)
+ have "Im x = linepath (Im y) (Im z) t"
+ by (simp_all add: t Im_linepath')
+ with t(1) show ?thesis
+ using linepath_in_open_segment[of t "Im y" "Im z"] assms by auto
+qed
+
lemma bounded_linear_linepath:
assumes "bounded_linear f"
shows "f (linepath a b x) = linepath (f a) (f b) x"
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Thu Apr 03 21:08:36 2025 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Fri Apr 04 16:37:58 2025 +0100
@@ -620,7 +620,7 @@
have **: "\<And>f' x' f x::complex. f'*x' - f*x = f' * (x' - x) + x * (f' - f)"
by (simp add: algebra_simps)
have "norm (pathint (shrink u) (shrink v) - pathint u v)
- \<le> (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))"
+ \<le> (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * measure lborel (cbox 0 (1::real))"
apply (rule has_integral_bound
[of _ "\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
_ 0 1])
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy Thu Apr 03 21:08:36 2025 +0100
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Fri Apr 04 16:37:58 2025 +0100
@@ -808,7 +808,7 @@
"0 \<le> B" and B: "\<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B"
shows "norm i \<le> B * norm(b - a)"
proof -
- have "norm i \<le> (B * norm (b - a)) * content (cbox 0 (1::real))"
+ have "norm i \<le> (B * norm (b - a)) * measure lborel (cbox 0 (1::real))"
proof (rule has_integral_bound
[of _ "\<lambda>x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"])
show "cmod (f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1}))