Theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
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 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 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 ‹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
end