(* 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_notation 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_notation 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_notation 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_notation 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