# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1743781078 -3600
# Node ID 24d09a911713f1678ee252b94989ae1772e61596
# Parent  918c50e0447e9eafbe1fdf7f1832808d3a5ad100
Inserted more of Manuel Eberl's material

diff -r 918c50e0447e -r 24d09a911713 src/HOL/Analysis/FPS_Convergence.thy
--- 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>
 
diff -r 918c50e0447e -r 24d09a911713 src/HOL/Analysis/Path_Connected.thy
--- 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"
diff -r 918c50e0447e -r 24d09a911713 src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy
--- 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])
diff -r 918c50e0447e -r 24d09a911713 src/HOL/Complex_Analysis/Contour_Integration.thy
--- 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}))