Theory PNT_Remainder_Library

theory PNT_Remainder_Library
imports
  "PNT_Notation"
begin
unbundle pnt_notation
section ‹Auxiliary library for prime number theorem›

subsection ‹Zeta function›

lemma pre_zeta_1_bound:
  assumes "0 < Re s"
  shows "∥pre_zeta 1 s∥ ≤ ∥s∥ / Re s"
proof -
  have "∥pre_zeta 1 s∥ ≤ ∥s∥ / (Re s * 1 powr Re s)"
    by (rule pre_zeta_bound') (use assms in auto)
  also have "… = ∥s∥ / Re s" by auto
  finally show ?thesis .
qed

lemma zeta_pole_eq:
  assumes "s ≠ 1"
  shows "zeta s = pre_zeta 1 s + 1 / (s - 1)"
proof -
  have "zeta s - 1 / (s - 1) = pre_zeta 1 s" by (intro zeta_minus_pole_eq assms)
  thus ?thesis by (simp add: field_simps)
qed

definition zeta' where "zeta' s ≡ pre_zeta 1 s * (s - 1) + 1"

lemma zeta'_analytic:
  "zeta' analytic_on UNIV"
  unfolding zeta'_def by (intro analytic_intros) auto

lemma zeta'_analytic_on [analytic_intros]:
  "zeta' analytic_on A" using zeta'_analytic analytic_on_subset by auto

lemma zeta'_holomorphic_on [holomorphic_intros]:
  "zeta' holomorphic_on A" using zeta'_analytic_on by (intro analytic_imp_holomorphic)

lemma zeta_eq_zeta':
  "zeta s = zeta' s / (s - 1)"
proof (cases "s = 1")
  case True thus ?thesis using zeta_1 unfolding zeta'_def by auto
next
  case False with zeta_pole_eq [OF this]
  show ?thesis unfolding zeta'_def by (auto simp add: field_simps)
qed

lemma zeta'_1 [simp]: "zeta' 1 = 1" unfolding zeta'_def by auto

lemma zeta_eq_zero_iff_zeta':
  shows "s ≠ 1 ⟹ zeta' s = 0 ⟷ zeta s = 0"
  using zeta_eq_zeta' [of s] by auto

lemma zeta'_eq_zero_iff:
  shows "zeta' s = 0 ⟷ zeta s = 0 ∧ s ≠ 1"
  by (cases "s = 1", use zeta_eq_zero_iff_zeta' in auto)

lemma zeta_eq_zero_iff:
  shows "zeta s = 0 ⟷ zeta' s = 0 ∨ s = 1"
  by (subst zeta'_eq_zero_iff, use zeta_1 in auto)

subsection ‹Logarithm derivatives›

definition "logderiv f x ≡ deriv f x / f x"
definition log_differentiable
  (infixr "(log'_differentiable)" 50)
where
  "f log_differentiable x ≡ (f field_differentiable (at x)) ∧ f x ≠ 0"

lemma logderiv_prod':
  fixes f :: "'n ⇒ 'f ⇒ 'f :: real_normed_field"
  assumes fin: "finite I"
    and lder: "⋀i. i ∈ I ⟹ f i log_differentiable a"
  shows "logderiv (λx. ∏i∈I. f i x) a = (∑i∈I. logderiv (f i) a)" (is ?P)
    and "(λx. ∏i∈I. f i x) log_differentiable a" (is ?Q)
proof -
  let ?a = "λi. deriv (f i) a"
  let ?b = "λi. ∏j∈I - {i}. f j a"
  let ?c = "λi. f i a"
  let ?d = "∏i∈I. ?c i"
  have der: "⋀i. i ∈ I ⟹ f i field_differentiable (at a)"
    and nz: "⋀i. i ∈ I ⟹ f i a ≠ 0"
    using lder unfolding log_differentiable_def by auto
  have 1: "(*) x = (λy. y * x)" for x :: 'f by auto
  have "((λx. ∏i∈I. f i x) has_derivative
    (λy. ∑i∈I. ?a i * y *?b i)) (at a within UNIV)"
    by (rule has_derivative_prod, fold has_field_derivative_def)
       (rule field_differentiable_derivI, elim der)
  hence 2: "DERIV (λx. ∏i∈I. f i x) a :> (∑i∈I. ?a i * ?b i)"
    unfolding has_field_derivative_def
    by (simp add: sum_distrib_left [symmetric] mult_ac)
       (subst 1, blast)
  have prod_nz: "(∏i∈I. ?c i) ≠ 0"
    using prod_zero_iff nz fin by auto
  have mult_cong: "b = c ⟹ a * b = a * c" for a b c :: real by auto
  have "logderiv (λx. ∏i∈I. f i x) a = deriv (λx. ∏i∈I. f i x) a / ?d"
    unfolding logderiv_def by auto
  also have "… = (∑i∈I. ?a i * ?b i) / ?d"
    using 2 DERIV_imp_deriv by auto
  also have "… = (∑i∈I. ?a i * (?b i / ?d))"
    by (auto simp add: sum_divide_distrib)
  also have "… = (∑i∈I. logderiv (f i) a)"
  proof -
    have "⋀a b c :: 'f. a ≠ 0 ⟹ a = b * c ⟹ c / a = inverse b"
      by (auto simp add: field_simps)
    moreover have "?d = ?c i * ?b i" if "i ∈ I" for i
      by (intro prod.remove that fin)
    ultimately have "?b i / ?d = inverse (?c i)" if "i ∈ I" for i
      using prod_nz that by auto
    thus ?thesis unfolding logderiv_def using 2
      by (auto simp add: divide_inverse intro: sum.cong)
  qed
  finally show ?P .
  show ?Q by (auto
    simp: log_differentiable_def field_differentiable_def
    intro!: 2 prod_nz)
qed

lemma logderiv_prod:
  fixes f :: "'n ⇒ 'f ⇒ 'f :: real_normed_field"
  assumes lder: "⋀i. i ∈ I ⟹ f i log_differentiable a"
  shows "logderiv (λx. ∏i∈I. f i x) a = (∑i∈I. logderiv (f i) a)" (is ?P)
    and "(λx. ∏i∈I. f i x) log_differentiable a" (is ?Q)
proof -
  consider "finite I" | "infinite I" by auto
  hence "?P ∧ ?Q"
  proof cases
    assume fin: "finite I"
    show ?thesis by (auto intro: logderiv_prod' lder fin)
  next
    assume nfin: "infinite I"
    show ?thesis using nfin
      unfolding logderiv_def log_differentiable_def by auto
  qed
  thus ?P ?Q by auto
qed

lemma logderiv_mult:
  assumes "f log_differentiable a"
    and "g log_differentiable a"
  shows "logderiv (λz. f z * g z) a = logderiv f a + logderiv g a" (is ?P)
    and "(λz. f z * g z) log_differentiable a" (is ?Q)
proof -
  have "logderiv (λz. f z * g z) a
      = logderiv (λz. ∏i∈{0, 1}. ([f, g]!i) z) a" by auto
  also have "… = (∑i∈{0, 1}. logderiv ([f, g]!i) a)"
    by (rule logderiv_prod(1), use assms in auto)
  also have "… = logderiv f a + logderiv g a"
    by auto
  finally show ?P .
  have "(λz. ∏i∈{0, 1}. ([f, g]!i) z) log_differentiable a"
    by (rule logderiv_prod(2), use assms in auto)
  thus ?Q by auto
qed

lemma logderiv_cong_ev:
  assumes "∀⇩F x in nhds x. f x = g x"
    and "x = y"
  shows "logderiv f x = logderiv g y"
proof -
  have "deriv f x = deriv g y" using assms by (rule deriv_cong_ev)
  moreover have "f x = g y" using assms by (auto intro: eventually_nhds_x_imp_x)
  ultimately show ?thesis unfolding logderiv_def by auto
qed

lemma logderiv_linear:
  assumes "z ≠ a"
  shows "logderiv (λw. w - a) z = 1 / (z - a)"
    and "(λw. w - z) log_differentiable a"
unfolding logderiv_def log_differentiable_def
  using assms by (auto simp add: derivative_intros)

lemma deriv_shift:
  assumes "f field_differentiable at (a + x)"
  shows "deriv (λt. f (a + t)) x = deriv f (a + x)"
proof -
  have "deriv (f ∘ (λt. a + t)) x = deriv f (a + x)"
    by (subst deriv_chain) (auto intro: assms)
  thus ?thesis unfolding comp_def by auto
qed

lemma logderiv_shift:
  assumes "f field_differentiable at (a + x)"
  shows "logderiv (λt. f (a + t)) x = logderiv f (a + x)"
  unfolding logderiv_def by (subst deriv_shift) (auto intro: assms)

lemma logderiv_inverse:
  assumes "x ≠ 0"
  shows "logderiv (λx. 1 / x) x = - 1 / x"
proof -
  have "deriv (λx. 1 / x) x = (deriv (λx. 1) x * x - 1 * deriv (λx. x) x) / x⇧2"
    by (rule deriv_divide) (use assms in auto)
  hence "deriv (λx. 1 / x) x = - 1 / x⇧2" by auto
  thus ?thesis unfolding logderiv_def power2_eq_square using assms by auto
qed

lemma logderiv_zeta_eq_zeta':
  assumes "s ≠ 1" "zeta s ≠ 0"
  shows "logderiv zeta s = logderiv zeta' s - 1 / (s - 1)"
proof -
  have "logderiv zeta s = logderiv (λs. zeta' s * (1 / (s - 1))) s"
    using zeta_eq_zeta' by auto metis
  also have "… = logderiv zeta' s + logderiv (λs. 1 / (s - 1)) s"
  proof -
    have "zeta' s ≠ 0" using assms zeta_eq_zero_iff_zeta' by auto
    hence "zeta' log_differentiable s"
      unfolding log_differentiable_def
      by (intro conjI analytic_on_imp_differentiable_at)
         (rule zeta'_analytic, auto)
    moreover have "(λz. 1 / (z - 1)) log_differentiable s"
      unfolding log_differentiable_def using assms(1)
      by (intro derivative_intros conjI, auto)
    ultimately show ?thesis using assms by (intro logderiv_mult(1))
  qed
  also have "logderiv (λs. 1 / (- 1 + s)) s = logderiv (λs. 1 / s) (- 1 + s)"
    by (rule logderiv_shift) (insert assms(1), auto intro: derivative_intros)
  moreover have "… = - 1 / (- 1 + s)"
    by (rule logderiv_inverse) (use assms(1) in auto)
  ultimately show ?thesis by auto
qed

lemma analytic_logderiv [analytic_intros]:
  assumes "f analytic_on A" "⋀z. z ∈ A ⟹ f z ≠ 0"
  shows "(λs. logderiv f s) analytic_on A"
  using assms unfolding logderiv_def by (intro analytic_intros)

subsection ‹Lemmas of integration and integrability›

lemma powr_has_integral:
  fixes a b w :: real
  assumes Hab: "a ≤ b" and Hw: "w > 0 ∧ w ≠ 1"
  shows "((λx. w powr x) has_integral w powr b / ln w - w powr a / ln w) {a..b}"
proof (rule fundamental_theorem_of_calculus)
  show "a ≤ b" using assms by auto
next
  fix x assume "x ∈ {a..b}"
  have "((λx. exp (x * ln w)) has_vector_derivative exp (x * ln w) * (1 * ln w)) (at x within {a..b})"
    by (subst has_real_derivative_iff_has_vector_derivative [symmetric])
       (rule derivative_intros DERIV_cmult_right)+
  hence "((powr) w has_vector_derivative w powr x * ln w) (at x within {a..b})"
    unfolding powr_def using Hw by (simp add: DERIV_fun_exp)
  moreover have "ln w ≠ 0" using Hw by auto
  ultimately show "((λx. w powr x / ln w) has_vector_derivative w powr x) (at x within {a..b})"
    by (auto intro: derivative_eq_intros)
qed

lemma powr_integrable:
  fixes a b w :: real
  assumes Hab: "a ≤ b" and Hw: "w > 0 ∧ w ≠ 1"
  shows "(λx. w powr x) integrable_on {a..b}"
by (rule has_integral_integrable, rule powr_has_integral)
   (use assms in auto)

lemma powr_integral_bound_gt_1:
  fixes a b w :: real
  assumes Hab: "a ≤ b" and Hw: "w > 1"
  shows "integral {a..b} (λx. w powr x) ≤ w powr b / ¦ln w¦"
proof -
  have "integral {a..b} (λx. w powr x) = w powr b / ln w - w powr a / ln w"
    by (intro integral_unique powr_has_integral) (use assms in auto)
  also have "… ≤ w powr b / ¦ln w¦" using Hw by auto
  finally show ?thesis .
qed

lemma powr_integral_bound_lt_1:
  fixes a b w :: real
  assumes Hab: "a ≤ b" and Hw: "0 < w ∧ w < 1"
  shows "integral {a..b} (λx. w powr x) ≤ w powr a / ¦ln w¦"
proof -
  have "integral {a..b} (λx. w powr x) = w powr b / ln w - w powr a / ln w"
    by (intro integral_unique powr_has_integral) (use assms in auto)
  also have "… ≤ w powr a / ¦ln w¦" using Hw by (auto simp add: field_simps)
  finally show ?thesis .
qed

lemma set_integrableI_bounded:
  fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
  shows "A ∈ sets M
  ⟹ (λx. indicator A x *⇩R f x) ∈ borel_measurable M
  ⟹ emeasure M A < ∞
  ⟹ (AE x in M. x ∈ A ⟶ norm (f x) ≤ B)
  ⟹ set_integrable M A f"
unfolding set_integrable_def
  by (rule integrableI_bounded_set[where A=A]) auto

lemma integrable_cut':
  fixes a b c :: real and f :: "real ⇒ real"
  assumes "a ≤ b" "b ≤ c"
  and Hf: "⋀x. a ≤ x ⟹ f integrable_on {a..x}"
  shows "f integrable_on {b..c}"
proof -
  have "a ≤ c" using assms by linarith
  hence "f integrable_on {a..c}" by (rule Hf)
  thus ?thesis by
    (rule integrable_subinterval_real)
    (subst subset_iff, (subst atLeastAtMost_iff)+,
    blast intro: ‹a ≤ b› order_trans [of a b])
qed

lemma integration_by_part':
  fixes a b :: real
    and f g :: "real ⇒ 'a :: {real_normed_field, banach}"
    and f' g' :: "real ⇒ 'a"
  assumes "a ≤ b"
    and "⋀x. x ∈ {a..b} ⟹ (f has_vector_derivative f' x) (at x)"
    and "⋀x. x ∈ {a..b} ⟹ (g has_vector_derivative g' x) (at x)"
    and int: "(λx. f x * g' x) integrable_on {a..b}"
  shows "((λx. f' x * g x) has_integral
    f b * g b - f a * g a - integral{a..b} (λx. f x * g' x)) {a..b}"
proof -
  define prod where "prod ≡ (*) :: 'a ⇒ 'a ⇒ 'a"
  define y where "y ≡ f b * g b - f a * g a - integral{a..b} (λx. f x * g' x)"
  have 0: "bounded_bilinear prod" unfolding prod_def
    by (rule bounded_bilinear_mult)
  have 1: "((λx. f x * g' x) has_integral f b * g b - f a * g a - y) {a..b}"
  using y_def and int and integrable_integral by auto
  note 2 = integration_by_parts
    [where y = y and prod = prod, OF 0, unfolded prod_def]
  have "continuous_on {a..b} f" "continuous_on {a..b} g"
    by (auto intro: has_vector_derivative_continuous
                    has_vector_derivative_at_within assms
             simp: continuous_on_eq_continuous_within)
  with assms and 1 show ?thesis by (fold y_def, intro 2) auto
qed

lemma integral_bigo:
  fixes a :: real and f g :: "real ⇒ real"
  assumes f_bound: "f ∈ O(g)"
    and Hf:  "⋀x. a ≤ x ⟹ f integrable_on {a..x}"
    and Hf': "⋀x. a ≤ x ⟹ (λx. ¦f x¦) integrable_on {a..x}"
    and Hg': "⋀x. a ≤ x ⟹ (λx. ¦g x¦) integrable_on {a..x}"
  shows "(λx. integral{a..x} f) ∈ O(λx. 1 + integral{a..x} (λx. ¦g x¦))"
proof -
  from ‹f ∈ O(g)› obtain c where "∀⇩F x in at_top. ¦f x¦ ≤ c * ¦g x¦"
    unfolding bigo_def by auto
  then obtain N' :: real where asymp: "⋀n. n≥N' ⟹ ¦f n¦ ≤ c * ¦g n¦"
    by (subst (asm) eventually_at_top_linorder) (blast)
  define N where "N ≡ max a N'"
  define I where "I ≡ ¦integral {a..N} f¦"
  define J where "J ≡ integral {a..N} (λx. ¦g x¦)"
  define c' where "c' ≡ max (I + J * ¦c¦) ¦c¦"
  have "⋀x. N ≤ x ⟹ ¦integral {a..x} f¦
      ≤ c' * ¦1 + integral {a..x} (λx. ¦g x¦)¦"
  proof -
    fix x :: real
    assume 1: "N ≤ x"
    define K where "K ≡ integral {a..x} (λx. ¦g x¦)"
    have 2: "a ≤ N" unfolding N_def by linarith
    hence 3: "a ≤ x" using 1 by linarith
    have nnegs: "0 ≤ I" "0 ≤ J" "0 ≤ K"
      unfolding I_def J_def K_def using 1 2 Hg'
      by (auto intro!: integral_nonneg)
    hence abs_eq: "¦I¦ = I" "¦J¦ = J" "¦K¦ = K"
      using nnegs by simp+
    have "int¦f¦": "(λx. ¦f x¦) integrable_on {N..x}"
      using 2 1 Hf' by (rule integrable_cut')
    have "intf": "f integrable_on {N..x}"
      using 2 1 Hf by (rule integrable_cut')
    have "⋀x. a ≤ x ⟹ (λx. c * ¦g x¦) integrable_on {a..x}"
      by (blast intro: Hg' integrable_cmul [OF Hg', simplified])
    hence "intc¦g¦": "(λx. c * ¦g x¦) integrable_on {N..x}"
      using 2 1 by (blast intro: integrable_cut')
    have "¦integral {a..x} f¦ ≤ I + ¦integral {N..x} f¦"
      unfolding I_def
      by (subst Henstock_Kurzweil_Integration.integral_combine
          [OF 2 1 Hf [of x], THEN sym])
         (rule 3, rule abs_triangle_ineq)
    also have "… ≤ I + integral {N..x} (λx. ¦f x¦)"
    proof -
      note integral_norm_bound_integral [OF "intf" "int¦f¦"]
      then have "¦integral {N..x} f¦ ≤ integral {N..x} (λx. ¦f x¦)" by auto
      then show ?thesis by linarith
    qed
    also have "… ≤ I + c * integral {N..x} (λx. ¦g x¦)"
    proof -
      have 1: "N' ≤ N" unfolding N_def by linarith
      hence "⋀y :: real. N ≤ y ⟹ ¦f y¦ ≤ c * ¦g y¦"
      proof -
        fix y :: real
        assume "N ≤ y"
        thus "¦f y¦ ≤ c * ¦g y¦"
          by (rule asymp [OF order_trans [OF 1]])
      qed
      hence "integral {N..x} (λx. ¦f x¦) ≤ integral {N..x} (λx. c * ¦g x¦)"
        by (rule integral_le [OF "int¦f¦" "intc¦g¦"]) simp
      thus ?thesis by simp
    qed
    also have "… ≤ I + ¦c¦ * (J + integral {a..x} (λx. ∥g x∥))"
    proof -
      note Henstock_Kurzweil_Integration.integral_combine [OF 2 1 Hg' [of x]]
      hence K_min_J: "integral {N..x} (λx. ¦g x¦) = K - J"
        unfolding J_def K_def using 3 by auto
      have "c * (K - J) ≤ ¦c¦ * (J + K)" proof -
        have "c * (K - J) ≤ ¦c * (K - J)¦" by simp
        also have "… = ¦c¦ * ¦K - J¦" by (simp add: abs_mult)
        also have "… ≤ ¦c¦ * (¦J¦ + ¦K¦)" by (simp add: mult_left_mono)
        finally show ?thesis by (simp add: abs_eq)
      qed
      thus ?thesis by simp (subst K_min_J, fold K_def)
    qed
    also have "… = (I + J * ¦c¦) + ¦c¦ * integral {a..x} (λx. ¦g x¦)"
      by (simp add: field_simps)
    also have "… ≤ c' + c' * integral {a..x} (λx. ¦g x¦)"
    proof -
      have "I + J * ¦c¦ ≤ c'" unfolding c'_def by auto
      thus ?thesis unfolding c'_def
        by (auto intro!: add_mono mult_mono integral_nonneg Hg' 3)
    qed
    finally show "¦integral {a..x} f¦
      ≤ c' * ¦1 + integral {a..x} (λx. ¦g x¦)¦"
      by (simp add: integral_nonneg Hg' 3 field_simps)
  qed
  note 0 = this
  show ?thesis proof (rule eventually_mono [THEN bigoI])
    show "∀⇩Fx in at_top. N ≤ x" by simp
    show "⋀x. N ≤ x ⟹ ∥integral {a..x} f∥ ≤ c' * 
      ∥1 + integral {a..x} (λx. ¦g x¦)∥" by (simp, rule 0)
  qed
qed

lemma integral_linepath_same_Re:
  assumes Ha: "Re a = Re b"
    and Hb: "Im a < Im b"
    and Hf: "(f has_contour_integral x) (linepath a b)"
  shows "((λt. f (Complex (Re a) t) * 𝗂) has_integral x) {Im a..Im b}"
proof -
  define path where "path ≡ linepath a b"
  define c d e g where "c ≡ Re a" and "d ≡ Im a" and "e ≡ Im b" and "g ≡ e - d"
  hence [simp]: "a = Complex c d" "b = Complex c e" by auto (subst Ha, auto)
  have hg: "0 < g" unfolding g_def using Hb by auto
  have [simp]: "a *⇩R z = a * z" for a and z :: complex by (rule complex_eqI) auto
  have "((λt. f (path t) * (b - a)) has_integral x) {0..1}"
    unfolding path_def by (subst has_contour_integral_linepath [symmetric]) (intro Hf)
  moreover have "path t = Complex c (g *⇩R t + d)" for t
    unfolding path_def linepath_def g_def
    by (auto simp add: field_simps legacy_Complex_simps)
  moreover have "b - a = g * 𝗂"
    unfolding g_def by (auto simp add: legacy_Complex_simps)
  ultimately have
    "((λt. f (Complex c (g *⇩R t + d)) * (g * 𝗂)) has_integral g * x /⇩R g ^ DIM(real))
     (cbox ((d - d) /⇩R g) ((e - d) /⇩R g))"
    by (subst (6) g_def) (auto simp add: field_simps)
  hence "((λt. f (Complex c t) * 𝗂 * g) has_integral x * g) {d..e}"
    by (subst (asm) has_integral_affinity_iff)
       (auto simp add: field_simps hg)
  hence "((λt. f (Complex c t) * 𝗂 * g * (1 / g)) has_integral x * g * (1 / g)) {d..e}"
    by (rule has_integral_mult_left)
  thus ?thesis using hg by auto
qed

subsection ‹Lemmas on asymptotics›

lemma eventually_at_top_linorderI':
  fixes c :: "'a :: {no_top, linorder}"
  assumes h: "⋀x. c < x ⟹ P x"
  shows "eventually P at_top"
proof (rule eventually_mono)
  show "∀⇩F x in at_top. c < x" by (rule eventually_gt_at_top)
  from h show "⋀x. c < x ⟹ P x" .
qed

lemma eventually_le_imp_bigo:
  assumes "∀⇩F x in F. ∥f x∥ ≤ g x"
  shows "f ∈ O[F](g)"
proof -
  from assms have "∀⇩F x in F. ∥f x∥ ≤ 1 * ∥g x∥" by eventually_elim auto
  thus ?thesis by (rule bigoI)
qed

lemma eventually_le_imp_bigo':
  assumes "∀⇩F x in F. ∥f x∥ ≤ g x"
  shows "(λx. ∥f x∥) ∈ O[F](g)"
proof -
  from assms have "∀⇩F x in F. ∥∥f x∥∥ ≤ 1 * ∥g x∥"
    by eventually_elim auto
  thus ?thesis by (rule bigoI)
qed

lemma le_imp_bigo:
  assumes "⋀x. ∥f x∥ ≤ g x"
  shows "f ∈ O[F](g)"
  by (intro eventually_le_imp_bigo eventuallyI assms)

lemma le_imp_bigo':
  assumes "⋀x. ∥f x∥ ≤ g x"
  shows "(λx. ∥f x∥) ∈ O[F](g)"
  by (intro eventually_le_imp_bigo' eventuallyI assms)

lemma exp_bigo:
  fixes f g :: "real ⇒ real"
  assumes "∀⇩F x in at_top. f x ≤ g x"
  shows "(λx. exp (f x)) ∈ O(λx. exp (g x))"
proof -
  from assms have "∀⇩F x in at_top. exp (f x) ≤ exp (g x)" by simp
  hence "∀⇩F x in at_top. ∥exp (f x)∥ ≤ 1 * ∥exp (g x)∥" by simp
  thus ?thesis by blast
qed

lemma ev_le_imp_exp_bigo:
  fixes f g :: "real ⇒ real"
  assumes hf: "∀⇩F x in at_top. 0 < f x"
    and hg: "∀⇩F x in at_top. 0 < g x"
    and le: "∀⇩F x in at_top. ln (f x) ≤ ln (g x)"
  shows "f ∈ O(g)"
proof -
  have "∀⇩F x in at_top. exp (ln (f x)) ≤ exp (ln (g x))"
    using le by simp
  hence "∀⇩F x in at_top. ∥f x∥ ≤ 1 * ∥g x∥"
    using hf hg by eventually_elim auto
  thus ?thesis by (intro bigoI)
qed

lemma smallo_ln_diverge_1:
  fixes f :: "real ⇒ real"
  assumes f_ln: "f ∈ o(ln)"
  shows "LIM x at_top. x * exp (- f x) :> at_top"
proof -
  have "(λx. ln x - f x) ∼[at_top] (λx. ln x)"
    using assms by (simp add: asymp_equiv_altdef)
  moreover have "filterlim (λx. ln x :: real) at_top at_top"
    by real_asymp
  ultimately have "filterlim (λx. ln x - f x) at_top at_top"
    using asymp_equiv_at_top_transfer asymp_equiv_sym by blast
  hence "filterlim (λx. exp (ln x - f x)) at_top at_top"
    by (rule filterlim_compose[OF exp_at_top])
  moreover have "∀⇩F x in at_top. exp (ln x - f x) = x * exp (- f x)"
    using eventually_gt_at_top[of 0]
    by eventually_elim (auto simp: exp_diff exp_minus field_simps)
  ultimately show ?thesis
    using filterlim_cong by fast
qed

lemma ln_ln_asymp_pos: "∀⇩F x :: real in at_top. 0 < ln (ln x)" by real_asymp
lemma ln_asymp_pos: "∀⇩F x :: real in at_top. 0 < ln x" by real_asymp
lemma x_asymp_pos: "∀⇩F x :: real in at_top. 0 < x" by auto

subsection ‹Lemmas of ‹floor›, ‹ceil› and ‹nat_powr››

lemma nat_le_self: "0 ≤ x ⟹ nat (int x) ≤ x" by auto
lemma floor_le: "⋀x :: real. ⌊x⌋ ≤ x" by auto
lemma ceil_ge: "⋀x :: real. x ≤ ⌈x⌉" by auto

lemma nat_lt_real_iff:
  "(n :: nat) < (a :: real) = (n < nat ⌈a⌉)"
proof -
  have "n < a = (of_int n < a)" by auto
  also have "… = (n < ⌈a⌉)" by (rule less_ceiling_iff [symmetric])
  also have "… = (n < nat ⌈a⌉)" by auto
  finally show ?thesis .
qed

lemma nat_le_real_iff:
  "(n :: nat) ≤ (a :: real) = (n < nat (⌊a⌋ + 1))"
proof -
  have "n ≤ a = (of_int n ≤ a)" by auto
  also have "… = (n ≤ ⌊a⌋)" by (rule le_floor_iff [symmetric])
  also have "… = (n < ⌊a⌋ + 1)" by auto
  also have "… = (n < nat (⌊a⌋ + 1))" by auto
  finally show ?thesis .
qed

lemma of_real_nat_power: "n nat_powr (of_real x :: complex) = of_real (n nat_powr x)" for n x
  by (subst of_real_of_nat_eq [symmetric])
     (subst powr_of_real, auto)

lemma norm_nat_power: "∥n nat_powr (s :: complex)∥ = n powr (Re s)"
  unfolding powr_def by auto

subsection ‹Elementary estimation of ‹exp› and ‹ln››

lemma ln_when_ge_3:
  "1 < ln x" if "3 ≤ x" for x :: real
proof (rule ccontr)
  assume "¬ 1 < ln x"
  hence "exp (ln x) ≤ exp 1" by auto
  hence "x ≤ exp 1" using that by auto
  thus False using e_less_272 that by auto
qed

lemma exp_lemma_1:
  fixes x :: real
  assumes "1 ≤ x"
  shows "1 + exp x ≤ exp (2 * x)"
proof -
  let ?y = "exp x"
  have "ln 2 ≤ x" using assms ln_2_less_1 by auto
  hence "exp (ln 2) ≤ ?y" by (subst exp_le_cancel_iff)
  hence "(3 / 2)⇧2 ≤ (?y - 1 / 2)⇧2" by auto
  hence "0 ≤ - 5 / 4 + (?y - 1 / 2)⇧2" by (simp add: power2_eq_square)
  also have "… = ?y⇧2 - ?y - 1" by (simp add: power2_eq_square field_simps)
  finally show ?thesis by (simp add: exp_double)
qed

lemma ln_bound_1:
  fixes t :: real
  assumes Ht: "0 ≤ t"
  shows "ln (14 + 4 * t) ≤ 4 * ln (t + 2)"
proof -
  have "ln (14 + 4 * t) ≤ ln (14 / 2 * (t + 2))" using Ht by auto
  also have "… = ln 7 + ln (t + 2)" using Ht by (subst ln_mult) auto
  also have "… ≤ 3 * ln (t + 2) + ln (t + 2)" proof -
    have "(14 :: real) ≤ 2 powr 4" by auto
    hence "exp (ln (14 :: real)) ≤ exp (4 * ln 2)"
      unfolding powr_def by (subst exp_ln) auto
    hence "ln (14 :: real) ≤ 4 * ln 2" by (subst (asm) exp_le_cancel_iff)
    hence "ln (14 / 2 :: real) ≤ 3 * ln 2" by (subst ln_div) auto
    also have "… ≤ 3 * ln (t + 2)" using Ht by auto
    finally show ?thesis by auto
  qed
  also have "… = 4 * ln (t + 2)" by auto
  finally show ?thesis by (auto simp add: field_simps)
qed

subsection ‹Miscellaneous lemmas›

abbreviation "fds_zeta_complex :: complex fds ≡ fds_zeta"

lemma powr_mono_lt_1_cancel:
  fixes x a b :: real
  assumes Hx: "0 < x ∧ x < 1"
  shows "(x powr a ≤ x powr b) = (b ≤ a)"
proof -
  have "(x powr a ≤ x powr b) = ((x powr -1) powr -a ≤ (x powr -1) powr -b)" by (simp add: powr_powr)
  also have "… = (-a ≤ -b)" using Hx by (intro powr_le_cancel_iff) (auto simp add: powr_neg_one)
  also have "… = (b ≤ a)" by auto
  finally show ?thesis .
qed

abbreviation "mangoldt_real :: _ ⇒ real ≡ mangoldt"
abbreviation "mangoldt_complex :: _ ⇒ complex ≡ mangoldt"

lemma norm_fds_mangoldt_complex:
  "⋀n. ∥fds_nth (fds mangoldt_complex) n∥ = mangoldt_real n" by (simp add: fds_nth_fds)

lemma suminf_norm_bound:
  fixes f :: "nat ⇒ 'a :: banach"
  assumes "summable g"
    and "⋀n. ∥f n∥ ≤ g n"
  shows "∥suminf f∥ ≤ (∑n. g n)"
proof -
  have *: "summable (λn. ∥f n∥)"
    by (rule summable_comparison_test' [where g = g])
       (use assms in auto)
  hence "∥suminf f∥ ≤ (∑n. ∥f n∥)" by (rule summable_norm)
  also have "(∑n. ∥f n∥) ≤ (∑n. g n)"
    by (rule suminf_le) (use assms * in auto)
  finally show ?thesis .
qed

lemma C⇩1_gt_zero: "0 < C⇩1" unfolding PNT_const_C⇩1_def by auto

unbundle no_pnt_notation
end