Theory Perron_Prerequisites
section ‹Auxiliary material›
theory Perron_Prerequisites
imports "Dirichlet_Series.Dirichlet_Series_Analysis"
begin
subsection ‹General analysis›
lemma at_infinity_conv_filtercomap_norm_at_top: "at_infinity = filtercomap norm at_top"
by (rule filter_eqI) (auto simp: eventually_at_infinity eventually_filtercomap_at_top_linorder)
lemma at_infinity_conv_filtercomap_abs_at_top:
"at_infinity = filtercomap (abs :: real ⇒ real) at_top"
unfolding at_infinity_conv_filtercomap_norm_at_top
using real_norm_def by metis
lemma tendsto_dist_sandwich:
assumes "eventually (λn. dist (f n) c ≤ g n) F"
assumes "(g ⤏ 0) F"
shows "(f ⤏ c) F"
proof -
have "((λn. dist (f n) c) ⤏ 0) F"
proof (rule tendsto_sandwich)
show "∀⇩F n in F. dist (f n) c ≥ 0"
by simp
show "∀⇩F n in F. dist (f n) c ≤ g n"
by fact
qed (use assms(2) in auto)
thus ?thesis
using tendsto_dist_iff by blast
qed
lemma summation_by_parts:
fixes f g :: "nat ⇒ 'a :: comm_ring_1"
assumes "m ≤ n"
shows "(∑k=m..n. f k * (g (Suc k) - g k)) =
f (Suc n) * g (Suc n) - f m * g m - (∑k=m..n. g (Suc k) * (f (Suc k) - f k))"
proof -
have "f (Suc n) * g (Suc n) - f m * g m - (∑k=m..n. g (Suc k) * (f (Suc k) - f k)) -
(∑k=m..n. f k * (g (Suc k) - g k)) =
(∑k=m..n. f k * g k) - f m * g m - ((∑k=m..n. f (Suc k) * g (Suc k)) -
f (Suc n) * g (Suc n))"
by (simp add: sum_subtractf algebra_simps)
also have "(∑k=m..n. f k * g k) = (∑k∈insert m {m<..n}. f k * g k)"
using assms by (intro sum.cong) auto
also have "… - f m * g m = (∑k∈{m<..n}. f k * g k)"
by (subst sum.insert) auto
also have "(∑k=m..n. f (Suc k) * g (Suc k)) = (∑k∈insert n {m..<n}. f (Suc k) * g (Suc k))"
using assms by (intro sum.cong) auto
also have "… - f (Suc n) * g (Suc n) = (∑k=m..<n. f (Suc k) * g (Suc k))"
by (subst sum.insert) auto
also have "… = (∑k∈{m<..n}. f k * g k)"
by (rule sum.reindex_bij_witness[of _ "λi. i - 1" "λi. i + 1"]) auto
finally show ?thesis
by simp
qed
lemma bounded_normE:
assumes "bounded A"
obtains C where "C > c" "⋀x. x ∈ A ⟹ norm x < C"
proof -
from assms obtain C' where C': "⋀x. x ∈ A ⟹ norm x ≤ C'"
by (auto simp: bounded_iff)
show ?thesis
by (intro that[of "max C' c + 1"]) (auto simp: max_def dest: C')
qed
lemma norm_suminf_le':
fixes f :: "nat ⇒ 'a :: banach"
assumes "⋀n. norm (f n) ≤ g n" "g sums A"
shows "norm (suminf f) ≤ A"
proof -
have "norm (suminf f) ≤ suminf g"
by (rule norm_suminf_le) (use assms in ‹auto simp: sums_iff›)
thus ?thesis
using assms by (simp add: sums_iff)
qed
proposition swap_uniform_limit':
assumes f: "∀⇩F n in F. (f n ⤏ g n) G"
assumes g: "(g ⤏ l) F"
assumes uc: "uniform_limit S f h F"
assumes ev: "∀⇩F x in G. x ∈ S"
assumes "¬trivial_limit F"
shows "(h ⤏ l) G"
proof (rule tendstoI)
fix e :: real
define e' where "e' = e/3"
assume "0 < e"
then have "0 < e'" by (simp add: e'_def)
from uniform_limitD[OF uc ‹0 < e'›]
have "∀⇩F n in F. ∀x∈S. dist (h x) (f n x) < e'"
by (simp add: dist_commute)
moreover
from f
have "∀⇩F n in F. ∀⇩F x in G. dist (g n) (f n x) < e'"
by eventually_elim (auto dest!: tendstoD[OF _ ‹0 < e'›] simp: dist_commute)
moreover
from tendstoD[OF g ‹0 < e'›] have "∀⇩F x in F. dist l (g x) < e'"
by (simp add: dist_commute)
ultimately
have "∀⇩F _ in F. ∀⇩F x in G. dist (h x) l < e"
proof eventually_elim
case (elim n)
note fh = elim(1)
note gl = elim(3)
show ?case
using elim(2) ev
proof eventually_elim
case (elim x)
from fh[rule_format, OF ‹x ∈ S›] elim(1)
have "dist (h x) (g n) < e' + e'"
by (rule dist_triangle_lt[OF add_strict_mono])
from dist_triangle_lt[OF add_strict_mono, OF this gl]
show ?case by (simp add: e'_def)
qed
qed
thus "∀⇩F x in G. dist (h x) l < e"
using eventually_happens by (metis ‹¬trivial_limit F›)
qed
lemma uniform_limit_compose':
assumes "uniform_limit A f g F" and "h ` B ⊆ A"
shows "uniform_limit B (λn x. f n (h x)) (λx. g (h x)) F"
unfolding uniform_limit_iff
proof safe
fix e :: real
assume e: "e > 0"
from e and assms(1) have "∀⇩F n in F. ∀x∈A. dist (f n x) (g x) < e"
by (auto simp: uniform_limit_iff)
thus "∀⇩F n in F. ∀x∈B. dist (f n (h x)) (g (h x)) < e"
by eventually_elim (use assms(2) in blast)
qed
lemma integrable_stretch_real:
fixes f :: "real ⇒ 'b::real_normed_vector"
assumes "f integrable_on {a..b}" and "m ≠ 0"
shows "(λx. f (m * x)) integrable_on ((λx. x / m) ` {a..b})"
proof -
from assms obtain I where "(f has_integral I) {a..b}"
by (auto simp: integrable_on_def)
from has_integral_stretch_real[OF this assms(2)] show ?thesis
by (auto simp: integrable_on_def)
qed
lemma integrable_stretch_real_iff:
fixes f :: "real ⇒ 'b::real_normed_vector"
assumes "m ≠ 0"
shows "(λx. f (m * x)) integrable_on ((λx. x / m) ` {a..b}) ⟷ f integrable_on {a..b}"
proof
assume "f integrable_on {a..b}"
thus "(λx. f (m * x)) integrable_on ((λx. x / m) ` {a..b})"
using assms by (intro integrable_stretch_real) auto
next
assume *: "(λx. f (m * x)) integrable_on ((λx. x / m) ` {a..b})"
define a' where "a' = (if m > 0 then a / m else b / m)"
define b' where "b' = (if m > 0 then b / m else a / m)"
have "bij_betw (λx. x / m) {a..b} {a'..b'}"
by (rule bij_betwI[of _ _ _ "λx. x * m"]) (use assms in ‹auto simp: field_simps a'_def b'_def›)
hence eq: "(λx. x / m) ` {a..b} = {a'..b'}"
by (simp add: bij_betw_def)
from * have "(λx. f (m * x)) integrable_on {a'..b'}"
unfolding eq .
hence "(λx. f (m * (1 / m * x))) integrable_on (λx. x / (1 / m)) ` {a'..b'}"
using assms by (intro integrable_stretch_real) auto
also have "(λx. f (m * (1 / m * x))) = f"
using assms by simp
also have "bij_betw (λx. x / (1 / m)) {a'..b'} {a..b}"
by (rule bij_betwI[of _ _ _ "λx. x / m"]) (use assms in ‹auto simp: field_simps a'_def b'_def›)
hence "(λx. x / (1 / m)) ` {a'..b'} = {a..b}"
by (simp add: bij_betw_def)
finally show "f integrable_on {a..b}" .
qed
lemma integral_stretch_real:
fixes f :: "real ⇒ 'b::real_normed_vector"
assumes "m ≠ 0"
shows "integral ((λx. x / m) ` {a..b}) (λx. f (m * x)) = (1 / ¦m¦) *⇩R integral {a..b} f"
proof (cases "f integrable_on {a..b}")
case True
hence "(f has_integral integral {a..b} f) {a..b}"
by blast
from has_integral_stretch_real[OF this assms] show ?thesis
by (simp add: has_integral_iff)
next
case False
hence "¬(λx. f (m * x)) integrable_on ((λx. x / m) ` {a..b})"
using assms by (subst integrable_stretch_real_iff)
with False show ?thesis
by (simp add: not_integrable_integral)
qed
lemma cbox_shift: "(+) c ` cbox a b = cbox (a + c) (b + c)"
proof -
have "bij_betw ((+) c) (cbox a b) (cbox (a + c) (b + c))"
by (rule bij_betwI[of _ _ _ "λx. x - c"]) (auto simp: cbox_def algebra_simps)
thus ?thesis
by (simp add: bij_betw_def)
qed
lemma cbox_shift': "(λx. x + c) ` cbox a b = cbox (a + c) (b + c)"
using cbox_shift[of c a b] by (simp add: add.commute)
lemma cbox_shift'': "(λx. x - c) ` cbox a b = cbox (a - c) (b - c)"
using cbox_shift[of "-c" a b] by simp
lemma has_integral_shift_cbox:
fixes f :: "'a :: euclidean_space ⇒ 'b :: real_normed_vector"
assumes "(f has_integral I) (cbox a b)"
shows "((λx. f (x + c)) has_integral I) (cbox (a - c) (b - c))"
proof -
have "((λx. f (x + c)) has_integral (1 / 1) *⇩R I) ((λx. x - c) ` cbox a b)"
by (rule has_integral_twiddle)
(use assms in ‹auto simp: cbox_shift'' cbox_shift' content_cbox_if
algebra_simps box_eq_empty›)
thus ?thesis
by (simp add: cbox_shift'')
qed
lemma integrable_shift_cbox:
fixes f :: "'a :: euclidean_space ⇒ 'b :: real_normed_vector"
assumes "f integrable_on cbox a b"
shows "(λx. f (x + c)) integrable_on (cbox (a - c) (b - c))"
using has_integral_shift_cbox[of f _ a b c] assms
by (auto simp: integrable_on_def)
lemma integrable_shift_cbox_iff:
fixes f :: "'a :: euclidean_space ⇒ 'b :: real_normed_vector"
shows "(λx. f (x + c)) integrable_on (cbox (a - c) (b - c)) ⟷ f integrable_on cbox a b"
using integrable_shift_cbox[of f a b c]
integrable_shift_cbox[of "λx. f (x + c)" "a - c" "b - c" "-c"] by auto
lemma integral_shift_cbox:
fixes f :: "'a :: euclidean_space ⇒ 'b :: real_normed_vector"
shows "integral (cbox (a - c) (b - c)) (λx. f (x + c)) = integral (cbox a b) f"
proof (cases "f integrable_on cbox a b")
case True
thus ?thesis
using has_integral_shift_cbox[of f "integral (cbox a b) f" a b c] by auto
next
case False
hence "¬(λx. f (x + c)) integrable_on (cbox (a - c) (b - c))"
by (subst integrable_shift_cbox_iff)
with False show ?thesis
by (simp add: not_integrable_integral)
qed
lemma has_integral_shift_real_ivl:
fixes f :: "real ⇒ 'b :: real_normed_vector"
assumes "(f has_integral I) {a..b}"
shows "((λx. f (x + c)) has_integral I) {a-c..b-c}"
using has_integral_shift_cbox[of f I a b c] assms by simp
lemma integrable_shift_real_ivl:
fixes f :: "real ⇒ 'b :: real_normed_vector"
assumes "f integrable_on {a..b}"
shows "(λx. f (x + c)) integrable_on {a-c..b-c}"
using integrable_shift_cbox[of f a b c] assms by simp
lemma integrable_shift_real_ivl_iff:
fixes f :: "real ⇒ 'b :: real_normed_vector"
shows "(λx. f (x + c)) integrable_on {a-c..b-c} ⟷ f integrable_on {a..b}"
using integrable_shift_cbox_iff[of f c a b] by simp
lemma integral_shift_real_ivl:
fixes f :: "real ⇒ 'b :: real_normed_vector"
shows "integral {a-c..b-c} (λx. f (x + c)) = integral {a..b} f"
using integral_shift_cbox[of a c b f] by simp
lemma Union_atLeastAtMost_real_of_nat:
assumes "a < b"
shows "(⋃n∈{a..<b}. {real n..real (n + 1)}) = {real a..real b}"
proof (intro equalityI subsetI)
fix x assume x: "x ∈ {real a..real b}"
thus "x ∈ (⋃n∈{a..<b}. {real n..real (n + 1)})"
proof (cases "x = real b")
case True
with assms show ?thesis by (auto intro!: bexI[of _ "b - 1"])
next
case False
with x have x: "x ≥ real a" "x < real b" by simp_all
hence "x ≥ real (nat ⌊x⌋)" "x ≤ real (Suc (nat ⌊x⌋))" by linarith+
moreover from x have "nat ⌊x⌋ ≥ a" "nat ⌊x⌋ < b" by linarith+
ultimately show ?thesis by force
qed
qed auto
lemma nat_sum_has_integral_floor:
fixes f :: "nat ⇒ 'a :: banach"
shows "((λx. f (nat ⌊x⌋)) has_integral sum f {m..<n}) {real m..real n}"
proof (cases "m < n")
case mn: True
define D where "D = (λi. {real i..real (Suc i)}) ` {m..<n}"
have D: "D division_of {m..n}"
using Union_atLeastAtMost_real_of_nat[OF mn] by (simp add: division_of_def D_def)
have "((λx. f (nat ⌊x⌋)) has_integral (∑X∈D. f (nat ⌊Inf X⌋))) {real m..real n}"
proof (rule has_integral_combine_division)
fix X assume X: "X ∈ D"
have "nat ⌊x⌋ = nat ⌊Inf X⌋" if "x ∈ X - {Sup X}" for x
using that X by (auto simp: D_def nat_eq_iff floor_eq_iff)
hence "((λx. f (nat ⌊x⌋)) has_integral f (nat ⌊Inf X⌋)) X ⟷
((λx. f (nat ⌊Inf X⌋)) has_integral f (nat ⌊Inf X⌋)) X" using X
by (intro has_integral_spike_eq[of "{Sup X}"]) auto
also from X have "…" using has_integral_const_real[of "f (nat ⌊Inf X⌋)" "Inf X" "Sup X"]
by (auto simp: D_def)
finally show "((λx. f (nat ⌊x⌋)) has_integral f (nat ⌊Inf X⌋)) X" .
qed fact+
also have "(∑X∈D. f (nat ⌊Inf X⌋)) = (∑k∈{m..<n}. f k)"
unfolding D_def by (subst sum.reindex) (auto simp: inj_on_def nat_add_distrib)
finally show ?thesis .
qed auto
lemma nat_sum_has_integral_ceiling:
fixes f :: "nat ⇒ 'a :: banach"
shows "((λx. f (nat ⌈x⌉)) has_integral sum f {m<..n}) {real m..real n}"
proof (cases "m < n")
case mn: True
define D where "D = (λi. {real i..real (Suc i)}) ` {m..<n}"
have D: "D division_of {m..n}"
using Union_atLeastAtMost_real_of_nat[OF mn] by (simp add: division_of_def D_def)
have "((λx. f (nat ⌈x⌉)) has_integral (∑X∈D. f (nat ⌊Sup X⌋))) {real m..real n}"
proof (rule has_integral_combine_division)
fix X assume X: "X ∈ D"
have "nat ⌈x⌉ = nat ⌊Sup X⌋" if "x ∈ X - {Inf X}" for x
using that X by (auto simp: D_def nat_eq_iff ceiling_eq_iff)
hence "((λx. f (nat ⌈x⌉)) has_integral f (nat ⌊Sup X⌋)) X ⟷
((λx. f (nat ⌊Sup X⌋)) has_integral f (nat ⌊Sup X⌋)) X" using X
by (intro has_integral_spike_eq[of "{Inf X}"]) auto
also from X have "…" using has_integral_const_real[of "f (nat ⌊Sup X⌋)" "Inf X" "Sup X"]
by (auto simp: D_def)
finally show "((λx. f (nat ⌈x⌉)) has_integral f (nat ⌊Sup X⌋)) X" .
qed fact+
also have "(∑X∈D. f (nat ⌊Sup X⌋)) = (∑k∈{m..<n}. f (Suc k))"
unfolding D_def by (subst sum.reindex) (auto simp: inj_on_def nat_add_distrib)
also have "… = (∑k∈{m<..n}. f k)"
by (intro sum.reindex_bij_witness[of _ "λx. x - 1" Suc]) auto
finally show ?thesis .
qed auto
subsection ‹Complex analysis›
lemma analytic_imp_contour_integrable:
"f analytic_on path_image g ⟹ valid_path g ⟹ f contour_integrable_on g"
using contour_integrable_holomorphic_simple[of f _ g]
by (metis analytic_on_holomorphic)
lemma contour_integral_rectpath:
assumes "f analytic_on path_image (rectpath a b)"
shows "contour_integral (rectpath a b) f =
contour_integral (linepath a (Complex (Re b) (Im a))) f +
contour_integral (linepath (Complex (Re b) (Im a)) b) f +
contour_integral (linepath b (Complex (Re a) (Im b))) f +
contour_integral (linepath (Complex (Re a) (Im b)) a) f"
proof -
have *: "A ⊆ B ∪ C" if "(A :: complex set) ⊆ B ∨ A ⊆ C" for A B C
using that by blast
show ?thesis
unfolding rectpath_def Let_def
by (simp add: analytic_imp_contour_integrable[OF analytic_on_subset[OF assms]]
rectpath_def Let_def path_image_join *)
qed
lemma contour_integral_bound_linepath':
"⟦f contour_integrable_on (linepath a b);
0 ≤ B; ⋀x. x ∈ closed_segment a b ⟹ norm(f x) ≤ B; c = norm (b - a)⟧
⟹ norm(contour_integral (linepath a b) f) ≤ B * c"
using contour_integral_bound_linepath by metis
lemma contour_integral_linepath_same_Im:
assumes "Im z = T" "Im z' = T" "Re z = a" "Re z' = b" "a < b"
shows "contour_integral (linepath z z') f =
integral {a..b} (λx. f (Complex x T))"
proof -
have "contour_integral (((+) (𝗂 * of_real T)) ∘ linepath (of_real a) (of_real b)) f =
contour_integral (linepath (of_real a) (of_real b)) (λx. f (x + 𝗂 * of_real T))"
by (subst contour_integral_translate) auto
also have "… = integral {a..b} (λx. f (complex_of_real x + 𝗂 * complex_of_real T))"
by (subst contour_integral_linepath_Reals_eq) (use ‹a < b› in auto)
also have "(λx. complex_of_real x + 𝗂 * complex_of_real T) = (λx. Complex x T)"
by (auto simp: complex_eq_iff)
also have "((+) (𝗂 * of_real T)) ∘ linepath (of_real a) (of_real b) = linepath z z'"
using assms by (auto simp: fun_eq_iff complex_eq_iff algebra_simps linepath_def)
finally show ?thesis .
qed
lemma contour_integral_linepath_same_Re:
assumes "Re z = c" "Re z' = c" "Im z = a" "Im z' = b" "a < b"
shows "contour_integral (linepath z z') f =
𝗂 * integral {a..b} (λx. f (Complex c x))"
proof -
have zz': "z = Complex c a" "z' = Complex c b"
using assms by (auto simp: complex_eq_iff)
have "contour_integral (linepath z z') f =
(z' - z) * integral {0..1} (λx. f (linepath z z' x))"
by (simp add: contour_integral_integral)
also have "z' - z = 𝗂 * of_real (b - a)"
by (simp add: zz' Complex_eq algebra_simps)
also have "integral {0..1} (λx. f (linepath z z' x)) =
integral {0..1} (λx. f (Complex c (linepath a b x)))"
by (simp add: linepath_def Complex_eq scaleR_conv_of_real algebra_simps zz')
also have "… = integral {0..(b - a) / (b - a)} (λx. f (Complex c (a + (b - a) * x)))"
using ‹a < b› by (simp add: algebra_simps linepath_def)
also have "{0..(b - a) / (b - a)} = (λx. x / (b - a)) ` {0..b - a}"
using ‹a < b› by simp
also have "integral … (λx. f (Complex c (a + (b - a) * x))) =
integral {a-a..b-a} (λx. f (Complex c (x + a))) / of_real (b - a)"
using ‹a < b› by (subst integral_stretch_real) (auto simp: scaleR_conv_of_real add_ac)
also have "… = integral {a..b} (λx. f (Complex c x)) / of_real (b - a)"
by (subst integral_shift_real_ivl) (rule refl)
finally show ?thesis
using ‹a < b› by simp
qed
lemma continuous_on_Complex [continuous_intros]:
assumes "continuous_on A f" "continuous_on A g"
shows "continuous_on A (λx. Complex (f x) (g x))"
unfolding Complex_eq by (intro continuous_intros assms)
lemma contour_integral_primitive':
assumes "⋀x. x ∈ S ⟹ (f has_field_derivative f' x) (at x within S)"
and "valid_path g" "path_image g ⊆ S" "pathfinish g = b" "pathstart g = a"
shows "(f' has_contour_integral (f b - f a)) g"
using contour_integral_primitive[OF assms(1-3)] assms(4,5) by simp
lemma fds_converges_0_imp_summable_fds_nth:
assumes "fds_converges f 0"
shows "summable (fds_nth f)"
proof -
from assms have "summable (λn. fds_nth f n / nat_power n 0)"
by (simp add: fds_converges_def)
also have "eventually (λn. fds_nth f n / nat_power n 0 = fds_nth f n) at_top"
using eventually_gt_at_top[of 0] by eventually_elim auto
hence "summable (λn. fds_nth f n / nat_power n 0) ⟷ summable (λn. fds_nth f n)"
by (intro summable_cong)
finally show ?thesis .
qed
lemma contour_integral_rmul: "contour_integral g (λx. f x * c) = contour_integral g f * c"
proof (cases "c = 0")
case [simp]: False
show ?thesis
proof (cases "f contour_integrable_on g")
case True
thus ?thesis
by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_rmul)
next
case False
thus ?thesis
using contour_integrable_rmul_iff not_integrable_contour_integral by force
qed
qed auto
lemma contour_integral_lmul: "contour_integral g (λx. c * f x) = c * contour_integral g f"
by (subst (1 2) mult.commute) (rule contour_integral_rmul)
lemma contour_integral_divide: "contour_integral g (λx. f x / c) = contour_integral g f / c"
using contour_integral_rmul[of g f "inverse c"] by (simp add: field_simps)
lemma uniform_limit_contour_integral_linepath:
assumes u: "uniform_limit (path_image (linepath a b)) f g F"
assumes c: "⋀n. continuous_on (path_image (linepath a b)) (f n)"
assumes [simp]: "F ≠ bot"
obtains I J where
"⋀n. (f n has_contour_integral I n) (linepath a b)"
"(g has_contour_integral J) (linepath a b)"
"(I ⤏ J) F"
proof (rule uniform_limit_integral)
note [continuous_intros] = continuous_on_compose2[OF c]
show "uniform_limit {0..1} (λx t. f x (linepath a b t) * (b - a))
(λt. g (linepath a b t) * (b - a)) F"
proof (rule uniform_limit_intros)
show "uniform_limit {0..1} (λx t. f x (linepath a b t))
(λt. g (linepath a b t)) F"
using u unfolding path_image_def by (rule uniform_limit_compose') auto
qed
show "continuous_on {0..1} (λt. f n (linepath a b t) * (b - a))" for n
by (intro continuous_intros; unfold path_image_def) auto
fix I J
assume I: "⋀n. ((λt. f n (linepath a b t) * (b - a)) has_integral I n) {0..1}"
and J: "((λt. g (linepath a b t) * (b - a)) has_integral J) {0..1}"
and lim: "(I ⤏ J) F"
show ?thesis
by (rule that[of I J]) (use I J lim in ‹auto simp: has_contour_integral›)
qed auto
lemma contour_integral_sums_linepath:
assumes u: "uniform_limit (closed_segment a b) (λN w. ∑n<N. f n w) g sequentially"
assumes c: "⋀n. continuous_on (closed_segment a b) (f n)"
obtains J where
"(g has_contour_integral J) (linepath a b)"
"(λn. contour_integral (linepath a b) (f n)) sums J"
proof (rule uniform_limit_contour_integral_linepath)
show "uniform_limit (path_image (linepath a b)) (λN w. ∑n<N. f n w) g sequentially"
using u by simp
next
show "continuous_on (path_image (linepath a b)) (λw. ∑n<N. f n w)" for N
by (intro continuous_intros continuous_on_subset[OF c]) simp_all
next
fix I J
assume 1: "⋀N. ((λw. ∑n<N. f n w) has_contour_integral I N) (linepath a b)"
assume 2: "(g has_contour_integral J) (linepath a b)" and 3: "(I ⤏ J) sequentially"
have 4: "I = (λN. (∑n<N. contour_integral (linepath a b) (f n)))"
proof
fix N :: nat
have "f n contour_integrable_on (linepath a b)" for n
by (intro contour_integrable_continuous_linepath assms)
hence "((λw. ∑n<N. f n w) has_contour_integral
(∑n<N. contour_integral (linepath a b) (f n))) (linepath a b)"
using c by (intro has_contour_integral_sum) (simp_all add: has_contour_integral_integral)
with 1[of N] show "I N = (∑n<N. contour_integral (linepath a b) (f n))"
using contour_integral_unique by metis
qed
have 5: "(λn. contour_integral (linepath a b) (f n)) sums J"
using 1 2 3 4 unfolding sums_def by blast
from that[OF 2 5] show ?thesis .
qed auto
subsection ‹Dirichlet series›
lemma uniform_limit_eval_fds:
fixes f :: "'a :: dirichlet_series fds"
assumes "compact B" "⋀z. z ∈ B ⟹ conv_abscissa f < ereal (z ∙ 1)"
shows "uniform_limit B (λN z. ∑n≤N. fds_nth f n / nat_power n z) (eval_fds f) sequentially"
proof -
define g where "g = (λN z. ∑n≤N. fds_nth f n / nat_power n z)"
from assms have "uniformly_convergent_on B g"
unfolding g_def by (rule uniformly_convergent_eval_fds)
then obtain l where l: "uniform_limit B g l sequentially"
unfolding uniformly_convergent_on_def by blast
also have "?this ⟷ uniform_limit B g (eval_fds f) sequentially"
proof (intro uniform_limit_cong)
fix z assume z: "z ∈ B"
from tendsto_uniform_limitI[OF l z] have "(λy. g y z) ⇢ l z" .
hence "(λn. fds_nth f n / nat_power n z) sums l z"
by (simp add: g_def sums_def_le)
thus "l z = eval_fds f z"
by (simp add: eval_fds_def sums_iff)
qed auto
finally show ?thesis
by (simp add: g_def)
qed
lemma uniform_limit_eval_fds':
fixes f :: "'a :: dirichlet_series fds"
assumes "compact B" "⋀z. z ∈ B ⟹ conv_abscissa f < ereal (z ∙ 1)"
shows "uniform_limit B (λN z. ∑n<N. fds_nth f n / nat_power n z) (eval_fds f) sequentially"
proof -
have "uniform_limit B (λN z. ∑n≤N. fds_nth f n / nat_power n z) (eval_fds f) sequentially"
by (rule uniform_limit_eval_fds) (use assms in auto)
also have "(λN z. ∑n≤N. fds_nth f n / nat_power n z) =
(λN z. ∑n<Suc N. fds_nth f n / nat_power n z)"
by (intro ext sum.cong) auto
finally have "uniform_limit B (λN z. ∑n<N. fds_nth f n / nat_power n z)
(eval_fds f) (filtermap Suc sequentially)"
by (simp add: uniform_limit_iff eventually_filtermap)
also have "filtermap Suc sequentially = sequentially"
by (simp add: eventually_filtermap filter_eq_iff)
finally show ?thesis .
qed
lemma conv_abscissa_shift [simp]:
"conv_abscissa (fds_shift c f) = conv_abscissa (f :: 'a :: dirichlet_series fds) + c ∙ 1"
proof -
have "conv_abscissa (fds_shift c f) ≤ conv_abscissa f + c ∙ 1" for c :: 'a and f
proof (rule conv_abscissa_leI)
fix d assume "conv_abscissa f + c ∙ 1 < ereal d"
hence "conv_abscissa f < ereal (d - c ∙ 1)" by (cases "conv_abscissa f") auto
hence "fds_converges (fds_shift c f) (of_real d)"
by (auto intro!: fds_converges_shift fds_converges simp: algebra_simps)
thus "∃s. s ∙ 1 = d ∧ fds_converges (fds_shift c f) s"
by (auto intro!: exI[of _ "of_real d"])
qed
note * = this[of c f] this[of "-c" "fds_shift c f"]
show ?thesis by (cases "conv_abscissa (fds_shift c f)"; cases "conv_abscissa f")
(insert *, auto intro!: antisym)
qed
lemma abs_conv_abscissa_fds_zeta [simp]:
"abs_conv_abscissa (fds_zeta :: 'a :: dirichlet_series fds) = 1"
proof -
have "abs_conv_abscissa (fds_zeta :: 'a fds) = Inf (ereal ` (λx. x ∙ 1) ` {s::'a. 1 < s ∙ 1})"
by (simp add: abs_conv_abscissa_def image_image o_def)
also have "(λx. x ∙ 1) ` {s::'a. 1 < s ∙ 1} = {1<..}"
proof safe
fix x :: real
assume "x > 1"
show "x ∈ (λx. x ∙ 1) ` {s::'a. 1 < s ∙ 1}"
by (rule image_eqI[of _ _ "of_real x"]) (use ‹x > 1› in auto)
qed
also have "ereal ` {1<..} = {1<..<∞}"
proof safe
fix x :: ereal assume x: "x ∈ {1<..<∞}"
show "x ∈ ereal ` {1<..}"
using x by (cases x) (auto simp: image_def)
qed auto
also have "Inf … = 1"
by simp
finally show ?thesis .
qed
end