Theory Prime_Sum_Limits
theory Prime_Sum_Limits
imports Rational_Padic_Valuations "Prime_Number_Theorem.Prime_Number_Theorem"
"HOL-Real_Asymp.Real_Asymp"
begin
section ‹Riemann-sum limits of sums over primes from the prime number theorem›
text ‹From the prime number theorem in the form ‹θ(x) ∼ x› (the AFP's
@{text θ_asymptotics}):
for a bounded function ‹φ› on ‹[a,
b]› that is continuous off a countable set,
‹∑⇩a⇩K⇩<⇩p⇩≤⇩b⇩K φ(p/K) ln p ≤
(∫⇩a⇧b φ + ε) K›
for all large ‹K›, and the version in the variable
‹x = K/p›. The proof uses Chebyshev's ‹θ› over the cells of a
uniform partition, step majorants
of ‹φ› and dominated convergence as the mesh goes to zero. Also the bookkeeping
‹ψ - θ› for the valuations of small primes.›
text ‹The prime number theorem in the form used (from
@{text "Prime_Number_Theorem.θ_asymptotics"}).›
lemma pnt_theta: "((λx. primes_theta x / x) ⤏ 1) at_top"
using θ_asymptotics
by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 0]]]) auto
subsection ‹Chebyshev's @{text θ} over cells›
text ‹@{text "θ(x) = ∑_{p ≤ x} log p"} as a sum over a set of
naturals.›
lemma theta_eq_sum: "0 ≤ x ⟹ primes_theta x = (∑ p ∈ {p. prime p ∧
real p ≤ x}. ln (real p))"
by (simp add: primes_theta_def prime_sum_upto_def)
lemma finite_primes_le: "finite {p. prime p ∧ real p ≤ x}"
proof (rule finite_subset[of _ "{..nat ⌊x⌋}"])
show "{p. prime p ∧ real p ≤ x} ⊆ {..nat ⌊x⌋}"
by (auto intro: le_nat_floor)
qed simp
text ‹The sum of @{text "log p"} over the primes in @{text "(c, d]"} is
@{text "θ(d) - θ(c)"}.›
lemma sum_cell:
assumes "0 ≤ c" "c ≤ d"
shows "(∑ p ∈ {p. prime p ∧ c < real p ∧
real p ≤ d}. ln (real p)) = primes_theta d - primes_theta c"
proof -
have "{p. prime p ∧ real p ≤ d} = {p. prime p ∧
real p ≤ c} ∪ {p. prime p ∧ c < real p ∧ real p ≤ d}"
using assms by auto
moreover have "{p. prime p ∧ real p ≤ c} ∩ {p. prime p ∧ c < real p ∧
real p ≤ d} = {}" by auto
ultimately show ?thesis
unfolding theta_eq_sum[OF assms(1)] theta_eq_sum[OF order_trans[OF assms]]
using sum.union_disjoint[of "{p. prime p ∧ real p ≤ c}" "{p. prime p ∧
c < real p ∧ real p ≤ d}" "λp. ln (real p)"]
finite_primes_le[of c] finite_subset[OF _ finite_primes_le[of d], of "{p. prime p ∧
c < real p ∧ real p ≤ d}"]
by fastforce
qed
lemma theta_ratio_eq: "0 < c ⟹ 0 < K ⟹
c * (primes_theta (c * real K) / (c * real K)) = primes_theta (c * real K) / real K"
by (simp add: field_simps)
text ‹@{text "θ(cK)/K ⟶ c"} along @{text "K ∈ ℕ"}.›
lemma theta_tendsto:
assumes "0 ≤ c"
shows "((λK :: nat. primes_theta (c * real K) / real K) ⤏ c) at_top"
proof (cases "c = 0")
case True
thus ?thesis by (simp add: primes_theta_def prime_sum_upto_def)
next
case False
hence c0: "0 < c" using assms by simp
have lim: "((λK :: nat. primes_theta (c * real K) / (c *
real K)) ⤏ 1) at_top"
proof -
have cK: "filterlim (λK :: nat. c * real K) at_top at_top"
by (rule filterlim_tendsto_pos_mult_at_top[OF tendsto_const c0 filterlim_real_sequentially])
show ?thesis using filterlim_compose[OF pnt_theta cK] by simp
qed
have "((λK :: nat. c * (primes_theta (c * real K) / (c *
real K))) ⤏ c * 1) at_top"
by (rule tendsto_mult_left[OF lim])
thus ?thesis
using Lim_transform_eventually[OF _ eventually_mono[OF eventually_gt_at_top[of "0::nat"]
theta_ratio_eq[OF c0]]] by auto
qed
lemma cell_tendsto:
assumes "0 ≤ c" "0 ≤ d"
shows "((λK :: nat. (primes_theta (d * real K) - primes_theta (c * real K)) /
real K) ⤏ d - c) at_top"
using tendsto_diff[OF theta_tendsto[OF assms(2)] theta_tendsto[OF assms(1)]]
by (simp add: diff_divide_distrib)
text ‹Eventually @{text "θ(dK) - θ(cK) ≤ (d - c + δ) K"} resp.
@{text "≥ (d - c - δ) K"}.›
lemma cell_upper:
assumes "0 ≤ c" "0 ≤ d" "0 < δ"
shows "∀⇩F K :: nat in at_top. primes_theta (d * real K) - primes_theta (c *
real K) ≤ (d - c + δ) * real K"
proof -
have "∀⇩F K :: nat in at_top. (primes_theta (d * real K) - primes_theta (c *
real K)) / real K < d - c + δ"
using order_tendstoD(2)[OF cell_tendsto[OF assms(1,2)], of "d - c + δ"] assms(3) by simp
moreover have "∀⇩F K :: nat in at_top. 0 < K" by (rule eventually_gt_at_top)
ultimately show ?thesis
by eventually_elim (simp add: divide_less_eq)
qed
lemma cell_lower:
assumes "0 ≤ c" "0 ≤ d" "0 < δ"
shows "∀⇩F K :: nat in at_top. (d - c - δ) * real K ≤
primes_theta (d * real K) - primes_theta (c * real K)"
proof -
have "∀⇩F K :: nat in at_top. d - c - δ <
(primes_theta (d * real K) - primes_theta (c * real K)) / real K"
using order_tendstoD(1)[OF cell_tendsto[OF assms(1,2)], of "d - c - δ"] assms(3) by simp
moreover have "∀⇩F K :: nat in at_top. 0 < K" by (rule eventually_gt_at_top)
ultimately show ?thesis
by eventually_elim (simp add: less_divide_eq)
qed
subsection ‹Small primes: @{text "ψ - θ"} and the valuation of 24›
text ‹@{text "ψ(n) = ∑_{p ≤ n} ⌊log_p n⌋ log p"}
(@{text "nat_log p n = floorlog p n - 1 = ⌊log_p n⌋"}).›
lemma card_powers_le: "prime p ⟹ 0 < n ⟹ card {i. 0 < i ∧
p ^ i ≤ n} = nat_log p n"
proof -
assume p: "prime p" and n: "0 < n"
have p1: "1 < p" using p by (rule prime_gt_1_nat)
have "{i. 0 < i ∧ p ^ i ≤ n} = {1..floorlog p n - 1}"
proof (intro equalityI subsetI)
fix i assume "i ∈ {i. 0 < i ∧ p ^ i ≤ n}"
hence i: "0 < i" "p ^ i ≤ n" by auto
have "Suc i ≤ floorlog p n" by (rule floorlog_ge_SucI[OF i(2) p1])
thus "i ∈ {1..floorlog p n - 1}" using i(1) by auto
next
fix i assume "i ∈ {1..floorlog p n - 1}"
hence i: "1 ≤ i" "i + 1 ≤ floorlog p n" by auto
have "p ^ (i + 1 - 1) ≤ n" by (rule floorlog_geD[OF i(2)]) simp
thus "i ∈ {i. 0 < i ∧ p ^ i ≤ n}" using i(1) by simp
qed
thus ?thesis by (simp add: nat_log_def)
qed
lemma psi_eq_sum:
"0 < n ⟹ primes_psi (real n) = (∑ p ∈ {p. prime p ∧
p ≤ n}. real (nat_log p n) * ln (real p))"
proof -
assume n: "0 < n"
define P where "P = {p. prime p ∧ p ≤ n}"
define I where "I p = {i. 0 < i ∧ p ^ i ≤ n}" for p
have fP: "finite P" unfolding P_def by simp
have fI: "finite (I p)" if p: "p ∈ P" for p
proof (rule finite_subset[of _ "{..n}"])
have p2: "2 ≤ p" using p by (simp add: P_def prime_ge_2_nat)
show "I p ⊆ {..n}"
proof
fix i assume "i ∈ I p"
hence i: "p ^ i ≤ n" by (simp add: I_def)
have "i < 2 ^ i" by simp
also have "2 ^ i ≤ p ^ i" using p2 by (rule power_mono) simp
finally show "i ∈ {..n}" using i by simp
qed
qed simp
have "primes_psi (real n) = (∑ (p, i) | prime p ∧ i > 0 ∧
real (p ^ i) ≤ real n. ln (real p))"
unfolding primes_psi_def by (rule sum_upto_primepows) (simp_all add: mangoldt_non_primepow)
also have "{(p, i). prime p ∧ i > 0 ∧ real (p ^ i) ≤ real n} = Sigma P I"
proof (intro equalityI subsetI)
fix x assume "x ∈ {(p, i). prime p ∧ i > 0 ∧ real (p ^ i) ≤ real n}"
then obtain p i where x: "x = (p, i)" "prime p" "0 < i" "p ^ i ≤ n" by auto
have "p ≤ p ^ i" using x(2,3) prime_ge_1_nat[OF x(2)] by (intro self_le_power) simp_all
thus "x ∈ Sigma P I" using x by (simp add: P_def I_def)
next
fix x assume "x ∈ Sigma P I"
thus "x ∈ {(p, i). prime p ∧ i > 0 ∧ real (p ^ i) ≤ real n}"
by (force simp: P_def I_def)
qed
also have "(∑ (p, i) ∈ Sigma P I. ln (real p)) = (∑ p ∈ P. ∑ i ∈
I p. ln (real p))"
by (rule sum.Sigma[symmetric, OF fP]) (use fI in blast)
also have "… = (∑ p ∈ P. real (nat_log p n) * ln (real p))"
proof (rule sum.cong[OF refl])
fix p assume p: "p ∈ P"
have "card (I p) = nat_log p n" unfolding I_def using p n
by (intro card_powers_le) (simp_all add: P_def)
thus "(∑ i ∈ I p. ln (real p)) = real (nat_log p n) * ln (real p)" by simp
qed
finally show ?thesis unfolding P_def .
qed
text ‹@{text "∑_{p ≤ N} (⌊log_p N⌋ - 1) log p =
ψ(N) - θ(N) ≤ 2 log N √N"}.›
lemma psi_minus_theta_sum:
assumes "2 ≤ N"
shows "(∑ p ∈ {p. prime p ∧
p ≤ N}. (real (nat_log p N) - 1) * ln (real p)) ≤ 2 * ln (real N) * sqrt (real N)"
proof -
have "(∑ p ∈ {p. prime p ∧
p ≤ N}. (real (nat_log p N) - 1) * ln (real p)) =
primes_psi (real N) - primes_theta (real N)"
unfolding psi_eq_sum[of N] theta_eq_sum[of "real N"] using assms
by (simp add: sum_subtractf left_diff_distrib psi_eq_sum theta_eq_sum)
also have "… ≤ 2 * ln (real N) * sqrt (real N)" using assms
by (intro ψ_minus_θ_bound) simp
finally show ?thesis .
qed
lemma eventually_psi_theta_small:
assumes "0 < δ"
shows "∀⇩F K :: nat in at_top. 2 * ln (real (5 * K)) * sqrt (real (5 * K)) ≤
δ * real K"
proof -
have "((λK :: nat. 2 * ln (5 * real K) * sqrt (5 * real K) /
real K) ⤏ 0) at_top"
by real_asymp
hence "∀⇩F K :: nat in at_top. 2 * ln (5 * real K) * sqrt (5 * real K) / real K <
δ"
using assms by (rule order_tendstoD)
moreover have "∀⇩F K :: nat in at_top. 0 < K" by (rule eventually_gt_at_top)
ultimately show ?thesis by eventually_elim (simp add: divide_less_eq)
qed
lemma mult24_log_le:
"prime p ⟹ real (multiplicity p (24::nat)) * ln (real p) ≤ (if p ≤
24 then ln 24 else 0)"
proof -
assume p: "prime p"
have pos: "0 < p" using p by (rule prime_gt_0_nat)
show ?thesis
proof (cases "p ≤ 24")
case True
have "p ^ multiplicity p 24 dvd (24::nat)" by (rule multiplicity_dvd)
hence "p ^ multiplicity p 24 ≤ (24::nat)" by (rule dvd_imp_le) simp
hence le': "real (p ^ multiplicity p 24) ≤ 24" by linarith
have pp: "0 < real (p ^ multiplicity p 24)" using pos by simp
have "real (multiplicity p (24::nat)) * ln (real p) = ln (real (p ^ multiplicity p 24))"
using pos by (simp add: ln_realpow)
also have "… ≤ ln 24" using le' pp by (simp add: ln_le_cancel_iff)
finally show ?thesis using True by simp
next
case False
have "¬ p dvd (24::nat)" using False by (fastforce dest: dvd_imp_le)
thus ?thesis using False by (simp add: not_dvd_imp_multiplicity_0)
qed
qed
subsection ‹Step majorants on a uniform partition›
text ‹Grid points of the uniform partition of @{text "[a, b]"} into @{text n} cells.›
definition cx :: "real ⇒ real ⇒ nat ⇒ nat ⇒ real"
where
"cx a b n i = a + (b - a) * real i / real n"
text ‹The supremum of @{text φ} over the closed @{text i}-th cell.›
definition cM :: "(real ⇒ real) ⇒ real ⇒ real ⇒ nat
⇒ nat ⇒ real" where
"cM φ a b n i = Sup (φ ` ({cx a b n i..cx a b n (i + 1)} ∩ {a..b}))"
text ‹The step majorant of @{text "φ + B"}.›
definition cG :: "(real ⇒ real) ⇒ real ⇒ real ⇒ real
⇒ nat ⇒ real ⇒ real" where
"cG φ a b B n y = (∑ i < n. indicator {cx a b n i<..cx a b n (i + 1)} y *
(cM φ a b n i + B))"
lemma cx_mono: "a ≤ b ⟹ i ≤ j ⟹ cx a b n i ≤ cx a b n j"
unfolding cx_def by (intro add_left_mono divide_right_mono mult_left_mono) simp_all
lemma cx_zero: "cx a b n 0 = a" by (simp add: cx_def)
lemma cx_self: "0 < n ⟹ cx a b n n = b" by (simp add: cx_def)
lemma cx_succ_sub: "0 < n ⟹ cx a b n (i + 1) - cx a b n i = (b - a) / real n"
by (simp add: cx_def field_simps)
lemma cx_ge: "a ≤ b ⟹ a ≤ cx a b n i" using cx_mono[of a b 0 i n]
by (simp add: cx_zero)
lemma cx_le: "a ≤ b ⟹ 0 < n ⟹ i ≤ n ⟹
cx a b n i ≤ b" using cx_mono[of a b i n n] by (simp add: cx_self)
lemma cell_unique:
assumes "a ≤ b" "y ∈ {cx a b n i<..cx a b n (i + 1)}" "y ∈
{cx a b n j<..cx a b n (j + 1)}"
shows "i = j"
proof (rule ccontr)
assume ne: "i ≠ j"
show False
proof (cases "i < j")
case True
have "cx a b n (i + 1) ≤ cx a b n j" using True by (intro cx_mono[OF assms(1)]) simp
thus False using assms(2,3) by auto
next
case False
hence "j < i" using ne by simp
hence "cx a b n (j + 1) ≤ cx a b n i" by (intro cx_mono[OF assms(1)]) simp
thus False using assms(2,3) by force
qed
qed
lemma cell_exists:
assumes "a < b" "0 < n" "y ∈ {a<..b}"
shows "∃i < n. y ∈ {cx a b n i<..cx a b n (i + 1)}"
proof -
have w: "0 < b - a" using assms(1) by simp
have nr: "0 < real n" using assms(2) by simp
have y: "a < y" "y ≤ b" using assms(3) by auto
define t where "t = (y - a) * real n / (b - a)"
have t0: "0 < t" unfolding t_def using y w nr by simp
have tn: "t ≤ real n" unfolding t_def using y w nr by (simp add: field_simps)
define k where "k = nat ⌈t⌉"
have k1: "1 ≤ k" unfolding k_def using t0 by linarith
have kn: "k ≤ n" unfolding k_def using tn by simp
have kt1: "real k - 1 < t" unfolding k_def using t0 by linarith
have kt2: "t ≤ real k" unfolding k_def using t0 by simp
have e: "real (k - 1) = real k - 1" using k1 by simp
have e2: "k - 1 + 1 = k" using k1 by simp
have lo: "cx a b n (k - 1) < y" unfolding cx_def e using kt1 w nr by (simp add: t_def field_simps)
have hi: "y ≤ cx a b n (k - 1 + 1)" unfolding cx_def e2 using kt2 w nr
by (simp add: t_def field_simps)
have "k - 1 < n" using k1 kn by linarith
thus ?thesis using lo hi by auto
qed
lemma cM_bdd:
fixes φ :: "real ⇒ real"
assumes "⋀y. y ∈ {a..b} ⟹ ¦φ y¦ ≤ B"
shows "bdd_above (φ ` ({cx a b n i..cx a b n (i + 1)} ∩ {a..b}))"
proof (rule bdd_aboveI[of _ B])
fix z assume "z ∈ φ ` ({cx a b n i..cx a b n (i + 1)} ∩ {a..b})"
then obtain y where y: "y ∈ {a..b}" "z = φ y" by auto
show "z ≤ B" using assms[OF y(1)] y(2) abs_ge_self[of "φ y"] by linarith
qed
lemma cM_le:
assumes "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ B" "0 ≤ B" "a ≤ b" "0 < n" "i < n"
shows "cM φ a b n i ≤ B"
proof -
have mem: "cx a b n i ∈ {cx a b n i..cx a b n (i + 1)} ∩ {a..b}"
using cx_mono[OF assms(3), of i "i + 1" n] cx_ge[OF assms(3), of n i] cx_le[OF assms(3,4),
of i] assms(5) by auto
have "Sup (φ ` ({cx a b n i..cx a b n (i + 1)} ∩ {a..b})) ≤ B"
proof (rule cSup_least)
show "φ ` ({cx a b n i..cx a b n (i + 1)} ∩ {a..b}) ≠ {}" using mem by blast
fix x assume "x ∈ φ ` ({cx a b n i..cx a b n (i + 1)} ∩ {a..b})"
then obtain y where y: "y ∈ {a..b}" "x = φ y" by auto
show "x ≤ B" using assms(1)[OF y(1)] y(2) by linarith
qed
thus ?thesis unfolding cM_def .
qed
lemma cM_ge:
assumes "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ B" "a ≤ b" "0 < n" "i < n"
shows "- B ≤ cM φ a b n i"
proof -
have mem: "cx a b n i ∈ {cx a b n i..cx a b n (i + 1)} ∩ {a..b}"
using cx_mono[OF assms(2), of i "i + 1" n] cx_ge[OF assms(2), of n i] cx_le[OF assms(2,3),
of i] assms(4) by auto
have "φ (cx a b n i) ≤ cM φ a b n i" unfolding cM_def
by (rule cSup_upper[OF imageI[OF mem] cM_bdd[OF assms(1)]])
moreover have "- B ≤ φ (cx a b n i)" using assms(1)[of "cx a b n i"] mem by fastforce
ultimately show ?thesis by linarith
qed
lemma le_cM:
assumes "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ B" "y ∈ {cx a b n i..cx a b n (i + 1)} ∩ {a..b}"
shows "φ y ≤ cM φ a b n i"
unfolding cM_def by (rule cSup_upper[OF _ cM_bdd[OF assms(1)]]) (use assms(2) in auto)
lemma cG_eval:
assumes "a < b" "0 < n" "y ∈ {a<..b}"
shows "∃i < n. y ∈ {cx a b n i<..cx a b n (i + 1)} ∧
cG φ a b B n y = cM φ a b n i + B"
proof -
obtain i where i: "i < n" "y ∈ {cx a b n i<..cx a b n (i + 1)}" using cell_exists[OF assms]
by blast
have "cG φ a b B n y = cM φ a b n i + B"
unfolding cG_def
proof -
have z: "indicator {cx a b n j<..cx a b n (j + 1)} y * (cM φ a b n j + B) = 0"
if j: "j ∈ {..<n} - {i}" for j
proof -
have "y ∉ {cx a b n j<..cx a b n (j + 1)}"
proof
assume "y ∈ {cx a b n j<..cx a b n (j + 1)}"
hence "j = i" by (rule cell_unique[OF less_imp_le[OF assms(1)] _ i(2)])
thus False using j by simp
qed
thus ?thesis by simp
qed
have "(∑ j < n. indicator {cx a b n j<..cx a b n (j + 1)} y * (cM φ a b n j + B)) =
indicator {cx a b n i<..cx a b n (i + 1)} y * (cM φ a b n i + B) + (∑ j ∈
{..<n} - {i}. indicator {cx a b n j<..cx a b n (j + 1)} y * (cM φ a b n j + B))"
by (rule sum.remove) (use i in auto)
also have "(∑ j ∈ {..<n} - {i}. indicator {cx a b n j<..cx a b n (j + 1)} y *
(cM φ a b n j + B)) = 0"
by (rule sum.neutral) (use z in blast)
also have "indicator {cx a b n i<..cx a b n (i + 1)} y * (cM φ a b n i + B) =
cM φ a b n i + B" using i(2) by simp
finally show "(∑ j < n. indicator {cx a b n j<..cx a b n (j + 1)} y * (cM φ a b n j +
B)) = cM φ a b n i + B" by simp
qed
thus ?thesis using i by blast
qed
lemma cG_bounds:
assumes "a < b" "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ B" "0 ≤ B" "0 < n" "y ∈ {a<..b}"
shows "φ y + B ≤ cG φ a b B n y ∧ 0 ≤ cG φ a b B n y ∧
cG φ a b B n y ≤ 2 * B"
proof -
obtain i where i: "i < n" "y ∈ {cx a b n i<..cx a b n (i + 1)}" and e: "cG φ a b B n y =
cM φ a b n i + B"
using cG_eval[OF assms(1,4,5)] by blast
have "φ y ≤ cM φ a b n i" using i assms(5) by (intro le_cM[OF assms(2)]) auto
moreover have "cM φ a b n i ≤ B"
by (rule cM_le[OF assms(2,3) less_imp_le[OF assms(1)] assms(4) i(1)])
moreover have "- B ≤ cM φ a b n i"
by (rule cM_ge[OF assms(2) less_imp_le[OF assms(1)] assms(4) i(1)])
ultimately show ?thesis unfolding e by linarith
qed
lemma cG_measurable [measurable]: "cG φ a b B n ∈ borel_measurable borel"
unfolding cG_def by measurable
text ‹At a continuity point of @{text φ} inside @{text "(a, b)"},
the majorants converge to @{text "φ y + B"}.›
lemma cG_tendsto:
assumes "a < b" "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ B" "y ∈ {a<..<b}" "isCont φ y"
shows "((λn. cG φ a b B n y) ⤏ φ y + B) at_top"
proof (rule tendstoI)
fix η :: real assume η: "0 < η"
obtain δ where δ: "0 < δ" "⋀u. dist u y < δ ⟹
dist (φ u) (φ y) < η / 2"
proof -
have h: "∀r>0. ∃s>0. ∀x. x ≠ y ∧
dist x y < s ⟶ dist (φ x) (φ y) < r"
using assms(4) unfolding isCont_def LIM_eq dist_norm .
have "∃s>0. ∀x. x ≠ y ∧ dist x y < s ⟶
dist (φ x) (φ y) < η / 2"
by (rule h[rule_format]) (use η in simp)
then obtain s where s: "0 < s" "⋀x. x ≠ y ⟹
dist x y < s ⟹ dist (φ x) (φ y) < η / 2" by blast
have "dist (φ u) (φ y) < η / 2" if "dist u y < s" for u
proof (cases "u = y")
case True thus ?thesis using η by simp
next
case False thus ?thesis using s(2) that by blast
qed
thus ?thesis using s(1) that by blast
qed
obtain N :: nat where N: "(b - a) / δ < real N" using reals_Archimedean2 by blast
show "∀⇩F n in at_top. dist (cG φ a b B n y) (φ y + B) < η"
proof (rule eventually_at_top_linorderI[of "N + 1"])
fix n :: nat assume n: "N + 1 ≤ n"
have n0: "0 < n" using n by simp
obtain i where i: "i < n" "y ∈ {cx a b n i<..cx a b n (i +
1)}" and e: "cG φ a b B n y = cM φ a b n i + B"
using cG_eval[OF assms(1) n0, of y φ B] assms(3) by auto
have low: "φ y ≤ cM φ a b n i" using i assms(3) by (intro le_cM[OF assms(2)]) auto
have width: "cx a b n (i + 1) - cx a b n i < δ"
proof -
have "b - a < real N * δ" using N δ(1) by (simp add: divide_less_eq)
moreover have "real N * δ ≤ real n * δ" using n δ(1) by simp
ultimately have "b - a < real n * δ" by linarith
thus ?thesis unfolding cx_succ_sub[OF n0] using n0
by (simp add: pos_divide_less_eq mult.commute)
qed
have up: "cM φ a b n i ≤ φ y + η / 2"
unfolding cM_def
proof (rule cSup_least)
show "φ ` ({cx a b n i..cx a b n (i + 1)} ∩ {a..b}) ≠ {}"
using i(2) assms(3) by force
fix z assume "z ∈ φ ` ({cx a b n i..cx a b n (i + 1)} ∩ {a..b})"
then obtain u where u: "u ∈ {cx a b n i..cx a b n (i + 1)} ∩ {a..b}" "z =
φ u" by auto
have "dist u y < δ" using u(1) i(2) width by (fastforce simp: dist_real_def)
hence "dist (φ u) (φ y) < η / 2" by (rule δ(2))
thus "z ≤ φ y + η / 2" using u(2) abs_ge_self[of "φ u - φ y"]
unfolding dist_real_def by linarith
qed
show "dist (cG φ a b B n y) (φ y + B) < η" unfolding e dist_real_def
using low up η by simp
qed
qed
lemma set_integral_sum_nat:
fixes f :: "nat ⇒ real ⇒ real"
assumes "⋀i. i ∈ I ⟹ set_integrable lborel A (f i)"
shows "set_integrable lborel A (λx. ∑ i ∈ I. f i x) ∧
set_lebesgue_integral lborel A (λx. ∑ i ∈ I. f i x) = (∑ i ∈
I. set_lebesgue_integral lborel A (f i))"
proof -
have i: "⋀i. i ∈ I ⟹
integrable lborel (λx. indicator A x *⇩R f i x)" using assms
unfolding set_integrable_def .
have e: "(λx. indicator A x *⇩R (∑ i ∈ I. f i x)) =
(λx. ∑ i ∈ I. indicator A x *⇩R f i x)"
by (simp add: sum_distrib_left)
show ?thesis unfolding set_integrable_def set_lebesgue_integral_def e
using Bochner_Integration.integrable_sum[OF i] Bochner_Integration.integral_sum[OF i]
by (rule conjI)
qed
lemma integral_cG:
assumes "a < b" "0 < n"
shows "interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a b B n) = (∑ i <
n. (cM φ a b n i + B) * ((b - a) / real n))"
proof -
have ab: "a ≤ b" using assms(1) by simp
define C where "C i = {cx a b n i<..cx a b n (i + 1)}" for i
define c where "c i = cM φ a b n i + B" for i
have cx3: "a ≤ cx a b n i ∧ cx a b n (i + 1) ≤ b ∧
cx a b n i ≤ cx a b n (i + 1)" if "i < n" for i
using cx_ge[OF ab, of n i] cx_le[OF ab assms(2), of "i + 1"] cx_mono[OF ab,
of i "i + 1" n] that by auto
have nb: "{b} ∈ null_sets lborel" by (simp add: finite_imp_null_set_lborel)
have meas: "measure lborel (C i ∩ {a<..<b}) = (b - a) / real n" if i: "i < n" for i
proof -
have "C i ∩ {a<..<b} = C i - {b}" using cx3[OF i] unfolding C_def by fastforce
hence "measure lborel (C i ∩ {a<..<b}) = measure lborel (C i - {b})" by simp
also have "… = measure lborel (C i)" unfolding C_def
by (rule measure_Diff_null_set[OF _ nb]) simp
also have "… = cx a b n (i + 1) - cx a b n i" unfolding C_def using cx3[OF i] by simp
also have "… = (b - a) / real n" by (rule cx_succ_sub[OF assms(2)])
finally show ?thesis .
qed
have one: "set_lebesgue_integral lborel {a<..<b} (λy. indicator (C i) y * c i) =
c i * ((b - a) / real n)" if i: "i < n" for i
proof -
have "(λy. indicator {a<..<b} y *⇩R (indicator (C i) y * c i)) =
(λy. c i * indicator (C i ∩ {a<..<b}) y)"
by (auto simp: fun_eq_iff indicator_def)
hence "set_lebesgue_integral lborel {a<..<b} (λy. indicator (C i) y * c i) =
c i * measure lborel (C i ∩ {a<..<b})"
unfolding set_lebesgue_integral_def by simp
thus ?thesis unfolding meas[OF i] .
qed
have ints: "set_integrable lborel {a<..<b} (λy. indicator (C i) y * c i)"
if i: "i ∈ {..<n}" for i
proof -
have "(λy. indicator {a<..<b} y *⇩R (indicator (C i) y * c i)) =
(λy. c i * indicator (C i ∩ {a<..<b}) y)"
by (auto simp: fun_eq_iff indicator_def)
moreover have "integrable lborel (indicator (C i ∩ {a<..<b}) :: real ⇒ real)"
proof -
have "emeasure lborel (C i ∩ {a<..<b}) ≤ emeasure lborel {a<..<b}"
by (rule emeasure_mono) (simp_all add: C_def)
also have "… = ennreal (b - a)" using ab by simp
finally have "emeasure lborel (C i ∩ {a<..<b}) < ∞"
using ennreal_less_top[of "b - a"] by (auto intro: order.strict_trans1)
thus ?thesis by (simp add: integrable_indicator_iff C_def)
qed
ultimately show ?thesis unfolding set_integrable_def by simp
qed
have "interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a b B n) =
set_lebesgue_integral lborel {a<..<b} (λy. ∑ i < n. indicator (C i) y * c i)"
using ab unfolding cG_def C_def c_def by (simp add: interval_lebesgue_integral_le_eq)
also have "… = (∑ i < n. set_lebesgue_integral lborel {a<..<b} (λy. indicator
(C i) y * c i))"
by (rule conjunct2[OF set_integral_sum_nat[OF ints]])
also have "… = (∑ i < n. c i * ((b - a) / real n))"
by (rule sum.cong[OF refl]) (rule one, simp)
finally show ?thesis unfolding c_def .
qed
subsection ‹Dominated convergence for the majorants›
lemma ae_cG_tendsto:
assumes "a < b" "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ B" "countable D"
and "⋀y. y ∈ {a<..<b} ⟹ y ∉ D ⟹ isCont φ y"
shows "AE y in lborel. y ∈ {a<..<b} ⟶
((λn. cG φ a b B n y) ⤏ φ y + B) at_top"
proof -
have "AE y in lborel. y ∉ D" by (rule AE_not_in[OF countable_imp_null_set_lborel[OF
assms(3)]])
thus ?thesis
proof eventually_elim
case (elim y)
show ?case using cG_tendsto[of a b φ B y, OF assms(1,2)] assms(4) elim by blast
qed
qed
text ‹@{text "φ"} (restricted to @{text "(a, b)"}) is Borel measurable and
integrable.›
lemma phi_measurable:
fixes φ :: "real ⇒ real"
assumes "countable D" "⋀y. y ∈ {a<..<b} ⟹ y ∉ D ⟹
isCont φ y"
shows "(λy. indicator {a<..<b} y * φ y) ∈ borel_measurable borel"
proof (rule borel_measurable_continuous_countable_exceptions[of "D ∪ {a, b}"])
show "countable (D ∪ {a, b})" using assms(1) by simp
show "continuous_on (- (D ∪ {a, b})) (λy. indicator {a<..<b} y * φ y)"
proof (rule continuous_at_imp_continuous_on, rule ballI)
fix x assume x: "x ∈ - (D ∪ {a, b})"
show "isCont (λy. indicator {a<..<b} y * φ y) x"
proof (cases "x ∈ {a<..<b}")
case True
have "eventually (λy. y ∈ {a<..<b}) (nhds x)"
by (rule eventually_nhds_in_open) (use True in auto)
hence e: "eventually (λy. indicator {a<..<b} y * φ y = φ y) (nhds x)"
by eventually_elim simp
have "isCont φ x" using assms(2) True x by auto
thus ?thesis using isCont_cong[OF e] by simp
next
case False
hence "x ∈ {..<a} ∪ {b<..}" using x by force
hence "eventually (λy. y ∈ {..<a} ∪ {b<..}) (nhds x)"
by (intro eventually_nhds_in_open) auto
hence e: "eventually (λy. indicator {a<..<b} y * φ y = 0) (nhds x)"
by eventually_elim auto
have "isCont (λy. 0::real) x" by simp
thus ?thesis using isCont_cong[OF e] by simp
qed
qed
qed
lemma phi_integrable:
fixes φ :: "real ⇒ real"
assumes "a < b" "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ B" "countable D"
and "⋀y. y ∈ {a<..<b} ⟹ y ∉ D ⟹ isCont φ y"
shows "interval_lebesgue_integrable lborel (ereal a) (ereal b) φ"
proof -
have "integrable lborel (λy. indicator {a<..<b} y *⇩R φ y)"
proof (rule Bochner_Integration.integrable_bound)
show "integrable lborel (λy. indicator {a<..<b} y *⇩R B)"
using interval_integral_const(1)[of a b B] assms(1)
unfolding interval_lebesgue_integrable_def set_integrable_def by force
show "(λy. indicator {a<..<b} y *⇩R φ y) ∈ borel_measurable lborel"
using phi_measurable[of D a b φ, OF assms(3,4)] by fastforce
show "AE y in lborel. norm (indicator {a<..<b} y *⇩R φ y) ≤
norm (indicator {a<..<b} y *⇩R B)"
proof (rule AE_I2)
fix y :: real
show "norm (indicator {a<..<b} y *⇩R φ y) ≤
norm (indicator {a<..<b} y *⇩R B)"
using assms(2)[of y] by (force simp: indicator_def)
qed
qed
thus ?thesis unfolding interval_lebesgue_integrable_def set_integrable_def using assms(1) by force
qed
lemma integral_cG_tendsto:
assumes "a < b" "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ B" "0 ≤ B" "countable D"
and "⋀y. y ∈ {a<..<b} ⟹ y ∉ D ⟹ isCont φ y"
shows "((λn. interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a b B n))
⤏ interval_lebesgue_integral lborel (ereal a) (ereal b) (λy.
φ y + B)) at_top"
proof -
have ab: "ereal a ≤ ereal b" using assms(1) by simp
define s where "s n y = indicator {a<..<b} y *⇩R cG φ a b B n y" for n y
define g where "g y = indicator {a<..<b} y *⇩R (φ y + B)" for y
define w where "w y = indicator {a<..<b} y *⇩R (2 * B)" for y
have gm: "g ∈ borel_measurable lborel"
proof -
have "(λy. indicator {a<..<b} y * φ y) ∈ borel_measurable borel"
by (rule phi_measurable[of D a b φ, OF assms(4,5)])
moreover have "(λy. indicator {a<..<b} y * B :: real) ∈ borel_measurable borel"
by measurable
ultimately have "(λy. indicator {a<..<b} y * φ y + indicator {a<..<b} y * B) ∈
borel_measurable borel" by measurable
thus ?thesis unfolding g_def by (simp add: distrib_left)
qed
have sm: "s n ∈ borel_measurable lborel" for n unfolding s_def by measurable
have wi: "integrable lborel w"
using interval_integral_const(1)[of a b "2 * B"] assms(1)
unfolding interval_lebesgue_integrable_def set_integrable_def w_def by simp
have "AE y in lborel. y ∈ {a<..<b} ⟶
((λn. cG φ a b B n y) ⤏ φ y + B) at_top"
using assms(1,2,4,5) by (rule ae_cG_tendsto)
hence lim: "AE y in lborel. (λn. s n y) ⇢ g y"
proof (eventually_elim)
case (elim y)
show ?case
proof (cases "y ∈ {a<..<b}")
case True thus ?thesis using elim by (simp add: s_def g_def)
next
case False thus ?thesis by (simp add: s_def g_def)
qed
qed
have bound: "AE y in lborel. norm (s n y) ≤ w y" for n
proof (rule AE_I2)
fix y :: real
show "norm (s n y) ≤ w y"
proof (cases "y ∈ {a<..<b} ∧ 0 < n")
case True
have "0 ≤ cG φ a b B n y ∧ cG φ a b B n y ≤ 2 * B"
using cG_bounds[of a b φ B n y, OF assms(1,2,3)] True by auto
thus ?thesis using True by (simp add: s_def w_def)
next
case False
thus ?thesis using assms(3) by (auto simp: s_def w_def cG_def)
qed
qed
have "(λn. integral⇧L lborel (s n)) ⇢ integral⇧L
lborel g"
by (rule integral_dominated_convergence[OF gm sm wi lim bound])
thus ?thesis unfolding interval_lebesgue_integral_le_eq[OF ab] einterval_eq_Icc
set_lebesgue_integral_def s_def g_def .
qed
text ‹The change of variables @{text "x = 1/y"}:
@{text "∫_{1/M}^{1/3} y f(1/y) dy = ∫_3^M f(x)/x^3 dx"}.›
lemma integral_inv_subst:
fixes f :: "real ⇒ real"
assumes "3 ≤ M" "(λx. indicator {3<..<M} x * f x) ∈
borel_measurable borel" "⋀x. x ∈ {3..M} ⟹ ¦f x¦ ≤ Bd"
shows "interval_lebesgue_integral lborel (ereal (1 / M)) (ereal (1 / 3)) (λy. y * f (1 /
y))
= interval_lebesgue_integral lborel (ereal 3) (ereal M) (λx. f x / x ^ 3)"
proof (cases "M = 3")
case True
show ?thesis using True by simp
next
case False
note M = assms(1) and hm = assms(2) and Bnd = assms(3)
have M0: "0 < M" using M by simp
have M3: "3 < M" using M False by simp
have iM: "0 < 1 / M" using M0 by simp
define h where "h x = indicator {3<..<M} x * f x" for x :: real
have hm': "h ∈ borel_measurable borel" using hm unfolding h_def[abs_def] .
define F where "F u = - u * f (- 1 / u)" for u :: real
define g where "g x = - 1 / x" for x :: real
define g' where "g' x = 1 / x ^ 2" for x :: real
define c where "c = - (1 / 3 :: real)"
define d where "d = - (1 / M)"
have cd: "c < d" unfolding c_def d_def using M3 by (simp add: field_simps)
have gc: "g 3 = c" "g M = d" unfolding g_def c_def d_def by simp_all
have r: "interval_lebesgue_integral lborel (ereal (1 / M)) (ereal (1 / 3)) (λy. y * f (1 /
y))
= interval_lebesgue_integral lborel (ereal c) (ereal d) F"
using interval_integral_reflect[of "ereal (1 / M)" "ereal (1 / 3)" "λy. y * f (1 / y)"]
unfolding F_def c_def d_def by simp
have Fo: "set_integrable lborel {c<..<d} F"
proof -
have eq: "(λu. indicator {c<..<d} u *⇩R F u) =
(λu. indicator {c<..<d} u * (- u * h (- 1 / u)))"
proof (rule ext)
fix u :: real
show "indicator {c<..<d} u *⇩R F u = indicator {c<..<d} u * (- u * h (- 1 / u))"
proof (cases "u ∈ {c<..<d}")
case True
hence ud: "u < - (1 / M)" unfolding d_def by simp
hence u0: "u < 0" using iM by linarith
have "3 < - 1 / u" "- 1 / u < M" using True u0 M0 unfolding c_def d_def
by (auto simp: field_simps)
thus ?thesis unfolding F_def h_def using True by simp
qed simp
qed
have mm: "(λu. indicator {c<..<d} u * (- u * h (- 1 / u))) ∈
borel_measurable lborel"
using hm' by simp
show ?thesis unfolding set_integrable_def eq
proof (rule Bochner_Integration.integrable_bound)
show "integrable lborel (λu. indicator {c<..<d} u *⇩R Bd)"
using interval_integral_const(1)[of c d Bd] cd
unfolding interval_lebesgue_integrable_def set_integrable_def by simp
show "(λu. indicator {c<..<d} u * (- u * h (- 1 / u))) ∈ borel_measurable lborel"
by (rule mm)
show "AE u in lborel. norm (indicator {c<..<d} u * (- u * h (- 1 / u))) ≤
norm (indicator {c<..<d} u *⇩R Bd)"
proof (rule AE_I2)
fix u :: real
show "norm (indicator {c<..<d} u * (- u * h (- 1 / u))) ≤
norm (indicator {c<..<d} u *⇩R Bd)"
proof (cases "u ∈ {c<..<d}")
case True
hence ud: "u < - (1 / M)" "- (1 / 3) < u" unfolding c_def d_def by simp_all
hence u0: "u < 0" "- 1 ≤ u" using iM by linarith+
have i: "3 < - 1 / u" "- 1 / u < M" using True u0 M0 unfolding c_def d_def
by (auto simp: field_simps)
have fb: "¦f (- 1 / u)¦ ≤ Bd" using Bnd i by simp
have "¦- u * h (- 1 / u)¦ = ¦u¦ * ¦f (- 1 / u)¦"
unfolding h_def using i by (simp add: abs_mult)
also have "… ≤ 1 * Bd" by (rule mult_mono) (use u0 fb in auto)
finally show ?thesis using True by fastforce
qed simp
qed
qed
qed
have Fc: "set_integrable lborel {g 3..g M} F"
proof -
have "{g 3..g M} = {c<..<d} ∪ {c} ∪ {d}" unfolding gc using cd by force
moreover have "set_integrable lborel ({c<..<d} ∪ {c} ∪ {d}) F"
by (intro set_integrable_Un Fo set_borel_integrable_singleton) simp_all
ultimately show ?thesis by simp
qed
have derivg: "(g has_real_derivative g' x) (at x)" if "x ∈ {3..M}" for x
proof -
have "x ≠ 0" using that by simp
thus ?thesis unfolding g_def g'_def
by (fastforce simp: power2_eq_square intro: derivative_eq_intros)
qed
have contg': "continuous_on {3..M} g'" unfolding g'_def by (fastforce intro: continuous_intros)
have nn: "0 ≤ g' x" if "x ∈ {3..M}" for x unfolding g'_def by simp
have "interval_lebesgue_integral lborel (ereal (g 3)) (ereal (g M)) F =
interval_lebesgue_integral lborel (ereal 3) (ereal M) (λx. F (g x) * g' x)"
by (rule interval_integral_substitution(2)[OF Fc derivg contg' nn M])
moreover have "interval_lebesgue_integral lborel (ereal 3) (ereal M) (λx. F (g x) *
g' x) = interval_lebesgue_integral lborel (ereal 3) (ereal M) (λx. f x / x ^ 3)"
proof (rule interval_integral_cong)
fix x assume "x ∈ einterval (min (ereal 3) (ereal M)) (max (ereal 3) (ereal M))"
hence x: "3 < x" using M by simp
show "F (g x) * g' x = f x / x ^ 3" unfolding F_def g_def g'_def using x
by (simp add: field_simps power2_eq_square power3_eq_cube)
qed
ultimately show ?thesis unfolding r unfolding gc by simp
qed
subsection ‹The Riemann-sum bounds›
lemma split2_aux: "c * ((x + d) * k) = c * x * k + d * k * (c :: real)"
by (simp add: algebra_simps)
text ‹Outer range, variable @{text "y = p/K"}: Riemann-sum upper bound
for a bounded, almost-everywhere
continuous @{text φ} (step majorants + the PNT cell estimates).›
theorem outer_prime_sum_bound:
assumes a: "0 < a" and ab: "a ≤ b" and Bd: "⋀y. y ∈ {a..b} ⟹
¦φ y¦ ≤ Bd" and D: "countable D"
and cont: "⋀y. y ∈ {a<..<b} ⟹ y ∉ D ⟹
isCont φ y" and e: "0 < ε"
shows "∀⇩F K in at_top.
(∑ p ∈ {p. p ≤ nat (floor (b * real K)) ∧ prime p ∧
a * real K < real p ∧ real p ≤ b * real K}.
φ (real p / real K) * ln (real p))
≤ (interval_lebesgue_integral lborel (ereal a) (ereal b) φ + ε) * real K"
proof (cases "a = b")
case True
show ?thesis
proof (rule always_eventually, rule allI)
fix K :: nat
have e0: "{p. p ≤ nat (floor (b * real K)) ∧ prime p ∧ a * real K < real p ∧
real p ≤ b * real K} = {}"
using True by simp
show "(∑ p ∈ {p. p ≤ nat (floor (b * real K)) ∧ prime p ∧
a * real K < real p ∧ real p ≤ b * real K}.
φ (real p / real K) * ln (real p)) ≤
(interval_lebesgue_integral lborel (ereal a) (ereal b) φ + ε) * real K"
unfolding e0 using True e by auto
qed
next
case False
hence ab': "a < b" using ab by simp
have B0: "0 ≤ Bd" using Bd[of a] ab by auto
define I where "I = interval_lebesgue_integral lborel (ereal a) (ereal b) φ"
have IB: "interval_lebesgue_integral lborel (ereal a) (ereal b) (λy. φ y + Bd) =
I + (b - a) * Bd"
unfolding I_def
proof -
have phiI: "interval_lebesgue_integrable lborel (ereal a) (ereal b) φ" using ab' Bd D cont
by (rule phi_integrable)
show "interval_lebesgue_integral lborel (ereal a) (ereal b) (λy. φ y + Bd) =
interval_lebesgue_integral lborel (ereal a) (ereal b) φ + (b - a) * Bd"
using interval_lebesgue_integral_add(2)[OF phiI interval_integral_const(1)[of a b Bd]]
interval_integral_const(2)[of a b Bd] by simp
qed
obtain n where n0: "0 < n" and n1: "interval_lebesgue_integral lborel (ereal a) (ereal b) (cG
φ a b Bd n) < I + (b - a) * Bd + ε / 2"
proof -
have "((λn. interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a b Bd n))
⤏ interval_lebesgue_integral lborel (ereal a) (ereal b) (λy.
φ y + Bd)) at_top"
using ab' Bd B0 D cont by (rule integral_cG_tendsto)
hence lim: "((λn. interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a b
Bd n)) ⤏ I + (b - a) * Bd) at_top"
unfolding IB .
have "∀⇩F n in at_top. interval_lebesgue_integral lborel (ereal a) (ereal b) (cG
φ a b Bd n) < I + (b - a) * Bd + ε / 2"
using order_tendstoD(2)[OF lim, of "I + (b - a) * Bd + ε / 2"] e by auto
moreover have "∀⇩F n :: nat in at_top. 0 < n" by (rule eventually_gt_at_top)
ultimately have "∀⇩F n in at_top. 0 < n ∧
interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a b Bd n) <
I + (b - a) * Bd + ε / 2"
by eventually_elim simp
then obtain n where "0 < n" "interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a
b Bd n) < I + (b - a) * Bd + ε / 2"
by (auto simp: eventually_at_top_linorder)
thus ?thesis using that by blast
qed
define T where "T = (∑ i < n. cM φ a b n i + Bd)"
define δ where "δ = ε / (2 * ((2 * real n + 1) * Bd + 1))"
have d0: "0 < δ"
proof -
have "0 ≤ (2 * real n + 1) * Bd" by (intro mult_nonneg_nonneg B0) simp
hence "0 < 2 * ((2 * real n + 1) * Bd + 1)" by simp
thus ?thesis unfolding δ_def using e by simp
qed
have dB: "(2 * real n + 1) * Bd * δ ≤ ε / 2"
proof -
have "0 ≤ (2 * real n + 1) * Bd" by (intro mult_nonneg_nonneg B0) simp
hence "0 < 2 * ((2 * real n + 1) * Bd + 1)" by simp
hence eq: "δ * (2 * ((2 * real n + 1) * Bd + 1)) = ε" unfolding δ_def
by simp
have "(2 * real n + 1) * Bd * δ ≤ ((2 * real n + 1) * Bd + 1) * δ" using d0
by simp
also have "… = ε / 2" using eq by force
finally show ?thesis .
qed
have "∀⇩F K :: nat in at_top. ∀i < n.
primes_theta (cx a b n (i + 1) * real K) - primes_theta (cx a b n i * real K) ≤
((b - a) / real n + δ) * real K"
proof -
have "∀i∈{..<n}. ∀⇩F K :: nat in at_top.
primes_theta (cx a b n (i + 1) * real K) - primes_theta (cx a b n i * real K) ≤
((b - a) / real n + δ) * real K"
proof
fix i assume i: "i ∈ {..<n}"
have "0 ≤ cx a b n i" "0 ≤ cx a b n (i + 1)"
using cx_ge[OF ab, of n i] cx_ge[OF ab, of n "i + 1"] a by linarith+
hence "∀⇩F K :: nat in at_top. primes_theta (cx a b n (i + 1) * real K) -
primes_theta (cx a b n i * real K)
≤ (cx a b n (i + 1) - cx a b n i + δ) * real K" by (rule cell_upper[OF _ _ d0])
thus "∀⇩F K :: nat in at_top. primes_theta (cx a b n (i + 1) * real K) -
primes_theta (cx a b n i * real K)
≤ ((b - a) / real n + δ) * real K" unfolding cx_succ_sub[OF n0] .
qed
hence "∀⇩F K :: nat in at_top. ∀i∈{..<n}.
primes_theta (cx a b n (i + 1) * real K) - primes_theta (cx a b n i * real K) ≤
((b - a) / real n + δ) * real K"
by (rule eventually_ball_finite[OF finite_lessThan])
thus ?thesis by (rule eventually_mono) simp
qed
moreover have "∀⇩F K :: nat in at_top. (b - a - δ) * real K ≤
primes_theta (b * real K) - primes_theta (a * real K)"
by (rule cell_lower) (use a ab d0 in auto)
ultimately show ?thesis
using eventually_gt_at_top[of "0 :: nat"]
proof (eventually_elim)
case (elim K)
have Kr: "0 < real K" using elim(3) by simp
let ?s = "{p. p ≤ nat (floor (b * real K)) ∧ prime p ∧ a * real K < real p ∧
real p ≤ b * real K}"
have fin: "finite ?s" by simp
have seq: "?s = {p. prime p ∧ a * real K < real p ∧ real p ≤ b * real K}"
by (auto intro: le_nat_floor)
have tot: "(∑ p ∈ ?s. ln (real p)) =
primes_theta (b * real K) - primes_theta (a * real K)"
unfolding seq by (rule sum_cell) (use a ab Kr in ‹auto intro: mult_right_mono›)
have mem: "⋀p. p ∈ ?s ⟹ real p / real K ∈ {a<..b}"
using Kr by (auto simp: less_divide_eq divide_le_eq)
have maj: "(∑ p ∈ ?s. (φ (real p / real K) + Bd) * ln (real p)) ≤
(∑ p ∈ ?s. cG φ a b Bd n (real p / real K) * ln (real p))"
proof (rule sum_mono)
fix p assume p: "p ∈ ?s"
have "φ (real p / real K) + Bd ≤ cG φ a b Bd n (real p / real K)"
using ab' Bd B0 n0 mem[OF p] by (rule cG_bounds[THEN conjunct1])
moreover have "0 ≤ ln (real p)" using p prime_ge_1_nat[of p] by (intro ln_ge_zero) auto
ultimately show "(φ (real p / real K) + Bd) * ln (real p) ≤
cG φ a b Bd n (real p / real K) * ln (real p)"
by (rule mult_right_mono)
qed
have cGsum: "(∑ p ∈ ?s. cG φ a b Bd n (real p / real K) * ln (real p)) ≤
(∑ i < n. (cM φ a b n i + Bd) * (((b - a) / real n + δ) * real K))"
proof -
have "(∑ p ∈ ?s. cG φ a b Bd n (real p / real K) * ln (real p))
= (∑ i < n. (cM φ a b n i + Bd) * (∑ p ∈ {p ∈
?s. real p / real K ∈ {cx a b n i<..cx a b n (i + 1)}}. ln (real p)))"
proof -
have "(∑ p ∈ ?s. cG φ a b Bd n (real p / real K) * ln (real p)) =
(∑ p ∈ ?s. ∑ i <
n. indicator {cx a b n i<..cx a b n (i + 1)} (real p / real K) * (cM φ a b n i +
Bd) * ln (real p))"
unfolding cG_def sum_distrib_right ..
also have "… = (∑ i < n. ∑ p ∈
?s. indicator {cx a b n i<..cx a b n (i + 1)} (real p / real K) * (cM φ a b n i +
Bd) * ln (real p))"
by (rule sum.swap)
also have "… = (∑ i < n. (cM φ a b n i + Bd) * (∑ p ∈ {p ∈
?s. real p / real K ∈ {cx a b n i<..cx a b n (i + 1)}}. ln (real p)))"
proof (rule sum.cong[OF refl])
fix i assume "i ∈ {..<n}"
have "(∑ p ∈ ?s. indicator {cx a b n i<..cx a b n (i + 1)} (real p / real K) *
(cM φ a b n i + Bd) * ln (real p)) =
(∑ p ∈ ?s. if real p / real K ∈
{cx a b n i<..cx a b n (i + 1)} then (cM φ a b n i + Bd) * ln (real p) else 0)"
by (rule sum.cong[OF refl]) (simp add: indicator_def)
also have "… = (∑ p ∈ {p ∈ ?s. real p / real K ∈
{cx a b n i<..cx a b n (i + 1)}}. (cM φ a b n i + Bd) * ln (real p))"
by (rule sum.inter_filter[OF fin, symmetric])
also have "… = (cM φ a b n i + Bd) * (∑ p ∈ {p ∈
?s. real p / real K ∈ {cx a b n i<..cx a b n (i + 1)}}. ln (real p))"
by (rule sum_distrib_left[symmetric])
finally show "(∑ p ∈ ?s. indicator {cx a b n i<..cx a b n (i + 1)} (real p /
real K) * (cM φ a b n i + Bd) * ln (real p)) =
(cM φ a b n i + Bd) * (∑ p ∈ {p ∈ ?s. real p / real K ∈
{cx a b n i<..cx a b n (i + 1)}}. ln (real p))" .
qed
finally show ?thesis .
qed
also have "… ≤ (∑ i <
n. (cM φ a b n i + Bd) * (((b - a) / real n + δ) * real K))"
proof (rule sum_mono, rule mult_left_mono)
fix i assume i: "i ∈ {..<n}"
show "0 ≤ cM φ a b n i + Bd"
proof -
have "- Bd ≤ cM φ a b n i"
using Bd less_imp_le[OF ab'] n0 i[unfolded lessThan_iff] by (rule cM_ge)
thus ?thesis by linarith
qed
have "(∑ p ∈ {p ∈ ?s. real p / real K ∈
{cx a b n i<..cx a b n (i + 1)}}. ln (real p))
≤ (∑ p ∈ {p. prime p ∧ cx a b n i * real K < real p ∧
real p ≤ cx a b n (i + 1) * real K}. ln (real p))"
proof (rule sum_mono2)
show "finite {p. prime p ∧ cx a b n i * real K < real p ∧
real p ≤ cx a b n (i + 1) * real K}"
by (rule finite_subset[OF _ finite_primes_le[of "cx a b n (i + 1) * real K"]]) auto
show "{p ∈ ?s. real p / real K ∈ {cx a b n i<..cx a b n (i + 1)}} ⊆
{p. prime p ∧ cx a b n i * real K < real p ∧
real p ≤ cx a b n (i + 1) * real K}"
using Kr by (auto simp: less_divide_eq divide_le_eq)
fix p assume "p ∈ {p. prime p ∧ cx a b n i * real K < real p ∧
real p ≤ cx a b n (i + 1) * real K} -
{p ∈ ?s. real p / real K ∈ {cx a b n i<..cx a b n (i + 1)}}"
hence "prime p" by simp
thus "0 ≤ ln (real p)" using prime_ge_1_nat[of p] by (intro ln_ge_zero) auto
qed
also have "… = primes_theta (cx a b n (i + 1) * real K) - primes_theta (cx a b n i *
real K)"
proof (rule sum_cell)
show "0 ≤ cx a b n i * real K" using cx_ge[OF ab, of n i] a Kr by auto
show "cx a b n i * real K ≤ cx a b n (i + 1) * real K"
using cx_mono[OF ab, of i "i + 1" n] Kr by simp
qed
also have "… ≤ ((b - a) / real n + δ) * real K" using elim(1) i by auto
finally show "(∑ p ∈ {p ∈ ?s. real p / real K ∈
{cx a b n i<..cx a b n (i + 1)}}. ln (real p)) ≤
((b - a) / real n + δ) * real K" .
qed
finally show ?thesis .
qed
have split: "(∑ p ∈ ?s. φ (real p / real K) * ln (real p))
= (∑ p ∈ ?s. (φ (real p / real K) + Bd) * ln (real p)) - Bd * (∑ p ∈
?s. ln (real p))"
by (simp add: sum_subtractf sum_distrib_left sum.distrib algebra_simps)
have split2: "(∑ i < n. (cM φ a b n i + Bd) * (((b - a) / real n + δ) *
real K))
= interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a b Bd n) * real K +
δ * real K * T"
unfolding integral_cG[OF ab' n0] T_def
proof -
have "(∑ i < n. (cM φ a b n i + Bd) * (((b - a) / real n + δ) * real K)) =
(∑ i < n. (cM φ a b n i + Bd) * ((b - a) / real n) * real K + δ *
real K * (cM φ a b n i + Bd))"
by (rule sum.cong[OF refl]) (rule split2_aux)
also have "… = (∑ i < n. (cM φ a b n i + Bd) * ((b - a) / real n) * real K) +
(∑ i < n. δ * real K * (cM φ a b n i + Bd))"
by (rule sum.distrib)
also have "(∑ i < n. (cM φ a b n i + Bd) * ((b - a) / real n) * real K) =
(∑ i < n. (cM φ a b n i + Bd) * ((b - a) / real n)) * real K"
by (rule sum_distrib_right[symmetric])
also have "(∑ i < n. δ * real K * (cM φ a b n i + Bd)) =
δ * real K * (∑ i < n. cM φ a b n i + Bd)"
by (rule sum_distrib_left[symmetric])
finally show "(∑ i < n. (cM φ a b n i + Bd) * (((b - a) / real n + δ) *
real K)) =
(∑ i < n. (cM φ a b n i + Bd) * ((b - a) / real n)) * real K + δ *
real K * (∑ i < n. cM φ a b n i + Bd)" .
qed
have "T ≤ real n * (2 * Bd)"
unfolding T_def
proof -
have "(∑ i < n. cM φ a b n i + Bd) ≤ (∑ i < n. 2 * Bd)"
proof (rule sum_mono)
fix i assume i: "i ∈ {..<n}"
have "cM φ a b n i ≤ Bd"
using Bd B0 less_imp_le[OF ab'] n0 i[unfolded lessThan_iff] by (rule cM_le)
thus "cM φ a b n i + Bd ≤ 2 * Bd" by linarith
qed
thus "(∑ i < n. cM φ a b n i + Bd) ≤ real n * (2 * Bd)" by fastforce
qed
hence m1: "δ * real K * T ≤ δ * real K * (real n * (2 * Bd))"
by (rule mult_left_mono) (use d0 Kr in simp)
have m2: "Bd * ((b - a - δ) * real K) ≤
Bd * (primes_theta (b * real K) - primes_theta (a * real K))"
by (rule mult_left_mono[OF elim(2) B0])
have m3: "interval_lebesgue_integral lborel (ereal a) (ereal b) (cG φ a b Bd n) *
real K ≤ (I + (b - a) * Bd + ε / 2) * real K"
by (rule mult_right_mono[OF less_imp_le[OF n1]]) (use Kr in simp)
have m4: "(2 * real n + 1) * Bd * δ * real K ≤ ε / 2 * real K"
by (rule mult_right_mono[OF dB]) (use Kr in simp)
show ?case
unfolding split tot I_def[symmetric]
using maj cGsum split2 m1 m2 m3 m4
by (simp only: algebra_simps) argo
qed
qed
text ‹Inner range, variable @{text "x = K/p"}: substitute @{text "y = 1/x"} in the outer
bound.›
theorem inner_prime_sum_bound:
assumes M: "3 < M" and Bd: "⋀x. x ∈ {3..real M} ⟹
¦f x¦ ≤ Bd" and D: "countable D"
and cont: "⋀x. x ∈ {3<..<real M} ⟹ x ∉ D ⟹
isCont f x" and e: "0 < ε"
shows "∀⇩F K in at_top.
(∑ p ∈ {p. p ≤ K ∧ prime p ∧ K < p * M ∧
3 * p ≤ K}. real p * f (real K / real p) * ln (real p))
≤ (interval_lebesgue_integral lborel (ereal 3) (ereal (real M)) (λx. f x /
x ^ 3) + ε) * real K ^ 2"
proof -
have Mr: "3 < real M" using M by simp
have M0: "0 < real M" using Mr by simp
let ?φ = "λy. y * f (1 / y)"
have B0: "0 ≤ Bd" using Bd[of 3] Mr by auto
have phiB: "⋀y. y ∈ {1 / real M..1 / 3} ⟹ ¦?φ y¦ ≤ Bd"
proof -
fix y assume y: "y ∈ {1 / real M..1 / 3}"
have iM: "0 < 1 / real M" using M0 by simp
have "1 / real M ≤ y" using y by simp
hence y0: "0 < y" using iM by linarith
have y1: "y ≤ 1" using y by simp
have "3 ≤ 1 / y" using y y0 by (simp add: le_divide_eq)
moreover have "1 / y ≤ real M" using y y0 M0 by (simp add: field_simps)
ultimately have fb: "¦f (1 / y)¦ ≤ Bd" using Bd by simp
have "¦y * f (1 / y)¦ = y * ¦f (1 / y)¦" using y0 by (simp add: abs_mult)
also have "… ≤ 1 * Bd" by (rule mult_mono[OF y1 fb]) (use B0 in simp_all)
finally show "¦?φ y¦ ≤ Bd" by simp
qed
have phiC: "⋀y. y ∈ {1 / real M<..<1 / 3} ⟹
y ∉ (λx. 1 / x) ` D ⟹ isCont ?φ y"
proof -
fix y assume y: "y ∈ {1 / real M<..<1 / 3}" and yD: "y ∉ (λx. 1 / x) ` D"
have iM: "0 < 1 / real M" using M0 by simp
have "1 / real M < y" using y by simp
hence y0: "0 < y" using iM by linarith
have "3 < 1 / y" using y y0 by (simp add: less_divide_eq)
moreover have "1 / y < real M" using y y0 M0 by (simp add: field_simps)
moreover have "1 / y ∉ D"
proof
assume "1 / y ∈ D"
hence "1 / (1 / y) ∈ (λx. 1 / x) ` D" by (rule imageI)
thus False using yD by simp
qed
ultimately have c2: "isCont f (1 / y)" using cont by simp
have c1: "isCont (λy. 1 / y) y" using y0 by (auto intro: continuous_intros)
have "isCont (λy. f (1 / y)) y" using isCont_o2[OF c1 c2] by simp
thus "isCont ?φ y" by (auto intro: continuous_intros)
qed
have ho: "∀⇩F K in at_top.
(∑ p ∈ {p. p ≤ nat (floor (1 / 3 * real K)) ∧ prime p ∧
1 / real M * real K < real p ∧ real p ≤ 1 / 3 * real K}.
?φ (real p / real K) * ln (real p))
≤ (interval_lebesgue_integral lborel (ereal (1 / real M)) (ereal (1 / 3)) ?φ +
ε) * real K"
by (rule outer_prime_sum_bound[OF _ _ phiB countable_image[OF D] phiC e]) (use M0 Mr in
‹auto simp: divide_le_eq›)
have subst: "interval_lebesgue_integral lborel (ereal (1 / real M)) (ereal (1 / 3)) ?φ
= interval_lebesgue_integral lborel (ereal 3) (ereal (real M)) (λx. f x / x ^ 3)"
proof -
have m: "(λx. indicator {3<..<real M} x * f x) ∈ borel_measurable borel"
using D cont by (rule phi_measurable)
show ?thesis using less_imp_le[OF Mr] m Bd by (rule integral_inv_subst)
qed
show ?thesis
using ho eventually_gt_at_top[of "0 :: nat"]
proof (eventually_elim)
case (elim K)
have Kr: "0 < real K" using elim(2) by simp
have seq: "{p. p ≤ nat (floor (1 / 3 * real K)) ∧ prime p ∧
1 / real M * real K < real p ∧ real p ≤ 1 / 3 * real K}
= {p. p ≤ K ∧ prime p ∧ K < p * M ∧ 3 * p ≤ K}"
proof (intro equalityI subsetI)
fix p assume "p ∈ {p. p ≤ nat (floor (1 / 3 * real K)) ∧ prime p ∧
1 / real M * real K < real p ∧ real p ≤ 1 / 3 * real K}"
hence p: "prime p" "1 / real M * real K < real p" "real p ≤ 1 / 3 * real K" by auto
have "real K < real p * real M" using p(2) M0 by (simp add: field_simps)
hence b1: "K < p * M" by (metis of_nat_mult of_nat_less_iff)
have "3 * real p ≤ real K" using p(3) by simp
hence b2: "3 * p ≤ K" by simp
show "p ∈ {p. p ≤ K ∧ prime p ∧ K < p * M ∧ 3 * p ≤ K}"
using p(1) b1 b2 by simp
next
fix p assume "p ∈ {p. p ≤ K ∧ prime p ∧ K < p * M ∧ 3 * p ≤ K}"
hence p: "prime p" "K < p * M" "3 * p ≤ K" by auto
have a1: "real K < real p * real M" using p(2) by (metis of_nat_mult of_nat_less_iff)
have a2: "3 * real p ≤ real K" using p(3) by simp
have c1: "1 / real M * real K < real p" using a1 M0 by (simp add: field_simps)
have c2: "real p ≤ 1 / 3 * real K" using a2 by simp
have c3: "p ≤ nat (floor (1 / 3 * real K))" using c2 by (rule le_nat_floor)
show "p ∈ {p. p ≤ nat (floor (1 / 3 * real K)) ∧ prime p ∧
1 / real M * real K < real p ∧ real p ≤ 1 / 3 * real K}"
using p(1) c1 c2 c3 by simp
qed
have trm: "⋀p. prime p ⟹
real p * f (real K / real p) * ln (real p) =
real K * (?φ (real p / real K) * ln (real p))"
proof -
fix p :: nat assume p: "prime p"
have e1: "1 / (real p / real K) = real K / real p" by simp
have e2: "real K * (real p / real K) = real p" using Kr by simp
show "real p * f (real K / real p) * ln (real p) =
real K * (?φ (real p / real K) * ln (real p))"
unfolding e1 using e2 by (auto simp: mult.assoc[symmetric])
qed
have "(∑ p ∈ {p. p ≤ K ∧ prime p ∧ K < p * M ∧
3 * p ≤ K}. real p * f (real K / real p) * ln (real p))
= real K * (∑ p ∈ {p. p ≤ nat (floor (1 / 3 * real K)) ∧ prime p ∧
1 / real M * real K < real p ∧ real p ≤ 1 / 3 * real K}.
?φ (real p / real K) * ln (real p))"
unfolding seq sum_distrib_left
by (rule sum.cong[OF refl]) (rule trm, simp)
also have "… ≤ real K * ((interval_lebesgue_integral lborel (ereal (1 /
real M)) (ereal (1 / 3)) ?φ + ε) * real K)"
by (rule mult_left_mono[OF elim(1)]) (use Kr in simp)
finally show ?case unfolding subst
by (simp add: power2_eq_square mult_ac)
qed
qed
end