Theory Prime_Number_Theorem_Library
section ‹Auxiliary material›
theory Prime_Number_Theorem_Library
imports
Zeta_Function.Zeta_Function
"HOL-Real_Asymp.Real_Asymp"
begin
text ‹Conflicting notation from \<^theory>‹HOL-Analysis.Infinite_Sum››
no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
lemma homotopic_loopsI:
fixes h :: "real × real ⇒ _"
assumes "continuous_on ({0..1} × {0..1}) h"
"h ` ({0..1} × {0..1}) ⊆ s"
"⋀x. x ∈ {0..1} ⟹ h (0, x) = p x"
"⋀x. x ∈ {0..1} ⟹ h (1, x) = q x"
"⋀x. x ∈ {0..1} ⟹ pathfinish (h ∘ Pair x) = pathstart (h ∘ Pair x)"
shows "homotopic_loops s p q"
using assms unfolding homotopic_loops by (intro exI[of _ h]) auto
lemma homotopic_pathsI:
fixes h :: "real × real ⇒ _"
assumes "continuous_on ({0..1} × {0..1}) h"
assumes "h ` ({0..1} × {0..1}) ⊆ s"
assumes "⋀x. x ∈ {0..1} ⟹ h (0, x) = p x"
assumes "⋀x. x ∈ {0..1} ⟹ h (1, x) = q x"
assumes "⋀x. x ∈ {0..1} ⟹ pathstart (h ∘ Pair x) = pathstart p"
assumes "⋀x. x ∈ {0..1} ⟹ pathfinish (h ∘ Pair x) = pathfinish p"
shows "homotopic_paths s p q"
using assms unfolding homotopic_paths by (intro exI[of _ h]) auto
lemma sum_upto_ln_conv_sum_upto_mangoldt:
"sum_upto (λn. ln (real n)) x = sum_upto (λn. mangoldt n * nat ⌊x / real n⌋) x"
proof -
have "sum_upto (λn. ln (real n)) x =
sum_upto (λn. ∑d | d dvd n. mangoldt d) x"
by (intro sum_upto_cong) (simp_all add: mangoldt_sum)
also have "… = sum_upto (λk. sum_upto (λd. mangoldt k) (x / real k)) x"
by (rule sum_upto_sum_divisors)
also have "… = sum_upto (λn. mangoldt n * nat ⌊x / real n⌋) x"
unfolding sum_upto_altdef by (simp add: mult_ac)
finally show ?thesis .
qed
lemma ln_fact_conv_sum_upto_mangoldt:
"ln (fact n) = sum_upto (λk. mangoldt k * (n div k)) n"
proof -
have [simp]: "{0<..Suc n} = insert (Suc n) {0<..n}" for n by auto
have "ln (fact n) = sum_upto (λn. ln (real n)) n"
by (induction n) (auto simp: sum_upto_altdef nat_add_distrib ln_mult)
also have "… = sum_upto (λk. mangoldt k * (n div k)) n"
unfolding sum_upto_ln_conv_sum_upto_mangoldt
by (intro sum_upto_cong) (auto simp: floor_divide_of_nat_eq)
finally show ?thesis .
qed
lemma fds_abs_converges_comparison_test:
fixes s :: "'a :: dirichlet_series"
assumes "eventually (λn. norm (fds_nth f n) ≤ fds_nth g n) at_top" and "fds_converges g (s ∙ 1)"
shows "fds_abs_converges f s"
unfolding fds_abs_converges_def
proof (rule summable_comparison_test_ev)
from assms(2) show "summable (λn. fds_nth g n / n powr (s ∙ 1))"
by (auto simp: fds_converges_def)
from assms(1) eventually_gt_at_top[of 0]
show "eventually (λn. norm (norm (fds_nth f n / nat_power n s)) ≤
fds_nth g n / real n powr (s ∙ 1)) at_top"
by eventually_elim (auto simp: norm_divide norm_nat_power intro!: divide_right_mono)
qed
lemma fds_converges_scaleR [intro]:
assumes "fds_converges f s"
shows "fds_converges (c *⇩R f) s"
proof -
from assms have "summable (λn. c *⇩R (fds_nth f n / nat_power n s))"
by (intro summable_scaleR_right) (auto simp: fds_converges_def)
also have "(λn. c *⇩R (fds_nth f n / nat_power n s)) = (λn. (c *⇩R fds_nth f n / nat_power n s))"
by (simp add: scaleR_conv_of_real)
finally show ?thesis by (simp add: fds_converges_def)
qed
lemma fds_abs_converges_scaleR [intro]:
assumes "fds_abs_converges f s"
shows "fds_abs_converges (c *⇩R f) s"
proof -
from assms have "summable (λn. abs c * norm (fds_nth f n / nat_power n s))"
by (intro summable_mult) (auto simp: fds_abs_converges_def)
also have "(λn. abs c * norm (fds_nth f n / nat_power n s)) =
(λn. norm ((c *⇩R fds_nth f n) / nat_power n s))" by (simp add: norm_divide)
finally show ?thesis by (simp add: fds_abs_converges_def)
qed
lemma conv_abscissa_scaleR: "conv_abscissa (scaleR c f) ≤ conv_abscissa f"
by (rule conv_abscissa_mono) auto
lemma abs_conv_abscissa_scaleR: "abs_conv_abscissa (scaleR c f) ≤ abs_conv_abscissa f"
by (rule abs_conv_abscissa_mono) auto
lemma fds_abs_converges_mult_const_left [intro]:
"fds_abs_converges f s ⟹ fds_abs_converges (fds_const c * f) s"
by (auto simp: fds_abs_converges_def norm_mult norm_divide dest: summable_mult[of _ "norm c"])
lemma conv_abscissa_mult_const_left:
"conv_abscissa (fds_const c * f) ≤ conv_abscissa f"
by (intro conv_abscissa_mono) auto
lemma abs_conv_abscissa_mult_const_left:
"abs_conv_abscissa (fds_const c * f) ≤ abs_conv_abscissa f"
by (intro abs_conv_abscissa_mono) auto
lemma fds_abs_converges_mult_const_right [intro]:
"fds_abs_converges f s ⟹ fds_abs_converges (f * fds_const c) s"
by (metis mult.commute fds_abs_converges_mult_const_left)
lemma conv_abscissa_mult_const_right:
"conv_abscissa (f * fds_const c) ≤ conv_abscissa f"
by (intro conv_abscissa_mono) auto
lemma abs_conv_abscissa_mult_const_right:
"abs_conv_abscissa (f * fds_const c) ≤ abs_conv_abscissa f"
by (intro abs_conv_abscissa_mono) auto
lemma bounded_coeffs_imp_fds_abs_converges:
fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
assumes "Bseq (fds_nth f)" "s ∙ 1 > 1"
shows "fds_abs_converges f s"
proof -
from assms obtain C where C: "⋀n. norm (fds_nth f n) ≤ C"
by (auto simp: Bseq_def)
show ?thesis
proof (rule fds_abs_converges_comparison_test)
from ‹s ∙ 1 > 1› show "fds_converges (C *⇩R fds_zeta) (s ∙ 1)"
by (intro fds_abs_converges_imp_converges) auto
from C show "eventually (λn. norm (fds_nth f n) ≤ fds_nth (C *⇩R fds_zeta) n) at_top"
by (intro always_eventually) (auto simp: fds_nth_zeta)
qed
qed
lemma bounded_coeffs_imp_fds_abs_converges':
fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
assumes "Bseq (λn. fds_nth f n * nat_power n s0)" "s ∙ 1 > 1 - s0 ∙ 1"
shows "fds_abs_converges f s"
proof -
have "fds_nth (fds_shift s0 f) = (λn. fds_nth f n * nat_power n s0)"
by (auto simp: fun_eq_iff)
with assms have "Bseq (fds_nth (fds_shift s0 f))" by simp
with assms(2) have "fds_abs_converges (fds_shift s0 f) (s + s0)"
by (intro bounded_coeffs_imp_fds_abs_converges) (auto simp: algebra_simps)
thus ?thesis by simp
qed
lemma bounded_coeffs_imp_abs_conv_abscissa_le:
fixes s :: "'a :: dirichlet_series" and f :: "'a fds" and c :: ereal
assumes "Bseq (λn. fds_nth f n * nat_power n s)" "1 - s ∙ 1 ≤ c"
shows "abs_conv_abscissa f ≤ c"
proof (rule abs_conv_abscissa_leI_weak)
fix x assume "c < ereal x"
have "ereal (1 - s ∙ 1) ≤ c" by fact
also have "… < ereal x" by fact
finally have "1 - s ∙ 1 < ereal x" by simp
thus "fds_abs_converges f (of_real x)"
by (intro bounded_coeffs_imp_fds_abs_converges'[OF assms(1)]) auto
qed
lemma bounded_coeffs_imp_abs_conv_abscissa_le_1:
fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
assumes "Bseq (λn. fds_nth f n)"
shows "abs_conv_abscissa f ≤ 1"
proof -
have [simp]: "fds_nth f n * nat_power n 0 = fds_nth f n" for n
by (cases "n = 0") auto
show ?thesis
by (rule bounded_coeffs_imp_abs_conv_abscissa_le[where s = 0]) (insert assms, auto simp:)
qed
lemma
fixes a b c :: real
assumes ab: "a + b > 0" and c: "c < -1"
shows set_integrable_powr_at_top: "(λx. (b + x) powr c) absolutely_integrable_on {a<..}"
and set_lebesgue_integral_powr_at_top:
"(∫x∈{a<..}. ((b + x) powr c) ∂lborel) = -((b + a) powr (c + 1) / (c + 1))"
and powr_has_integral_at_top:
"((λx. (b + x) powr c) has_integral -((b + a) powr (c + 1) / (c + 1))) {a<..}"
proof -
let ?f = "λx. (b + x) powr c" and ?F = "λx. (b + x) powr (c + 1) / (c + 1)"
have limits: "((?F ∘ real_of_ereal) ⤏ ?F a) (at_right (ereal a))"
"((?F ∘ real_of_ereal) ⤏ 0) (at_left ∞)"
using c ab unfolding ereal_tendsto_simps1 by (real_asymp simp: field_simps)+
have 1: "set_integrable lborel (einterval a ∞) ?f" using ab c limits
by (intro interval_integral_FTC_nonneg) (auto intro!: derivative_eq_intros)
thus 2: "?f absolutely_integrable_on {a<..}"
by (auto simp: set_integrable_def integrable_completion)
have "LBINT x=ereal a..∞. (b + x) powr c = 0 - ?F a" using ab c limits
by (intro interval_integral_FTC_nonneg) (auto intro!: derivative_eq_intros)
thus 3: "(∫x∈{a<..}. ((b + x) powr c) ∂lborel) = -((b + a) powr (c + 1) / (c + 1))"
by (simp add: interval_integral_to_infinity_eq)
show "(?f has_integral -((b + a) powr (c + 1) / (c + 1))) {a<..}"
using set_borel_integral_eq_integral[OF 1] 3 by (simp add: has_integral_iff)
qed
lemma fds_converges_altdef2:
"fds_converges f s ⟷ convergent (λN. eval_fds (fds_truncate N f) s)"
unfolding fds_converges_def summable_iff_convergent' eval_fds_truncate
by (auto simp: not_le intro!: convergent_cong always_eventually sum.mono_neutral_right)
lemma tendsto_eval_fds_truncate:
assumes "fds_converges f s"
shows "(λN. eval_fds (fds_truncate N f) s) ⇢ eval_fds f s"
proof -
have "(λN. eval_fds (fds_truncate N f) s) ⇢ eval_fds f s ⟷
(λN. ∑i≤N. fds_nth f i / nat_power i s) ⇢ eval_fds f s"
unfolding eval_fds_truncate
by (intro filterlim_cong always_eventually allI sum.mono_neutral_left) (auto simp: not_le)
also have … using assms
by (simp add: fds_converges_iff sums_def' atLeast0AtMost)
finally show ?thesis .
qed
lemma linepath_translate_left: "linepath (c + a) (c + a) = (λx. c + a) ∘ linepath a b"
by auto
lemma linepath_translate_right: "linepath (a + c) (b + c) = (λx. x + c) ∘ linepath a b"
by (auto simp: fun_eq_iff linepath_def algebra_simps)
lemma has_contour_integral_linepath_same_Im_iff:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "Im a = Im b" "Re a < Re b"
shows "(f has_contour_integral I) (linepath a b) ⟷
((λx. f (of_real x + Im a * 𝗂)) has_integral I) {Re a..Re b}"
proof -
have deriv: "vector_derivative ((λx. x - Im a * 𝗂) ∘ linepath a b) (at y) = b - a" for y
using linepath_translate_right[of a "-Im a * 𝗂" b, symmetric] by simp
have "(f has_contour_integral I) (linepath a b) ⟷
((λx. f (x + Im a * 𝗂)) has_contour_integral I) (linepath (a - Im a * 𝗂) (b - Im a * 𝗂))"
using linepath_translate_right[of a "-Im a * 𝗂" b] deriv by (simp add: has_contour_integral)
also have "… ⟷ ((λx. f (x + Im a * 𝗂)) has_integral I) {Re a..Re b}" using assms
by (subst has_contour_integral_linepath_Reals_iff) (auto simp: complex_is_Real_iff)
finally show ?thesis .
qed
lemma contour_integrable_linepath_same_Im_iff:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "Im a = Im b" "Re a < Re b"
shows "(f contour_integrable_on linepath a b) ⟷
(λx. f (of_real x + Im a * 𝗂)) integrable_on {Re a..Re b}"
using contour_integrable_on_def has_contour_integral_linepath_same_Im_iff[OF assms] by blast
lemma contour_integral_linepath_same_Im:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "Im a = Im b" "Re a < Re b"
shows "contour_integral (linepath a b) f = integral {Re a..Re b} (λx. f (x + Im a * 𝗂))"
proof (cases "f contour_integrable_on linepath a b")
case True
thus ?thesis using has_contour_integral_linepath_same_Im_iff[OF assms, of f]
using has_contour_integral_integral has_contour_integral_unique by blast
next
case False
thus ?thesis using contour_integrable_linepath_same_Im_iff[OF assms, of f]
by (simp add: not_integrable_contour_integral not_integrable_integral)
qed
lemmas [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1
interpretation cis: periodic_fun_simple cis "2 * pi"
by standard (simp_all add: complex_eq_iff)
lemma analytic_onE_box:
assumes "f analytic_on A" "s ∈ A"
obtains a b where "Re a < Re b" "Im a < Im b" "s ∈ box a b" "f analytic_on box a b"
proof -
from assms obtain r where r: "r > 0" "f holomorphic_on ball s r"
by (auto simp: analytic_on_def)
with open_contains_box[of "ball s r" s] obtain a b
where "box a b ⊆ ball s r" "s ∈ box a b" "∀i∈Basis. a ∙ i < b ∙ i" by auto
moreover from r have "f analytic_on ball s r" by (simp add: analytic_on_open)
ultimately show ?thesis using that[of a b] analytic_on_subset[of _ "ball s r" "box a b"]
by (auto simp: Basis_complex_def)
qed
lemma Re_image_box:
assumes "Re a < Re b" "Im a < Im b"
shows "Re ` box a b = {Re a<..<Re b}"
using inner_image_box[of "1::complex" a b] assms by (auto simp: Basis_complex_def)
lemma Im_image_box:
assumes "Re a < Re b" "Im a < Im b"
shows "Im ` box a b = {Im a<..<Im b}"
using inner_image_box[of "𝗂::complex" a b] assms by (auto simp: Basis_complex_def)
lemma Re_image_cbox:
assumes "Re a ≤ Re b" "Im a ≤ Im b"
shows "Re ` cbox a b = {Re a..Re b}"
using inner_image_cbox[of "1::complex" a b] assms by (auto simp: Basis_complex_def)
lemma Im_image_cbox:
assumes "Re a ≤ Re b" "Im a ≤ Im b"
shows "Im ` cbox a b = {Im a..Im b}"
using inner_image_cbox[of "𝗂::complex" a b] assms by (auto simp: Basis_complex_def)
lemma analytic_onE_cball:
assumes "f analytic_on A" "s ∈ A" "ub > (0::real)"
obtains R where "R > 0" "R < ub" "f analytic_on cball s R"
proof -
from assms obtain r where "r > 0" "f holomorphic_on ball s r"
by (auto simp: analytic_on_def)
hence "f analytic_on ball s r" by (simp add: analytic_on_open)
hence "f analytic_on cball s (min (ub / 2) (r / 2))"
by (rule analytic_on_subset, subst cball_subset_ball_iff) (use ‹r > 0› in auto)
moreover have "min (ub / 2) (r / 2) > 0" and "min (ub / 2) (r / 2) < ub"
using ‹r > 0› and ‹ub > 0› by (auto simp: min_def)
ultimately show ?thesis using that[of "min (ub / 2) (r / 2)"]
by blast
qed
corollary analytic_pre_zeta' [analytic_intros]:
assumes "f analytic_on A" "a > 0"
shows "(λx. pre_zeta a (f x)) analytic_on A"
using analytic_on_compose_gen[OF assms(1) analytic_pre_zeta[of a UNIV]] assms(2)
by (auto simp: o_def)
corollary analytic_hurwitz_zeta' [analytic_intros]:
assumes "f analytic_on A" "(⋀x. x ∈ A ⟹ f x ≠ 1)" "a > 0"
shows "(λx. hurwitz_zeta a (f x)) analytic_on A"
using analytic_on_compose_gen[OF assms(1) analytic_hurwitz_zeta[of a "-{1}"]] assms(2,3)
by (auto simp: o_def)
corollary analytic_zeta' [analytic_intros]:
assumes "f analytic_on A" "(⋀x. x ∈ A ⟹ f x ≠ 1)"
shows "(λx. zeta (f x)) analytic_on A"
using analytic_on_compose_gen[OF assms(1) analytic_zeta[of "-{1}"]] assms(2)
by (auto simp: o_def)
lemma logderiv_zeta_analytic: "(λs. deriv zeta s / zeta s) analytic_on {s. Re s ≥ 1} - {1}"
using zeta_Re_ge_1_nonzero by (auto intro!: analytic_intros)
lemma mult_real_sqrt: "x ≥ 0 ⟹ x * sqrt y = sqrt (x ^ 2 * y)"
by (simp add: real_sqrt_mult)
lemma arcsin_pos: "x ∈ {0<..1} ⟹ arcsin x > 0"
using arcsin_less_arcsin[of 0 x] by simp
lemmas analytic_imp_holomorphic' = holomorphic_on_subset[OF analytic_imp_holomorphic]
lemma residue_simple':
assumes "open s" "0 ∈ s" "f holomorphic_on s"
shows "residue (λw. f w / w) 0 = f 0"
using residue_simple[of s 0 f] assms by simp
lemma fds_converges_cong:
assumes "eventually (λn. fds_nth f n = fds_nth g n) at_top" "s = s'"
shows "fds_converges f s ⟷ fds_converges g s'"
unfolding fds_converges_def
by (intro summable_cong eventually_mono[OF assms(1)]) (simp_all add: assms)
lemma fds_abs_converges_cong:
assumes "eventually (λn. fds_nth f n = fds_nth g n) at_top" "s = s'"
shows "fds_abs_converges f s ⟷ fds_abs_converges g s'"
unfolding fds_abs_converges_def
by (intro summable_cong eventually_mono[OF assms(1)]) (simp_all add: assms)
lemma conv_abscissa_cong:
assumes "eventually (λn. fds_nth f n = fds_nth g n) at_top"
shows "conv_abscissa f = conv_abscissa g"
proof -
have "fds_converges f = fds_converges g"
by (intro ext fds_converges_cong assms refl)
thus ?thesis by (simp add: conv_abscissa_def)
qed
lemma abs_conv_abscissa_cong:
assumes "eventually (λn. fds_nth f n = fds_nth g n) at_top"
shows "abs_conv_abscissa f = abs_conv_abscissa g"
proof -
have "fds_abs_converges f = fds_abs_converges g"
by (intro ext fds_abs_converges_cong assms refl)
thus ?thesis by (simp add: abs_conv_abscissa_def)
qed
definition fds_remainder where
"fds_remainder m = fds_subseries (λn. n > m)"
lemma fds_nth_remainder: "fds_nth (fds_remainder m f) = (λn. if n > m then fds_nth f n else 0)"
by (simp add: fds_remainder_def fds_subseries_def fds_nth_fds')
lemma fds_converges_remainder_iff [simp]:
"fds_converges (fds_remainder m f) s ⟷ fds_converges f s"
by (intro fds_converges_cong eventually_mono[OF eventually_gt_at_top[of m]])
(auto simp: fds_nth_remainder)
lemma fds_abs_converges_remainder_iff [simp]:
"fds_abs_converges (fds_remainder m f) s ⟷ fds_abs_converges f s"
by (intro fds_abs_converges_cong eventually_mono[OF eventually_gt_at_top[of m]])
(auto simp: fds_nth_remainder)
lemma fds_converges_remainder [intro]:
"fds_converges f s ⟹ fds_converges (fds_remainder m f) s"
and fds_abs_converges_remainder [intro]:
"fds_abs_converges f s ⟹ fds_abs_converges (fds_remainder m f) s"
by simp_all
lemma conv_abscissa_remainder [simp]:
"conv_abscissa (fds_remainder m f) = conv_abscissa f"
by (intro conv_abscissa_cong eventually_mono[OF eventually_gt_at_top[of m]])
(auto simp: fds_nth_remainder)
lemma abs_conv_abscissa_remainder [simp]:
"abs_conv_abscissa (fds_remainder m f) = abs_conv_abscissa f"
by (intro abs_conv_abscissa_cong eventually_mono[OF eventually_gt_at_top[of m]])
(auto simp: fds_nth_remainder)
lemma eval_fds_remainder:
"eval_fds (fds_remainder m f) s = (∑n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)"
(is "_ = suminf (λn. ?f (n + Suc m))")
proof (cases "fds_converges f s")
case False
hence "¬fds_converges (fds_remainder m f) s" by simp
hence "(λx. (λn. fds_nth (fds_remainder m f) n / nat_power n s) sums x) = (λ_. False)"
by (auto simp: fds_converges_def summable_def)
hence "eval_fds (fds_remainder m f) s = (THE _. False)"
by (simp add: eval_fds_def suminf_def)
moreover from False have "¬summable (λn. ?f (n + Suc m))" unfolding fds_converges_def
by (subst summable_iff_shift) auto
hence "(λx. (λn. ?f (n + Suc m)) sums x) = (λ_. False)"
by (auto simp: summable_def)
hence "suminf (λn. ?f (n + Suc m)) = (THE _. False)"
by (simp add: suminf_def)
ultimately show ?thesis by simp
next
case True
hence *: "fds_converges (fds_remainder m f) s" by simp
have "eval_fds (fds_remainder m f) s = (∑n. fds_nth (fds_remainder m f) n / nat_power n s)"
unfolding eval_fds_def ..
also have "… = (∑n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)"
using * unfolding fds_converges_def
by (subst suminf_minus_initial_segment) (auto simp: fds_nth_remainder)
also have "(λn. fds_nth (fds_remainder m f) (n + Suc m)) = (λn. fds_nth f (n + Suc m))"
by (intro ext) (auto simp: fds_nth_remainder)
finally show ?thesis .
qed
lemma fds_truncate_plus_remainder: "fds_truncate m f + fds_remainder m f = f"
by (intro fds_eqI) (auto simp: fds_truncate_def fds_remainder_def fds_subseries_def)
lemma holomorphic_fds_eval' [holomorphic_intros]:
assumes "g holomorphic_on A" "⋀x. x ∈ A ⟹ Re (g x) > conv_abscissa f"
shows "(λx. eval_fds f (g x)) holomorphic_on A"
using holomorphic_on_compose_gen[OF assms(1) holomorphic_fds_eval[OF order.refl, of f]] assms(2)
by (auto simp: o_def)
lemma analytic_fds_eval' [analytic_intros]:
assumes "g analytic_on A" "⋀x. x ∈ A ⟹ Re (g x) > conv_abscissa f"
shows "(λx. eval_fds f (g x)) analytic_on A"
using analytic_on_compose_gen[OF assms(1) analytic_fds_eval[OF order.refl, of f]] assms(2)
by (auto simp: o_def)
lemma continuous_on_linepath [continuous_intros]:
assumes "continuous_on A a" "continuous_on A b" "continuous_on A f"
shows "continuous_on A (λx. linepath (a x) (b x) (f x))"
using assms by (auto simp: linepath_def intro!: continuous_intros assms)
lemma continuous_on_part_circlepath [continuous_intros]:
assumes "continuous_on A c" "continuous_on A r" "continuous_on A a" "continuous_on A b"
"continuous_on A f"
shows "continuous_on A (λx. part_circlepath (c x) (r x) (a x) (b x) (f x))"
using assms by (auto simp: part_circlepath_def intro!: continuous_intros assms)
lemma homotopic_loops_part_circlepath:
assumes "sphere c r ⊆ A" and "r ≥ 0" and
"b1 = a1 + 2 * of_int k * pi" and "b2 = a2 + 2 * of_int k * pi"
shows "homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)"
proof -
define h where "h = (λ(x,y). part_circlepath c r (linepath a1 a2 x) (linepath b1 b2 x) y)"
show ?thesis
proof (rule homotopic_loopsI)
show "continuous_on ({0..1} × {0..1}) h"
by (auto simp: h_def case_prod_unfold intro!: continuous_intros)
next
from assms have "h ` ({0..1} × {0..1}) ⊆ sphere c r"
by (auto simp: h_def part_circlepath_def dist_norm norm_mult)
also have "… ⊆ A" by fact
finally show "h ` ({0..1} × {0..1}) ⊆ A" .
next
fix x :: real assume x: "x ∈ {0..1}"
show "h (0, x) = part_circlepath c r a1 b1 x" and "h (1, x) = part_circlepath c r a2 b2 x"
by (simp_all add: h_def linepath_def)
have "cis (pi * (real_of_int k * 2)) = 1"
using cis.plus_of_int[of 0 k] by (simp add: algebra_simps)
thus "pathfinish (h ∘ Pair x) = pathstart (h ∘ Pair x)"
by (simp add: h_def o_def exp_eq_polar linepath_def algebra_simps
cis_mult [symmetric] cis_divide [symmetric] assms)
qed
qed
lemma part_circlepath_conv_subpath:
"part_circlepath c r a b = subpath (a / (2*pi)) (b / (2*pi)) (circlepath c r)"
by (simp add: part_circlepath_def circlepath_def subpath_def linepath_def algebra_simps exp_eq_polar)
lemma homotopic_paths_part_circlepath:
assumes "a ≤ b" "b ≤ c"
assumes "path_image (part_circlepath C r a c) ⊆ A" "r ≥ 0"
shows "homotopic_paths A (part_circlepath C r a c)
(part_circlepath C r a b +++ part_circlepath C r b c)"
(is "homotopic_paths _ ?g (?h1 +++ ?h2)")
proof (cases "a = c")
case False
with assms have "a < c" by simp
define slope where "slope = (b - a) / (c - a)"
from assms and ‹a < c› have slope: "slope ∈ {0..1}"
by (auto simp: field_simps slope_def)
define f :: "real ⇒ real" where
"f = linepath 0 slope +++ linepath slope 1"
show ?thesis
proof (rule homotopic_paths_reparametrize)
fix t :: real assume t: "t ∈ {0..1}"
show "(?h1 +++ ?h2) t = ?g (f t)"
proof (cases "t ≤ 1 / 2")
case True
hence "?g (f t) = C + r * cis ((1 - f t) * a + f t * c)"
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
also from True ‹a < c› have "(1 - f t) * a + f t * c = (1 - 2 * t) * a + 2 * t * b"
unfolding f_def slope_def linepath_def joinpaths_def
by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
(simp add: algebra_simps)?
also from True have "C + r * cis … = (?h1 +++ ?h2) t"
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
finally show ?thesis ..
next
case False
hence "?g (f t) = C + r * cis ((1 - f t) * a + f t * c)"
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
also from False ‹a < c› have "(1 - f t) * a + f t * c = (2 - 2 * t) * b + (2 * t - 1) * c"
unfolding f_def slope_def linepath_def joinpaths_def
by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
(simp add: algebra_simps)?
also from False have "C + r * cis … = (?h1 +++ ?h2) t"
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
finally show ?thesis ..
qed
next
from slope have "path_image f ⊆ {0..1}"
by (auto simp: f_def path_image_join closed_segment_eq_real_ivl)
thus "f ∈ {0..1} → {0..1}" by (force simp add: path_image_def)
next
have "path f" unfolding f_def by auto
thus "continuous_on {0..1} f" by (simp add: path_def)
qed (insert assms, auto simp: f_def joinpaths_def linepath_def)
next
case [simp]: True
with assms have [simp]: "b = c" by auto
have "part_circlepath C r c c +++ part_circlepath C r c c = part_circlepath C r c c"
by (simp add: fun_eq_iff joinpaths_def part_circlepath_def)
thus ?thesis using assms by simp
qed
lemma path_image_part_circlepath_subset:
assumes "a ≤ a'" "a' ≤ b'" "b' ≤ b"
shows "path_image (part_circlepath c r a' b') ⊆ path_image (part_circlepath c r a b)"
using assms by (subst (1 2) path_image_part_circlepath) auto
lemma part_circlepath_mirror:
assumes "a' = a + pi + 2 * pi * of_int k" "b' = b + pi + 2 * pi * of_int k" "c' = -c"
shows "-part_circlepath c r a b = part_circlepath c' r a' b'"
proof
fix x :: real
have "part_circlepath c' r a' b' x = c' + r * cis (linepath a b x + pi + k * (2 * pi))"
by (simp add: part_circlepath_def exp_eq_polar assms linepath_translate_right mult_ac)
also have "cis (linepath a b x + pi + k * (2 * pi)) = cis (linepath a b x + pi)"
by (rule cis.plus_of_int)
also have "… = -cis (linepath a b x)"
by (simp add: minus_cis)
also have "c' + r * … = -part_circlepath c r a b x"
by (simp add: part_circlepath_def assms exp_eq_polar)
finally show "(- part_circlepath c r a b) x = part_circlepath c' r a' b' x"
by simp
qed
lemma path_mirror [intro]: "path (g :: _ ⇒ 'b::topological_group_add) ⟹ path (-g)"
by (auto simp: path_def intro!: continuous_intros)
lemma path_mirror_iff [simp]: "path (-g :: _ ⇒ 'b::topological_group_add) ⟷ path g"
using path_mirror[of g] path_mirror[of "-g"] by (auto simp: fun_Compl_def)
lemma valid_path_mirror [intro]: "valid_path g ⟹ valid_path (-g)"
by (auto simp: valid_path_def fun_Compl_def piecewise_C1_differentiable_neg)
lemma valid_path_mirror_iff [simp]: "valid_path (-g) ⟷ valid_path g"
using valid_path_mirror[of g] valid_path_mirror[of "-g"] by (auto simp: fun_Compl_def)
lemma pathstart_mirror [simp]: "pathstart (-g) = -pathstart g"
and pathfinish_mirror [simp]: "pathfinish (-g) = -pathfinish g"
by (simp_all add: pathstart_def pathfinish_def)
lemma path_image_mirror: "path_image (-g) = uminus ` path_image g"
by (auto simp: path_image_def)
lemma cos_le_zero:
assumes "x ∈ {pi/2..3*pi/2}"
shows "cos x ≤ 0"
proof -
have "cos x = -cos (x - pi)" by (simp add: cos_diff)
moreover from assms have "cos (x - pi) ≥ 0"
by (intro cos_ge_zero) auto
ultimately show ?thesis by simp
qed
lemma cos_le_zero': "x ∈ {-3*pi/2..-pi/2} ⟹ cos x ≤ 0"
using cos_le_zero[of "-x"] by simp
lemma winding_number_join_pos_combined':
"⟦valid_path γ1 ∧ z ∉ path_image γ1 ∧ 0 < Re (winding_number γ1 z);
valid_path γ2 ∧ z ∉ path_image γ2 ∧ 0 < Re (winding_number γ2 z);
pathfinish γ1 = pathstart γ2⟧
⟹ valid_path(γ1 +++ γ2) ∧ z ∉ path_image(γ1 +++ γ2) ∧ 0 < Re(winding_number(γ1 +++ γ2) z)"
by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path)
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"
assumes mn: "m < n"
shows "((λx. f (nat ⌊x⌋)) has_integral sum f {m..<n}) {real m..real n}"
proof -
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
lemma nat_sum_has_integral_ceiling:
fixes f :: "nat ⇒ 'a :: banach"
assumes mn: "m < n"
shows "((λx. f (nat ⌈x⌉)) has_integral sum f {m<..n}) {real m..real n}"
proof -
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
lemma zeta_partial_sum_le:
fixes x :: real and m :: nat
assumes x: "x ∈ {0<..1}"
shows "(∑k=1..m. real k powr (x - 1)) ≤ real m powr x / x"
proof -
consider "m = 0" | "m = 1" | "m > 1" by force
thus ?thesis
proof cases
assume m: "m > 1"
hence "{1..m} = insert 1 {1<..m}" by auto
also have "(∑k∈…. real k powr (x - 1)) = 1 + (∑k∈{1<..m}. real k powr (x - 1))"
by simp
also have "(∑k∈{1<..m}. real k powr (x - 1)) ≤ real m powr x / x - 1 / x"
proof (rule has_integral_le)
show "((λt. (nat ⌈t⌉) powr (x - 1)) has_integral (∑n∈{1<..m}. n powr (x - 1))) {real 1..m}"
using m by (intro nat_sum_has_integral_ceiling) auto
next
have "((λt. t powr (x - 1)) has_integral (real m powr x / x - real 1 powr x / x))
{real 1..real m}"
by (intro fundamental_theorem_of_calculus)
(insert x m, auto simp flip: has_real_derivative_iff_has_vector_derivative
intro!: derivative_eq_intros)
thus "((λt. t powr (x - 1)) has_integral (real m powr x / x - 1 / x)) {real 1..real m}"
by simp
qed (insert x, auto intro!: powr_mono2')
also have "1 + (real m powr x / x - 1 / x) ≤ real m powr x / x"
using x by (simp add: field_simps)
finally show ?thesis by simp
qed (use assms in auto)
qed
lemma zeta_partial_sum_le':
fixes x :: real and m :: nat
assumes x: "x > 0" and m: "m > 0"
shows "(∑n=1..m. real n powr (x - 1)) ≤ m powr x * (1 / x + 1 / m)"
proof (cases "x > 1")
case False
with assms have "(∑n=1..m. real n powr (x - 1)) ≤ m powr x / x"
by (intro zeta_partial_sum_le) auto
also have "… ≤ m powr x * (1 / x + 1 / m)"
using assms by (simp add: field_simps)
finally show ?thesis .
next
case True
have "(∑n∈{1..m}. n powr (x - 1)) = (∑n∈insert m {0..<m}. n powr (x - 1))"
by (intro sum.mono_neutral_left) auto
also have "… = m powr (x - 1) + (∑n∈{0..<m}. n powr (x - 1))" by simp
also have "(∑n∈{0..<m}. n powr (x - 1)) ≤ real m powr x / x"
proof (rule has_integral_le)
show "((λt. (nat ⌊t⌋) powr (x - 1)) has_integral (∑n∈{0..<m}. n powr (x - 1))) {real 0..m}"
using m by (intro nat_sum_has_integral_floor) auto
next
show "((λt. t powr (x - 1)) has_integral (real m powr x / x)) {real 0..real m}"
using has_integral_powr_from_0[of "x - 1"] x by auto
next
fix t assume "t ∈ {real 0..real m}"
with ‹x > 1› show "real (nat ⌊t⌋) powr (x - 1) ≤ t powr (x - 1)"
by (cases "t = 0") (auto intro: powr_mono2)
qed
also have "m powr (x - 1) + m powr x / x = m powr x * (1 / x + 1 / m)"
using m x by (simp add: powr_diff field_simps)
finally show ?thesis by simp
qed
lemma natfun_bigo_1E:
assumes "(f :: nat ⇒ _) ∈ O(λ_. 1)"
obtains C where "C ≥ lb" "⋀n. norm (f n) ≤ C"
proof -
from assms obtain C N where "∀n≥N. norm (f n) ≤ C"
by (auto elim!: landau_o.bigE simp: eventually_at_top_linorder)
hence *: "norm (f n) ≤ Max ({C, lb} ∪ (norm ` f ` {..<N}))" for n
by (cases "n ≥ N") (subst Max_ge_iff; force simp: image_iff)+
moreover have "Max ({C, lb} ∪ (norm ` f ` {..<N})) ≥ lb"
by (intro Max.coboundedI) auto
ultimately show ?thesis using that by blast
qed
lemma natfun_bigo_iff_Bseq: "f ∈ O(λ_. 1) ⟷ Bseq f"
proof
assume "Bseq f"
then obtain C where "C > 0" "⋀n. norm (f n) ≤ C" by (auto simp: Bseq_def)
thus "f ∈ O(λ_. 1)" by (intro bigoI[of _ C]) auto
next
assume "f ∈ O(λ_. 1)"
from natfun_bigo_1E[OF this, where lb = 1] obtain C where "C ≥ 1" "⋀n. norm (f n) ≤ C"
by auto
thus "Bseq f" by (auto simp: Bseq_def intro!: exI[of _ C])
qed
lemma enn_decreasing_sum_le_set_nn_integral:
fixes f :: "real ⇒ ennreal"
assumes decreasing: "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ f y ≤ f x"
shows "(∑n. f (real (Suc n))) ≤ set_nn_integral lborel {0..} f"
proof -
have "(∑n. (f (Suc n))) =
(∑n. ∫⇧+x∈{real n<..real (Suc n)}. (f (Suc n)) ∂lborel)"
by (subst nn_integral_cmult_indicator) auto
also have "nat ⌈x⌉ = Suc n" if "x ∈ {real n<..real (Suc n)}" for x n
using that by (auto simp: nat_eq_iff ceiling_eq_iff)
hence "(∑n. ∫⇧+x∈{real n<..real (Suc n)}. (f (Suc n)) ∂lborel) =
(∑n. ∫⇧+x∈{real n<..real (Suc n)}. (f (real (nat ⌈x⌉))) ∂lborel)"
by (intro suminf_cong nn_integral_cong) (auto simp: indicator_def)
also have "… = (∫⇧+x∈(⋃i. {real i<..real (Suc i)}). (f (nat ⌈x::real⌉)) ∂lborel)"
by (subst nn_integral_disjoint_family)
(auto simp: disjoint_family_on_def)
also have "… ≤ (∫⇧+x∈{0..}. (f x) ∂lborel)"
by (intro nn_integral_mono) (auto simp: indicator_def intro!: decreasing)
finally show ?thesis .
qed
lemma abs_summable_on_uminus_iff:
"(λx. -f x) abs_summable_on A ⟷ f abs_summable_on A"
by (simp add: abs_summable_on_def)
lemma abs_summable_on_cmult_right_iff:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_field, second_countable_topology}"
assumes "c ≠ 0"
shows "(λx. c * f x) abs_summable_on A ⟷ f abs_summable_on A"
by (simp add: abs_summable_on_altdef assms)
lemma abs_summable_on_cmult_left_iff:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_field, second_countable_topology}"
assumes "c ≠ 0"
shows "(λx. f x * c) abs_summable_on A ⟷ f abs_summable_on A"
by (simp add: abs_summable_on_altdef assms)
lemma decreasing_sum_le_integral:
fixes f :: "real ⇒ real"
assumes nonneg: "⋀x. x ≥ 0 ⟹ f x ≥ 0"
assumes decreasing: "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ f y ≤ f x"
assumes integral: "(f has_integral I) {0..}"
shows "summable (λi. f (real (Suc i)))" and "suminf (λi. f (real (Suc i))) ≤ I"
proof -
have [simp]: "I ≥ 0"
by (intro has_integral_nonneg[OF integral] nonneg) auto
have "(∑n. ennreal (f (Suc n))) =
(∑n. ∫⇧+x∈{real n<..real (Suc n)}. ennreal (f (Suc n)) ∂lborel)"
by (subst nn_integral_cmult_indicator) auto
also have "nat ⌈x⌉ = Suc n" if "x ∈ {real n<..real (Suc n)}" for x n
using that by (auto simp: nat_eq_iff ceiling_eq_iff)
hence "(∑n. ∫⇧+x∈{real n<..real (Suc n)}. ennreal (f (Suc n)) ∂lborel) =
(∑n. ∫⇧+x∈{real n<..real (Suc n)}. ennreal (f (real (nat ⌈x⌉))) ∂lborel)"
by (intro suminf_cong nn_integral_cong) (auto simp: indicator_def)
also have "… = (∫⇧+x∈(⋃i. {real i<..real (Suc i)}). ennreal (f (nat ⌈x::real⌉)) ∂lborel)"
by (subst nn_integral_disjoint_family)
(auto simp: disjoint_family_on_def intro!: measurable_completion)
also have "… ≤ (∫⇧+x∈{0..}. ennreal (f x) ∂lborel)"
by (intro nn_integral_mono) (auto simp: indicator_def nonneg intro!: decreasing)
also have "… = (∫⇧+ x. ennreal (indicat_real {0..} x * f x) ∂lborel)"
by (intro nn_integral_cong) (auto simp: indicator_def)
also have "… = ennreal I"
using nn_integral_has_integral_lebesgue[OF nonneg integral] by (auto simp: nonneg)
finally have *: "(∑n. ennreal (f (Suc n))) ≤ ennreal I" .
from * show summable: "summable (λi. f (real (Suc i)))"
by (intro summable_suminf_not_top) (auto simp: top_unique intro: nonneg)
note *
also from summable have "(∑n. ennreal (f (Suc n))) = ennreal (∑n. f (Suc n))"
by (subst suminf_ennreal2) (auto simp: o_def nonneg)
finally show "(∑n. f (real (Suc n))) ≤ I" by (subst (asm) ennreal_le_iff) auto
qed
lemma decreasing_sum_le_integral':
fixes f :: "real ⇒ real"
assumes "⋀x. x ≥ 0 ⟹ f x ≥ 0"
assumes "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ f y ≤ f x"
assumes "(f has_integral I) {0..}"
shows "summable (λi. f (real i))" and "suminf (λi. f (real i)) ≤ f 0 + I"
proof -
have "summable ((λi. f (real (Suc i))))"
using decreasing_sum_le_integral[OF assms] by (simp add: o_def)
thus *: "summable (λi. f (real i))" by (subst (asm) summable_Suc_iff)
have "(∑n. f (real (Suc n))) ≤ I" by (intro decreasing_sum_le_integral assms)
thus "suminf (λi. f (real i)) ≤ f 0 + I"
using * by (subst (asm) suminf_split_head) auto
qed
lemma of_nat_powr_neq_1_complex [simp]:
assumes "n > 1" "Re s ≠ 0"
shows "of_nat n powr s ≠ (1::complex)"
proof -
have "norm (of_nat n powr s) = real n powr Re s"
by (simp add: norm_powr_real_powr)
also have "… ≠ 1"
using assms by (auto simp: powr_def)
finally show ?thesis by auto
qed
lemma fds_logderiv_completely_multiplicative:
fixes f :: "'a :: {real_normed_field} fds"
assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 ≠ 0"
shows "fds_deriv f / f = - fds (λn. fds_nth f n * mangoldt n)"
proof -
have "fds_deriv f / f = - fds (λn. fds_nth f n * mangoldt n) * f / f"
using completely_multiplicative_fds_deriv[of "fds_nth f"] assms by simp
also have "… = - fds (λn. fds_nth f n * mangoldt n)"
using assms by (simp add: divide_fds_def fds_right_inverse)
finally show ?thesis .
qed
lemma fds_nth_logderiv_completely_multiplicative:
fixes f :: "'a :: {real_normed_field} fds"
assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 ≠ 0"
shows "fds_nth (fds_deriv f / f) n = -fds_nth f n * mangoldt n"
using assms by (subst fds_logderiv_completely_multiplicative) (simp_all add: fds_nth_fds')
lemma eval_fds_logderiv_completely_multiplicative:
fixes s :: "'a :: dirichlet_series" and l :: 'a and f :: "'a fds"
defines "h ≡ fds_deriv f / f"
assumes "completely_multiplicative_function (fds_nth f)" and [simp]: "fds_nth f 1 ≠ 0"
assumes "s ∙ 1 > abs_conv_abscissa f"
shows "(λp. of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1))
abs_summable_on {p. prime p}" (is ?th1)
and "eval_fds h s = -(∑⇩ap | prime p. of_real (ln (real p)) *
(1 / (1 - fds_nth f p / nat_power p s) - 1))" (is ?th2)
proof -
let ?P = "{p::nat. prime p}"
interpret f: completely_multiplicative_function "fds_nth f" by fact
have "fds_abs_converges h s"
using abs_conv_abscissa_completely_multiplicative_log_deriv[OF assms(2)] assms
by (intro fds_abs_converges) auto
hence *: "(λn. fds_nth h n / nat_power n s) abs_summable_on UNIV"
by (auto simp: h_def fds_abs_converges_altdef')
note *
also have "(λn. fds_nth h n / nat_power n s) abs_summable_on UNIV ⟷
(λx. -fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow"
unfolding h_def using fds_nth_logderiv_completely_multiplicative[OF assms(2)]
by (intro abs_summable_on_cong_neutral) (auto simp: fds_nth_fds mangoldt_def)
finally have sum1: "(λx. -fds_nth f x * mangoldt x / nat_power x s)
abs_summable_on Collect primepow"
by (rule abs_summable_on_subset) auto
also have "?this ⟷ (λ(p,k). -fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) /
nat_power (p ^ Suc k) s) abs_summable_on (?P × UNIV)"
using bij_betw_primepows unfolding case_prod_unfold
by (intro abs_summable_on_reindex_bij_betw [symmetric])
also have "… ⟷ (λ(p,k). -((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p))))
abs_summable_on (?P × UNIV)"
unfolding case_prod_unfold
by (intro abs_summable_on_cong, subst mangoldt_primepow)
(auto simp: f.mult f.power nat_power_mult_distrib nat_power_power_left power_divide
dest: prime_gt_1_nat)
finally have sum2: … .
have sum4: "summable (λn. (norm (fds_nth f p / nat_power p s)) ^ Suc n)" if p: "prime p" for p
proof -
have "summable (λn. ¦ln (real p)¦ * (norm (fds_nth f p / nat_power p s)) ^ Suc n)"
using p abs_summable_on_Sigma_project2[OF sum2, of p] unfolding abs_summable_on_nat_iff'
by (simp add: norm_power norm_mult norm_divide mult_ac del: power_Suc)
thus ?thesis by (rule summable_mult_D) (insert p, auto dest: prime_gt_1_nat)
qed
have sums: "(λn. (fds_nth f p / nat_power p s) ^ Suc n) sums
(1 / (1 - fds_nth f p / nat_power p s) - 1)" if p: "prime p" for p :: nat
proof -
from sum4[OF p] have "norm (fds_nth f p / nat_power p s) < 1"
unfolding summable_Suc_iff by (simp add: summable_geometric_iff)
from geometric_sums[OF this] show ?thesis by (subst sums_Suc_iff) auto
qed
have eq: "(∑⇩ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) =
-(of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1))"
if p: "prime p" for p
proof -
have "(∑⇩ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) =
(∑⇩ak. (fds_nth f p / nat_power p s) ^ Suc k) * of_real (-ln (real p))"
using sum4[of p] p
by (subst infsetsum_cmult_left [symmetric])
(auto simp: abs_summable_on_nat_iff' norm_power simp del: power_Suc)
also have "(∑⇩ak. (fds_nth f p / nat_power p s) ^ Suc k) =
(1 / (1 - fds_nth f p / nat_power p s) - 1)" using sum4[OF p] sums[OF p]
by (subst infsetsum_nat')
(auto simp: sums_iff abs_summable_on_nat_iff' norm_power simp del: power_Suc)
finally show ?thesis by (simp add: mult_ac)
qed
have sum3: "(λx. ∑⇩ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x))))
abs_summable_on {p. prime p}"
using sum2 by (rule abs_summable_on_Sigma_project1') auto
also have "?this ⟷ (λp. -(of_real (ln (real p)) *
(1 / (1 - fds_nth f p / nat_power p s) - 1))) abs_summable_on {p. prime p}"
by (intro abs_summable_on_cong eq) auto
also have "… ⟷ ?th1" by (subst abs_summable_on_uminus_iff) auto
finally show ?th1 .
have "eval_fds h s = (∑⇩an. fds_nth h n / nat_power n s)"
using * unfolding eval_fds_def by (subst infsetsum_nat') auto
also have "… = (∑⇩an ∈ {n. primepow n}. -fds_nth f n * mangoldt n / nat_power n s)"
unfolding h_def using fds_nth_logderiv_completely_multiplicative[OF assms(2)]
by (intro infsetsum_cong_neutral) (auto simp: fds_nth_fds mangoldt_def)
also have "… = (∑⇩a(p,k)∈(?P × UNIV). -fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) /
nat_power (p ^ Suc k) s)"
using bij_betw_primepows unfolding case_prod_unfold
by (intro infsetsum_reindex_bij_betw [symmetric])
also have "… = (∑⇩a(p,k)∈(?P × UNIV).
-((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))"
by (intro infsetsum_cong)
(auto simp: f.mult f.power mangoldt_def aprimedivisor_prime_power ln_realpow prime_gt_0_nat
nat_power_power_left divide_simps simp del: power_Suc)
also have "… = (∑⇩ap | prime p. ∑⇩ak.
- ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))"
using sum2 by (subst infsetsum_Times) (auto simp: case_prod_unfold)
also have "… = (∑⇩ap | prime p. -(of_real (ln (real p)) *
(1 / (1 - fds_nth f p / nat_power p s) - 1)))"
using eq by (intro infsetsum_cong) auto
finally show ?th2 by (subst (asm) infsetsum_uminus)
qed
lemma eval_fds_logderiv_zeta:
assumes "Re s > 1"
shows "(λp. of_real (ln (real p)) / (p powr s - 1))
abs_summable_on {p. prime p}" (is ?th1)
and "deriv zeta s / zeta s =
-(∑⇩ap | prime p. of_real (ln (real p)) / (p powr s - 1))" (is ?th2)
proof -
have *: "completely_multiplicative_function (fds_nth fds_zeta :: _ ⇒ complex)"
by standard auto
note abscissa = le_less_trans[OF abs_conv_abscissa_completely_multiplicative_log_deriv[OF *]]
have "(λp. ln (real p) * (1 / (1 - fds_nth fds_zeta p / p powr s) - 1))
abs_summable_on {p. prime p}"
using eval_fds_logderiv_completely_multiplicative[OF *, of s] assms by auto
also have "?this ⟷ (λp. ln (real p) / (p powr s - 1)) abs_summable_on {p. prime p}" using assms
by (intro abs_summable_on_cong) (auto simp: fds_nth_zeta divide_simps dest: prime_gt_1_nat)
finally show ?th1 .
from assms have ev: "eventually (λz. z ∈ {z. Re z > 1}) (nhds s)"
by (intro eventually_nhds_in_open open_halfspace_Re_gt) auto
have "deriv zeta s = deriv (eval_fds fds_zeta) s"
by (intro deriv_cong_ev[OF eventually_mono[OF ev]]) (auto simp: eval_fds_zeta)
also have "deriv (eval_fds fds_zeta) s / zeta s = eval_fds (fds_deriv fds_zeta / fds_zeta) s"
using assms zeta_Re_gt_1_nonzero[of s]
by (subst eval_fds_log_deriv) (auto simp: eval_fds_zeta eval_fds_deriv intro!: abscissa)
also have "eval_fds (fds_deriv fds_zeta / fds_zeta) s =
-(∑⇩ap | prime p. ln (real p) * (1 / (1 - fds_nth fds_zeta p / p powr s) - 1))"
(is "_ = -?S") using eval_fds_logderiv_completely_multiplicative[OF *, of s] assms by auto
also have "?S = (∑⇩ap | prime p. ln (real p) / (p powr s - 1))" using assms
by (intro infsetsum_cong) (auto simp: fds_nth_zeta divide_simps dest: prime_gt_1_nat)
finally show ?th2 .
qed
lemma sums_logderiv_zeta:
assumes "Re s > 1"
shows "(λp. if prime p then of_real (ln (real p)) / (of_nat p powr s - 1) else 0) sums
-(deriv zeta s / zeta s)" (is "?f sums _")
proof -
note * = eval_fds_logderiv_zeta[OF assms]
from sums_infsetsum_nat[OF *(1)] and *(2) show ?thesis by simp
qed
lemma range_add_nat: "range (λn. n + c) = {(c::nat)..}"
using Nat.le_imp_diff_is_add by auto
lemma abs_summable_hurwitz_zeta:
assumes "Re s > 1" "a + real b > 0"
shows "(λn. 1 / (of_nat n + a) powr s) abs_summable_on {b..}"
proof -
from assms have "summable (λn. cmod (1 / (of_nat (n + b) + a) powr s))"
using summable_hurwitz_zeta_real[of "Re s" "a + b"]
by (auto simp: norm_divide powr_minus field_simps norm_powr_real_powr)
hence "(λn. 1 / (of_nat (n + b) + a) powr s) abs_summable_on UNIV"
by (auto simp: abs_summable_on_nat_iff' add_ac)
also have "?this ⟷ (λn. 1 / (of_nat n + a) powr s) abs_summable_on range (λn. n + b)"
by (rule abs_summable_on_reindex_iff) auto
also have "range (λn. n + b) = {b..}" by (rule range_add_nat)
finally show ?thesis .
qed
lemma hurwitz_zeta_nat_conv_infsetsum:
assumes "a > 0" and "Re s > 1"
shows "hurwitz_zeta (real a) s = (∑⇩an. of_nat (n + a) powr -s)"
"hurwitz_zeta (real a) s = (∑⇩an∈{a..}. of_nat n powr -s)"
proof -
have "hurwitz_zeta (real a) s = (∑n. of_nat (n + a) powr -s)"
using assms by (subst hurwitz_zeta_conv_suminf) auto
also have "… = (∑⇩an. of_nat (n + a) powr -s)"
using abs_summable_hurwitz_zeta[of s a 0] assms
by (intro infsetsum_nat' [symmetric]) (auto simp: powr_minus field_simps)
finally show "hurwitz_zeta (real a) s = (∑⇩an. of_nat (n + a) powr -s)" .
also have "… = (∑⇩an∈range (λn. n + a). of_nat n powr -s)"
by (rule infsetsum_reindex [symmetric]) auto
also have "range (λn. n + a) = {a..}" by (rule range_add_nat)
finally show "hurwitz_zeta (real a) s = (∑⇩an∈{a..}. of_nat n powr -s)" .
qed
lemma pre_zeta_bound:
assumes "0 < Re s" and a: "a > 0"
shows "norm (pre_zeta a s) ≤ (1 + norm s / Re s) / 2 * a powr -Re s"
proof -
let ?f = "λx. - (s * (x + a) powr (-1-s))"
let ?g' = "λx. norm s * (x + a) powr (-1-Re s)"
let ?g = "λx. -norm s / Re s * (x + a) powr (-Re s)"
define R where "R = EM_remainder 1 ?f 0"
have [simp]: "-Re s - 1 = -1 - Re s" by (simp add: algebra_simps)
have "¦frac x - 1 / 2¦ ≤ 1 / 2" for x :: real unfolding frac_def
by linarith
hence "¦pbernpoly (Suc 0) x¦ ≤ 1 / 2" for x
by (simp add: pbernpoly_def bernpoly_def)
moreover have "((λb. cmod s * (b + a) powr - Re s / Re s) ⤏ 0) at_top"
using ‹Re s > 0› ‹a > 0› by real_asymp
ultimately have *: "∀x. x ≥ real 0 ⟶ norm (EM_remainder 1 ?f (int x)) ≤
(1 / 2) / fact 1 * (-?g (real x))"
using ‹a > 0› ‹Re s > 0›
by (intro norm_EM_remainder_le_strong_nat'[where g' = ?g' and Y = "{}"])
(auto intro!: continuous_intros derivative_eq_intros
simp: field_simps norm_mult norm_powr_real_powr add_eq_0_iff)
have R: "norm R ≤ norm s / (2 * Re s) * a powr -Re s"
unfolding R_def using spec[OF *, of 0] by simp
from assms have "pre_zeta a s = a powr -s / 2 + R"
by (simp add: pre_zeta_def pre_zeta_aux_def R_def)
also have "norm … ≤ a powr -Re s / 2 + norm s / (2 * Re s) * a powr -Re s" using a
by (intro order.trans[OF norm_triangle_ineq] add_mono R) (auto simp: norm_powr_real_powr)
also have "… = (1 + norm s / Re s) / 2 * a powr -Re s"
by (simp add: field_simps)
finally show ?thesis .
qed
lemma pre_zeta_bound':
assumes "0 < Re s" and a: "a > 0"
shows "norm (pre_zeta a s) ≤ norm s / (Re s * a powr Re s)"
proof -
from assms have "norm (pre_zeta a s) ≤ (1 + norm s / Re s) / 2 * a powr -Re s"
by (intro pre_zeta_bound) auto
also have "… = (Re s + norm s) / 2 / (Re s * a powr Re s)"
using assms by (auto simp: field_simps powr_minus)
also have "Re s + norm s ≤ norm s + norm s" by (intro add_right_mono complex_Re_le_cmod)
also have "(norm s + norm s) / 2 = norm s" by simp
finally show "norm (pre_zeta a s) ≤ norm s / (Re s * a powr Re s)"
using assms by (simp add: divide_right_mono)
qed
lemma deriv_zeta_eq:
assumes s: "s ≠ 1"
shows "deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)⇧2"
proof -
from s have ev: "eventually (λz. z ≠ 1) (nhds s)" by (intro t1_space_nhds)
have [derivative_intros]: "(pre_zeta 1 has_field_derivative deriv (pre_zeta 1) s) (at s)"
by (intro holomorphic_derivI[of _ UNIV] holomorphic_intros) auto
have "((λs. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative
(deriv (pre_zeta 1) s - 1 / (s - 1)⇧2)) (at s)"
using s by (auto intro!: derivative_eq_intros simp: power2_eq_square)
also have "?this ⟷ (zeta has_field_derivative (deriv (pre_zeta 1) s - 1 / (s - 1)⇧2)) (at s)"
by (intro has_field_derivative_cong_ev eventually_mono[OF ev])
(auto simp: zeta_def hurwitz_zeta_def)
finally show ?thesis by (rule DERIV_imp_deriv)
qed
lemma zeta_remove_zero:
assumes "Re s ≥ 1"
shows "(s - 1) * pre_zeta 1 s + 1 ≠ 0"
proof (cases "s = 1")
case False
hence "(s - 1) * pre_zeta 1 s + 1 = (s - 1) * zeta s"
by (simp add: zeta_def hurwitz_zeta_def divide_simps)
also from False assms have "… ≠ 0" using zeta_Re_ge_1_nonzero[of s] by auto
finally show ?thesis .
qed auto
lemma eval_fds_deriv_zeta:
assumes "Re s > 1"
shows "eval_fds (fds_deriv fds_zeta) s = deriv zeta s"
proof -
have ev: "eventually (λz. z ∈ {z. Re z > 1}) (nhds s)"
using assms by (intro eventually_nhds_in_open open_halfspace_Re_gt) auto
from assms have "eval_fds (fds_deriv fds_zeta) s = deriv (eval_fds fds_zeta) s"
by (subst eval_fds_deriv) auto
also have "… = deriv zeta s"
by (intro deriv_cong_ev eventually_mono[OF ev]) (auto simp: eval_fds_zeta)
finally show ?thesis .
qed
lemma le_nat_iff': "x ≤ nat y ⟷ x = 0 ∧ y ≤ 0 ∨ int x ≤ y"
by auto
lemma sum_upto_plus1:
assumes "x ≥ 0"
shows "sum_upto f (x + 1) = sum_upto f x + f (Suc (nat ⌊x⌋))"
proof -
have "sum_upto f (x + 1) = sum f {0<..Suc (nat ⌊x⌋)}"
using assms by (simp add: sum_upto_altdef nat_add_distrib)
also have "{0<..Suc (nat ⌊x⌋)} = insert (Suc (nat ⌊x⌋)) {0<..nat ⌊x⌋}"
by auto
also have "sum f … = sum_upto f x + f (Suc (nat ⌊x⌋))"
by (subst sum.insert) (auto simp: sum_upto_altdef add_ac)
finally show ?thesis .
qed
lemma sum_upto_minus1:
assumes "x ≥ 1"
shows "sum_upto f (x - 1) = (sum_upto f x - f (nat ⌊x⌋) :: 'a :: ab_group_add)"
using sum_upto_plus1[of "x - 1" f] assms by (simp add: algebra_simps nat_diff_distrib)
lemma integral_smallo:
fixes f g g' :: "real ⇒ real"
assumes "f ∈ o(g')" and "filterlim g at_top at_top"
assumes "⋀a' x. a ≤ a' ⟹ a' ≤ x ⟹ f integrable_on {a'..x}"
assumes deriv: "⋀x. x ≥ a ⟹ (g has_field_derivative g' x) (at x)"
assumes cont: "continuous_on {a..} g'"
assumes nonneg: "⋀x. x ≥ a ⟹ g' x ≥ 0"
shows "(λx. integral {a..x} f) ∈ o(g)"
proof (rule landau_o.smallI)
fix c :: real assume c: "c > 0"
note [continuous_intros] = continuous_on_subset[OF cont]
define c' where "c' = c / 2"
from c have c': "c' > 0" by (simp add: c'_def)
from landau_o.smallD[OF assms(1) this]
obtain b where b: "⋀x. x ≥ b ⟹ norm (f x) ≤ c' * norm (g' x)"
unfolding eventually_at_top_linorder by blast
define b' where "b' = max a b"
define D where "D = norm (integral {a..b'} f)"
have "filterlim (λx. c' * g x) at_top at_top"
using c' by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] assms)
hence "eventually (λx. c' * g x ≥ D - c' * g b') at_top"
by (auto simp: filterlim_at_top)
thus "eventually (λx. norm (integral {a..x} f) ≤ c * norm (g x)) at_top"
using eventually_ge_at_top[of b']
proof eventually_elim
case (elim x)
have b': "a ≤ b'" "b ≤ b'" by (auto simp: b'_def)
from elim b' have integrable: "(λx. ¦g' x¦) integrable_on {b'..x}"
by (intro integrable_continuous_real continuous_intros) auto
have "integral {a..x} f = integral {a..b'} f + integral {b'..x} f"
using elim b' by (intro Henstock_Kurzweil_Integration.integral_combine [symmetric] assms) auto
also have "norm … ≤ D + norm (integral {b'..x} f)"
unfolding D_def by (rule norm_triangle_ineq)
also have "norm (integral {b'..x} f) ≤ integral {b'..x} (λx. c' * norm (g' x))"
using b' elim assms c' integrable by (intro integral_norm_bound_integral b assms) auto
also have "… = c' * integral {b'..x} (λx. ¦g' x¦)" by simp
also have "integral {b'..x} (λx. ¦g' x¦) = integral {b'..x} g'"
using assms b' by (intro integral_cong) auto
also have "(g' has_integral (g x - g b')) {b'..x}" using b' elim
by (intro fundamental_theorem_of_calculus)
(auto simp flip: has_real_derivative_iff_has_vector_derivative
intro!: has_field_derivative_at_within[OF deriv])
hence "integral {b'..x} g' = g x - g b'"
by (simp add: has_integral_iff)
also have "D + c' * (g x - g b') ≤ c * g x"
using elim by (simp add: field_simps c'_def)
also have "… ≤ c * norm (g x)"
using c by (intro mult_left_mono) auto
finally show ?case by simp
qed
qed
lemma integral_bigo:
fixes f g g' :: "real ⇒ real"
assumes "f ∈ O(g')" and "filterlim g at_top at_top"
assumes "⋀a' x. a ≤ a' ⟹ a' ≤ x ⟹ f integrable_on {a'..x}"
assumes deriv: "⋀x. x ≥ a ⟹ (g has_field_derivative g' x) (at x within {a..})"
assumes cont: "continuous_on {a..} g'"
assumes nonneg: "⋀x. x ≥ a ⟹ g' x ≥ 0"
shows "(λx. integral {a..x} f) ∈ O(g)"
proof -
note [continuous_intros] = continuous_on_subset[OF cont]
from landau_o.bigE[OF assms(1)]
obtain c b where c: "c > 0" and b: "⋀x. x ≥ b ⟹ norm (f x) ≤ c * norm (g' x)"
unfolding eventually_at_top_linorder by metis
define c' where "c' = c / 2"
define b' where "b' = max a b"
define D where "D = norm (integral {a..b'} f)"
have "filterlim (λx. c * g x) at_top at_top"
using c by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] assms)
hence "eventually (λx. c * g x ≥ D - c * g b') at_top"
by (auto simp: filterlim_at_top)
hence "eventually (λx. norm (integral {a..x} f) ≤ 2 * c * norm (g x)) at_top"
using eventually_ge_at_top[of b']
proof eventually_elim
case (elim x)
have b': "a ≤ b'" "b ≤ b'" by (auto simp: b'_def)
from elim b' have integrable: "(λx. ¦g' x¦) integrable_on {b'..x}"
by (intro integrable_continuous_real continuous_intros) auto
have "integral {a..x} f = integral {a..b'} f + integral {b'..x} f"
using elim b' by (intro Henstock_Kurzweil_Integration.integral_combine [symmetric] assms) auto
also have "norm … ≤ D + norm (integral {b'..x} f)"
unfolding D_def by (rule norm_triangle_ineq)
also have "norm (integral {b'..x} f) ≤ integral {b'..x} (λx. c * norm (g' x))"
using b' elim assms c integrable by (intro integral_norm_bound_integral b assms) auto
also have "… = c * integral {b'..x} (λx. ¦g' x¦)" by simp
also have "integral {b'..x} (λx. ¦g' x¦) = integral {b'..x} g'"
using assms b' by (intro integral_cong) auto
also have "(g' has_integral (g x - g b')) {b'..x}" using b' elim
by (intro fundamental_theorem_of_calculus)
(auto simp flip: has_real_derivative_iff_has_vector_derivative
intro!: DERIV_subset[OF deriv])
hence "integral {b'..x} g' = g x - g b'"
by (simp add: has_integral_iff)
also have "D + c * (g x - g b') ≤ 2 * c * g x"
using elim by (simp add: field_simps c'_def)
also have "… ≤ 2 * c * norm (g x)"
using c by (intro mult_left_mono) auto
finally show ?case by simp
qed
thus ?thesis by (rule bigoI)
qed
lemma primepows_le_subset:
assumes x: "x > 0" and l: "l > 0"
shows "{(p, i). prime p ∧ l ≤ i ∧ real (p ^ i) ≤ x} ⊆ {..nat ⌊root l x⌋} × {..nat ⌊log 2 x⌋}"
proof safe
fix p i :: nat assume pi: "prime p" "i ≥ l" "real (p ^ i) ≤ x"
have "real p ^ l ≤ real p ^ i" using pi x l
by (intro power_increasing) (auto dest: prime_gt_0_nat)
also have "… ≤ x" using pi by simp
finally have "root l (real p ^ l) ≤ root l x"
using x pi l by (subst real_root_le_iff) auto
also have "root l (real p ^ l) = real p"
using pi l by (subst real_root_pos2) auto
finally show "p ≤ nat ⌊root l x⌋" using pi l x by (simp add: le_nat_iff' le_floor_iff)
from pi have "2 ^ i ≤ real p ^ i" using l
by (intro power_mono) (auto dest: prime_gt_1_nat)
also have "… ≤ x" using pi by simp
finally show "i ≤ nat ⌊log 2 x⌋" using pi x
by (auto simp: le_nat_iff' le_floor_iff le_log_iff powr_realpow)
qed
lemma mangoldt_non_primepow: "¬primepow n ⟹ mangoldt n = 0"
by (auto simp: mangoldt_def)
lemma ln_minus_ln_floor_bigo: "(λx. ln x - ln (real (nat ⌊x⌋))) ∈ O(λ_. 1)"
proof (intro le_imp_bigo_real[of 1] eventually_mono[OF eventually_ge_at_top[of 1]])
fix x :: real assume x: "x ≥ 1"
from x have *: "x - real (nat ⌊x⌋) ≤ 1" by linarith
from x have "ln x - ln (real (nat ⌊x⌋)) ≤ (x - real (nat ⌊x⌋)) / real (nat ⌊x⌋)"
by (intro ln_diff_le) auto
also have "… ≤ 1 / 1" using x * by (intro frac_le) auto
finally show "ln x - ln (real (nat ⌊x⌋)) ≤ 1 * 1" by simp
qed auto
lemma cos_geD:
assumes "cos x ≥ cos a" "0 ≤ a" "a ≤ pi" "-pi ≤ x" "x ≤ pi"
shows "x ∈ {-a..a}"
proof (cases "x ≥ 0")
case True
with assms show ?thesis
by (subst (asm) cos_mono_le_eq) auto
next
case False
with assms show ?thesis using cos_mono_le_eq[of a "-x"]
by auto
qed
lemma path_image_part_circlepath_same_Re:
assumes "0 ≤ b" "b ≤ pi" "a = -b" "r ≥ 0"
shows "path_image (part_circlepath c r a b) = sphere c r ∩ {s. Re s ≥ Re c + r * cos a}"
proof safe
fix z assume "z ∈ path_image (part_circlepath c r a b)"
with assms obtain t where t: "t ∈ {a..b}" "z = c + of_real r * cis t"
by (auto simp: path_image_part_circlepath exp_eq_polar)
from t and assms show "z ∈ sphere c r"
by (auto simp: dist_norm norm_mult)
from t and assms show "Re z ≥ Re c + r * cos a"
using cos_monotone_0_pi_le[of t b] cos_monotone_minus_pi_0'[of a t]
by (cases "t ≥ 0") (auto intro!: mult_left_mono)
next
fix z assume z: "z ∈ sphere c r" "Re z ≥ Re c + r * cos a"
show "z ∈ path_image (part_circlepath c r a b)"
proof (cases "r = 0")
case False
with assms have r: "r > 0" by simp
with z have z_eq: "z = c + r * cis (Arg (z - c))"
using Arg_eq[of "z - c"] by (auto simp: dist_norm exp_eq_polar norm_minus_commute)
moreover from z(2) r assms have "cos b ≤ cos (Arg (z - c))"
by (subst (asm) z_eq) auto
with assms have "Arg (z - c) ∈ {-b..b}"
using Arg_le_pi[of "z - c"] mpi_less_Arg[of "z - c"] by (intro cos_geD) auto
ultimately show "z ∈ path_image (part_circlepath c r a b)"
using assms by (subst path_image_part_circlepath) (auto simp: exp_eq_polar)
qed (insert assms z, auto simp: path_image_part_circlepath)
qed
lemma part_circlepath_rotate_left:
"part_circlepath c r (x + a) (x + b) = (λz. c + cis x * (z - c)) ∘ part_circlepath c r a b"
by (simp add: part_circlepath_def exp_eq_polar fun_eq_iff
linepath_translate_left linepath_translate_right cis_mult add_ac)
lemma part_circlepath_rotate_right:
"part_circlepath c r (a + x) (b + x) = (λz. c + cis x * (z - c)) ∘ part_circlepath c r a b"
by (simp add: part_circlepath_def exp_eq_polar fun_eq_iff
linepath_translate_left linepath_translate_right cis_mult add_ac)
lemma path_image_semicircle_Re_ge:
assumes "r ≥ 0"
shows "path_image (part_circlepath c r (-pi/2) (pi/2)) =
sphere c r ∩ {s. Re s ≥ Re c}"
by (subst path_image_part_circlepath_same_Re) (simp_all add: assms)
lemma sphere_rotate: "(λz. c + cis x * (z - c)) ` sphere c r = sphere c r"
proof safe
fix z assume z: "z ∈ sphere c r"
hence "z = c + cis x * (c + cis (-x) * (z - c) - c)"
"c + cis (-x) * (z - c) ∈ sphere c r"
by (auto simp: dist_norm norm_mult norm_minus_commute
cis_conv_exp exp_minus field_simps norm_divide)
with z show "z ∈ (λz. c + cis x * (z - c)) ` sphere c r" by blast
qed (auto simp: dist_norm norm_minus_commute norm_mult)
lemma path_image_semicircle_Re_le:
assumes "r ≥ 0"
shows "path_image (part_circlepath c r (pi/2) (3/2*pi)) =
sphere c r ∩ {s. Re s ≤ Re c}"
proof -
let ?f = "(λz. c + cis pi * (z - c))"
have *: "part_circlepath c r (pi/2) (3/2*pi) = part_circlepath c r (pi + (-pi/2)) (pi + pi/2)"
by simp
have "path_image (part_circlepath c r (pi/2) (3/2*pi)) =
?f ` sphere c r ∩ ?f ` {s. Re c ≤ Re s}"
unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms]
by auto
also have "?f ` sphere c r = sphere c r"
by (rule sphere_rotate)
also have "?f ` {s. Re c ≤ Re s} = {s. Re c ≥ Re s}"
by (auto simp: image_iff intro!: exI[of _ "2 * c - x" for x])
finally show ?thesis .
qed
lemma path_image_semicircle_Im_ge:
assumes "r ≥ 0"
shows "path_image (part_circlepath c r 0 pi) =
sphere c r ∩ {s. Im s ≥ Im c}"
proof -
let ?f = "(λz. c + cis (pi/2) * (z - c))"
have *: "part_circlepath c r 0 pi = part_circlepath c r (pi / 2 + (-pi/2)) (pi / 2 + pi/2)"
by simp
have "path_image (part_circlepath c r 0 pi) =
?f ` sphere c r ∩ ?f ` {s. Re c ≤ Re s}"
unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms]
by auto
also have "?f ` sphere c r = sphere c r"
by (rule sphere_rotate)
also have "?f ` {s. Re c ≤ Re s} = {s. Im c ≤ Im s}"
by (auto simp: image_iff intro!: exI[of _ "c - 𝗂 * (x - c)" for x])
finally show ?thesis .
qed
lemma path_image_semicircle_Im_le:
assumes "r ≥ 0"
shows "path_image (part_circlepath c r pi (2 * pi)) =
sphere c r ∩ {s. Im s ≤ Im c}"
proof -
let ?f = "(λz. c + cis (3*pi/2) * (z - c))"
have *: "part_circlepath c r pi (2*pi) = part_circlepath c r (3*pi/2 + (-pi/2)) (3*pi/2 + pi/2)"
by simp
have "path_image (part_circlepath c r pi (2 * pi)) =
?f ` sphere c r ∩ ?f ` {s. Re c ≤ Re s}"
unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms]
by auto
also have "?f ` sphere c r = sphere c r"
by (rule sphere_rotate)
also have "cis (3 * pi / 2) = -𝗂"
using cis_mult[of pi "pi / 2"] by simp
hence "?f ` {s. Re c ≤ Re s} = {s. Im c ≥ Im s}"
by (auto simp: image_iff intro!: exI[of _ "c + 𝗂 * (x - c)" for x])
finally show ?thesis .
qed
lemma eval_fds_logderiv_zeta_real:
assumes "x > (1 :: real)"
shows "(λp. ln (real p) / (p powr x - 1)) abs_summable_on {p. prime p}" (is ?th1)
and "deriv zeta (of_real x) / zeta (of_real x) =
-of_real (∑⇩ap | prime p. ln (real p) / (p powr x - 1))" (is ?th2)
proof -
have "(λp. Re (of_real (ln (real p)) / (of_nat p powr of_real x - 1)))
abs_summable_on {p. prime p}" using assms
by (intro abs_summable_Re eval_fds_logderiv_zeta) auto
also have "?this ⟷ ?th1"
by (intro abs_summable_on_cong) (auto simp: powr_Reals_eq)
finally show ?th1 .
show ?th2 using assms
by (subst eval_fds_logderiv_zeta) (auto simp: infsetsum_of_real [symmetric] powr_Reals_eq)
qed
lemma
fixes a b c d :: real
assumes ab: "d * a + b ≥ 1" and c: "c < -1" and d: "d > 0"
defines "C ≡ - ((ln (d * a + b) - 1 / (c + 1)) * (d * a + b) powr (c + 1) / (d * (c + 1)))"
shows set_integrable_ln_powr_at_top:
"(λx. (ln (d * x + b) * ((d * x + b) powr c))) absolutely_integrable_on {a<..}" (is ?th1)
and set_lebesgue_integral_ln_powr_at_top:
"(∫x∈{a<..}. (ln (d * x + b) * ((d * x + b) powr c)) ∂lborel) = C" (is ?th2)
and ln_powr_has_integral_at_top:
"((λx. ln (d * x + b) * (d * x + b) powr c) has_integral C) {a<..}" (is ?th3)
proof -
define f where "f = (λx. ln (d * x + b) * (d * x + b) powr c)"
define F where "F = (λx. (ln (d * x + b) - 1 / (c + 1)) * (d * x + b) powr (c + 1) / (d * (c + 1)))"
have *: "(F has_field_derivative f x) (at x)" "isCont f x" "f x ≥ 0" if "x > a" for x
proof -
have "1 ≤ d * a + b" by fact
also have "… < d * x + b" using that assms
by (intro add_strict_right_mono mult_strict_left_mono)
finally have gt_1: "d * x + b > 1" .
show "(F has_field_derivative f x) (at x)" "isCont f x" using ab c d gt_1
by (auto simp: F_def f_def divide_simps intro!: derivative_eq_intros continuous_intros)
(auto simp: algebra_simps powr_add)?
show "f x ≥ 0" using gt_1 by (auto simp: f_def)
qed
have limits: "((F ∘ real_of_ereal) ⤏ F a) (at_right (ereal a))"
"((F ∘ real_of_ereal) ⤏ 0) (at_left ∞)"
using c ab d unfolding ereal_tendsto_simps1 F_def by (real_asymp; simp add: field_simps)+
have 1: "set_integrable lborel (einterval a ∞) f" using ab c limits
by (intro interval_integral_FTC_nonneg) (auto intro!: * AE_I2)
thus 2: "f absolutely_integrable_on {a<..}"
by (auto simp: set_integrable_def integrable_completion)
have "(LBINT x=ereal a..∞. f x) = 0 - F a" using ab c limits
by (intro interval_integral_FTC_nonneg) (auto intro!: *)
thus 3: ?th2
by (simp add: interval_integral_to_infinity_eq F_def f_def C_def)
show ?th3
using set_borel_integral_eq_integral[OF 1] 3 by (simp add: has_integral_iff f_def C_def)
qed
lemma ln_fact_conv_sum_upto: "ln (fact n) = sum_upto ln n"
by (induction n) (auto simp: sum_upto_plus1 add.commute[of 1] ln_mult)
lemma sum_upto_ln_conv_ln_fact: "sum_upto ln x = ln (fact (nat ⌊x⌋))"
by (simp add: ln_fact_conv_sum_upto sum_upto_altdef)
lemma real_of_nat_div: "real (a div b) = real_of_int ⌊real a / real b⌋"
by (simp add: floor_divide_of_nat_eq)
lemma measurable_sum_upto [measurable]:
fixes f :: "'a ⇒ nat ⇒ real"
assumes [measurable]: "⋀y. (λt. f t y) ∈ M →⇩M borel"
assumes [measurable]: "x ∈ M →⇩M borel"
shows "(λt. sum_upto (f t) (x t)) ∈ M →⇩M borel"
proof -
have meas: "(λt. set_lebesgue_integral lborel {y. y ≥ 0 ∧ y - real (nat ⌊x t⌋) ≤ 0} (λy. f t (nat ⌈y⌉)))
∈ M →⇩M borel" (is "?f ∈ _") unfolding set_lebesgue_integral_def
by measurable
also have "?f = (λt. sum_upto (f t) (x t))"
proof
fix t :: 'a
show "?f t = sum_upto (f t) (x t)"
proof (cases "x t < 1")
case True
hence "{y. y ≥ 0 ∧ y - real (nat ⌊x t⌋) ≤ 0} = {0}" by auto
thus ?thesis using True
by (simp add: set_integral_at_point sum_upto_altdef)
next
case False
define n where "n = nat ⌊x t⌋"
from False have "n > 0" by (auto simp: n_def)
have *: "((λx. f t (nat ⌈x⌉)) has_integral sum (f t) {0<..n}) {real 0..real n}"
using ‹n > 0› by (intro nat_sum_has_integral_ceiling) auto
have **: "(λx. f t (nat ⌈x⌉)) absolutely_integrable_on {real 0..real n}"
proof (rule absolutely_integrable_absolutely_integrable_ubound)
show "(λ_. MAX n∈{0..n}. ¦f t n¦) absolutely_integrable_on {real 0..real n}"
using ‹n > 0› by (subst absolutely_integrable_on_iff_nonneg)
(auto simp: Max_ge_iff intro!: exI[of _ "f t 0"])
show "(λx. f t (nat ⌈x⌉)) integrable_on {real 0..real n}"
using * by (simp add: has_integral_iff)
next
fix y :: real assume y: "y ∈ {real 0..real n}"
have "f t (nat ⌈y⌉) ≤ ¦f t (nat ⌈y⌉)¦"
by simp
also have "… ≤ (MAX n∈{0..n}. ¦f t n¦)"
using y by (intro Max.coboundedI) auto
finally show "f t (nat ⌈y⌉) ≤ (MAX n∈{0..n}. ¦f t n¦)" .
qed
have "sum (f t) {0<..n} = (∫x∈{real 0..real n}. f t (nat ⌈x⌉) ∂lebesgue)"
using has_integral_set_lebesgue[OF **] * by (simp add: has_integral_iff)
also have "… = (∫x∈{real 0..real n}. f t (nat ⌈x⌉) ∂lborel)"
unfolding set_lebesgue_integral_def by (subst integral_completion) auto
also have "{real 0..real n} = {y. 0 ≤ y ∧ y - real (nat ⌊x t⌋) ≤ 0}"
by (auto simp: n_def)
also have "sum (f t) {0<..n} = sum_upto (f t) (x t)"
by (simp add: sum_upto_altdef n_def)
finally show ?thesis ..
qed
qed
finally show ?thesis .
qed
end