Theory Prime_Distribution_Elementary_Library

(*
  File:    Prime_Distribution_Elementary_Library.thy
  Author:  Manuel Eberl, TU München

  Various auxiliary material, much of which should probably be moved somewhere else
  eventually.
*)
section ‹Auxiliary material›
theory Prime_Distribution_Elementary_Library
imports
  Zeta_Function.Zeta_Function
  Prime_Number_Theorem.Prime_Counting_Functions
  Stirling_Formula.Stirling_Formula
begin

lemma divisor_count_pos [intro]: "n > 0 ⟹ divisor_count n > 0"
  by (auto simp: divisor_count_def intro!: Nat.gr0I)

lemma divisor_count_eq_0_iff [simp]: "divisor_count n = 0 ⟷ n = 0"
  by (cases "n = 0") auto

lemma divisor_count_pos_iff [simp]: "divisor_count n > 0 ⟷ n > 0"
  by (cases "n = 0") auto

lemma smallest_prime_beyond_eval:
  "prime n ⟹ smallest_prime_beyond n = n"
  "¬prime n ⟹ smallest_prime_beyond n = smallest_prime_beyond (Suc n)"
proof -
  assume "prime n"
  thus "smallest_prime_beyond n = n"
    by (rule smallest_prime_beyond_eq) auto
next
  assume "¬prime n"
  show "smallest_prime_beyond n = smallest_prime_beyond (Suc n)"
  proof (rule antisym)
    show "smallest_prime_beyond n ≤ smallest_prime_beyond (Suc n)"
      by (rule smallest_prime_beyond_smallest)
         (auto intro: order.trans[OF _ smallest_prime_beyond_le])
  next
    have "smallest_prime_beyond n ≠ n"
      using prime_smallest_prime_beyond[of n] ‹¬prime n› by metis
    hence "smallest_prime_beyond n > n"
      using smallest_prime_beyond_le[of n] by linarith
    thus "smallest_prime_beyond n ≥ smallest_prime_beyond (Suc n)"
      by (intro smallest_prime_beyond_smallest) auto
  qed
qed

lemma nth_prime_numeral:
  "nth_prime (numeral n) = smallest_prime_beyond (Suc (nth_prime (pred_numeral n)))"
  by (subst nth_prime_Suc[symmetric]) auto

lemmas nth_prime_eval = smallest_prime_beyond_eval nth_prime_Suc nth_prime_numeral

lemma nth_prime_1 [simp]: "nth_prime (Suc 0) = 3"
  by (simp add: nth_prime_eval)

lemma nth_prime_2 [simp]: "nth_prime 2 = 5"
  by (simp add: nth_prime_eval)

lemma nth_prime_3 [simp]: "nth_prime 3 = 7"
  by (simp add: nth_prime_eval)

(* TODO: copied from afp-devel; delete in AFP 2019 *)
lemma strict_mono_sequence_partition:
  assumes "strict_mono (f :: nat ⇒ 'a :: {linorder, no_top})"
  assumes "x ≥ f 0"
  assumes "filterlim f at_top at_top"
  shows   "∃k. x ∈ {f k..<f (Suc k)}"
