(* File: Newman_Ingham_Tauberian.thy Author: Manuel Eberl (TU München) A proof of Newman's "analytic theorem", originally stated by Ingham *) section ‹Ingham's Tauberian Theorem› theory Newman_Ingham_Tauberian imports "HOL-Real_Asymp.Real_Asymp" Prime_Number_Theorem_Library begin text ‹ In his proof of the Prime Number Theorem, Newman~\<^cite>‹"newman1998analytic"› uses a Tauberian theorem that was first proven by Ingham. Newman gives a nice and straightforward proof of this theorem based on contour integration. This section will be concerned with proving this theorem. This Tauberian theorem is probably the part of the Newman's proof of the Prime Number Theorem where most of the ``heavy lifting'' is done. Its purpose is to extend the summability of a Dirichlet series with bounded coefficients from the region $\mathfrak{R}(s)>1$ to $\mathfrak{R}(s)\geq 1$. In order to show it, we first require a number of auxiliary bounding lemmas. › lemma newman_ingham_aux1: fixes R :: real and z :: complex assumes R: "R > 0" and z : "norm z = R" shows "norm (1 / z + z / R⇧^{2}) = 2 * ¦Re z¦ / R⇧^{2}" proof - from z and R have [simp]: "z ≠ 0" by auto have "1 / z + z / R⇧^{2}= (R⇧^{2}+ z⇧^{2}) * (1 / R⇧^{2}/ z)" using R by (simp add: field_simps power2_eq_square) also have "norm … = norm (R⇧^{2}+ z⇧^{2}) / R ^ 3" by (simp add: numeral_3_eq_3 z norm_divide norm_mult power2_eq_square) also have "R⇧^{2}+ z⇧^{2}= z * (z + cnj z)" using complex_norm_square[of z] by (simp add: z power2_eq_square algebra_simps) also have "norm … = 2 * ¦Re z¦ * R" by (subst complex_add_cnj) (simp_all add: z norm_mult) also have "… / R ^ 3 = 2 * ¦Re z¦ / R⇧^{2}" using R by (simp add: field_simps numeral_3_eq_3 power2_eq_square) finally show ?thesis . qed lemma newman_ingham_aux2: fixes m :: nat and w z :: complex assumes "1 ≤ m" "1 ≤ Re w" "0 < Re z" and f: "⋀n. 1 ≤ n ⟹ norm (f n) ≤ C" shows "norm (∑n=1..m. f n / n powr (w - z)) ≤ C * (m powr Re z) * (1 / m + 1 / Re z)" proof - have [simp]: "C ≥ 0" by (rule order.trans[OF _ f[of 1]]) auto have "norm (∑n=1..m. f n / n powr (w - z)) ≤ (∑n=1..m. C / n powr (1 - Re z))" by (rule sum_norm_le) (insert assms, auto simp: norm_divide norm_powr_real_powr intro!: frac_le assms powr_mono) also have "… = C * (∑n=1..m. n powr (Re z - 1))" by (subst sum_distrib_left) (simp_all add: powr_diff) also have "… ≤ C * (m powr Re z * (1 / Re z + 1 / m))" using zeta_partial_sum_le'[of "Re z" m] assms by (intro mult_left_mono) auto finally show ?thesis by (simp add: mult_ac add_ac) qed lemma hurwitz_zeta_real_bound_aux: fixes a x :: real assumes ax: "a > 0" "x > 1" shows "(∑i. (a + real (Suc i)) powr (-x)) ≤ a powr (1 - x) / (x - 1)" proof (rule decreasing_sum_le_integral, goal_cases) have "((λt. (a + t) powr -x) has_integral -(a powr (-x + 1)) / (-x + 1)) (interior {0..})" using powr_has_integral_at_top[of 0 a "-x"] using ax by (simp add: interior_real_atLeast) also have "-(a powr (- x + 1)) / (- x + 1) = a powr (1 - x) / (x - 1)" using ax by (simp add: field_simps) finally show "((λt. (a + t) powr -x) has_integral a powr (1 - x) / (x - 1)) {0..}" by (subst (asm) has_integral_interior) auto qed (insert ax, auto intro!: powr_mono2') text ‹ Given a function that is analytic on some vertical line segment, we can find a rectangle around that line segment on which the function is also analytic. › lemma analytic_on_axis_extend: fixes y1 y2 x :: real defines "S ≡ {z. Re z = x ∧ Im z ∈ {y1..y2}}" assumes "y1 ≤ y2" assumes "f analytic_on S" obtains x1 x2 :: real where "x1 < x" "x2 > x" "f analytic_on cbox (Complex x1 y1) (Complex x2 y2)" proof - define C where "C = {box a b |a b z. f analytic_on box a b ∧ z ∈ box a b ∧ z ∈ S}" have "S = cbox (Complex x y1) (Complex x y2)" by (auto simp: S_def in_cbox_complex_iff) also have "compact …" by simp finally have 1: "compact S" . have 2: "S ⊆ ⋃C" proof (intro subsetI) fix z assume "z ∈ S" from ‹f analytic_on S› and this obtain a b where "z ∈ box a b" "f analytic_on box a b" by (blast elim: analytic_onE_box) with ‹z ∈ S› show "z ∈ ⋃C" unfolding C_def by blast qed have 3: "open X" if "X ∈ C" for X using that by (auto simp: C_def) from compactE[OF 1 2 3] obtain T where T: "T ⊆ C" "finite T" "S ⊆ ⋃T" by blast define x1 where "x1 = Max (insert (x - 1) ((λX. x + (Inf (Re ` X) - x) / 2) ` T))" define x2 where "x2 = Min (insert (x + 1) ((λX. x + (Sup (Re ` X) - x) / 2) ` T))" have *: "x + (Inf (Re ` X) - x) / 2 < x ∧ x + (Sup (Re ` X) - x) / 2 > x" if "X ∈ T" for X proof - from that and T obtain a b s where [simp]: "X = box a b" and s: "s ∈ box a b" "s ∈ S" by (force simp: C_def) hence le: "Re a < Re b" "Im a < Im b" by (auto simp: in_box_complex_iff) show ?thesis using le s unfolding ‹X = box a b› Re_image_box[OF le] Im_image_box[OF le] by (auto simp: S_def in_box_complex_iff) qed from * T have "x1 < x" unfolding x1_def by (subst Max_less_iff) auto from * T have "x2 > x" unfolding x2_def by (subst Min_gr_iff) auto have "f analytic_on (⋃T)" using T by (subst analytic_on_Union) (auto simp: C_def) moreover have "z ∈ ⋃T" if "z ∈ cbox (Complex x1 y1) (Complex x2 y2)" for z proof - from that have "Complex x (Im z) ∈ S" by (auto simp: in_cbox_complex_iff S_def) with T obtain X where X: "X ∈ T" "Complex x (Im z) ∈ X" by auto with T obtain a b where [simp]: "X = box a b" by (auto simp: C_def) from X have le: "Re a < Re b" "Im a < Im b" by (auto simp: in_box_complex_iff) from that have "Re z ≤ x2" by (simp add: in_cbox_complex_iff) also have "… ≤ x + (Sup (Re ` X) - x) / 2" unfolding x2_def by (rule Min.coboundedI)(use T X in auto) also have "… = (x + Re b) / 2" using le unfolding ‹X = box a b› Re_image_box[OF le] by (simp add: field_simps) also have "… < (Re b + Re b) / 2" using X by (intro divide_strict_right_mono add_strict_right_mono) (auto simp: in_box_complex_iff) also have "… = Re b" by simp finally have [simp]: "Re z < Re b" . have "Re a = (Re a + Re a) / 2" by simp also have "… < (x + Re a) / 2" using X by (intro divide_strict_right_mono add_strict_right_mono) (auto simp: in_box_complex_iff) also have "… = x + (Inf (Re ` X) - x) / 2" using le unfolding ‹X = box a b› Re_image_box[OF le] by (simp add: field_simps) also have "… ≤ x1" unfolding x1_def by (rule Max.coboundedI)(use T X in auto) also have "… ≤ Re z" using that by (simp add: in_cbox_complex_iff) finally have [simp]: "Re z > Re a" . from X have "z ∈ X" by (simp add: in_box_complex_iff) with T X show ?thesis by blast qed hence "cbox (Complex x1 y1) (Complex x2 y2) ⊆ ⋃T" by blast ultimately have "f analytic_on cbox (Complex x1 y1) (Complex x2 y2)" by (rule analytic_on_subset) with ‹x1 < x› and ‹x2 > x› and that[of x1 x2] show ?thesis by blast qed text ‹ We will now prove the theorem. The precise setting is this: Consider a Dirichlet series $F(s) = \sum a_n n^{-s}$ with bounded coefficients. Clearly, this converges to an analytic function $f(s)$ on $\{s\mid \mathfrak R(s)>1\}$. If $f(s)$ is analytic on the larger set $\{s\mid \mathfrak R(s)\geq 1\}$, $F$ converges to $f(s)$ for all $\mathfrak R(s) \geq 1$. The proof follows Newman's argument very closely, but some of the precise bounds we use are a bit different from his. Also, like Harrison, we choose a combination of a semicircle and a rectangle as our contour, whereas Newman uses a circle with a vertical cut-off. The result of the Residue theorem is the same in both cases, but the bounding of the contributions of the different parts is somewhat different. The reason why we picked Harrison's contour over Newman's is because we could not understand how his bounding of the different contributions fits to his contour, and it seems likely that this is also the reason why Harrison altered the contour in the first place. › lemma Newman_Ingham_1: fixes F :: "complex fds" and f :: "complex ⇒ complex" assumes coeff_bound: "fds_nth F ∈ O(λ_. 1)" assumes f_analytic: "f analytic_on {s. Re s ≥ 1}" assumes F_conv_f: "⋀s. Re s > 1 ⟹ eval_fds F s = f s" assumes w: "Re w ≥ 1" shows "fds_converges F w" and "eval_fds F w = f w" proof - ― ‹We get a bound on our coefficients and call it ‹C›.› obtain C where C: "C ≥ 1" "⋀n. norm (fds_nth F n) ≤ C" using natfun_bigo_1E[OF coeff_bound, where lb = 1] by blast write contour_integral ("∮[_]") ― ‹We show convergence directly by showing that the difference between the partial sums and the limit vanishes.› have "(λN. eval_fds (fds_truncate N F) w) ⇢ f w" unfolding tendsto_iff dist_norm norm_minus_commute[of "eval_fds F s" for F s] proof safe fix ε :: real assume ε: "ε > 0" ― ‹We choose an integration radius that is big enough for the error to be sufficiently small.› define R where "R = max 1 (3 * C / ε)" have R: "R ≥ 3 * C / ε" "R ≥ 1" by (auto simp: R_def) ― ‹Next, we extend the analyticity of ‹f (w + z)› to the left of the complex plane within a thin rectangle that is at least as high as the circle.› obtain l where l: "l > 0" "(λz. f (w + z)) analytic_on {s. Re s > 0 ∨ Im s ∈ {-R-1<..<R+1} ∧ Re s > -l}" proof - have f_analytic': "(λz. f (w + z)) analytic_on {s. Re s ≥ 0}" by (rule analytic_on_compose_gen[OF _ f_analytic, unfolded o_def]) (insert w, auto intro: analytic_intros) hence "(λz. f (w + z)) analytic_on {s. Re s = 0 ∧ Im s ∈ {-R-1..R+1}}" by (rule analytic_on_subset) auto from analytic_on_axis_extend[OF _ this] obtain x1 x2 where x12: "x1 < 0" "x2 > 0" "(λz. f (w + z)) analytic_on cbox (Complex x1 (-R-1)) (Complex x2 (R+1))" using ‹R ≥ 1› by auto from this(3) have "(λz. f (w + z)) analytic_on {s. Re s ∈ {x1..0} ∧ Im s ∈ {-R-1..R+1}}" by (rule analytic_on_subset) (insert x12, auto simp: in_cbox_complex_iff) with f_analytic' have "(λz. f (w + z)) analytic_on ({s. Re s ≥ 0} ∪ {s. Re s ∈ {x1..0} ∧ Im s ∈ {-R-1..R+1}})" by (subst analytic_on_Un) auto hence "(λz. f (w + z)) analytic_on {s. Re s > 0 ∨ Im s ∈ {-R-1<..<R+1} ∧ Re s > x1}" by (rule analytic_on_subset) auto with ‹x1 < 0› and that[of "-x1"] show ?thesis by auto qed ― ‹The function ‹f (w + z)› is now analytic on the open box $(-l; R+1) + i(-R+1; R+1)$. We call this region ‹X›.› define X where "X = box (Complex (-l) (-R-1)) (Complex (R+1) (R+1))" have [simp, intro]: "open X" "convex X" by (simp_all add: X_def open_box) from R l have [simp]: "0 ∈ X" by (auto simp: X_def in_box_complex_iff) have analytic: "(λz. f (w + z)) analytic_on X" by (rule analytic_on_subset[OF l(2)]) (auto simp: X_def in_box_complex_iff) note f_analytic' [analytic_intros] = analytic_on_compose_gen[OF _ analytic, unfolded o_def] note f_holo [holomorphic_intros] = holomorphic_on_compose_gen[OF _ analytic_imp_holomorphic[OF analytic], unfolded o_def] note f_cont [continuous_intros] = continuous_on_compose2[OF holomorphic_on_imp_continuous_on[OF analytic_imp_holomorphic[OF analytic]]] ― ‹We now pick a smaller closed box ‹X'› inside the big open box ‹X›. This is because we need a compact set for the next step. our integration path still lies entirely within ‹X'›, and since ‹X'› is compact, ‹f (w + z)› is bounded on it, so we obtain such a bound and call it ‹M›.› define δ where "δ = min (1/2) (l/2)" from l have δ: "δ > 0" "δ ≤ 1/2" "δ < l" by (auto simp: δ_def) define X' where "X' = cbox (Complex (-δ) (-R)) (Complex R R)" have "X' ⊆ X" unfolding X'_def X_def using l(1) R δ by (intro subset_box_imp) (auto simp: Basis_complex_def) have [intro]: "compact X'" by (simp add: X'_def) moreover have "continuous_on X' (λz. f (w + z))" using w ‹X' ⊆ X› by (auto intro!: continuous_intros) ultimately obtain M where M: "M ≥ 0" "⋀z. z ∈ X' ⟹ norm (f (w + z)) ≤ M" using continuous_on_compact_bound by blast ― ‹Our objective is now to show that the difference between the ‹N›-th partial sum and the limit is below a certain bound (depending on ‹N›) which tends to ‹0› for ‹N → ∞›. We use the following bound:› define bound where "bound = (λN::nat. (2*C/R + C/N + 3*M / (pi*R*ln N) + 3*R*M / (δ*pi * N powr δ)))" have "2 * C / R < ε" using M(1) R C(1) δ(1) ε by (auto simp: field_simps) ― ‹Evidently this is below @{term ε} for sufficiently large ‹N›.› hence "eventually (λN::nat. bound N < ε) at_top" using M(1) R C(1) δ(1) ε unfolding bound_def by real_asymp ― ‹It now only remains to show that the difference is indeed less than the claimed bound.› thus "eventually (λN. norm (f w - eval_fds (fds_truncate N F) w) < ε) at_top" using eventually_gt_at_top[of 1] proof eventually_elim case (elim N) note N = this ― ‹Like Harrison (and unlike Newman), our integration path ‹Γ› consists of a semicircle ‹A› of radius ‹R› in the right-halfplane and a box of width ‹δ› and height ‹2R› on the left halfplane. The latter consists of three straight lines, which we call ‹B1› to ‹B3›.› define A where "A = part_circlepath 0 R (-pi/2) (pi/2)" define B2 where "B2 = linepath (Complex (-δ) R) (Complex (-δ) (-R))" define B1 where "B1 = linepath (R * 𝗂) (R * 𝗂 - δ)" define B3 where "B3 = linepath (-R * 𝗂 - δ) (-R * 𝗂)" define Γ where "Γ = A +++ B1 +++ B2 +++ B3" ― ‹We first need to show some basic facts about the geometry of our integration path.› have [simp, intro]: "path A" "path B1" "path B3" "path B2" "valid_path A" "valid_path B1" "valid_path B3" "valid_path B2" "arc A" "arc B1" "arc B3" "arc B2" "pathstart A = -𝗂 * R" "pathfinish A = 𝗂 * R" "pathstart B1 = 𝗂 * R" "pathfinish B1 = R * 𝗂 - δ" "pathstart B3 = -R * 𝗂 - δ" "pathfinish B3 = -𝗂 * R" "pathstart B2 = R * 𝗂 - δ" "pathfinish B2 = -R * 𝗂 - δ" using R δ by (simp_all add: A_def B1_def B3_def exp_eq_polar B2_def Complex_eq arc_part_circlepath) hence [simp, intro]: "valid_path Γ" by (simp add: Γ_def A_def B1_def B3_def B2_def exp_eq_polar Complex_eq) hence [simp, intro]: "path Γ" using valid_path_imp_path by blast have [simp]: "pathfinish Γ = pathstart Γ" by (simp add: Γ_def exp_eq_polar) have image_B2: "path_image B2 = {s. Re s = -δ ∧ Im s ∈ {-R..R}}" using R by (auto simp: closed_segment_same_Re closed_segment_eq_real_ivl B2_def) have image_B1: "path_image B1 = {s. Re s ∈ {-δ..0} ∧ Im s = R}" and image_B3: "path_image B3 = {s. Re s ∈ {-δ..0} ∧ Im s = -R}" using δ by (auto simp: B1_def B3_def closed_segment_same_Im closed_segment_eq_real_ivl) have image_A: "path_image A = {s. Re s ≥ 0 ∧ norm s = R}" unfolding A_def using R by (subst path_image_semicircle_Re_ge) auto also have "z ∈ … ⟶ z ∈ X' - {0}" for z using complex_Re_le_cmod[of z] abs_Im_le_cmod[of z] δ R by (auto simp: X'_def in_cbox_complex_iff) hence "{s. Re s ≥ 0 ∧ norm s = R} ⊆ X' - {0}" by auto finally have "path_image B2 ⊆ X' - {0}" "path_image A ⊆ X' - {0}" "path_image B1 ⊆ X' - {0}" "path_image B3 ⊆ X' - {0}" using ‹δ > 0› by (auto simp: X'_def in_cbox_complex_iff image_B2 image_B1 image_B3) note path_images = this ‹X' ⊆ X› ― ‹‹Γ› is a simple path, which, combined with its simple geometric shape, makes reasoning about its winding numbers trivial.› from R have "simple_path A" unfolding A_def by (subst simple_path_part_circlepath) auto have "simple_path Γ" unfolding Γ_def proof (intro simple_path_join_loop subsetI arc_join, goal_cases) fix z assume z: "z ∈ path_image A ∩ path_image (B1 +++ B2 +++ B3)" with image_A have "Re z ≥ 0" "norm z = R" by auto with z R δ show "z ∈ {pathstart A, pathstart (B1 +++ B2 +++ B3)}" by (auto simp: path_image_join image_B1 image_B2 image_B3 complex_eq_iff) qed (insert R, auto simp: image_B1 image_B3 path_image_join image_B2 complex_eq_iff) ― ‹We define the integrands in the same fashion as Newman:› define g where "g = (λz::complex. f (w + z) * N powr z * (1 / z + z / R⇧^{2}))" define S where "S = eval_fds (fds_truncate N F)" define g_S where "g_S = (λz::complex. S (w + z) * N powr z * (1 / z + z / R⇧^{2}))" define rem where "rem = (λz::complex. f z - S z)" define g_rem where "g_rem = (λz::complex. rem (w + z) * N powr z * (1 / z + z / R⇧^{2}))" have g_holo: "g holomorphic_on X - {0}" unfolding g_def by (auto intro!: holomorphic_intros analytic_imp_holomorphic'[OF analytic]) have rem_altdef: "rem z = eval_fds (fds_remainder N F) z" if "Re z > 1" for z proof - have abscissa: "abs_conv_abscissa F ≤ 1" using assms by (intro bounded_coeffs_imp_abs_conv_abscissa_le_1) (simp_all add: natfun_bigo_iff_Bseq) from assms and that have "f z = eval_fds F z" by auto also have "F = fds_truncate N F + fds_remainder N F" by (rule fds_truncate_plus_remainder [symmetric]) also from that have "eval_fds … z = S z + eval_fds (fds_remainder N F) z" unfolding S_def by (subst eval_fds_add) (auto intro!: fds_abs_converges_imp_converges fds_abs_converges[OF le_less_trans[OF abscissa]]) finally show ?thesis by (simp add: rem_def) qed ― ‹We now come to the first application of the residue theorem along the path ‹Γ›:› have "∮[Γ] g = 2 * pi * 𝗂 * winding_number Γ 0 * residue g 0" proof (subst Residue_theorem) show "g holomorphic_on X - {0}" by fact show "path_image Γ ⊆ X - {0}" using path_images by (auto simp: Γ_def path_image_join) thus "∀z. z ∉ X ⟶ winding_number Γ z = 0" by (auto intro!: simply_connected_imp_winding_number_zero[of X] convex_imp_simply_connected) qed (insert path_images, auto intro: convex_connected) also have "winding_number Γ 0 = 1" proof (rule simple_closed_path_winding_number_pos) from R δ have "∀g∈{A, B1, B2, B3}. Re (winding_number g 0) > 0" unfolding A_def B1_def B2_def B3_def by (auto intro!: winding_number_linepath_pos_lt winding_number_part_circlepath_pos_less) hence "valid_path Γ ∧ 0 ∉ path_image Γ ∧ Re (winding_number Γ 0) > 0" unfolding Γ_def using path_images(1-4) by (intro winding_number_join_pos_combined') auto thus "Re (winding_number Γ 0) > 0" by simp qed (insert path_images ‹simple_path Γ›, auto simp: Γ_def path_image_join) also have "residue g 0 = f w" proof - have "g = (λz::complex. f (w + z) * N powr z * (1 + z⇧^{2}/ R⇧^{2}) / z)" by (auto simp: g_def divide_simps fun_eq_iff power2_eq_square simp del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1) moreover from N have "residue … 0 = f w" by (subst residue_simple'[of X]) (auto intro!: holomorphic_intros analytic_imp_holomorphic[OF analytic]) ultimately show ?thesis by (simp only:) qed finally have "2 * pi * 𝗂 * f w = ∮[Γ] g" by simp also have "… = ∮[A] g + ∮[B2] g + ∮[B1] g + ∮[B3] g" unfolding Γ_def by (subst contour_integral_join, (insert path_images, auto intro!: contour_integral_join contour_integrable_holomorphic_simple g_holo)[4])+ (simp_all add: add_ac) finally have integral1: "2 * pi * 𝗂 * f w = ∮[A] g + ∮[B2] g + ∮[B1] g + ∮[B3] g" . ― ‹Next, we apply the residue theorem along a circle of radius ‹R› to another integrand that is related to the partial sum:› have "∮[circlepath 0 R] g_S = 2 * pi * 𝗂 * residue g_S 0" proof (subst Residue_theorem) show "g_S holomorphic_on UNIV - {0}" by (auto simp: g_S_def S_def intro!: holomorphic_intros) qed (insert R, auto simp: winding_number_circlepath_centre) also have "residue g_S 0 = S w" proof - have "g_S = (λz::complex. S (w + z) * N powr z * (1 + z⇧^{2}/ R⇧^{2}) / z)" by (auto simp: g_S_def divide_simps fun_eq_iff power2_eq_square simp del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1) moreover from N have "residue … 0 = S w" by (subst residue_simple'[of X]) (auto intro!: holomorphic_intros simp: S_def) ultimately show ?thesis by (simp only:) qed finally have "2 * pi * 𝗂 * S w = ∮[circlepath 0 R] g_S" .. ― ‹We split this integral into integrals along two semicircles in the left and right half-plane, respectively:› also have "… = ∮[part_circlepath 0 R (-pi/2) (3*pi/2)] g_S" proof (rule Cauchy_theorem_homotopic_loops) show "homotopic_loops (-{0}) (circlepath 0 R) (part_circlepath 0 R (- pi / 2) (3 * pi / 2))" unfolding circlepath_def using R by (intro homotopic_loops_part_circlepath[where k = 1]) auto qed (auto simp: g_S_def S_def intro!: holomorphic_intros) also have "… = ∮[A +++ -A] g_S" proof (rule Cauchy_theorem_homotopic_paths) have *: "-A = part_circlepath 0 R (pi/2) (3*pi/2)" unfolding A_def by (intro part_circlepath_mirror[where k = 0]) auto from R show "homotopic_paths (-{0}) (part_circlepath 0 R (-pi/2) (3*pi/2)) (A +++ -A)" unfolding * unfolding A_def by (intro homotopic_paths_part_circlepath) (auto dest!: in_path_image_part_circlepath) qed (auto simp: g_S_def S_def A_def exp_eq_polar intro!: holomorphic_intros) also have "… = ∮[A] g_S + ∮[-A] g_S" using R by (intro contour_integral_join contour_integrable_holomorphic_simple[of _ "-{0}"]) (auto simp: A_def g_S_def S_def path_image_mirror dest!: in_path_image_part_circlepath intro!: holomorphic_intros) also have "∮[-A] g_S = -∮[A] (λx. g_S (-x))" by (simp add: A_def contour_integral_mirror contour_integral_neg) finally have integral2: "2 * pi * 𝗂 * S w = ∮[A] g_S - ∮[A] (λx. g_S (-x))" by simp ― ‹Next, we show a small bounding lemma that we will need for the final estimate:› have circle_bound: "norm (1 / z + z / R⇧^{2}) ≤ 2 / R" if [simp]: "norm z = R" for z :: complex proof - have "norm (1 / z + z / R⇧^{2}) ≤ 1 / R + 1 / R" by (intro order.trans[OF norm_triangle_ineq] add_mono) (insert R, simp_all add: norm_divide norm_mult power2_eq_square) thus ?thesis by simp qed ― ‹The next bound differs somewhat from Newman's, but it works just as well. Its purpose is to bound the contribution of the two short horizontal line segments.› have B12_bound: "norm (integral {- δ..0} (λx. g (x + R' * 𝗂))) ≤ 3 * M / R / ln N" (is "?I ≤ _") if "¦R'¦ = R" for R' proof - have "?I ≤ integral {-δ..0} (λx. 3 * M / R * N powr x)" proof (rule integral_norm_bound_integral) fix x assume x: "x ∈ {-δ..0}" define z where "z = x + 𝗂 * R'" from R that have [simp]: "z ≠ 0" "Re z = x" "Im z = R'" by (auto simp: z_def complex_eq_iff) from x R that have "z ∈ X'" by (auto simp: z_def X'_def in_cbox_complex_iff) from x R that have "norm z ≤ δ + R" by (intro order.trans[OF cmod_le add_mono]) auto hence "norm (1 / z + z / R⇧^{2}) ≤ 1 / R + (δ / R + 1) / R" using R that abs_Im_le_cmod[of z] by (intro order.trans[OF norm_triangle_ineq add_mono]) (auto simp: norm_divide norm_mult power2_eq_square field_simps ) also have "δ / R ≤ 1" using δ R by auto finally have "norm (1 / z + z / R⇧^{2}) ≤ 3 / R" using R by (simp add: divide_right_mono) hence "norm (g z) ≤ M * N powr x * (3 / R)" unfolding g_def norm_mult using ‹M ≥ 0› ‹z ∈ X'› by (intro mult_mono mult_nonneg_nonneg M) (auto simp: norm_powr_real_powr) thus "norm (g (x + R' * 𝗂)) ≤ 3 * M / R * N powr x" by (simp add: mult_ac z_def) qed (insert N R l that δ, auto intro!: integrable_continuous_real continuous_intros simp: g_def X_def complex_eq_iff in_box_complex_iff) also have "… = 3 * M / R * integral {-δ..0} (λx. N powr x)" by simp also have "((λx. N powr x) has_integral (N powr 0 / ln N - N powr (-δ) / ln N)) {-δ..0}" using δ N by (intro fundamental_theorem_of_calculus) (auto simp: has_real_derivative_iff_has_vector_derivative [symmetric] powr_def intro!: derivative_eq_intros) hence "integral {-δ..0} (λx. N powr x) = 1 / ln (real N) - real N powr - δ / ln (real N)" using N by (simp add: has_integral_iff) also have "… ≤ 1 / ln (real N)" using N by simp finally show ?thesis using M R by (simp add: mult_left_mono divide_right_mono) qed ― ‹We combine the two results from the residue theorem and obtain an integral representation of the difference between the partial sums and the limit:› have "2 * pi * 𝗂 * (f w - S w) = ∮[A] g - ∮[A] g_S + ∮[A] (λx. g_S (-x)) + ∮[B1] g + ∮[B3] g + ∮[B2] g" unfolding ring_distribs integral1 integral2 by (simp add: algebra_simps) also have "∮[A] g - ∮[A] g_S = ∮[A] (λx. g x - g_S x)" using path_images by (intro contour_integral_diff [symmetric]) (auto intro!: contour_integrable_holomorphic_simple[of _ "X - {0}"] holomorphic_intros simp: g_S_def g_holo S_def) also have "… = ∮[A] g_rem" by (simp add: g_rem_def g_def g_S_def algebra_simps rem_def) finally have "2 * pi * 𝗂 * (f w - S w) = ∮[A] g_rem + ∮[A] (λx. g_S (- x)) + ∮[B1] g + ∮[B3] g + ∮[B2] g" . ― ‹We now bound each of these integrals individually:› also have "norm … ≤ 2 * C * pi / R + 2 * C * pi * (1 / N + 1 / R) + 3 * M / R / ln N + 3 * M / R / ln N + 6 * R * M * N powr (-δ) / δ" proof (rule order.trans[OF norm_triangle_ineq] add_mono)+ have "∮[B1] g = -∮[reversepath B1] g" by (simp add: contour_integral_reversepath) also have "∮[reversepath B1] g = integral {-δ..0} (λx. g (x + R * 𝗂))" unfolding B1_def reversepath_linepath using δ by (subst contour_integral_linepath_same_Im) auto also have "norm (-…) = norm …" by simp also have "… ≤ 3 * M / R / ln N" using R by (intro B12_bound) auto finally show "norm (∮[B1] g) ≤ …" . next have "∮[B3] g = integral {-δ..0} (λx. g (x + (-R) * 𝗂))" unfolding B3_def using δ by (subst contour_integral_linepath_same_Im) auto also have "norm … ≤ 3 * M / R / ln N" using R by (intro B12_bound) auto finally show "norm (∮[B3] g) ≤ …" . next have "norm (∮[B2] g) ≤ M * N powr (-δ) * (3 / δ) * norm (Complex (- δ) (-R) - Complex (- δ) R)" unfolding B2_def proof ((rule contour_integral_bound_linepath; (fold B2_def)?), goal_cases) case (3 z) from 3 δ R have [simp]: "z ≠ 0" and Re_z: "Re z = -δ" and Im_z: "Im z ∈ {-R..R}" by (auto simp: closed_segment_same_Re closed_segment_eq_real_ivl) from 3 have "z ∈ X'" using R δ path_images by (auto simp: B2_def) from 3 δ R have "norm z ≤ sqrt (δ^2 + R^2)" unfolding cmod_def using Re_z Im_z by (intro real_sqrt_le_mono add_mono) (auto simp: power2_le_iff_abs_le) from power_mono[OF this, of 2] have norm_sqr: "norm z ^ 2 ≤ δ⇧^{2}+ R⇧^{2}" by simp have "norm (1 / z + z / R⇧^{2}) ≤ (1 + (norm z)⇧^{2}/ R⇧^{2}) / δ" unfolding add_divide_distrib using δ R abs_Re_le_cmod[of z] by (intro order.trans[OF norm_triangle_ineq] add_mono) (auto simp: norm_divide norm_mult field_simps power2_eq_square Re_z) also have "… ≤ (1 + (1 + δ⇧^{2}/ R⇧^{2})) / δ" using δ R ‹z ∈ X'› norm_sqr unfolding X'_def by (intro divide_right_mono add_left_mono) (auto simp: field_simps in_cbox_complex_iff intro!: power_mono) also have "δ⇧^{2}/ R⇧^{2}≤ 1" using δ R by (auto simp: field_simps intro!: power_mono) finally have "norm (1 / z + z / R⇧^{2}) ≤ 3 / δ" using δ by(simp add: divide_right_mono) with ‹z ∈ X'› show "norm (g z) ≤ M * N powr (-δ) * (3 / δ)" unfolding g_def norm_mult by (intro mult_mono mult_nonneg_nonneg M) (auto simp: norm_powr_real_powr Re_z) qed (insert path_images M δ, auto intro!: contour_integrable_holomorphic_simple[OF g_holo]) thus "norm (∮[B2] g) ≤ 6 * R * M * N powr (-δ) / δ" using R by (simp add: field_simps cmod_def real_sqrt_mult) next have "norm (∮[A] (λx. g_S (- x))) ≤ (2 * C / (real N * R) + 2 * C / R⇧^{2}) * R * ((pi/2) - (-pi/2))" unfolding A_def proof ((rule contour_integral_bound_part_circlepath_strong[where k = "{R * 𝗂, -R*𝗂}"]; (fold A_def)?), goal_cases) case (6 z) hence [simp]: "z ≠ 0" and "norm z = R" using R by (auto simp: A_def dest!: in_path_image_part_circlepath) from 6 have "Re z ≠ 0" using ‹norm z = R› by (auto simp: cmod_def abs_if complex_eq_iff split: if_splits) with 6 have "Re z > 0" using image_A by auto have "S (w - z) = (∑k = 1..N. fds_nth F k / of_nat k powr (w - z))" by (simp add: S_def eval_fds_truncate) also have "norm … ≤ C * N powr Re z * (1 / N + 1 / Re z)" using ‹Re z > 0› w N by (intro newman_ingham_aux2 C) auto finally have "norm (S (w - z)) ≤ …" . hence "norm (g_S (-z)) ≤ (C * N powr (Re z) * (1 / N + 1 / Re z)) * N powr (-Re z) * (2 * Re z / R⇧^{2})" unfolding g_S_def norm_mult using newman_ingham_aux1[OF _ ‹norm z = R›] ‹Re z > 0› ‹C ≥ 1› R by (intro mult_mono mult_nonneg_nonneg circle_bound) (auto simp: norm_powr_real_powr norm_uminus_minus) also have "… = 2 * C * (Re z / N + 1) / R⇧^{2}" using R N ‹Re z > 0› by (simp add: powr_minus algebra_simps) also have "… ≤ 2 * C / (N * R) + 2 * C / R⇧^{2}" unfolding add_divide_distrib ring_distribs using R N abs_Re_le_cmod[of z] ‹norm z = R› ‹Re z > 0› ‹C ≥ 1› by (intro add_mono) (auto simp: power2_eq_square field_simps mult_mono) finally show ?case . qed (insert R N image_A C, auto intro!: contour_integrable_holomorphic_simple[of _ "-{0}"] holomorphic_intros simp: g_S_def S_def) also have "… = 2 * C * pi * (1 / N + 1 / R)" using R N by (simp add: power2_eq_square field_simps) finally show "norm (∮[A] (λx. g_S (- x))) ≤ …" . next have "norm (∮[A] g_rem) ≤ (2 * C / R⇧^{2}) * R * ((pi/2) - (-pi/2))" unfolding A_def proof ((rule contour_integral_bound_part_circlepath_strong[where k = "{R * 𝗂, -R*𝗂}"]; (fold A_def)?), goal_cases) case (6 z) hence [simp]: "z ≠ 0" and "norm z = R" using R by (auto simp: A_def dest!: in_path_image_part_circlepath) from 6 have "Re z ≠ 0" using ‹norm z = R› by (auto simp: cmod_def abs_if complex_eq_iff split: if_splits) with 6 have "Re z > 0" using image_A by auto have summable: "summable (λn. C * (1 / (Suc n + N) powr (Re w + Re z)))" using summable_hurwitz_zeta_real[of "Re w + Re z" "Suc N"] ‹Re z > 0› w unfolding powr_minus by (intro summable_mult) (auto simp: field_simps) have "rem (w + z) = (∑n. fds_nth F (Suc n + N) / (Suc n + N) powr (w + z))" using ‹Re z > 0› w by (simp add: rem_altdef eval_fds_remainder) also have "norm … ≤ (∑n. C / (Suc n + N) powr Re (w + z))" using summable by (intro norm_suminf_le) (auto simp: norm_divide norm_powr_real_powr intro!: divide_right_mono C) also have "… = (∑n. C * (Suc n + N) powr -Re (w + z))" unfolding powr_minus by (simp add: field_simps) also have "… = C * (∑n. (Suc n + N) powr -Re (w + z))" using summable_hurwitz_zeta_real[of "Re w + Re z" "Suc N"] ‹Re z > 0› w by (subst suminf_mult) (auto simp: add_ac) also have "(∑n. (Suc n + N) powr -Re (w + z)) ≤ N powr (1 - Re (w + z)) / (Re (w + z) - 1)" using ‹Re z > 0› w N hurwitz_zeta_real_bound_aux[of N "Re (w + z)"] by (auto simp: add_ac) also have "… ≤ N powr -Re z / Re z" using w N ‹Re z > 0› by (intro frac_le powr_mono) auto finally have "norm (rem (w + z)) ≤ C / (Re z * N powr Re z)" using C by (simp add: mult_left_mono mult_right_mono powr_minus field_simps) hence "norm (g_rem z) ≤ (C / (Re z * N powr Re z)) * N powr (Re z) * (2 * Re z / R⇧^{2})" unfolding g_rem_def norm_mult using newman_ingham_aux1[OF _ ‹norm z = R›] R ‹Re z > 0› C by (intro mult_mono mult_nonneg_nonneg circle_bound) (auto simp: norm_powr_real_powr norm_uminus_minus) also have "… = 2 * C / R⇧^{2}" using R N ‹Re z > 0› by (simp add: powr_minus field_simps) finally show ?case . next show "g_rem contour_integrable_on A" using path_images by (auto simp: g_rem_def rem_def S_def intro!: contour_integrable_holomorphic_simple[of _ "X-{0}"] holomorphic_intros) qed (insert R N C, auto) also have "(2 * C / R⇧^{2}) * R * ((pi/2) - (-pi/2)) = 2 * C * pi / R" using R by (simp add: power2_eq_square field_simps) finally show "norm (∮[A] g_rem) ≤ …" . qed also have "… = 4*C*pi/R + 2*C*pi/N + 6*M/R / ln N + 6*R*M*N powr - δ / δ" by (simp add: algebra_simps) also have "… = 2*pi * (2*C/R + C/N + 3*M / (pi*R*ln N) + 3*R*M / (δ*pi * N powr δ))" by (simp add: field_simps powr_minus ) also have "norm (2 * pi * 𝗂 * (f w - S w)) = 2 * pi * norm (f w - S w)" by (simp add: norm_mult) finally have "norm (f w - S w) ≤ bound N" by (simp add: bound_def) also have "bound N < ε" by fact finally show "norm (f w - S w) < ε" . qed qed thus "fds_converges F w" by (auto simp: fds_converges_altdef2 intro: convergentI) thus "eval_fds F w = f w" using ‹(λN. eval_fds (fds_truncate N F) w) ⇢ f w› by (intro tendsto_unique[OF _ tendsto_eval_fds_truncate]) auto qed text ‹ The theorem generalises in a trivial way; we can replace the requirement that the coefficients of $f(s)$ be $O(1)$ by $O(n^{\sigma-1})$ for some $\sigma\in\mathbb{R}$, then $f(s)$ converges for $\mathfrak{R}(s)>\sigma$. If it can be analytically continued to $\mathfrak{R}(s)\geq\sigma$, it is also convergent there. › theorem Newman_Ingham: fixes F :: "complex fds" and f :: "complex ⇒ complex" assumes coeff_bound: "fds_nth F ∈ O(λn. n powr of_real (σ - 1))" assumes f_analytic: "f analytic_on {s. Re s ≥ σ}" assumes F_conv_f: "⋀s. Re s > σ ⟹ eval_fds F s = f s" assumes w: "Re w ≥ σ" shows "fds_converges F w" and "eval_fds F w = f w" proof - define F' where "F' = fds_shift (-of_real (σ - 1)) F" define f' where "f' = f ∘ (λs. s + of_real (σ - 1))" have "fds_nth F' = (λn. fds_nth F n * of_nat n powr -of_real(σ - 1))" by (auto simp: fun_eq_iff F'_def) also have "… ∈ O(λn. of_nat n powr of_real (σ - 1) * of_nat n powr -of_real(σ - 1))" by (intro landau_o.big.mult_right assms) also have "(λn. of_nat n powr of_real (σ - 1) * of_nat n powr -of_real (σ - 1)) ∈ Θ(λ_. 1)" by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 0]]) (auto simp: powr_minus powr_diff) finally have bigo: "fds_nth F' ∈ O(λ_. 1)" . from f_analytic have analytic: "f' analytic_on {s. Re s ≥ 1}" unfolding f'_def by (intro analytic_on_compose_gen[OF _ f_analytic]) (auto intro!: analytic_intros) have F'_f: "eval_fds F' s = f' s" if "Re s > 1" for s using assms that by (auto simp: F'_def f'_def algebra_simps) have w': "1 ≤ Re (w - of_real (σ - 1))" using w by simp have 1: "fds_converges F' (w - of_real (σ - 1))" using bigo analytic F'_f w' by (rule Newman_Ingham_1) thus "fds_converges F w" by (auto simp: F'_def) have 2: "eval_fds F' (w - of_real (σ - 1)) = f' (w - of_real (σ - 1))" using bigo analytic F'_f w' by (rule Newman_Ingham_1) thus "eval_fds F w = f w" using assms by (simp add: F'_def f'_def) qed end