Theory Irrational_Series_Erdos_Straus
theory "Irrational_Series_Erdos_Straus" imports
Prime_Number_Theorem.Prime_Number_Theorem
Prime_Distribution_Elementary.PNT_Consequences
begin
section ‹Miscellaneous›
lemma suminf_comparison:
assumes "summable f" and gf: "⋀n. norm (g n) ≤ f n"
shows "suminf g ≤ suminf f"
proof (rule suminf_le)
show "g n ≤ f n" for n
using gf[of n] by auto
show "summable g"
using assms summable_comparison_test' by blast
show "summable f" using assms(1) .
qed
lemma tendsto_of_int_diff_0:
assumes "(λn. f n - of_int(g n)) ⇢ (0::real)" "∀⇩F n in sequentially. f n > 0"
shows "∀⇩F n in sequentially. 0 ≤ g n"
proof -
have "∀⇩F n in sequentially. ¦f n - of_int(g n)¦ < 1 / 2"
using assms(1)[unfolded tendsto_iff,rule_format,of "1/2"] by auto
then show ?thesis using assms(2)
by eventually_elim linarith
qed
lemma eventually_mono_sequentially:
assumes "eventually P sequentially"
assumes "⋀x. P (x+k) ⟹ Q (x+k)"
shows "eventually Q sequentially"
using sequentially_offset[OF assms(1),of k]
apply (subst eventually_sequentially_seg[symmetric,of _ k])
apply (elim eventually_mono)
by fact
lemma frequently_eventually_at_top:
fixes P Q::"'a::linorder ⇒ bool"
assumes "frequently P at_top" "eventually Q at_top"
shows "frequently (λx. P x ∧ (∀y≥x. Q y) ) at_top"
using assms
unfolding frequently_def eventually_at_top_linorder
by (metis (mono_tags, opaque_lifting) le_cases order_trans)
lemma eventually_at_top_mono:
fixes P Q::"'a::linorder ⇒ bool"
assumes event_P:"eventually P at_top"
assumes PQ_imp:"⋀x. x≥z ⟹ ∀y≥x. P y ⟹ Q x"
shows "eventually Q at_top"
proof -
obtain N where "∀n≥N. P n"
by (meson event_P eventually_at_top_linorder)
then have "Q x" when "x ≥ max N z" for x
using PQ_imp that by auto
then show ?thesis unfolding eventually_at_top_linorder
by blast
qed
lemma frequently_at_top_elim:
fixes P Q::"'a::linorder ⇒ bool"
assumes "∃⇩Fx in at_top. P x"
assumes "⋀i. P i ⟹ ∃j>i. Q j"
shows "∃⇩Fx in at_top. Q x"
using assms unfolding frequently_def eventually_at_top_linorder
by (meson leD le_cases less_le_trans)
lemma less_Liminf_iff:
fixes X :: "_ ⇒ _ :: complete_linorder"
shows "Liminf F X < C ⟷ (∃y<C. frequently (λx. y ≥ X x) F)"
by (force simp: not_less not_frequently not_le le_Liminf_iff simp flip: Not_eq_iff)
lemma sequentially_even_odd_imp:
assumes "∀⇩F N in sequentially. P (2*N)" "∀⇩F N in sequentially. P (2*N+1)"
shows "∀⇩F n in sequentially. P n"
proof -
obtain N where N_P:"∀x≥N. P (2 * x) ∧ P (2 * x + 1)"
using eventually_conj[OF assms]
unfolding eventually_at_top_linorder by auto
have "P n" when "n ≥ 2*N" for n
proof -
define n' where "n'= n div 2"
then have "n' ≥ N" using that by auto
then have "P (2 * n') ∧ P (2 * n' + 1)"
using N_P by auto
then show ?thesis unfolding n'_def
by (cases "even n") auto
qed
then show ?thesis unfolding eventually_at_top_linorder by auto
qed
section ‹Theorem 2.1 and Corollary 2.10›
context
fixes a b ::"nat⇒int "
assumes a_pos: "∀ n. a n >0 " and a_large: "∀⇩F n in sequentially. a n > 1"
and ab_tendsto: "(λn. ¦b n¦ / (a (n-1) * a n)) ⇢ 0"
begin
private lemma aux_series_summable: "summable (λn. b n / (∏k≤n. a k))"
proof -
have "⋀e. e>0 ⟹ ∀⇩F x in sequentially. ¦b x¦ / (a (x-1) * a x) < e"
using ab_tendsto[unfolded tendsto_iff]
apply (simp add: abs_mult flip: of_int_abs)
by (subst (asm) (2) abs_of_pos,use ‹∀ n. a n > 0› in auto)+
from this[of 1]
have "∀⇩F x in sequentially. ¦real_of_int(b x)¦ < (a (x-1) * a x)"
using ‹∀ n. a n > 0› by auto
moreover have "∀n. (∏k≤n. real_of_int (a k)) > 0"
using a_pos by (auto intro!:linordered_semidom_class.prod_pos)
ultimately have "∀⇩F n in sequentially. ¦b n¦ / (∏k≤n. a k)
< (a (n-1) * a n) / (∏k≤n. a k)"
apply (elim eventually_mono)
by (auto simp:field_simps)
moreover have "¦b n¦ / (∏k≤n. a k) = norm (b n / (∏k≤n. a k))" for n
using ‹∀n. (∏k≤n. real_of_int (a k)) > 0›[rule_format,of n] by auto
ultimately have "∀⇩F n in sequentially. norm (b n / (∏k≤n. a k))
< (a (n-1) * a n) / (∏k≤n. a k)"
by algebra
moreover have "summable (λn. (a (n-1) * a n) / (∏k≤n. a k))"
proof -
obtain s where a_gt_1:"∀ n≥s. a n >1"
using a_large[unfolded eventually_at_top_linorder] by auto
define cc where "cc= (∏k<s. a k)"
have "cc>0"
unfolding cc_def by (meson a_pos prod_pos)
have "(∏k≤n+s. a k) ≥ cc * 2^n" for n
proof -
have "prod a {s..<Suc (s + n)} ≥ 2^n"
proof (induct n)
case 0
then show ?case using a_gt_1 by auto
next
case (Suc n)
moreover have "a (s + Suc n) ≥ 2"
by (smt (verit, ccfv_threshold) a_gt_1 le_add1)
ultimately show ?case
apply (subst prod.atLeastLessThan_Suc,simp)
using mult_mono'[of 2 "a (Suc (s + n))" " 2 ^ n" "prod a {s..<Suc (s + n)}"]
by (simp add: mult.commute)
qed
moreover have "prod a {0..(n + s)} = prod a {..<s} * prod a {s..<Suc (s + n)} "
using prod.atLeastLessThan_concat[of 0 s "s+n+1" a]
by (simp add: add.commute lessThan_atLeast0 prod.atLeastLessThan_concat prod.head_if)
ultimately show ?thesis
using ‹cc>0› unfolding cc_def by (simp add: atLeast0AtMost)
qed
then have "1/(∏k≤n+s. a k) ≤ 1/(cc * 2^n)" for n
proof -
assume asm:"⋀n. cc * 2 ^ n ≤ prod a {..n + s}"
then have "real_of_int (cc * 2 ^ n) ≤ prod a {..n + s}" using of_int_le_iff by blast
moreover have "prod a {..n + s} >0" using ‹cc>0› by (simp add: a_pos prod_pos)
ultimately show ?thesis using ‹cc>0›
by (auto simp:field_simps simp del:of_int_prod)
qed
moreover have "summable (λn. 1/(cc * 2^n))"
proof -
have "summable (λn. 1/(2::int)^n)"
using summable_geometric[of "1/(2::int)"] by (simp add:power_one_over)
from summable_mult[OF this,of "1/cc"] show ?thesis by auto
qed
ultimately have "summable (λn. 1 / (∏k≤n+s. a k))"
apply (elim summable_comparison_test'[where N=0])
apply (unfold real_norm_def, subst abs_of_pos)
by (auto simp: ‹∀n. 0 < (∏k≤n. real_of_int (a k))›)
then have "summable (λn. 1 / (∏k≤n. a k))"
apply (subst summable_iff_shift[where k=s,symmetric])
by simp
then have "summable (λn. (a (n+1) * a (n+2)) / (∏k≤n+2. a k))"
proof -
assume asm:"summable (λn. 1 / real_of_int (prod a {..n}))"
have "1 / real_of_int (prod a {..n}) = (a (n+1) * a (n+2)) / (∏k≤n+2. a k)" for n
proof -
have "a (Suc (Suc n)) ≠ 0" "a (Suc n) ≠0"
using a_pos by (metis less_irrefl)+
then show ?thesis
by (simp add: atLeast0_atMost_Suc atMost_atLeast0)
qed
then show ?thesis using asm by auto
qed
then show "summable (λn. (a (n-1) * a n) / (∏k≤n. a k))"
apply (subst summable_iff_shift[symmetric,of _ 2])
by auto
qed
ultimately show ?thesis
apply (elim summable_comparison_test_ev[rotated])
by (simp add: eventually_mono)
qed
private fun get_c::"(nat ⇒ int) ⇒ (nat ⇒ int) ⇒ int ⇒ nat ⇒ (nat ⇒ int)" where
"get_c a' b' B N 0 = round (B * b' N / a' N)"|
"get_c a' b' B N (Suc n) = get_c a' b' B N n * a' (n+N) - B * b' (n+N)"
lemma ab_rationality_imp:
assumes ab_rational:"(∑n. (b n / (∏i ≤ n. a i))) ∈ ℚ"
shows "∃ (B::int)>0. ∃ c::nat⇒ int.
(∀⇩F n in sequentially. B*b n = c n * a n - c(n+1) ∧ ¦c(n+1)¦<a n/2)
∧ (λn. c (Suc n) / a n) ⇢ 0"
proof -
have [simp]:"a n ≠ 0" for n using a_pos by (metis less_numeral_extra(3))
obtain A::int and B::int where
AB_eq:"(∑n. real_of_int (b n) / real_of_int (prod a {..n})) = A / B" and "B>0"
proof -
obtain q::rat where "(∑n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q"
using ab_rational by (rule Rats_cases) simp
moreover obtain A::int and B::int where "q = Rat.Fract A B" "B > 0" "coprime A B"
by (rule Rat_cases) auto
ultimately show ?thesis by (auto intro!: that[of A B] simp:of_rat_rat)
qed
define f where "f ≡ (λn. b n / real_of_int (prod a {..n}))"
define R where "R ≡ (λN. (∑n. B*b (n+N+1) / prod a {N..n+N+1}))"
have all_e_ubound:"∀e>0. ∀⇩F M in sequentially. ∀n. ¦B*b (n+M+1) / prod a {M..n+M+1}¦ < e/4 * 1/2^n"
proof safe
fix e::real assume "e>0"
obtain N where N_a2: "∀n ≥ N. a n ≥ 2"
and N_ba: "∀n ≥ N. ¦b n¦ / (a (n-1) * a n) < e/(4*B)"
proof -
have "∀⇩F n in sequentially. ¦b n¦ / (a (n - 1) * a n) < e/(4*B)"
using order_topology_class.order_tendstoD[OF ab_tendsto,of "e/(4*B)"] ‹B>0› ‹e>0›
by auto
moreover have "∀⇩F n in sequentially. a n ≥ 2"
using a_large by (auto elim: eventually_mono)
ultimately have "∀⇩F n in sequentially. ¦b n¦ / (a (n - 1) * a n) < e/(4*B) ∧ a n ≥ 2"
by eventually_elim auto
then show ?thesis unfolding eventually_at_top_linorder using that
by auto
qed
have geq_N_bound:"¦B*b (n+M+1) / prod a {M..n+M+1}¦ < e/4 * 1/2^n" when "M≥N" for n M
proof -
define D where "D = B*b (n+M+1)/ (a (n+M) * a (n+M+1))"
have "¦B*b (n+M+1) / prod a {M..n+M+1}¦ = ¦D / prod a {M..<n+M}¦"
proof -
have "{M..n+M+1} = {M..<n+M} ∪ {n+M,n+M+1}" by auto
then have "prod a {M..n+M+1} = a (n+M) * a (n+M+1)* prod a {M..<n+M}" by simp
then show ?thesis unfolding D_def by (simp add:algebra_simps)
qed
also have "... < ¦e/4 * (1/prod a {M..<n+M})¦"
proof -
have "¦D¦ < e/4"
unfolding D_def using N_ba[rule_format, of "n+M+1"] ‹B>0› ‹M ≥ N› ‹e>0› a_pos
by (auto simp:field_simps abs_mult abs_of_pos)
from mult_strict_right_mono[OF this,of "1/prod a {M..<n+M}"] a_pos ‹e>0›
show ?thesis
apply (auto simp:abs_prod abs_mult prod_pos)
by (subst (2) abs_of_pos,auto)+
qed
also have "... ≤ e/4 * 1/2^n"
proof -
have "prod a {M..<n+M} ≥ 2^n"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case
using ‹M≥N› by (simp add: N_a2 mult.commute mult_mono' prod.atLeastLessThan_Suc)
qed
then have "real_of_int (prod a {M..<n+M}) ≥ 2^n"
using numeral_power_le_of_int_cancel_iff by blast
then show ?thesis using ‹e>0› by (auto simp:divide_simps)
qed
finally show ?thesis .
qed
show "∀⇩F M in sequentially. ∀n. ¦real_of_int (B * b (n + M + 1))
/ real_of_int (prod a {M..n + M + 1})¦ < e / 4 * 1 / 2 ^ n"
apply (rule eventually_sequentiallyI[of N])
using geq_N_bound by blast
qed
have R_tendsto_0:"R ⇢ 0"
proof (rule tendstoI)
fix e::real assume "e>0"
show "∀⇩F x in sequentially. dist (R x) 0 < e" using all_e_ubound[rule_format,OF ‹e>0›]
proof eventually_elim
case (elim M)
define g where "g = (λn. B*b (n+M+1) / prod a {M..n+M+1})"
have g_lt:"¦g n¦ < e/4 * 1/2^n" for n
using elim unfolding g_def by auto
have §: "summable (λn. (e/4) * (1/2)^n)"
by simp
then have g_abs_summable:"summable (λn. ¦g n¦)"
apply (elim summable_comparison_test')
by (metis abs_idempotent g_lt less_eq_real_def power_one_over real_norm_def times_divide_eq_right)
have "¦∑n. g n¦ ≤ (∑n. ¦g n¦)" by (rule summable_rabs[OF g_abs_summable])
also have "... ≤(∑n. e/4 * 1/2^n)"
proof (rule suminf_comparison)
show "summable (λn. e/4 * 1/2^n)"
using § unfolding power_divide by simp
show "⋀n. norm ¦g n¦ ≤ e / 4 * 1 / 2 ^ n" using g_lt less_eq_real_def by auto
qed
also have "... = (e/4) * (∑n. (1/2)^n)"
apply (subst suminf_mult[symmetric])
by (auto simp: algebra_simps power_divide)
also have "... = e/2" by (simp add:suminf_geometric[of "1/2"])
finally have "¦∑n. g n¦ ≤ e / 2" .
then show "dist (R M) 0 < e" unfolding R_def g_def using ‹e>0› by auto
qed
qed
obtain N where R_N_bound:"∀M ≥ N. ¦R M¦ ≤ 1 / 4"
and N_geometric:"∀M≥N. ∀n. ¦real_of_int (B * b (n + M + 1)) / (prod a {M..n + M + 1})¦ < 1 / 2 ^ n"
proof -
obtain N1 where N1:"∀M ≥ N1. ¦R M¦ ≤ 1 / 4"
using metric_LIMSEQ_D[OF R_tendsto_0,of "1/4"] all_e_ubound[rule_format,of 4,unfolded eventually_sequentially]
by (auto simp:less_eq_real_def)
obtain N2 where N2:"∀M≥N2. ∀n. ¦real_of_int (B * b (n + M + 1))
/ (prod a {M..n + M + 1})¦ < 1 / 2 ^ n"
using all_e_ubound[rule_format,of 4,unfolded eventually_sequentially]
by (auto simp:less_eq_real_def)
define N where "N=max N1 N2"
show ?thesis using that[of N] N1 N2 unfolding N_def by simp
qed
define C where "C = B * prod a {..<N} * (∑n<N. f n)"
have "summable f"
unfolding f_def using aux_series_summable .
have "A * prod a {..<N} = C + B * b N / a N + R N"
proof -
have "A * prod a {..<N} = B * prod a {..<N} * (∑n. f n)"
unfolding AB_eq f_def using ‹B>0› by auto
also have "... = B * prod a {..<N} * ((∑n<N+1. f n) + (∑n. f (n+N+1)))"
using suminf_split_initial_segment[OF ‹summable f›, of "N+1"] by auto
also have "... = B * prod a {..<N} * ((∑n<N. f n) + f N + (∑n. f (n+N+1)))"
using sum.atLeast0_lessThan_Suc by simp
also have "... = C + B * b N / a N + (∑n. B*b (n+N+1) / prod a {N..n+N+1})"
proof -
have "B * prod a {..<N} * f N = B * b N / a N"
proof -
have "{..N} = {..<N} ∪ {N}" using ivl_disj_un_singleton(2) by blast
then show ?thesis unfolding f_def by auto
qed
moreover have "B * prod a {..<N} * (∑n. f (n+N+1)) = (∑n. B*b (n+N+1) / prod a {N..n+N+1})"
proof -
have "summable (λn. f (n + N + 1))"
using ‹summable f› summable_iff_shift[of f "N+1"] by auto
moreover have "prod a {..<N} * f (n + N + 1) = b (n + N + 1) / prod a {N..n + N + 1}" for n
proof -
have "{..n + N + 1} = {..<N} ∪ {N..n + N + 1}" by auto
then show ?thesis
unfolding f_def
apply simp
apply (subst prod.union_disjoint)
by auto
qed
ultimately show ?thesis
apply (subst suminf_mult[symmetric])
by (auto simp: mult.commute mult.left_commute)
qed
ultimately show ?thesis unfolding C_def by (auto simp:algebra_simps)
qed
also have "... = C +B * b N / a N + R N"
unfolding R_def by simp
finally show ?thesis .
qed
have R_bound:"¦R M¦ ≤ 1 / 4" and R_Suc:"R (Suc M) = a M * R M - B * b (Suc M) / a (Suc M)"
when "M ≥ N" for M
proof -
define g where "g = (λn. B*b (n+M+1) / prod a {M..n+M+1})"
have g_abs_summable:"summable (λn. ¦g n¦)"
proof -
have "summable (λn. (1/2::real) ^ n)"
by simp
moreover have "¦g n¦ < 1/2^n" for n
using N_geometric[rule_format,OF that] unfolding g_def by simp
ultimately show ?thesis
apply (elim summable_comparison_test')
by (simp add: less_eq_real_def power_one_over)
qed
show "¦R M¦ ≤ 1 / 4" using R_N_bound[rule_format,OF that] .
have "R M = (∑n. g n)" unfolding R_def g_def by simp
also have "... = g 0 + (∑n. g (Suc n))"
apply (subst suminf_split_head)
using summable_rabs_cancel[OF g_abs_summable] by auto
also have "... = g 0 + 1/a M * (∑n. a M * g (Suc n))"
apply (subst suminf_mult)
by (auto simp: g_abs_summable summable_Suc_iff summable_rabs_cancel)
also have "... = g 0 + 1/a M * R (Suc M)"
proof -
have "a M * g (Suc n) = B * b (n + M + 2) / prod a {Suc M..n + M + 2}" for n
proof -
have "{M..Suc (Suc (M + n))} = {M} ∪ {Suc M..Suc (Suc (M + n))}" by auto
then show ?thesis
unfolding g_def using ‹B>0› by (auto simp:algebra_simps)
qed
then have "(∑n. a M * g (Suc n)) = R (Suc M)"
unfolding R_def by auto
then show ?thesis by auto
qed
finally have "R M = g 0 + 1 / a M * R (Suc M)" .
then have "R (Suc M) = a M * R M - g 0 * a M"
by (auto simp:algebra_simps)
moreover have "{M..Suc M} = {M,Suc M}" by auto
ultimately show "R (Suc M) = a M * R M - B * b (Suc M) / a (Suc M)"
unfolding g_def by auto
qed
define c where "c = (λn. if n≥N then get_c a b B N (n-N) else undefined)"
have c_rec:"c (n+1) = c n * a n - B * b n" when "n ≥ N" for n
unfolding c_def using that by (auto simp:Suc_diff_le)
have c_R:"c (Suc n) / a n = R n" when "n ≥ N" for n
using that
proof (induct rule:nat_induct_at_least)
case base
have "¦ c (N+1) / a N ¦ ≤ 1/2"
proof -
have "c N = round (B * b N / a N)" unfolding c_def by simp
moreover have "c (N+1) / a N = c N - B * b N / a N"
using a_pos[rule_format,of N]
by (auto simp:c_rec[of N,simplified] divide_simps)
ultimately show ?thesis using of_int_round_abs_le by auto
qed
moreover have "¦R N¦ ≤ 1 / 4" using R_bound[of N] by simp
ultimately have "¦c (N+1) / a N - R N ¦ < 1" by linarith
moreover have "c (N+1) / a N - R N ∈ ℤ"
proof -
have "c (N+1) / a N = c N - B * b N / a N"
using a_pos[rule_format,of N]
by (auto simp:c_rec[of N,simplified] divide_simps)
moreover have " B * b N / a N + R N ∈ ℤ"
proof -
have "C = B * (∑n<N. prod a {..<N} * (b n / prod a {..n}))"
unfolding C_def f_def by (simp add:sum_distrib_left algebra_simps)
also have "... = B * (∑n<N. prod a {n<..<N} * b n)"
proof -
have "{..<N} = {n<..<N} ∪ {..n}" if "n<N" for n
by (simp add: ivl_disj_un_one(1) sup_commute that)
then show ?thesis
using ‹B>0›
apply simp
apply (subst prod.union_disjoint)
by auto
qed
finally have "C = real_of_int (B * (∑n<N. prod a {n<..<N} * b n))" .
then have "C ∈ ℤ" using Ints_of_int by blast
moreover note ‹A * prod a {..<N} = C + B * b N / a N + R N›
ultimately show ?thesis
by (metis Ints_diff Ints_of_int add.assoc add_diff_cancel_left')
qed
ultimately show ?thesis by (simp add: diff_diff_add)
qed
ultimately have "c (N+1) / a N - R N = 0"
by (metis Ints_cases less_irrefl of_int_0 of_int_lessD)
then show ?case by simp
next
case (Suc n)
have "c (Suc (Suc n)) / a (Suc n) = c (Suc n) - B * b (Suc n) / a (Suc n)"
apply (subst c_rec[of "Suc n",simplified])
using ‹N ≤ n› by (auto simp: divide_simps)
also have "... = a n * R n - B * b (Suc n) / a (Suc n)"
using Suc by (auto simp: divide_simps)
also have "... = R (Suc n)"
using R_Suc[OF ‹N ≤ n›] by simp
finally show ?case .
qed
have ca_tendsto_zero:"(λn. c (Suc n) / a n) ⇢ 0"
using R_tendsto_0
apply (elim filterlim_mono_eventually)
using c_R by (auto intro!:eventually_sequentiallyI[of N])
have ca_bound:"¦c (n + 1)¦ < a n / 2" when "n ≥ N" for n
proof -
have "¦c (Suc n)¦ / a n = ¦c (Suc n) / a n¦" using a_pos[rule_format,of n] by auto
also have "... = ¦R n¦" using c_R[OF that] by auto
also have "... < 1/2" using R_bound[OF that] by auto
finally have "¦c (Suc n)¦ / a n < 1/2" .
then show ?thesis using a_pos[rule_format,of n] by auto
qed
show "∃B>0. ∃c. (∀⇩F n in sequentially. B * b n = c n * a n - c (n + 1)
∧ real_of_int ¦c (n + 1)¦ < a n / 2) ∧ (λn. c (Suc n) / a n) ⇢ 0"
unfolding eventually_at_top_linorder
apply (rule exI[of _ B],use ‹B>0› in simp)
apply (intro exI[of _c] exI[of _ N])
using c_rec ca_bound ca_tendsto_zero
by fastforce
qed
private lemma imp_ab_rational:
assumes "∃ (B::int)>0. ∃ c::nat⇒ int.
(∀⇩F n in sequentially. B*b n = c n * a n - c(n+1) ∧ ¦c(n+1)¦<a n/2)"
shows "(∑n. (b n / (∏i ≤ n. a i))) ∈ ℚ"
proof -
obtain B::int and c::"nat⇒int" and N::nat where "B>0" and
large_n:"∀n≥N. B * b n = c n * a n - c (n + 1) ∧ real_of_int ¦c (n + 1)¦ < a n / 2
∧ a n≥2"
proof -
obtain B c where "B>0" and event1:"∀⇩F n in sequentially. B * b n = c n * a n - c (n + 1)
∧ real_of_int ¦c (n + 1)¦ < real_of_int (a n) / 2"
using assms by auto
from eventually_conj[OF event1 a_large,unfolded eventually_at_top_linorder]
obtain N where "∀n≥N. (B * b n = c n * a n - c (n + 1)
∧ real_of_int ¦c (n + 1)¦ < real_of_int (a n) / 2) ∧ 2 ≤ a n"
by fastforce
then show ?thesis using that[of B N c] ‹B>0› by auto
qed
define f where "f=(λn. real_of_int (b n) / real_of_int (prod a {..n}))"
define S where "S = (∑n. f n)"
have "summable f"
unfolding f_def by (rule aux_series_summable)
define C where "C=B*prod a {..<N} * (∑n<N. f n)"
have "B*prod a {..<N} * S = C + real_of_int (c N)"
proof -
define h1 where "h1 ≡ (λn. (c (n+N) * a (n+N)) / prod a {N..n+N})"
define h2 where "h2 ≡ (λn. c (n+N+1) / prod a {N..n+N})"
have f_h12: "B * prod a {..<N}*f (n+N) = h1 n - h2 n" for n
proof -
define g1 where "g1 ≡ (λn. B * b (n+N))"
define g2 where "g2 ≡ (λn. prod a {..<N} / prod a {..n + N})"
have "B * prod a {..<N}*f (n+N) = (g1 n * g2 n)"
unfolding f_def g1_def g2_def by (auto simp:algebra_simps)
moreover have "g1 n = c (n+N) * a (n+N) - c (n+N+1)"
using large_n[rule_format,of "n+N"] unfolding g1_def by auto
moreover have "g2 n = (1/prod a {N..n+N})"
proof -
have "prod a ({..<N} ∪ {N..n + N}) = prod a {..<N} * prod a {N..n + N}"
apply (rule prod.union_disjoint[of "{..<N}" "{N..n+N}" a])
by auto
moreover have "prod a ({..<N} ∪ {N..n + N}) = prod a {..n+N}"
by (simp add: ivl_disj_un_one(4))
ultimately show ?thesis
unfolding g2_def
apply simp
using a_pos by (metis less_irrefl)
qed
ultimately have "B*prod a {..<N}*f (n+N) = (c (n+N) * a (n+N) - c (n+N+1)) / prod a {N..n+N}"
by auto
also have "... = h1 n - h2 n"
unfolding h1_def h2_def by (auto simp:algebra_simps diff_divide_distrib)
finally show ?thesis by simp
qed
have "B*prod a {..<N} * S = B*prod a {..<N} * ((∑n<N. f n) + (∑n. f (n+N)))"
using suminf_split_initial_segment[OF ‹summable f›,of N]
unfolding S_def by (auto simp:algebra_simps)
also have "... = C + B*prod a {..<N}*(∑n. f (n+N))"
unfolding C_def by (auto simp:algebra_simps)
also have "... = C + (∑n. h1 n - h2 n)"
apply (subst suminf_mult[symmetric])
using ‹summable f› f_h12 by auto
also have "... = C + h1 0"
proof -
have "(λn. ∑i≤n. h1 i - h2 i) ⇢ (∑i. h1 i - h2 i)"
proof (rule summable_LIMSEQ')
have "(λi. h1 i - h2 i) = (λi. real_of_int (B * prod a {..<N}) * f (i + N))"
using f_h12 by auto
then show "summable (λi. h1 i - h2 i)"
using ‹summable f› by (simp add: summable_mult)
qed
moreover have "(∑i≤n. h1 i - h2 i) = h1 0 - h2 n" for n
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
have "(∑i≤Suc n. h1 i - h2 i) = (∑i≤n. h1 i - h2 i) + h1 (n+1) - h2 (n+1)"
by auto
also have "... = h1 0 - h2 n + h1 (n+1) - h2 (n+1)" using Suc by auto
also have "... = h1 0 - h2 (n+1)"
proof -
have "h2 n = h1 (n+1)"
unfolding h2_def h1_def
apply (auto simp:prod.nat_ivl_Suc')
using a_pos by (metis less_numeral_extra(3))
then show ?thesis by auto
qed
finally show ?case by simp
qed
ultimately have "(λn. h1 0 - h2 n) ⇢ (∑i. h1 i - h2 i)" by simp
then have "h2 ⇢ (h1 0 - (∑i. h1 i - h2 i))"
apply (elim metric_tendsto_imp_tendsto)
by (auto intro!:eventuallyI simp add:dist_real_def)
moreover have "h2 ⇢ 0"
proof -
have h2_n:"¦h2 n¦ < (1 / 2)^(n+1)" for n
proof -
have "¦h2 n¦ = ¦c (n + N + 1)¦ / prod a {N..n + N}"
unfolding h2_def abs_divide
using a_pos by (simp add: abs_of_pos prod_pos)
also have "... < (a (N+n) / 2) / prod a {N..n + N}"
unfolding h2_def
apply (rule divide_strict_right_mono)
subgoal using large_n[rule_format,of "N+n"] by (auto simp:algebra_simps)
subgoal using a_pos by (simp add: prod_pos)
done
also have "... = 1 / (2*prod a {N..<n + N})"
apply (subst ivl_disj_un(6)[of N "n+N",symmetric])
using a_pos[rule_format,of "N+n"] by (auto simp:algebra_simps)
also have "... ≤ (1/2)^(n+1)"
proof (induct n)
case 0
then show ?case by auto
next
case (Suc n)
define P where "P=1 / real_of_int (2 * prod a {N..<n + N})"
have "1 / real_of_int (2 * prod a {N..<Suc n + N}) = P / a (n+N)"
unfolding P_def by (auto simp: prod.atLeastLessThan_Suc)
also have "... ≤ ( (1 / 2) ^ (n + 1) ) / a (n+N) "
apply (rule divide_right_mono)
subgoal unfolding P_def using Suc by auto
subgoal by (simp add: a_pos less_imp_le)
done
also have "... ≤ ( (1 / 2) ^ (n + 1) ) / 2 "
apply (rule divide_left_mono)
using large_n[rule_format,of "n+N",simplified] by auto
also have "... = (1 / 2) ^ (n + 2)" by auto
finally show ?case by simp
qed
finally show ?thesis .
qed
have "(λn. (1 / 2)^(n+1)) ⇢ (0::real)"
using tendsto_mult_right_zero[OF LIMSEQ_abs_realpow_zero2[of "1/2",simplified],of "1/2"]
by auto
then show ?thesis
apply (elim Lim_null_comparison[rotated])
using h2_n less_eq_real_def by (auto intro!:eventuallyI)
qed
ultimately have "(∑i. h1 i - h2 i) = h1 0"
using LIMSEQ_unique by fastforce
then show ?thesis by simp
qed
also have "... = C + c N"
unfolding h1_def using a_pos
by auto (metis less_irrefl)
finally show ?thesis .
qed
then have "S = (C + real_of_int (c N)) / (B*prod a {..<N})"
by (metis ‹0 < B› a_pos less_irrefl mult.commute mult_pos_pos
nonzero_mult_div_cancel_right of_int_eq_0_iff prod_pos)
moreover have "... ∈ ℚ"
unfolding C_def f_def by (intro Rats_divide Rats_add Rats_mult Rats_of_int Rats_sum)
ultimately show "S ∈ ℚ" by auto
qed
theorem theorem_2_1_Erdos_Straus :
"(∑n. (b n / (∏i ≤ n. a i))) ∈ ℚ ⟷ (∃ (B::int)>0. ∃ c::nat⇒ int.
(∀⇩F n in sequentially. B*b n = c n * a n - c(n+1) ∧ ¦c(n+1)¦<a n/2))"
using ab_rationality_imp imp_ab_rational by auto
text‹The following is a Corollary to Theorem 2.1. ›
corollary corollary_2_10_Erdos_Straus:
assumes ab_event:"∀⇩F n in sequentially. b n > 0 ∧ a (n+1) ≥ a n"
and ba_lim_leq:"lim (λn. (b(n+1) - b n )/a n) ≤ 0"
and ba_lim_exist:"convergent (λn. (b(n+1) - b n )/a n)"
and "liminf (λn. a n / b n) = 0 "
shows "(∑n. (b n / (∏i ≤ n. a i))) ∉ ℚ"
proof
assume "(∑n. (b n / (∏i ≤ n. a i))) ∈ ℚ"
then obtain B c where "B>0" and abc_event:"∀⇩F n in sequentially. B * b n = c n * a n - c (n + 1)
∧ ¦c (n + 1)¦ < a n / 2" and ca_vanish: "(λn. c (Suc n) / a n) ⇢ 0"
using ab_rationality_imp by auto
have bac_close:"(λn. B * b n / a n - c n) ⇢ 0"
proof -
have "∀⇩F n in sequentially. B * b n - c n * a n + c (n + 1) = 0"
using abc_event by (auto elim!:eventually_mono)
then have "∀⇩F n in sequentially. (B * b n - c n * a n + c (n+1)) / a n = 0 "
apply eventually_elim
by auto
then have "∀⇩F n in sequentially. B * b n / a n - c n + c (n + 1) / a n = 0"
apply eventually_elim
using a_pos by (auto simp:divide_simps) (metis less_irrefl)
then have "(λn. B * b n / a n - c n + c (n + 1) / a n) ⇢ 0"
by (simp add: eventually_mono tendsto_iff)
from tendsto_diff[OF this ca_vanish]
show ?thesis by auto
qed
have c_pos:"∀⇩F n in sequentially. c n > 0"
proof -
from bac_close have *:"∀⇩F n in sequentially. c n ≥ 0"
apply (elim tendsto_of_int_diff_0)
using ab_event a_large apply (eventually_elim)
using ‹B>0› by auto
show ?thesis
proof (rule ccontr)
assume "¬ (∀⇩F n in sequentially. c n > 0)"
moreover have "∀⇩F n in sequentially. c (Suc n) ≥ 0 ∧ c n≥0"
using * eventually_sequentially_Suc[of "λn. c n≥0"]
by (metis (mono_tags, lifting) eventually_at_top_linorder le_Suc_eq)
ultimately have "∃⇩F n in sequentially. c n = 0 ∧ c (Suc n) ≥ 0"
using eventually_elim2 frequently_def by fastforce
moreover have "∀⇩F n in sequentially. b n > 0 ∧ B * b n = c n * a n - c (n + 1)"
using ab_event abc_event by eventually_elim auto
ultimately have "∃⇩F n in sequentially. c n = 0 ∧ c (Suc n) ≥ 0 ∧ b n > 0
∧ B * b n = c n * a n - c (n + 1)"
using frequently_eventually_frequently by fastforce
from frequently_ex[OF this]
obtain n where "c n = 0" "c (Suc n) ≥ 0" "b n > 0"
"B * b n = c n * a n - c (n + 1)"
by auto
then have "B * b n ≤ 0" by auto
then show False using ‹b n>0› ‹B > 0› using mult_pos_pos not_le by blast
qed
qed
have bc_epsilon:"∀⇩F n in sequentially. b (n+1) / b n > (c (n+1) - ε) / c n" when "ε>0" "ε<1" for ε::real
proof -
have "∀⇩F x in sequentially. ¦c (Suc x) / a x¦ < ε / 2"
using ca_vanish[unfolded tendsto_iff,rule_format, of "ε/2"] ‹ε>0› by auto
moreover then have "∀⇩F x in sequentially. ¦c (x+2) / a (x+1)¦ < ε / 2"
apply (subst (asm) eventually_sequentially_Suc[symmetric])
by simp
moreover have "∀⇩F n in sequentially. B * b (n+1) = c (n+1) * a (n+1) - c (n + 2)"
using abc_event
apply (subst (asm) eventually_sequentially_Suc[symmetric])
by (auto elim:eventually_mono)
moreover have "∀⇩F n in sequentially. c n > 0 ∧ c (n+1) > 0 ∧ c (n+2) > 0"
proof -
have "∀⇩F n in sequentially. 0 < c (Suc n)"
using c_pos by (subst eventually_sequentially_Suc) simp
moreover then have "∀⇩F n in sequentially. 0 < c (Suc (Suc n))"
using c_pos by (subst eventually_sequentially_Suc) simp
ultimately show ?thesis using c_pos by eventually_elim auto
qed
ultimately show ?thesis using ab_event abc_event
proof eventually_elim
case (elim n)
define ε⇩0 ε⇩1 where "ε⇩0 = c (n+1) / a n" and "ε⇩1 = c (n+2) / a (n+1)"
have "ε⇩0 > 0" "ε⇩1 > 0" "ε⇩0 < ε/2" "ε⇩1 < ε/2" using a_pos elim by (auto simp: ε⇩0_def ε⇩1_def)
have "(ε - ε⇩1) * c n > 0"
using ‹ε⇩1 < ε / 2› elim(4) that(1) by auto
moreover have "ε⇩0 * (c (n+1) - ε) > 0"
using ‹0 < ε⇩0› elim(4) that(2) by auto
ultimately have "(ε - ε⇩1) * c n + ε⇩0 * (c (n+1) - ε) > 0" by auto
moreover have gt0: "c n - ε⇩0 > 0" using ‹ε⇩0 < ε / 2› elim(4) that(2) by linarith
moreover have "c n > 0" by (simp add: elim(4))
ultimately have "(c (n+1) - ε) / c n < (c (n+1) - ε⇩1) / (c n - ε⇩0)"
by (auto simp: field_simps)
also have "... ≤ (c (n+1) - ε⇩1) / (c n - ε⇩0) * (a (n+1) / a n)"
proof -
have "(c (n+1) - ε⇩1) / (c n - ε⇩0) > 0"
using gt0 ‹ε⇩1 < ε / 2› elim(4) that(2) by force
moreover have "(a (n+1) / a n) ≥ 1"
using a_pos elim(5) by auto
ultimately show ?thesis by (metis mult_cancel_left1 mult_le_cancel_left_pos)
qed
also have "... = (B * b (n+1)) / (B * b n)"
proof -
have "B * b n = c n * a n - c (n + 1)"
using elim by auto
also have "... = a n * (c n - ε⇩0)"
using a_pos[rule_format,of n] unfolding ε⇩0_def by (auto simp:field_simps)
finally have "B * b n = a n * (c n - ε⇩0)" .
moreover have "B * b (n+1) = a (n+1) * (c (n+1) - ε⇩1)"
unfolding ε⇩1_def
using a_pos[rule_format,of "n+1"]
apply (subst ‹B * b (n + 1) = c (n + 1) * a (n + 1) - c (n + 2)›)
by (auto simp:field_simps)
ultimately show ?thesis by (simp add: mult.commute)
qed
also have "... = b (n+1) / b n"
using ‹B>0› by auto
finally show ?case .
qed
qed
have eq_2_11:"∃⇩F n in sequentially. b (n+1) > b n + (1 - ε)^2 * a n / B"
when "ε>0" "ε<1" "¬ (∀⇩F n in sequentially. c (n+1) ≤ c n)" for ε::real
proof -
have "∃⇩F x in sequentially. c x < c (Suc x) " using that(3)
by (simp add:not_eventually frequently_elim1)
moreover have "∀⇩F x in sequentially. ¦c (Suc x) / a x¦ < ε"
using ca_vanish[unfolded tendsto_iff,rule_format, of ε] ‹ε>0› by auto
moreover have "∀⇩F n in sequentially. c n > 0 ∧ c (n+1) > 0"
proof -
have "∀⇩F n in sequentially. 0 < c (Suc n)"
using c_pos by (subst eventually_sequentially_Suc) simp
then show ?thesis using c_pos by eventually_elim auto
qed
ultimately show ?thesis using ab_event abc_event bc_epsilon[OF ‹ε>0› ‹ε<1›]
proof (elim frequently_rev_mp,eventually_elim)
case (elim n)
then have "c (n+1) / a n < ε"
using a_pos[rule_format,of n] by auto
also have "... ≤ ε * c n" using elim(7) that(1) by auto
finally have "c (n+1) / a n < ε * c n" .
then have "c (n+1) / c n < ε * a n"
using a_pos[rule_format,of n] elim by (auto simp:field_simps)
then have "(1 - ε) * a n < a n - c (n+1) / c n"
by (auto simp:algebra_simps)
then have "(1 - ε)^2 * a n / B < (1 - ε) * (a n - c (n+1) / c n) / B"
apply (subst (asm) mult_less_cancel_right_pos[symmetric, of "(1-ε)/B"])
using ‹ε<1› ‹B>0› by (auto simp: divide_simps power2_eq_square mult_less_cancel_right_pos)
then have "b n + (1 - ε)^2 * a n / B < b n + (1 - ε) * (a n - c (n+1) / c n) / B"
using ‹B>0› by auto
also have "... = b n + (1 - ε) * ((c n *a n - c (n+1)) / c n) / B"
using elim by (auto simp:field_simps)
also have "... = b n + (1 - ε) * (b n / c n)"
proof -
have "B * b n = c n * a n - c (n + 1)" using elim by auto
from this[symmetric] show ?thesis
using ‹B>0› by simp
qed
also have "... = (1+(1-ε)/c n) * b n"
by (auto simp:algebra_simps)
also have "... = ((c n+1-ε)/c n) * b n"
using elim by (auto simp:divide_simps)
also have "... ≤ ((c (n+1) -ε)/c n) * b n"
proof -
define cp where "cp = c n+1"
have "c (n+1) ≥ cp" unfolding cp_def using ‹c n < c (Suc n)› by auto
moreover have "c n>0" "b n>0" using elim by auto
ultimately show ?thesis
apply (fold cp_def)
by (auto simp:divide_simps)
qed
also have "... < b (n+1)"
using elim by (auto simp:divide_simps)
finally show ?case .
qed
qed
have "∀⇩F n in sequentially. c (n+1) ≤ c n"
proof (rule ccontr)
assume "¬ (∀⇩F n in sequentially. c (n + 1) ≤ c n)"
from eq_2_11[OF _ _ this,of "1/2"]
have "∃⇩F n in sequentially. b (n+1) > b n + 1/4 * a n / B"
by (auto simp:algebra_simps power2_eq_square)
then have *:"∃⇩F n in sequentially. (b (n+1) - b n) / a n > 1 / (B * 4)"
apply (elim frequently_elim1)
subgoal for n
using a_pos[rule_format,of n] by (auto simp:field_simps)
done
define f where "f = (λn. (b (n+1) - b n) / a n)"
have "f ⇢ lim f"
using convergent_LIMSEQ_iff ba_lim_exist unfolding f_def by auto
from this[unfolded tendsto_iff,rule_format, of "1 / (B*4)"]
have "∀⇩F x in sequentially. ¦f x - lim f¦ < 1 / (B * 4)"
using ‹B>0› by (auto simp:dist_real_def)
moreover have "∃⇩F n in sequentially. f n > 1 / (B * 4)"
using * unfolding f_def by auto
ultimately have "∃⇩F n in sequentially. f n > 1 / (B * 4) ∧ ¦f n - lim f¦ < 1 / (B * 4)"
by (auto elim:frequently_eventually_frequently[rotated])
from frequently_ex[OF this]
obtain n where "f n > 1 / (B * 4)" "¦f n - lim f¦ < 1 / (B * 4)"
by auto
moreover have "lim f ≤ 0" using ba_lim_leq unfolding f_def by auto
ultimately show False by linarith
qed
then obtain N where N_dec:"∀n≥N. c (n+1) ≤ c n" by (meson eventually_at_top_linorder)
define max_c where "max_c = (MAX n ∈ {..N}. c n)"
have max_c:"c n ≤ max_c" for n
proof (cases "n≤N")
case True
then show ?thesis unfolding max_c_def by simp
next
case False
then have "n≥N" by auto
then have "c n≤c N"
proof (induct rule:nat_induct_at_least)
case base
then show ?case by simp
next
case (Suc n)
then have "c (n+1) ≤ c n" using N_dec by auto
then show ?case using ‹c n ≤ c N› by auto
qed
moreover have "c N ≤ max_c" unfolding max_c_def by auto
ultimately show ?thesis by auto
qed
have "max_c > 0 "
proof -
obtain N where "∀n≥N. 0 < c n"
using c_pos[unfolded eventually_at_top_linorder] by auto
then have "c N > 0" by auto
then show ?thesis using max_c[of N] by simp
qed
have ba_limsup_bound:"1/(B*(B+1)) ≤ limsup (λn. b n/a n)"
"limsup (λn. b n/a n) ≤ max_c / B + 1 / (B+1)"
proof -
define f where "f = (λn. b n/a n)"
from tendsto_mult_right_zero[OF bac_close,of "1/B"]
have "(λn. f n - c n / B) ⇢ 0"
unfolding f_def using ‹B>0› by (auto simp:algebra_simps)
from this[unfolded tendsto_iff,rule_format,of "1/(B+1)"]
have "∀⇩F x in sequentially. ¦f x - c x / B¦ < 1 / (B+1)"
using ‹B>0› by auto
then have *:"∀⇩F n in sequentially. 1/(B*(B+1)) ≤ ereal (f n) ∧ ereal (f n) ≤ max_c / B + 1 / (B+1)"
using c_pos
proof eventually_elim
case (elim n)
then have "f n - c n / B < 1 / (B+1)" by auto
then have "f n < c n / B + 1 / (B+1)" by simp
also have "... ≤ max_c / B + 1 / (B+1)"
using max_c[of n] using ‹B>0› by (auto simp:divide_simps)
finally have *:"f n < max_c / B + 1 / (B+1)" .
have "1/(B*(B+1)) = 1/B - 1 / (B+1)"
using ‹B>0› by (auto simp:divide_simps)
also have "... ≤ c n/B - 1 / (B+1)"
using ‹0 < c n› ‹B>0› by (auto,auto simp:divide_simps)
also have "... < f n" using elim by auto
finally have "1/(B*(B+1)) < f n" .
with * show ?case by simp
qed
show "limsup f ≤ max_c / B + 1 / (B+1)"
apply (rule Limsup_bounded)
using * by (auto elim:eventually_mono)
have "1/(B*(B+1)) ≤ liminf f"
apply (rule Liminf_bounded)
using * by (auto elim:eventually_mono)
also have "liminf f ≤ limsup f" by (simp add: Liminf_le_Limsup)
finally show "1/(B*(B+1)) ≤ limsup f" .
qed
have "0 < inverse (ereal (max_c / B + 1 / (B+1)))"
using ‹max_c > 0› ‹B>0›
by (simp add: pos_add_strict)
also have "... ≤ inverse (limsup (λn. b n/a n))"
proof (rule ereal_inverse_antimono[OF _ ba_limsup_bound(2)])
have "0<1/(B*(B+1))" using ‹B>0› by auto
also have "... ≤ limsup (λn. b n/a n)" using ba_limsup_bound(1) .
finally show "0≤limsup (λn. b n/a n)" using zero_ereal_def by auto
qed
also have "... = liminf (λn. inverse (ereal ( b n/a n)))"
apply (subst Liminf_inverse_ereal[symmetric])
using a_pos ab_event by (auto elim!:eventually_mono simp:divide_simps)
also have "... = liminf (λn. ( a n/b n))"
apply (rule Liminf_eq)
using a_pos ab_event
apply (auto elim!:eventually_mono)
by (metis less_int_code(1))
finally have "liminf (λn. ( a n/b n)) > 0" .
then show False using ‹liminf (λn. a n / b n) = 0› by simp
qed
end
section‹Some auxiliary results on the prime numbers. ›
lemma nth_prime_nonzero[simp]:"nth_prime n ≠ 0"
by (simp add: prime_gt_0_nat prime_nth_prime)
lemma nth_prime_gt_zero[simp]:"nth_prime n >0"
by (simp add: prime_gt_0_nat prime_nth_prime)
lemma ratio_of_consecutive_primes:
"(λn. nth_prime (n+1)/nth_prime n) ⇢1"
proof -
define f where "f=(λx. real (nth_prime (Suc x)) /real (nth_prime x))"
define g where "g=(λx. (real x * ln (real x))
/ (real (Suc x) * ln (real (Suc x))))"
have p_n:"(λx. real (nth_prime x) / (real x * ln (real x))) ⇢ 1"
using nth_prime_asymptotics[unfolded asymp_equiv_def,simplified] .
moreover have p_sn:"(λn. real (nth_prime (Suc n))
/ (real (Suc n) * ln (real (Suc n)))) ⇢ 1"
using nth_prime_asymptotics[unfolded asymp_equiv_def,simplified
,THEN LIMSEQ_Suc] .
ultimately have "(λx. f x * g x) ⇢ 1"
using tendsto_divide[OF p_sn p_n]
unfolding f_def g_def by (auto simp:algebra_simps)
moreover have "g ⇢ 1" unfolding g_def
by real_asymp
ultimately have "(λx. if g x = 0 then 0 else f x) ⇢ 1"
apply (drule_tac tendsto_divide[OF _ ‹g ⇢ 1›])
by auto
then have "f ⇢ 1"
proof (elim filterlim_mono_eventually)
have "∀⇩F x in sequentially. (if g (x+3) = 0 then 0
else f (x+3)) = f (x+3)"
unfolding g_def by auto
then show "∀⇩F x in sequentially. (if g x = 0 then 0 else f x) = f x"
apply (subst (asm) eventually_sequentially_seg)
by simp
qed auto
then show ?thesis unfolding f_def by auto
qed
lemma nth_prime_double_sqrt_less:
assumes "ε > 0"
shows "∀⇩F n in sequentially. (nth_prime (2*n) - nth_prime n)
/ sqrt (nth_prime n) < n powr (1/2+ε)"
proof -
define pp ll where
"pp=(λn. (nth_prime (2*n) - nth_prime n) / sqrt (nth_prime n))" and
"ll=(λx::nat. x * ln x)"
have pp_pos:"pp (n+1) > 0" for n
unfolding pp_def by simp
have "(λx. nth_prime (2 * x)) ∼[sequentially] (λx. (2 * x) * ln (2 * x))"
using nth_prime_asymptotics[THEN asymp_equiv_compose
,of "(*) 2" sequentially,unfolded comp_def]
using mult_nat_left_at_top pos2 by blast
also have "... ∼[sequentially] (λx. 2 *x * ln x)"
by real_asymp
finally have "(λx. nth_prime (2 * x)) ∼[sequentially] (λx. 2 *x * ln x)" .
from this[unfolded asymp_equiv_def, THEN tendsto_mult_left,of 2]
have "(λx. nth_prime (2 * x) / (x * ln x)) ⇢ 2"
unfolding asymp_equiv_def by auto
moreover have *:"(λx. nth_prime x / (x * ln x)) ⇢ 1"
using nth_prime_asymptotics unfolding asymp_equiv_def by auto
ultimately
have "(λx. (nth_prime (2 * x) - nth_prime x) / ll x) ⇢ 1"
unfolding ll_def
apply -
apply (drule (1) tendsto_diff)
apply (subst of_nat_diff,simp)
by (subst diff_divide_distrib,simp)
moreover have "(λx. sqrt (nth_prime x) / sqrt (ll x)) ⇢ 1"
unfolding ll_def
using tendsto_real_sqrt[OF *]
by (auto simp: real_sqrt_divide)
ultimately have "(λx. pp x * (sqrt (ll x) / (ll x))) ⇢ 1"
apply -
apply (drule (1) tendsto_divide,simp)
by (auto simp:field_simps of_nat_diff pp_def)
moreover have "∀⇩F x in sequentially. sqrt (ll x) / ll x = 1/sqrt (ll x)"
apply (subst eventually_sequentially_Suc[symmetric])
by (auto intro!:eventuallyI simp:ll_def divide_simps)
ultimately have "(λx. pp x / sqrt (ll x)) ⇢ 1"
apply (elim filterlim_mono_eventually)
by (auto elim!:eventually_mono) (metis mult.right_neutral times_divide_eq_right)
moreover have "(λx. sqrt (ll x) / x powr (1/2+ε)) ⇢ 0"
unfolding ll_def using ‹ε>0› by real_asymp
ultimately have "(λx. pp x / x powr (1/2+ε) *
(sqrt (ll x) / sqrt (ll x))) ⇢ 0"
apply -
apply (drule (1) tendsto_mult)
by (auto elim:filterlim_mono_eventually)
moreover have "∀⇩F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1"
apply (subst eventually_sequentially_Suc[symmetric])
by (auto intro!:eventuallyI simp:ll_def )
ultimately have "(λx. pp x / x powr (1/2+ε)) ⇢ 0"
apply (elim filterlim_mono_eventually)
by (auto elim:eventually_mono)
from tendstoD[OF this, of 1,simplified]
show "∀⇩F x in sequentially. pp x < x powr (1 / 2 + ε)"
apply (elim eventually_mono_sequentially[of _ 1])
using pp_pos by auto
qed
section ‹Theorem 3.1›
text‹Theorem 3.1 is an application of Theorem 2.1 with the sequences considered involving
the prime numbers.›
theorem theorem_3_10_Erdos_Straus:
fixes a::"nat ⇒ int"
assumes a_pos:"∀ n. a n >0" and "mono a"
and nth_1:"(λn. nth_prime n / (a n)^2) ⇢ 0"
and nth_2:"liminf (λn. a n / nth_prime n) = 0"
shows "(∑n. (nth_prime n / (∏i ≤ n. a i))) ∉ ℚ"
proof
assume asm:"(∑n. (nth_prime n / (∏i ≤ n. a i))) ∈ ℚ"
have a2_omega:"(λn. (a n)^2) ∈ ω(λx. x * ln x)"
proof -
have "(λn. real (nth_prime n)) ∈ o(λn. real_of_int ((a n)⇧2))"
apply (rule smalloI_tendsto[OF nth_1])
using a_pos by (metis (mono_tags, lifting) less_int_code(1)
not_eventuallyD of_int_0_eq_iff zero_eq_power2)
moreover have "(λx. real (nth_prime x)) ∈ Ω(λx. real x * ln (real x))"
using nth_prime_bigtheta
by blast
ultimately show ?thesis
using landau_omega.small_big_trans smallo_imp_smallomega by blast
qed
have a_gt_1:"∀⇩F n in sequentially. 1 < a n"
proof -
have "∀⇩F x in sequentially. ¦x * ln x¦ ≤ (a x)⇧2"
using a2_omega[unfolded smallomega_def,simplified,rule_format,of 1]
by auto
then have "∀⇩F x in sequentially. ¦(x+3) * ln (x+3)¦ ≤ (a (x+3))⇧2"
apply (subst (asm) eventually_sequentially_seg[symmetric, of _ 3])
by simp
then have "∀⇩F n in sequentially. 1 < a ( n+3)"
proof (elim eventually_mono)
fix x
assume "¦real (x + 3) * ln (real (x + 3))¦ ≤ real_of_int ((a (x + 3))⇧2)"
moreover have "¦real (x + 3) * ln (real (x + 3))¦ > 3"
proof -
have "ln (real (x + 3)) > 1"
using ln3_gt_1 ln_gt_1 by force
moreover have "real(x+3) ≥ 3" by simp
ultimately have "(x+3)*ln (real (x + 3)) > 3*1"
by (smt (verit, best) mult_less_cancel_left1)
then show ?thesis by auto
qed
ultimately have "(a (x + 3))⇧2 > 3"
by linarith
then show "1 < a (x + 3)"
by (smt (verit) assms(1) one_power2)
qed
then show ?thesis
using eventually_sequentially_seg[symmetric, of _ 3]
by blast
qed
obtain B::int and c where
"B>0" and Bc_large:"∀⇩F n in sequentially. B * nth_prime n
= c n * a n - c (n + 1) ∧ ¦c (n + 1)¦ < a n / 2"
and ca_vanish: "(λn. c (Suc n) / real_of_int (a n)) ⇢ 0"
proof -
note a_gt_1
moreover have "(λn. real_of_int ¦int (nth_prime n)¦
/ real_of_int (a (n - 1) * a n)) ⇢ 0"
proof -
define f where "f=(λn. nth_prime (n+1) / (a n * a (n+1)))"
define g where "g=(λn. 2*nth_prime n / (a n)^2)"
have "∀⇩F x in sequentially. norm (f x) ≤ g x"
proof -
have "∀⇩F n in sequentially. nth_prime (n+1) < 2*nth_prime n"
using ratio_of_consecutive_primes[unfolded tendsto_iff
,rule_format,of 1,simplified]
apply (elim eventually_mono)
by (auto simp :divide_simps dist_norm)
moreover have "∀⇩F n in sequentially. real_of_int (a n * a (n+1))
≥ (a n)^2"
apply (rule eventuallyI)
using ‹mono a› by (auto simp:power2_eq_square a_pos incseq_SucD)
ultimately show ?thesis unfolding f_def g_def
apply eventually_elim
apply (subst norm_divide)
apply (rule_tac linordered_field_class.frac_le)
using a_pos[rule_format, THEN order.strict_implies_not_eq ]
by auto
qed
moreover have "g ⇢ 0 "
using nth_1[THEN tendsto_mult_right_zero,of 2] unfolding g_def
by auto
ultimately have "f ⇢ 0"
using Lim_null_comparison[of f g sequentially]
by auto
then show ?thesis
unfolding f_def
by (rule_tac LIMSEQ_imp_Suc) auto
qed
moreover have "(∑n. real_of_int (int (nth_prime n))
/ real_of_int (prod a {..n})) ∈ ℚ"
using asm by simp
ultimately have "∃B>0. ∃c. (∀⇩F n in sequentially.
B * int (nth_prime n) = c n * a n - c (n + 1) ∧
real_of_int ¦c (n + 1)¦ < real_of_int (a n) / 2) ∧
(λn. real_of_int (c (Suc n)) / real_of_int (a n)) ⇢ 0"
using ab_rationality_imp[OF a_pos,of nth_prime] by fast
then show thesis
apply clarify
apply (rule_tac c=c and B=B in that)
by auto
qed
have bac_close:"(λn. B * nth_prime n / a n - c n) ⇢ 0"
proof -
have "∀⇩F n in sequentially. B * nth_prime n - c n * a n + c (n + 1) = 0"
using Bc_large by (auto elim!:eventually_mono)
then have "∀⇩F n in sequentially. (B * nth_prime n - c n * a n + c (n+1)) / a n = 0 "
by eventually_elim auto
then have "∀⇩F n in sequentially. B * nth_prime n / a n - c n + c (n + 1) / a n = 0"
apply eventually_elim
using a_pos by (auto simp:divide_simps) (metis less_irrefl)
then have "(λn. B * nth_prime n / a n - c n + c (n + 1) / a n) ⇢ 0"
by (simp add: eventually_mono tendsto_iff)
from tendsto_diff[OF this ca_vanish]
show ?thesis by auto
qed
have c_pos:"∀⇩F n in sequentially. c n > 0"
proof -
from bac_close have *:"∀⇩F n in sequentially. c n ≥ 0"
apply (elim tendsto_of_int_diff_0)
using a_gt_1 apply (eventually_elim)
using ‹B>0› by auto
show ?thesis
proof (rule ccontr)
assume "¬ (∀⇩F n in sequentially. c n > 0)"
moreover have "∀⇩F n in sequentially. c (Suc n) ≥ 0 ∧ c n≥0"
using * eventually_sequentially_Suc[of "λn. c n≥0"]
by (metis (mono_tags, lifting) eventually_at_top_linorder le_Suc_eq)
ultimately have "∃⇩F n in sequentially. c n = 0 ∧ c (Suc n) ≥ 0"
using eventually_elim2 frequently_def by fastforce
moreover have "∀⇩F n in sequentially. nth_prime n > 0
∧ B * nth_prime n = c n * a n - c (n + 1)"
using Bc_large by eventually_elim auto
ultimately have "∃⇩F n in sequentially. c n = 0 ∧ c (Suc n) ≥ 0
∧ B * nth_prime n = c n * a n - c (n + 1)"
using frequently_eventually_frequently by fastforce
from frequently_ex[OF this]
obtain n where "c n = 0" "c (Suc n) ≥ 0"
"B * nth_prime n = c n * a n - c (n + 1)"
by auto
then have "B * nth_prime n ≤ 0" by auto
then show False using ‹B > 0›
by (simp add: mult_le_0_iff)
qed
qed
have B_nth_prime:"∀⇩F n in sequentially. nth_prime n > B"
proof -
have "∀⇩F x in sequentially. B+1 ≤ nth_prime x"
using nth_prime_at_top[unfolded filterlim_at_top_ge[where c="nat B+1"]
,rule_format,of "nat B + 1",simplified]
apply (elim eventually_mono)
using ‹B>0› by auto
then show ?thesis
by (auto elim: eventually_mono)
qed
have bc_epsilon:"∀⇩F n in sequentially. nth_prime (n+1)
/ nth_prime n > (c (n+1) - ε) / c n" when "ε>0" "ε<1" for ε::real
proof -
have "∀⇩F x in sequentially. ¦c (Suc x) / a x¦ < ε / 2"
using ca_vanish[unfolded tendsto_iff,rule_format, of "ε/2"] ‹ε>0› by auto
moreover then have "∀⇩F x in sequentially. ¦c (x+2) / a (x+1)¦ < ε / 2"
apply (subst (asm) eventually_sequentially_Suc[symmetric])
by simp
moreover have "∀⇩F n in sequentially. B * nth_prime (n+1) = c (n+1) * a (n+1) - c (n + 2)"
using Bc_large
apply (subst (asm) eventually_sequentially_Suc[symmetric])
by (auto elim:eventually_mono)
moreover have "∀⇩F n in sequentially. c n > 0 ∧ c (n+1) > 0 ∧ c (n+2) > 0"
proof -
have "∀⇩F n in sequentially. 0 < c (Suc n)"
using c_pos by (subst eventually_sequentially_Suc) simp
moreover then have "∀⇩F n in sequentially. 0 < c (Suc (Suc n))"
using c_pos by (subst eventually_sequentially_Suc) simp
ultimately show ?thesis using c_pos by eventually_elim auto
qed
ultimately show ?thesis using Bc_large
proof eventually_elim
case (elim n)
define ε⇩0 ε⇩1 where "ε⇩0 = c (n+1) / a n" and "ε⇩1 = c (n+2) / a (n+1)"
have "ε⇩0 > 0" "ε⇩1 > 0" "ε⇩0 < ε/2" "ε⇩1 < ε/2"
using a_pos elim ‹mono a›
by (auto simp: ε⇩0_def ε⇩1_def abs_of_pos)
have "(ε - ε⇩1) * c n > 0"
using ‹ε⇩1 > 0› ‹ε⇩1 < ε/2› ‹ε>0› elim by auto
moreover have A: "ε⇩0 * (c (n+1) - ε) > 0"
using ‹ε⇩0 > 0› elim(4) that(2) by force
ultimately have "(ε - ε⇩1) * c n + ε⇩0 * (c (n+1) - ε) > 0" by auto
moreover have B: "c n - ε⇩0 > 0" using ‹ε⇩0 < ε / 2› elim(4) that(2) by linarith
moreover have "c n > 0" by (simp add: elim(4))
ultimately have "(c (n+1) - ε) / c n < (c (n+1) - ε⇩1) / (c n - ε⇩0)"
by (auto simp:field_simps)
also have "... ≤ (c (n+1) - ε⇩1) / (c n - ε⇩0) * (a (n+1) / a n)"
proof -
have "(c (n+1) - ε⇩1) / (c n - ε⇩0) > 0"
using A ‹0 < ε⇩0› B ‹ε⇩1 < ε / 2› divide_pos_pos that(1) by force
moreover have "(a (n+1) / a n) ≥ 1"
using a_pos ‹mono a› by (simp add: mono_def)
ultimately show ?thesis by (metis mult_cancel_left1 mult_le_cancel_left_pos)
qed
also have "... = (B * nth_prime (n+1)) / (B * nth_prime n)"
proof -
have "B * nth_prime n = c n * a n - c (n + 1)"
using elim by auto
also have "... = a n * (c n - ε⇩0)"
using a_pos[rule_format,of n] unfolding ε⇩0_def by (auto simp:field_simps)
finally have "B * nth_prime n = a n * (c n - ε⇩0)" .
moreover have "B * nth_prime (n+1) = a (n+1) * (c (n+1) - ε⇩1)"
unfolding ε⇩1_def
using a_pos[rule_format,of "n+1"]
apply (subst ‹B * nth_prime (n + 1) = c (n + 1) * a (n + 1) - c (n + 2)›)
by (auto simp:field_simps)
ultimately show ?thesis by (simp add: mult.commute)
qed
also have "... = nth_prime (n+1) / nth_prime n"
using ‹B>0› by auto
finally show ?case .
qed
qed
have c_ubound:"∀x. ∃n. c n > x"
proof (rule ccontr)
assume " ¬ (∀x. ∃n. x < c n)"
then obtain ub where "∀n. c n ≤ ub" "ub > 0"
by (meson dual_order.trans int_one_le_iff_zero_less le_cases not_le)
define pa where "pa = (λn. nth_prime n / a n)"
have pa_pos:"⋀n. pa n > 0" unfolding pa_def by (simp add: a_pos)
have "liminf (λn. 1 / pa n) = 0"
using nth_2 unfolding pa_def by auto
then have "(∃y<ereal (real_of_int B / real_of_int (ub + 1)).
∃⇩F x in sequentially. ereal (1 / pa x) ≤ y)"
apply (subst less_Liminf_iff[symmetric])
using ‹0 < B› ‹0 < ub› by auto
then have "∃⇩F x in sequentially. 1 / pa x < B/(ub+1)"
by (meson frequently_mono le_less_trans less_ereal.simps(1))
then have "∃⇩F x in sequentially. B*pa x > (ub+1)"
apply (elim frequently_elim1)
by (metis ‹0 < ub› mult.left_neutral of_int_0_less_iff pa_pos pos_divide_less_eq
pos_less_divide_eq times_divide_eq_left zless_add1_eq)
moreover have "∀⇩F x in sequentially. c x ≤ ub"
using ‹∀n. c n ≤ ub› by simp
ultimately have "∃⇩F x in sequentially. B*pa x - c x > 1"
by (elim frequently_rev_mp eventually_mono) linarith
moreover have "(λn. B * pa n - c n) ⇢0"
unfolding pa_def using bac_close by auto
from tendstoD[OF this,of 1]
have "∀⇩F n in sequentially. ¦B * pa n - c n¦ < 1"
by auto
ultimately have "∃⇩F x in sequentially. B*pa x - c x > 1 ∧ ¦B * pa x - c x¦ < 1"
using frequently_eventually_frequently by blast
then show False
by (simp add: frequently_def)
qed
have eq_2_11:"∀⇩F n in sequentially. c (n+1)>c n ⟶
nth_prime (n+1) > nth_prime n + (1 - ε)^2 * a n / B"
when "ε>0" "ε<1" for ε::real
proof -
have "∀⇩F x in sequentially. ¦c (Suc x) / a x¦ < ε"
using ca_vanish[unfolded tendsto_iff,rule_format, of ε] ‹ε>0› by auto
moreover have "∀⇩F n in sequentially. c n > 0 ∧ c (n+1) > 0"
proof -
have "∀⇩F n in sequentially. 0 < c (Suc n)"
using c_pos by (subst eventually_sequentially_Suc) simp
then show ?thesis using c_pos by eventually_elim auto
qed
ultimately show ?thesis using Bc_large bc_epsilon[OF ‹ε>0› ‹ε<1›]
proof (eventually_elim, rule_tac impI)
case (elim n)
assume "c n < c (n + 1)"
have "c (n+1) / a n < ε"
using a_pos[rule_format,of n] using elim(1,2) by auto
also have "... ≤ ε * c n" using elim(2) that(1) by auto
finally have "c (n+1) / a n < ε * c n" .
then have "c (n+1) / c n < ε * a n"
using a_pos[rule_format,of n] elim by (auto simp:field_simps)
then have "(1 - ε) * a n < a n - c (n+1) / c n"
by (auto simp:algebra_simps)
then have "(1 - ε)^2 * a n / B < (1 - ε) * (a n - c (n+1) / c n) / B"
apply (subst (asm) mult_less_cancel_right_pos[symmetric, of "(1-ε)/B"])
using ‹ε<1› ‹B>0› by (auto simp: divide_simps power2_eq_square mult_less_cancel_right_pos)
then have "nth_prime n + (1 - ε)^2 * a n / B < nth_prime n + (1 - ε) * (a n - c (n+1) / c n) / B"
using ‹B>0› by auto
also have "... = nth_prime n + (1 - ε) * ((c n *a n - c (n+1)) / c n) / B"
using elim by (auto simp:field_simps)
also have "... = nth_prime n + (1 - ε) * (nth_prime n / c n)"
proof -
have "B * nth_prime n = c n * a n - c (n + 1)" using elim by auto
from this[symmetric] show ?thesis
using ‹B>0› by simp
qed
also have "... = (1+(1-ε)/c n) * nth_prime n"
by (auto simp:algebra_simps)
also have "... = ((c n+1-ε)/c n) * nth_prime n"
using elim by (auto simp:divide_simps)
also have "... ≤ ((c (n+1) -ε)/c n) * nth_prime n"
proof -
define cp where "cp = c n+1"
have "c (n+1) ≥ cp" unfolding cp_def using ‹c n < c (n + 1)› by auto
moreover have "c n>0" "nth_prime n>0" using elim by auto
ultimately show ?thesis
apply (fold cp_def)
by (auto simp:divide_simps)
qed
also have "... < nth_prime (n+1)"
using elim by (auto simp:divide_simps)
finally show "real (nth_prime n) + (1 - ε)⇧2 * real_of_int (a n)
/ real_of_int B < real (nth_prime (n + 1))" .
qed
qed
have c_neq_large:"∀⇩F n in sequentially. c (n+1) ≠ c n"
proof (rule ccontr)
assume "¬ (∀⇩F n in sequentially. c (n + 1) ≠ c n)"
then have that:"∃⇩F n in sequentially. c (n + 1) = c n"
unfolding frequently_def .
have "∀⇩F x in sequentially. (B * int (nth_prime x) = c x * a x - c (x + 1)
∧ ¦real_of_int (c (x + 1))¦ < real_of_int (a x) / 2) ∧ 0 < c x ∧ B < int (nth_prime x)
∧ (c (x+1)>c x ⟶ nth_prime (x+1) > nth_prime x + a x / (2* B))"
using Bc_large c_pos B_nth_prime eq_2_11[of "1-1/ sqrt 2",simplified]
by eventually_elim (auto simp:divide_simps)
then have "∃⇩F m in sequentially. nth_prime (m+1) > (1+1/(2*B))*nth_prime m"
proof (elim frequently_eventually_at_top[OF that, THEN frequently_at_top_elim])
fix n
assume "c (n + 1) = c n ∧
(∀y≥n. (B * int (nth_prime y) = c y * a y - c (y + 1) ∧
¦real_of_int (c (y + 1))¦ < real_of_int (a y) / 2) ∧
0 < c y ∧ B < int (nth_prime y) ∧ (c y < c (y + 1) ⟶
real (nth_prime y) + real_of_int (a y) / real_of_int (2 * B)
< real (nth_prime (y + 1))))"
then have "c (n + 1) = c n"
and Bc_eq:"∀y≥n. B * int (nth_prime y) = c y * a y - c (y + 1) ∧ 0 < c y
∧ ¦real_of_int (c (y + 1))¦ < real_of_int (a y) / 2
∧ B < int (nth_prime y)
∧ (c y < c (y + 1) ⟶
real (nth_prime y) + real_of_int (a y) / real_of_int (2 * B)
< real (nth_prime (y + 1)))"
by auto
obtain m where "n<m" "c m ≤ c n" "c n<c (m+1)"
proof -
have "∃N. N > n ∧ c N > c n"
using c_ubound[rule_format, of "MAX x∈{..n}. c x"]
by (metis Max_ge atMost_iff dual_order.trans finite_atMost finite_imageI image_eqI
linorder_not_le order_refl)
then obtain N where "N>n" "c N>c n" by auto
define A m where "A={m. n<m ∧ (m+1)≤N ∧ c (m+1) > c n}" and "m = Min A"
have "finite A" unfolding A_def
by (metis (no_types, lifting) A_def add_leE finite_nat_set_iff_bounded_le mem_Collect_eq)
moreover have "N-1∈A" unfolding A_def
using ‹c n < c N› ‹n < N› ‹c (n + 1) = c n› nat_less_le by force
ultimately have "m∈A"
using Min_in unfolding m_def by auto
then have "n<m" "c n<c (m+1)" "m>0"
unfolding m_def A_def by auto
moreover have "c m ≤ c n"
proof (rule ccontr)
assume "¬ c m ≤ c n"
then have "m-1∈A"
using ‹m∈A› ‹c (n + 1) = c n› le_eq_less_or_eq less_diff_conv by (fastforce simp: A_def)
from Min_le[OF ‹finite A› this,folded m_def] ‹m>0› show False by auto
qed
ultimately show ?thesis using that[of m] by auto
qed
have "(1 + 1 / (2 * B)) * nth_prime m < nth_prime m + a m / (2*B)"
proof -
have "nth_prime m < a m"
proof -
have "B * int (nth_prime m) < c m * (a m - 1)"
using Bc_eq[rule_format,of m] ‹c m ≤ c n› ‹c n < c (m + 1)› ‹n < m›
by (auto simp:algebra_simps)
also have "... ≤ c n * (a m - 1)"
by (simp add: ‹c m ≤ c n› a_pos mult_right_mono)
finally have "B * int (nth_prime m) < c n * (a m - 1)" .
moreover have "c n≤B"
proof -
have B: "B * int (nth_prime n) = c n * (a n - 1)" "B < int (nth_prime n)"
and c_a: "¦real_of_int (c (n + 1))¦ < real_of_int (a n) / 2"
using Bc_eq[rule_format,of n] ‹c (n + 1) = c n› by (auto simp:algebra_simps)
from this(1) have " c n dvd (B * int (nth_prime n))"
by simp
moreover have "coprime (c n) (int (nth_prime n))"
proof -
have "c n < int (nth_prime n)"
proof (rule ccontr)
assume "¬ c n < int (nth_prime n)"
then have asm:"c n ≥ int (nth_prime n)" by auto
then have "a n > 2 * nth_prime n"
using c_a ‹c (n + 1) = c n› by auto
then have "a n -1 ≥ 2 * nth_prime n"
by simp
then have "a n - 1 > 2 * B"
using ‹B < int (nth_prime n)› by auto
from mult_le_less_imp_less[OF asm this] ‹B>0›
have "int (nth_prime n) * (2 * B) < c n * (a n - 1)"
by auto
then show False using B
by (smt (verit, best) ‹0 < B› mult.commute mult_right_mono)
qed
then have "¬ nth_prime n dvd c n"
by (simp add: Bc_eq zdvd_not_zless)
then have "coprime (int (nth_prime n)) (c n)"
by (auto intro!:prime_imp_coprime_int)
then show ?thesis using coprime_commute by blast
qed
ultimately have "c n dvd B"
using coprime_dvd_mult_left_iff by auto
then show ?thesis using ‹0 < B› zdvd_imp_le by blast
qed
moreover have "c n > 0 " using Bc_eq by blast
ultimately show ?thesis
using ‹B>0› by (smt (verit) a_pos mult_mono)
qed
then show ?thesis using ‹B>0› by (auto simp:field_simps)
qed
also have "... < nth_prime (m+1)"
using Bc_eq[rule_format, of m] ‹n<m› ‹c m ≤ c n› ‹c n < c (m+1)›
by linarith
finally show "∃j>n. (1 + 1 / real_of_int (2 * B)) * real (nth_prime j)
< real (nth_prime (j + 1))" using ‹m>n› by auto
qed
then have "∃⇩F m in sequentially. nth_prime (m+1)/nth_prime m > (1+1/(2*B))"
by (auto elim:frequently_elim1 simp:field_simps)
moreover have "∀⇩F m in sequentially. nth_prime (m+1)/nth_prime m < (1+1/(2*B))"
using ratio_of_consecutive_primes[unfolded tendsto_iff,rule_format,of "1/(2*B)"]
‹B>0›
unfolding dist_real_def
by (auto elim!:eventually_mono simp:algebra_simps)
ultimately show False by (simp add: eventually_mono frequently_def)
qed
have c_gt_half:"∀⇩F N in sequentially. card {n∈{N..<2*N}. c n > c (n+1)} > N / 2"
proof -
define h where "h=(λn. (nth_prime (2*n) - nth_prime n)
/ sqrt (nth_prime n))"
have "∀⇩F n in sequentially. h n < n / 2"
proof -
have "∀⇩F n in sequentially. h n < n powr (5/6)"
using nth_prime_double_sqrt_less[of "1/3"]
unfolding h_def by auto
moreover have "∀⇩F n in sequentially. n powr (5/6) < (n /2)"
by real_asymp
ultimately show ?thesis
by eventually_elim auto
qed
moreover have "∀⇩F n in sequentially. sqrt (nth_prime n) / a n < 1 / (2*B)"
using nth_1[THEN tendsto_real_sqrt,unfolded tendsto_iff
,rule_format,of "1/(2*B)"] ‹B>0› a_pos
by (auto simp:real_sqrt_divide abs_of_pos)
ultimately have "∀⇩F x in sequentially. c (x+1) ≠ c x
∧ sqrt (nth_prime x) / a x < 1 / (2*B)
∧ h x < x / 2
∧ (c (x+1)>c x ⟶ nth_prime (x+1) > nth_prime x + a x / (2* B))"
using c_neq_large B_nth_prime eq_2_11[of "1-1/ sqrt 2",simplified]
by eventually_elim (auto simp:divide_simps)
then show ?thesis
proof (elim eventually_at_top_mono)
fix N assume "N≥1" and N_asm:"∀y≥N. c (y + 1) ≠ c y ∧
sqrt (real (nth_prime y)) / real_of_int (a y)
< 1 / real_of_int (2 * B) ∧ h y < y / 2 ∧
(c y < c (y + 1) ⟶
real (nth_prime y) + real_of_int (a y) / real_of_int (2 * B)
< real (nth_prime (y + 1)))"
define S where "S={n ∈ {N..<2 * N}. c n < c (n + 1)}"
define g where "g=(λn. (nth_prime (n+1) - nth_prime n)
/ sqrt (nth_prime n))"
define f where "f=(λn. nth_prime (n+1) - nth_prime n)"
have g_gt_1:"g n>1" when "n≥N" "c n < c (n + 1)" for n
proof -
have "nth_prime n + sqrt (nth_prime n) < nth_prime (n+1)"
proof -
have "nth_prime n + sqrt (nth_prime n) < nth_prime n + a n / (2*B)"
using N_asm[rule_format,OF ‹n≥N›] a_pos
by (auto simp:field_simps)
also have "... < nth_prime (n+1)"
using N_asm[rule_format,OF ‹n≥N›] ‹c n < c (n + 1)› by auto
finally show ?thesis .
qed
then show ?thesis unfolding g_def
using ‹c n < c (n + 1)› by auto
qed
have g_geq_0:"g n ≥ 0" for n
unfolding g_def by auto
have "finite S" "∀x∈S. x≥N ∧ c x<c (x+1)"
unfolding S_def by auto
then have "card S ≤ sum g S"
proof (induct S)
case empty
then show ?case by auto
next
case (insert x F)
moreover have "g x>1"
proof -
have "c x < c (x+1)" "x≥N" using insert(4) by auto
then show ?thesis using g_gt_1 by auto
qed
ultimately show ?case by simp
qed
also have "... ≤ sum g {N..<2*N}"
apply (rule sum_mono2)
unfolding S_def using g_geq_0 by auto
also have "... ≤ sum (λn. f n/sqrt (nth_prime N)) {N..<2*N}"
unfolding f_def g_def by (auto intro!:sum_mono divide_left_mono)
also have "... = sum f {N..<2*N} / sqrt (nth_prime N)"
unfolding sum_divide_distrib[symmetric] by auto
also have "... = (nth_prime (2*N) - nth_prime N) / sqrt (nth_prime N)"
proof -
have "sum f {N..<2 * N} = nth_prime (2 * N) - nth_prime N"
proof (induct N)
case 0
then show ?case by simp
next
case (Suc N)
have ?case if "N=0"
proof -
have "sum f {Suc N..<2 * Suc N} = sum f {1}"
using that by (simp add: numeral_2_eq_2)
also have "... = nth_prime 2 - nth_prime 1"
unfolding f_def by (simp add:numeral_2_eq_2)
also have "... = nth_prime (2 * Suc N) - nth_prime (Suc N)"
using that by auto
finally show ?thesis .
qed
moreover have ?case if "N≠0"
proof -
have "sum f {Suc N..<2 * Suc N} = sum f {N..<2 * Suc N} - f N"
apply (subst (2) sum.atLeast_Suc_lessThan)
using that by auto
also have "... = sum f {N..<2 * N}+ f (2*N) + f(2*N+1) - f N"
by auto
also have "... = nth_prime (2 * Suc N) - nth_prime (Suc N)"
using Suc unfolding f_def by auto
finally show ?thesis .
qed
ultimately show ?case by blast
qed
then show ?thesis by auto
qed
also have "... = h N"
unfolding h_def by auto
also have "... < N/2"
using N_asm by auto
finally have "card S < N/2" .
define T where "T={n ∈ {N..<2 * N}. c n > c (n + 1)}"
have "T ∪ S = {N..<2 * N}" "T ∩ S = {}" "finite T"
unfolding T_def S_def using N_asm by fastforce+
then have "card T + card S = card {N..<2 * N}"
using card_Un_disjoint ‹finite S› by metis
also have "... = N"
by simp
finally have "card T + card S = N" .
with ‹card S < N/2›
show "card T > N/2" by linarith
qed
qed
text‹Inequality (3.5) in the original paper required a slight modification: ›
have a_gt_plus:"∀⇩F n in sequentially. c n > c (n+1) ⟶a (n+1) > a n + (a n - c(n+1) - 1) / c (n+1)"
proof -
note a_gt_1[THEN eventually_all_ge_at_top] c_pos[THEN eventually_all_ge_at_top]
moreover have "∀⇩F n in sequentially.
B * int (nth_prime (n+1)) = c (n+1) * a (n+1) - c (n + 2)"
using Bc_large
apply (subst (asm) eventually_sequentially_Suc[symmetric])
by (auto elim:eventually_mono)
moreover have "∀⇩F n in sequentially.
B * int (nth_prime n) = c n * a n - c (n + 1) ∧ ¦c (n + 1)¦ < a n / 2"
using Bc_large by (auto elim:eventually_mono)
ultimately show ?thesis
apply (eventually_elim)
proof (rule impI)
fix n
assume "∀y≥n. 1 < a y" "∀y≥n. 0 < c y"
and
Suc_n_eq:"B * int (nth_prime (n + 1)) = c (n + 1) * a (n + 1) - c (n + 2)" and
"B * int (nth_prime n) = c n * a n - c (n + 1) ∧
real_of_int ¦c (n + 1)¦ < real_of_int (a n) / 2"
and "c (n + 1) < c n"
then have n_eq:"B * int (nth_prime n) = c n * a n - c (n + 1)" and
c_less_a: "real_of_int ¦c (n + 1)¦ < real_of_int (a n) / 2"
by auto
from ‹∀y≥n. 1 < a y› ‹∀y≥n. 0 < c y›
have *:"a n>1" "a (n+1) > 1" "c n > 0"
"c (n+1) > 0" "c (n+2) > 0"
by auto
then have "(1+1/c (n+1))* (a n - 1)/a (n+1) = (c (n+1)+1) * ((a n - 1) / (c (n+1) * a (n+1)))"
by (auto simp:field_simps)
also have "... ≤ c n * ((a n - 1) / (c (n+1) * a (n+1)))"
by (smt (verit) "*"(4) ‹c (n + 1) < c n› a_pos divide_nonneg_nonneg mult_mono mult_nonneg_nonneg of_int_0_le_iff of_int_le_iff)
also have "... = (c n * (a n - 1)) / (c (n+1) * a (n+1))" by auto
also have "... < (c n * (a n - 1)) / (c (n+1) * a (n+1) - c (n+2))"
apply (rule divide_strict_left_mono)
subgoal using ‹c (n+2) > 0› by auto
unfolding Suc_n_eq[symmetric] using * ‹B>0› by auto
also have "... < (c n * a n - c (n+1)) / (c (n+1) * a (n+1) - c (n+2))"
apply (rule frac_less)
unfolding Suc_n_eq[symmetric] using * ‹B>0› ‹c (n + 1) < c n›
by (auto simp:algebra_simps)
also have "... = nth_prime n / nth_prime (n+1)"
unfolding Suc_n_eq[symmetric] n_eq[symmetric] using ‹B>0› by auto
also have "... < 1" by auto
finally have "(1 + 1 / real_of_int (c (n + 1))) * real_of_int (a n - 1)
/ real_of_int (a (n + 1)) < 1 " .
then show "a n + (a n - c (n + 1) - 1) / (c (n + 1)) < (a (n + 1))"
using * by (auto simp:field_simps)
qed
qed
have a_gt_1:"∀⇩F n in sequentially. c n > c (n+1) ⟶ a (n+1) > a n + 1"
using Bc_large a_gt_plus c_pos[THEN eventually_all_ge_at_top]
apply eventually_elim
proof (rule impI)
fix n assume
"c (n + 1) < c n ⟶ a n + (a n - c (n + 1) - 1) / c (n + 1) < a (n + 1)"
"c (n + 1) < c n" and B_eq:"B * int (nth_prime n) = c n * a n - c (n + 1) ∧
¦real_of_int (c (n + 1))¦ < real_of_int (a n) / 2" and c_pos:"∀y≥n. 0 < c y"
from this(1,2)
have "a n + (a n - c (n + 1) - 1) / c (n + 1) < a (n + 1)" by auto
moreover have "a n - 2 * c (n+1) > 0"
using B_eq c_pos[rule_format,of "n+1"] by auto
then have "a n - 2 * c (n+1) ≥ 1" by simp
then have "(a n - c (n + 1) - 1) / c (n + 1) ≥ 1"
using c_pos[rule_format,of "n+1"] by (auto simp:field_simps)
ultimately show "a n + 1 < a (n + 1)" by auto
qed
text‹The following corresponds to inequality (3.6) in the paper, which had to be
slightly corrected: ›
have a_gt_sqrt:"∀⇩F n in sequentially. c n > c (n+1) ⟶ a (n+1) > a n + (sqrt n - 2)"
proof -
have a_2N:"∀⇩F N in sequentially. a (2*N) ≥ N /2 +1"
using c_gt_half a_gt_1[THEN eventually_all_ge_at_top]
proof eventually_elim
case (elim N)
define S where "S={n ∈ {N..<2 * N}. c (n + 1) < c n}"
define f where "f = (λn. a (Suc n) - a n)"
have f_1:"∀x∈S. f x≥1" and f_0:"∀x. f x≥0"
subgoal using elim unfolding S_def f_def by auto
subgoal using ‹mono a›[THEN incseq_SucD] unfolding f_def by auto
done
have "N / 2 < card S"
using elim unfolding S_def by auto
also have "... ≤ sum f S"
unfolding of_int_sum
apply (rule sum_bounded_below[of _ 1,simplified])
using f_1 by auto
also have "... ≤ sum f {N..<2 * N}"
unfolding of_int_sum
apply (rule sum_mono2)
unfolding S_def using f_0 by auto
also have "... = a (2*N) - a N"
unfolding of_int_sum f_def of_int_diff
apply (rule sum_Suc_diff')
by auto
finally have "N / 2 < a (2*N) - a N" .
then show ?case using a_pos[rule_format,of N] by linarith
qed
have a_n4:"∀⇩F n in sequentially. a n > n/4"
proof -
obtain N where a_N:"∀n≥N. a (2*n) ≥ n /2+1"
using a_2N unfolding eventually_at_top_linorder by auto
have "a n>n/4" when "n≥2*N" for n
proof -
define n' where "n'=n div 2"
have "n'≥N" unfolding n'_def using that by auto
have "n/4 < n' /2+1"
unfolding n'_def by auto
also have "... ≤ a (2*n')"
using a_N ‹n'≥N› by auto
also have "... ≤a n" unfolding n'_def
apply (cases "even n")
subgoal by simp
subgoal by (simp add: assms(2) incseqD)
done
finally show ?thesis .
qed
then show ?thesis
unfolding eventually_at_top_linorder by auto
qed
have c_sqrt:"∀⇩F n in sequentially. c n < sqrt n / 4"
proof -
have "∀⇩F x in sequentially. x>1" by simp
moreover have "∀⇩F x in sequentially. real (nth_prime x) / (real x * ln (real x)) < 2"
using nth_prime_asymptotics[unfolded asymp_equiv_def,THEN order_tendstoD(2),of 2]
by simp
ultimately have "∀⇩F n in sequentially. c n < B*8 *ln n + 1" using a_n4 Bc_large
proof eventually_elim
case (elim n)
from this(4) have "c n=(B*nth_prime n+c (n+1))/a n"
using a_pos[rule_format,of n]
by (auto simp:divide_simps)
also have "... = (B*nth_prime n)/a n+c (n+1)/a n"
by (auto simp:divide_simps)
also have "... < (B*nth_prime n)/a n + 1"
proof -
have "c (n+1)/a n < 1" using elim(4) by auto
then show ?thesis by auto
qed
also have "... < B*8 * ln n + 1"
proof -
have "B*nth_prime n < 2*B*n*ln n"
using ‹real (nth_prime n) / (real n * ln (real n)) < 2› ‹B>0› ‹ 1 < n›
by (auto simp:divide_simps)
moreover have "real n / 4 < real_of_int (a n)" by fact
ultimately have "(B*nth_prime n) / a n < (2*B*n*ln n) / (n/4)"
apply (rule_tac frac_less)
using ‹B>0› ‹ 1 < n› by auto
also have "... = B*8 * ln n"
using ‹ 1 < n› by auto
finally show ?thesis by auto
qed
finally show ?case .
qed
moreover have "∀⇩F n in sequentially. B*8 *ln n + 1 < sqrt n / 4"
by real_asymp
ultimately show ?thesis
by eventually_elim auto
qed
have
"∀⇩F n in sequentially. 0 < c (n+1)"
"∀⇩F n in sequentially. c (n+1) < sqrt (n+1) / 4"
"∀⇩F n in sequentially. n > 4"
"∀⇩F n in sequentially. (n - 4) / sqrt (n + 1) + 1 > sqrt n"
subgoal using c_pos[THEN eventually_all_ge_at_top]
by eventually_elim auto
subgoal using c_sqrt[THEN eventually_all_ge_at_top]
by eventually_elim (use le_add1 in blast)
subgoal by simp
subgoal
by real_asymp
done
then show ?thesis using a_gt_plus a_n4
apply eventually_elim
proof (rule impI)
fix n assume asm:"0 < c (n + 1)" "c (n + 1) < sqrt (real (n + 1)) / 4" and
a_ineq:"c (n + 1) < c n ⟶ a n + (a n - c (n + 1) - 1) / c (n + 1) < a (n + 1)"
"c (n + 1) < c n" and "n / 4 < a n" "n > 4"
and n_neq:" sqrt (real n) < real (n - 4) / sqrt (real (n + 1)) + 1"
have "(n-4) / sqrt(n+1) = (n/4 - 1)/ (sqrt (real (n + 1)) / 4)"
using ‹n>4› by (auto simp:divide_simps)
also have "... < (a n - 1) / c (n + 1)"
apply (rule frac_less)
using ‹n > 4› ‹n / 4 < a n› ‹0 < c (n + 1)› ‹c (n + 1) < sqrt (real (n + 1)) / 4›
by auto
also have "... - 1 = (a n - c (n + 1) - 1) / c (n + 1)"
using ‹0 < c (n + 1)› by (auto simp:field_simps)
also have "a n + ... < a (n+1)"
using a_ineq by auto
finally have "a n + ((n - 4) / sqrt (n + 1) - 1) < a (n + 1)" by simp
moreover have "(n - 4) / sqrt (n + 1) - 1 > sqrt n - 2"
using n_neq[THEN diff_strict_right_mono,of 2] ‹n>4›
by (auto simp:algebra_simps of_nat_diff)
ultimately show "real_of_int (a n) + (sqrt (real n) - 2) < real_of_int (a (n + 1))"
by argo
qed
qed
text‹The following corresponds to inequality $ a_{2N} > N^{3/2}/2$ in the paper,
which had to be slightly corrected: ›
have a_2N_sqrt:"∀⇩F N in sequentially. a (2*N) > real N * (sqrt (real N)/2 - 1)"
using c_gt_half a_gt_sqrt[THEN eventually_all_ge_at_top] eventually_gt_at_top[of 4]
proof eventually_elim
case (elim N)
define S where "S={n ∈ {N..<2 * N}. c (n + 1) < c n}"
define f where "f = (λn. a (Suc n) - a n)"
have f_N:"∀x∈S. f x≥sqrt N - 2"
proof
fix x assume "x∈S"
then have "sqrt (real x) - 2 < f x" "x≥N"
using elim unfolding S_def f_def by auto
moreover have "sqrt x - 2 ≥ sqrt N - 2"
using ‹x≥N› by simp
ultimately show "sqrt (real N) - 2 ≤ real_of_int (f x)" by argo
qed
have f_0:"∀x. f x≥0"
using ‹mono a›[THEN incseq_SucD] unfolding f_def by auto
have "(N / 2) * (sqrt N - 2) < card S * (sqrt N - 2)"
apply (rule mult_strict_right_mono)
subgoal using elim unfolding S_def by auto
subgoal using ‹N>4›
by (metis diff_gt_0_iff_gt numeral_less_real_of_nat_iff real_sqrt_four real_sqrt_less_iff)
done
also have "... ≤ sum f S"
unfolding of_int_sum
apply (rule sum_bounded_below)
using f_N by auto
also have "... ≤ sum f {N..<2 * N}"
unfolding of_int_sum
apply (rule sum_mono2)
unfolding S_def using f_0 by auto
also have "... = a (2*N) - a N"
unfolding of_int_sum f_def of_int_diff
apply (rule sum_Suc_diff')
by auto
finally have "real N / 2 * (sqrt (real N) - 2) < real_of_int (a (2 * N) - a N)"
.
then have "real N / 2 * (sqrt (real N) - 2) < a (2 * N)"
using a_pos[rule_format,of N] by linarith
then show ?case by (auto simp:field_simps)
qed
text‹The following part is required to derive the final contradiction of the proof.›
have a_n_sqrt:"∀⇩F n in sequentially. a n > (((n-1)/2) powr (3/2) - (n-1)) /2"
proof (rule sequentially_even_odd_imp)
define f where "f=(λN. ((real (2 * N - 1) / 2) powr (3 / 2) - real (2 * N - 1)) / 2)"
define g where "g=(λN. real N * (sqrt (real N) / 2 - 1))"
have "∀⇩F N in sequentially. g N > f N"
unfolding f_def g_def
by real_asymp
moreover have "∀⇩F N in sequentially. a (2 * N) > g N"
unfolding g_def using a_2N_sqrt .
ultimately show "∀⇩F N in sequentially. f N < a (2 * N)"
by eventually_elim auto
next
define f where "f=(λN. ((real (2 * N + 1 - 1) / 2) powr (3 / 2)
- real (2 * N + 1 - 1)) / 2)"
define g where "g=(λN. real N * (sqrt (real N) / 2 - 1))"
have "∀⇩F N in sequentially. g N = f N"
using eventually_gt_at_top[of 0]
apply eventually_elim
unfolding f_def g_def
by (auto simp:algebra_simps powr_half_sqrt[symmetric] powr_mult_base)
moreover have "∀⇩F N in sequentially. a (2 * N) > g N"
unfolding g_def using a_2N_sqrt .
moreover have "∀⇩F N in sequentially. a (2 * N + 1) ≥ a (2*N)"
apply (rule eventuallyI)
using ‹mono a› by (simp add: incseqD)
ultimately show "∀⇩F N in sequentially. f N < (a (2 * N + 1))"
by eventually_elim auto
qed
have a_nth_prime_gt:"∀⇩F n in sequentially. a n / nth_prime n > 1"
proof -
define f where "f=(λn::nat. (((n-1)/2) powr (3/2) - (n-1)) /2)"
have "∀⇩F x in sequentially. real (nth_prime x) / (real x * ln (real x)) < 2"
using nth_prime_asymptotics[unfolded asymp_equiv_def,THEN order_tendstoD(2),of 2]
by simp
from this eventually_gt_at_top[of 1]
have "∀⇩F n in sequentially. real (nth_prime n) < 2*(real n * ln n)"
by eventually_elim (auto simp:field_simps)
moreover have *:"∀⇩F N in sequentially. f N >0 "
unfolding f_def
by real_asymp
moreover have " ∀⇩F n in sequentially. f n < a n"
using a_n_sqrt unfolding f_def .
ultimately have "∀⇩F n in sequentially. a n / nth_prime n > f n / (2*(real n * ln n))"
proof eventually_elim
case (elim n)
then show ?case
by (auto intro: frac_less2)
qed
moreover have "∀⇩F n in sequentially. (f n)/ (2*(real n * ln n)) > 1"
unfolding f_def by real_asymp
ultimately show ?thesis
by eventually_elim argo
qed
have a_nth_prime_lt:"∃⇩F n in sequentially. a n / nth_prime n < 1"
proof -
have "liminf (λx. a x / nth_prime x) < 1"
using nth_2 by auto
from this[unfolded less_Liminf_iff]
show ?thesis
by (smt (verit) ereal_less(3) frequently_elim1 le_less_trans)
qed
from a_nth_prime_gt a_nth_prime_lt show False
by (simp add: eventually_mono frequently_def)
qed
section‹Acknowledgements›
text‹A.K.-A. and W.L. were supported by the ERC Advanced Grant ALEXANDRIA (Project 742178)
funded by the European Research Council and led by Professor Lawrence Paulson
at the University of Cambridge, UK.›
end