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