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
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
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