proof -
  define k where "k = (LEAST k. f (Suc k) > x)"
  {
    obtain n where "x ≤ f n"
      using assms by (auto simp: filterlim_at_top eventually_at_top_linorder)
    also have "f n < f (Suc n)"
      using assms by (auto simp: strict_mono_Suc_iff)
    finally have "∃n. f (Suc n) > x" by auto
  }
  from LeastI_ex[OF this] have "x < f (Suc k)"
    by (simp add: k_def)
  moreover have "f k ≤ x"
  proof (cases k)
    case (Suc k')
    have "k ≤ k'" if "f (Suc k') > x"
      using that unfolding k_def by (rule Least_le)
    with Suc show "f k ≤ x" by (cases "f k ≤ x") (auto simp: not_le)
  qed (use assms in auto)
  ultimately show ?thesis by auto
qed

lemma nth_prime_partition:
  assumes "x ≥ 2"
  shows   "∃k. x ∈ {nth_prime k..<nth_prime (Suc k)}"
  using strict_mono_sequence_partition[OF strict_mono_nth_prime, of x] assms nth_prime_at_top
  by simp

lemma nth_prime_partition':
  assumes "x ≥ 2"
  shows   "∃k. x ∈ {real (nth_prime k)..<real (nth_prime (Suc k))}"
  by (rule strict_mono_sequence_partition)
     (auto simp: strict_mono_Suc_iff assms
           intro!: filterlim_real_sequentially filterlim_compose[OF _ nth_prime_at_top])

lemma between_nth_primes_imp_nonprime:
  assumes "n > nth_prime k" "n < nth_prime (Suc k)"
  shows   "¬prime n"
  using assms by (metis Suc_leI not_le nth_prime_Suc smallest_prime_beyond_smallest)

lemma nth_prime_partition'':
  includes prime_counting_syntax
  assumes "x ≥ (2 :: real)"
  shows "x ∈ {real (nth_prime (nat ⌊π x⌋ - 1))..<real (nth_prime (nat ⌊π x⌋))}"
proof -
  obtain n where n: "x ∈ {nth_prime n..<nth_prime (Suc n)}"
    using nth_prime_partition' assms by auto
  have "π (nth_prime n) = π x"
    unfolding π_def using between_nth_primes_imp_nonprime n
    by (intro prime_sum_upto_eqI) (auto simp: le_nat_iff le_floor_iff)
  hence "real n = π x - 1"
    by simp
  hence n_eq: "n = nat ⌊π x⌋ - 1" "Suc n = nat ⌊π x⌋"
    by linarith+
  with n show ?thesis 
    by simp
qed
(* END TODO *)

(* TODO: Move *)
lemma asymp_equivD_strong:
  assumes "f ∼[F] g" "eventually (λx. f x ≠ 0 ∨ g x ≠ 0) F"
  shows   "((λx. f x / g x) ⤏ 1) F"
proof -
  from assms(1) have "((λx. if f x = 0 ∧ g x = 0 then 1 else f x / g x) ⤏ 1) F"
    by (rule asymp_equivD)
  also have "?this ⟷ ?thesis"
    by (intro filterlim_cong eventually_mono[OF assms(2)]) auto
  finally show ?thesis .
qed

lemma hurwitz_zeta_shift:
  fixes s :: complex
  assumes "a > 0" and "s ≠ 1"
  shows   "hurwitz_zeta (a + real n) s = hurwitz_zeta a s - (∑k<n. (a + real k) powr -s)"
proof (rule analytic_continuation_open[where f = "λs. hurwitz_zeta (a + real n) s"])
  fix s assume s: "s ∈ {s. Re s > 1}"
  have "(λk. (a + of_nat (k + n)) powr -s) sums hurwitz_zeta (a + real n) s"
    using sums_hurwitz_zeta[of "a + real n" s] s assms by (simp add: add_ac)
  moreover have "(λk. (a + of_nat k) powr -s) sums hurwitz_zeta a s"
    using sums_hurwitz_zeta[of a s] s assms by (simp add: add_ac)
  hence "(λk. (a + of_nat (k + n)) powr -s) sums
            (hurwitz_zeta a s - (∑k<n. (a + of_nat k) powr -s))"
    by (rule sums_split_initial_segment)
  ultimately show "hurwitz_zeta (a + real n) s = hurwitz_zeta a s - (∑k<n. (a + real k) powr -s)"
    by (simp add: sums_iff)
next
  show "connected (-{1::complex})"
    by (rule connected_punctured_universe) auto
qed (use assms in ‹auto intro!: holomorphic_intros open_halfspace_Re_gt exI[of _ 2]›)

lemma pbernpoly_bigo: "pbernpoly n ∈ O(λ_. 1)"
proof -
  from bounded_pbernpoly[of n] obtain c where "⋀x. norm (pbernpoly n x) ≤ c"
    by auto
  thus ?thesis by (intro bigoI[of _ c]) auto
qed

lemma harm_le: "n ≥ 1 ⟹ harm n ≤ ln n + 1"
  using euler_mascheroni_sequence_decreasing[of 1 n]
  by (simp add: harm_expand)

lemma sum_upto_1 [simp]: "sum_upto f 1 = f 1"
proof -
  have "{0<..Suc 0} = {1}" by auto
  thus ?thesis by (simp add: sum_upto_altdef)
qed

(* TODO: replace original *)
lemma sum_upto_cong' [cong]:
  "(⋀n. n > 0 ⟹ real n ≤ x ⟹ f n = f' n) ⟹ x = x' ⟹ sum_upto f x = sum_upto f' x'"
  unfolding sum_upto_def by (intro sum.cong) auto

lemma finite_primes_le: "finite {p. prime p ∧ real p ≤ x}"
  by (rule finite_subset[of _ "{..nat ⌊x⌋}"]) (auto simp: le_nat_iff le_floor_iff)

lemma frequently_filtermap: "frequently P (filtermap f F) = frequently (λn. P (f n)) F"
  by (auto simp: frequently_def eventually_filtermap)

lemma frequently_mono_filter: "frequently P F ⟹ F ≤ F' ⟹ frequently P F'"
  using filter_leD[of F F' "λx. ¬P x"] by (auto simp: frequently_def)

lemma π_at_top: "filterlim primes_pi at_top at_top"
  unfolding filterlim_at_top
proof safe
  fix C :: real
  define x0 where "x0 = real (nth_prime (nat ⌈max 0 C⌉))"
  show "eventually (λx. primes_pi x ≥ C) at_top"
    using eventually_ge_at_top
  proof eventually_elim
    fix x assume "x ≥ x0"
    have "C ≤ real (nat ⌈max 0 C⌉ + 1)" by linarith
    also have "real (nat ⌈max 0 C⌉ + 1) = primes_pi x0"
      unfolding x0_def by simp
    also have "… ≤ primes_pi x" by (rule π_mono) fact
    finally show "primes_pi x ≥ C" .
  qed
qed

lemma sum_upto_ln_stirling_weak_bigo: "(λx. sum_upto ln x - x * ln x + x) ∈ O(ln)"
proof -
  let ?f = "λx. x * ln x - x + ln (2 * pi * x) / 2"
  have "ln (fact n) - (n * ln n - n + ln (2 * pi * n) / 2) ∈ {0..1/(12*n)}" if "n > 0" for n :: nat
    using ln_fact_bounds[OF that] by (auto simp: algebra_simps)
  hence "(λn. ln (fact n) - ?f n) ∈ O(λn. 1 / real n)"
    by (intro bigoI[of _ "1/12"] eventually_mono[OF eventually_gt_at_top[of 0]]) auto
  hence "(λx. ln (fact (nat ⌊x⌋)) - ?f (nat ⌊x⌋)) ∈ O(λx. 1 / real (nat ⌊x⌋))"
    by (rule landau_o.big.compose)
       (intro filterlim_compose[OF filterlim_nat_sequentially] filterlim_floor_sequentially)
  also have "(λx. 1 / real (nat ⌊x⌋)) ∈ O(λx::real. ln x)" by real_asymp
  finally have "(λx. ln (fact (nat ⌊x⌋)) - ?f (nat ⌊x⌋) + (?f (nat ⌊x⌋) - ?f x)) ∈ O(λx. ln x)"
    by (rule sum_in_bigo) real_asymp
  hence "(λx. ln (fact (nat ⌊x⌋)) - ?f x) ∈ O(λx. ln x)"
    by (simp add: algebra_simps)
  hence "(λx. ln (fact (nat ⌊x⌋)) - ?f x + ln (2 * pi * x) / 2) ∈ O(λx. ln x)"
    by (rule sum_in_bigo) real_asymp
  thus ?thesis by (simp add: sum_upto_ln_conv_ln_fact algebra_simps)
qed


subsection ‹Various facts about Dirichlet series›

lemma fds_mangoldt':
  "fds mangoldt = fds_zeta * fds_deriv (fds moebius_mu)"
proof -
  have "fds mangoldt = (fds moebius_mu * fds (λn. of_real (ln (real n)) :: 'a))"
    (is "_ = ?f") by (subst fds_mangoldt) auto
  also have "… = fds_zeta * fds_deriv (fds moebius_mu)"
  proof (intro fds_eqI)
    fix n :: nat assume n: "n > 0"
    have "fds_nth ?f n = (∑d | d dvd n. moebius_mu d * of_real (ln (real (n div d))))"
      by (auto simp: fds_eq_iff fds_nth_mult dirichlet_prod_def)
    also have "… = (∑d | d dvd n. moebius_mu d * of_real (ln (real n / real d)))"
      by (intro sum.cong) (auto elim!: dvdE simp: ln_mult split: if_splits)
    also have "… = (∑d | d dvd n. moebius_mu d * of_real (ln n - ln d))"
      using n by (intro sum.cong refl) (subst ln_div, auto elim!: dvdE)
    also have "… = of_real (ln n) * (∑d | d dvd n. moebius_mu d) -
                      (∑d | d dvd n. of_real (ln d) * moebius_mu d)"
      by (simp add: sum_subtractf sum_distrib_left sum_distrib_right algebra_simps)
    also have "of_real (ln n) * (∑d | d dvd n. moebius_mu d) = 0"
      by (subst sum_moebius_mu_divisors') auto
    finally show "fds_nth ?f n = fds_nth (fds_zeta * fds_deriv (fds moebius_mu) :: 'a fds) n"
      by (simp add: fds_nth_mult dirichlet_prod_altdef1 fds_nth_deriv sum_negf scaleR_conv_of_real)
  qed
  finally show ?thesis .
qed

lemma sum_upto_divisor_sum1:
  "sum_upto (λn. ∑d | d dvd n. f d :: real) x = sum_upto (λn. f n * floor (x / n)) x"
proof -
  have "sum_upto (λn. ∑d | d dvd n. f d :: real) x =
          sum_upto (λn. f n * real (nat (floor (x / n)))) x"
    using sum_upto_dirichlet_prod[of f "λ_. 1" x]
    by (simp add: dirichlet_prod_def sum_upto_altdef)
  also have "… = sum_upto (λn. f n * floor (x / n)) x"
    unfolding sum_upto_def by (intro sum.cong) auto
  finally show ?thesis .
qed

lemma sum_upto_divisor_sum2:
  "sum_upto (λn. ∑d | d dvd n. f d :: real) x = sum_upto (λn. sum_upto f (x / n)) x"
  using sum_upto_dirichlet_prod[of "λ_. 1" f x] by (simp add: dirichlet_prod_altdef1)

lemma sum_upto_moebius_times_floor_linear:
  "sum_upto (λn. moebius_mu n * ⌊x / real n⌋) x = (if x ≥ 1 then 1 else 0)"
proof -
  have "real_of_int (sum_upto (λn. moebius_mu n * ⌊x / real n⌋) x) =
          sum_upto (λn. moebius_mu n * of_int ⌊x / real n⌋) x"
    by (simp add: sum_upto_def)
  also have "… = sum_upto (λn. ∑d | d dvd n. moebius_mu d :: real) x"
    using sum_upto_divisor_sum1[of moebius_mu x] by auto
  also have "… = sum_upto (λn. if n = 1 then 1 else 0) x"
    by (intro sum_upto_cong sum_moebius_mu_divisors' refl)
  also have "… = real_of_int (if x ≥ 1 then 1 else 0)"
    by (auto simp: sum_upto_def)
  finally show ?thesis unfolding of_int_eq_iff .
qed

lemma ln_fact_conv_sum_mangoldt:
  "sum_upto (λn. mangoldt n * ⌊x / real n⌋) x = ln (fact (nat ⌊x⌋))"
proof -
  have "sum_upto (λn. mangoldt n * of_int ⌊x / real n⌋) x =
          sum_upto (λn. ∑d | d dvd n. mangoldt d :: real) x"
    using sum_upto_divisor_sum1[of mangoldt x] by auto
  also have "… = sum_upto (λn. of_real (ln (real n))) x"
    by (intro sum_upto_cong mangoldt_sum refl) auto
  also have "… = (∑n∈{0<..nat ⌊x⌋}. ln n)"
    by (simp add: sum_upto_altdef)
  also have "… = ln (∏{0<..nat ⌊x⌋})"
    unfolding of_nat_prod by (subst ln_prod) auto
  also have "{0<..nat ⌊x⌋} = {1..nat ⌊x⌋}" by auto
  also have "∏… = fact (nat ⌊x⌋)"
    by (simp add: fact_prod)
  finally show ?thesis by simp
qed


subsection ‹Facts about prime-counting functions›

lemma abs_π [simp]: "¦primes_pi x¦ = primes_pi x"
  by (subst abs_of_nonneg) auto

lemma π_less_self:
  includes prime_counting_syntax
  assumes "x > 0"
  shows   "π x < x"
proof -
  have "π x ≤ (∑n∈{1<..nat ⌊x⌋}. 1)"
    unfolding π_def prime_sum_upto_altdef2 by (intro sum_mono2) (auto dest: prime_gt_1_nat)
  also have "… = real (nat ⌊x⌋ - 1)"
    using assms by simp
  also have "… < x" using assms by linarith
  finally show ?thesis .
qed

lemma π_le_self':
  includes prime_counting_syntax
  assumes "x ≥ 1"
  shows   "π x ≤ x - 1"
proof -
  have "π x ≤ (∑n∈{1<..nat ⌊x⌋}. 1)"
    unfolding π_def prime_sum_upto_altdef2 by (intro sum_mono2) (auto dest: prime_gt_1_nat)
  also have "… = real (nat ⌊x⌋ - 1)"
    using assms by simp
  also have "… ≤ x - 1" using assms by linarith
  finally show ?thesis .
qed

lemma π_le_self:
  includes prime_counting_syntax
  assumes "x ≥ 0"
  shows   "π x ≤ x"
  using π_less_self[of x] assms by (cases "x = 0") auto

subsection ‹Strengthening `Big-O' bounds›

text ‹
  The following two statements are crucial: They allow us to strengthen a `Big-O' statement
  for $n\to\infty$ or $x\to\infty$ to a bound for ∗‹all› $n\geq n_0$ or all $x\geq x_0$ under
  some mild conditions.

  This allows us to use all the machinery of asymptotics in Isabelle and still get a bound
  that is applicable over the full domain of the function in the end. This is important because
  Newman often shows that $f(x) \in O(g(x))$ and then writes
  \[\sum_{n\leq x} f(\frac{x}{n}) = \sum_{n\leq x} O(g(\frac{x}{n}))\]
  which is not easy to justify otherwise.
›
lemma natfun_bigoE:
  fixes f :: "nat ⇒ _"
  assumes bigo: "f ∈ O(g)" and nz: "⋀n. n ≥ n0 ⟹ g n ≠ 0"
  obtains c where "c > 0" "⋀n. n ≥ n0 ⟹ norm (f n) ≤ c * norm (g n)"
proof -
  from bigo obtain c where c: "c > 0" "eventually (λn. norm (f n) ≤ c * norm (g n)) at_top"
    by (auto elim: landau_o.bigE)
  then obtain n0' where n0': "⋀n. n ≥ n0' ⟹ norm (f n) ≤ c * norm (g n)"
    by (auto simp: eventually_at_top_linorder)
  define c' where "c' = Max ((λn. norm (f n) / norm (g n)) ` (insert n0 {n0..<n0'}))"
  have "norm (f n) ≤ max 1 (max c c') * norm (g n)" if "n ≥ n0" for n
  proof (cases "n ≥ n0'")
    case False
    with that have "norm (f n) / norm (g n) ≤ c'"
      unfolding c'_def by (intro Max.coboundedI) auto
    also have "… ≤ max 1 (max c c')" by simp
    finally show ?thesis using nz[of n] that by (simp add: field_simps)
  next
    case True
    hence "norm (f n) ≤ c * norm (g n)" by (rule n0')
    also have "… ≤ max 1 (max c c') * norm (g n)"
      by (intro mult_right_mono) auto
    finally show ?thesis .
  qed
  with that[of "max 1 (max c c')"] show ?thesis by auto
qed

lemma bigoE_bounded_real_fun:
  fixes f g :: "real ⇒ real"
  assumes "f ∈ O(g)"
  assumes "⋀x. x ≥ x0 ⟹ ¦g x¦ ≥ cg" "cg > 0"
  assumes "⋀b. b ≥ x0 ⟹ bounded (f ` {x0..b})"
  shows   "∃c>0. ∀x≥x0. ¦f x¦ ≤ c * ¦g x¦"
proof -
  from assms(1) obtain c where c: "c > 0" "eventually (λx. ¦f x¦ ≤ c * ¦g x¦) at_top"
    by (elim landau_o.bigE) auto
  then obtain b where b: "⋀x. x ≥ b ⟹ ¦f x¦ ≤ c * ¦g x¦"
    by (auto simp: eventually_at_top_linorder)
  have "bounded (f ` {x0..max x0 b})" by (intro assms) auto
  then obtain C where C: "⋀x. x ∈ {x0..max x0 b} ⟹ ¦f x¦ ≤ C"
    unfolding bounded_iff by fastforce

  define c' where "c' = max c (C / cg)"
  have "¦f x¦ ≤ c' * ¦g x¦" if "x ≥ x0" for x
  proof (cases "x ≥ b")
    case False
    then have "¦f x¦ ≤ C"
      using C that by auto
    with False have "¦f x¦ / ¦g x¦ ≤ C / cg"
      by (meson abs_ge_zero assms frac_le landau_omega.R_trans that)
    also have "… ≤ c'" by (simp add: c'_def)
    finally show "¦f x¦ ≤ c' * ¦g x¦"
      using that False assms(2)[of x] assms(3) by (auto simp add: divide_simps split: if_splits)
  next
    case True
    hence "¦f x¦ ≤ c * ¦g x¦" by (intro b) auto
    also have "… ≤ c' * ¦g x¦" by (intro mult_right_mono) (auto simp: c'_def)
    finally show ?thesis .
  qed
  moreover from c(1) have "c' > 0" by (auto simp: c'_def)
  ultimately show ?thesis by blast
qed

lemma sum_upto_asymptotics_lift_nat_real_aux:
  fixes f :: "nat ⇒ real" and g :: "real ⇒ real"
  assumes bigo: "(λn. (∑k=1..n. f k) - g (real n)) ∈ O(λn. h (real n))"
  assumes g_bigo_self: "(λn. g (real n) - g (real (Suc n))) ∈ O(λn. h (real n))"
  assumes h_bigo_self: "(λn. h (real n)) ∈ O(λn. h (real (Suc n)))"
  assumes h_pos: "⋀x. x ≥ 1 ⟹ h x > 0"
  assumes mono_g: "mono_on {1..} g ∨ mono_on {1..} (λx. - g x)"
  assumes mono_h: "mono_on {1..} h ∨ mono_on {1..} (λx. - h x)"
  shows   "∃c>0. ∀x≥1. sum_upto f x - g x ≤ c * h x"
proof -
  have h_nz: "h (real n) ≠ 0" if "n ≥ 1" for n
    using h_pos[of n] that by simp

  from natfun_bigoE[OF bigo h_nz] obtain c1 where
    c1: "c1 > 0" "⋀n. n ≥ 1 ⟹ norm ((∑k=1..n. f k) - g (real n)) ≤ c1 * norm (h (real n))"
    by auto
  from natfun_bigoE[OF g_bigo_self h_nz] obtain c2 where
    c2: "c2 > 0" "⋀n. n ≥ 1 ⟹ norm (g (real n) - g (real (Suc n))) ≤ c2 * norm (h (real n))"
    by auto
  from natfun_bigoE[OF h_bigo_self h_nz] obtain c3 where
    c3: "c3 > 0" "⋀n. n ≥ 1 ⟹ norm (h (real n)) ≤ c3 * norm (h (real (Suc n)))"
    by auto

  {
    fix x :: real assume x: "x ≥ 1"
    define n where "n = nat ⌊x⌋"
    from x have n: "n ≥ 1" unfolding n_def by linarith

    have "(∑k = 1..n. f k) - g x ≤ (c1 + c2) * h (real n)" using mono_g
    proof
      assume mono: "mono_on {1..} (λx. -g x)"
      from x have "x ≤ real (Suc n)"
        unfolding n_def by linarith
      hence "(∑k=1..n. f k) - g x ≤ (∑k=1..n. f k) - g n + (g n - g (Suc n))"
        using mono_onD[OF mono, of x "real (Suc n)"] x by auto
      also have "… ≤ norm ((∑k=1..n. f k) - g n) + norm (g n - g (Suc n))"
        by simp
      also have "… ≤ c1 * norm (h n) + c2 * norm (h n)"
        using n by (intro add_mono c1 c2) auto
      also have "… = (c1 + c2) * h n"
        using h_pos[of "real n"] n by (simp add: algebra_simps)
      finally show ?thesis .
    next
      assume mono: "mono_on {1..} g"
      have "(∑k=1..n. f k) - g x ≤ (∑k=1..n. f k) - g n"
        using x by (intro diff_mono mono_onD[OF mono]) (auto simp: n_def)
      also have "… ≤ c1 * h (real n)"
        using c1(2)[of n] n h_pos[of n] by simp
      also have "… ≤ (c1 + c2) * h (real n)"
        using c2 h_pos[of n] n by (intro mult_right_mono) auto
      finally show ?thesis .
    qed
    also have "(c1 + c2) * h (real n) ≤ (c1 + c2) * (1 + c3) * h x"
      using mono_h
    proof
      assume mono: "mono_on {1..} (λx. -h x)"
      have "(c1 + c2) * h (real n) ≤ (c1 + c2) * (c3 * h (real (Suc n)))"
        using c3(2)[of n] n h_pos[of n] h_pos[of "Suc n"] c1(1) c2(1)
        by (intro mult_left_mono) (auto)
      also have "… = (c1 + c2) * c3 * h (real (Suc n))"
        by (simp add: mult_ac)
      also have "… ≤ (c1 + c2) * (1 + c3) * h (real (Suc n))"
        using c1(1) c2(1) c3(1) h_pos[of "Suc n"] by (intro mult_left_mono mult_right_mono) auto
      also from x have "x ≤ real (Suc n)"
        unfolding n_def by linarith
      hence "(c1 + c2) * (1 + c3) * h (real (Suc n)) ≤ (c1 + c2) * (1 + c3) * h x"
        using c1(1) c2(1) c3(1) mono_onD[OF mono, of x "real (Suc n)"] x
        by (intro mult_left_mono) (auto simp: n_def)
      finally show "(c1 + c2) * h (real n) ≤ (c1 + c2) * (1 + c3) * h x" .
    next
      assume mono: "mono_on {1..} h"
      have "(c1 + c2) * h (real n) = 1 * ((c1 + c2) * h (real n))" by simp
      also have "… ≤ (1 + c3) * ((c1 + c2) * h (real n))"
        using c1(1) c2(1) c3(1) h_pos[of n] x n by (intro mult_right_mono) auto
      also have "… = (1 + c3) * (c1 + c2) * h (real n)"
        by (simp add: mult_ac)
      also have "… ≤ (1 + c3) * (c1 + c2) * h x"
        using x c1(1) c2(1) c3(1) h_pos[of n] n
        by (intro mult_left_mono mono_onD[OF mono]) (auto simp: n_def)
      finally show "(c1 + c2) * h (real n) ≤ (c1 + c2) * (1 + c3) * h x"
        by (simp add: mult_ac)
    qed
    also have "(∑k = 1..n. f k) = sum_upto f x"
      unfolding sum_upto_altdef n_def by (intro sum.cong) auto
    finally have "sum_upto f x - g x ≤ (c1 + c2) * (1 + c3) * h x" .
  }
  moreover have "(c1 + c2) * (1 + c3) > 0"
    using c1(1) c2(1) c3(1) by (intro mult_pos_pos add_pos_pos) auto
  ultimately show ?thesis by blast
qed

lemma sum_upto_asymptotics_lift_nat_real:
  fixes f :: "nat ⇒ real" and g :: "real ⇒ real"
  assumes bigo: "(λn. (∑k=1..n. f k) - g (real n)) ∈ O(λn. h (real n))"
  assumes g_bigo_self: "(λn. g (real n) - g (real (Suc n))) ∈ O(λn. h (real n))"
  assumes h_bigo_self: "(λn. h (real n)) ∈ O(λn. h (real (Suc n)))"
  assumes h_pos: "⋀x. x ≥ 1 ⟹ h x > 0"
  assumes mono_g: "mono_on {1..} g ∨ mono_on {1..} (λx. - g x)"
  assumes mono_h: "mono_on {1..} h ∨ mono_on {1..} (λx. - h x)"
  shows   "∃c>0. ∀x≥1. ¦sum_upto f x - g x¦ ≤ c * h x"
proof -
  have "∃c>0. ∀x≥1. sum_upto f x - g x ≤ c * h x"
    by (intro sum_upto_asymptotics_lift_nat_real_aux assms)
  then obtain c1 where c1: "c1 > 0" "⋀x. x ≥ 1 ⟹ sum_upto f x - g x ≤ c1 * h x"
    by auto

  have "(λn. -(g (real n) - g (real (Suc n)))) ∈ O(λn. h (real n))"
    by (subst landau_o.big.uminus_in_iff) fact
  also have "(λn. -(g (real n) - g (real (Suc n)))) = (λn. g (real (Suc n)) - g (real n))"
    by simp
  finally have "(λn. g (real (Suc n)) - g (real n)) ∈ O(λn. h (real n))" .
  moreover {
    have "(λn. -((∑k=1..n. f k) - g (real n))) ∈ O(λn. h (real n))"
      by (subst landau_o.big.uminus_in_iff) fact
    also have "(λn. -((∑k=1..n. f k) - g (real n))) =
                 (λn. (∑k=1..n. -f k) + g (real n))" by (simp add: sum_negf)
    finally have "(λn. (∑k=1..n. - f k) + g (real n)) ∈ O(λn. h (real n))" .
  }
  ultimately have "∃c>0. ∀x≥1. sum_upto (λn. -f n) x - (-g x) ≤ c * h x" using mono_g
    by (intro sum_upto_asymptotics_lift_nat_real_aux assms) (simp_all add: disj_commute)
  then obtain c2 where c2: "c2 > 0" "⋀x. x ≥ 1 ⟹ sum_upto (λn. - f n) x + g x ≤ c2 * h x"
    by auto

  {
    fix x :: real assume x: "x ≥ 1"
    have "sum_upto f x - g x ≤ max c1 c2 * h x"
      using h_pos[of x] x by (intro order.trans[OF c1(2)] mult_right_mono) auto
    moreover have "sum_upto (λn. -f n) x + g x ≤ max c1 c2 * h x"
      using h_pos[of x] x by (intro order.trans[OF c2(2)] mult_right_mono) auto
    hence "-(sum_upto f x - g x) ≤ max c1 c2 * h x"
      by (simp add: sum_upto_def sum_negf)
    ultimately have "¦sum_upto f x - g x¦ ≤ max c1 c2 * h x" by linarith
  }
  moreover from c1(1) c2(1) have "max c1 c2 > 0" by simp
  ultimately show ?thesis by blast
qed

lemma (in factorial_semiring) primepow_divisors_induct [case_names zero unit factor]:
  assumes "P 0" "⋀x. is_unit x ⟹ P x"
          "⋀p k x. prime p ⟹ k > 0 ⟹ ¬p dvd x ⟹ P x ⟹ P (p ^ k * x)"
  shows   "P x"
proof -
  have "finite (prime_factors x)" by simp
  thus ?thesis
  proof (induction "prime_factors x" arbitrary: x rule: finite_induct)
    case empty
    hence "prime_factors x = {}" by metis
    hence "prime_factorization x = {#}" by simp
    thus ?case using assms(1,2) by (auto simp: prime_factorization_empty_iff)
  next
    case (insert p A x)
    define k where "k = multiplicity p x"
    have "k > 0" using insert.hyps
      by (auto simp: prime_factors_multiplicity k_def)
    have p: "p ∈ prime_factors x" using insert.hyps by auto
    from p have "x ≠ 0" "¬is_unit p" by (auto simp: in_prime_factors_iff)

    from multiplicity_decompose'[OF this] obtain y where y: "x = p ^ k * y" "¬p dvd y"
      by (auto simp: k_def)
    have "prime_factorization x = replicate_mset k p + prime_factorization y"
      using p ‹k > 0› y unfolding y
      by (subst prime_factorization_mult)
         (auto simp: prime_factorization_prime_power in_prime_factors_iff)
    moreover from y p have "p ∉ prime_factors y"
      by (auto simp: in_prime_factors_iff)
    ultimately have "prime_factors y = prime_factors x - {p}"
      by auto
    also have "… = A"
      using insert.hyps by auto
    finally have "P y" using insert by auto
    thus "P x"
      unfolding y using y ‹k > 0› p by (intro assms(3)) (auto simp: in_prime_factors_iff)
  qed
qed

end