diff --git a/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy b/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy --- a/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy +++ b/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy @@ -1,1062 +1,1059 @@ (* File: Irrationality_J_Hancl.thy Authors: Angeliki Koutsoukou-Argyraki and Wenda Li, Computer Laboratory, University of Cambridge, UK. Email: ak2110@cam.ac.uk, wl302@cam.ac.uk *) section \Irrational Rapidly Convergent Series\ theory Irrationality_J_Hancl imports "HOL-Analysis.Analysis" "HOL-Decision_Procs.Approximation" begin text \This is the formalisation of a proof by J. Hancl, in particular of the proof of his Theorem 3 in the paper: Irrational Rapidly Convergent Series, Rend. Sem. Mat. Univ. Padova, Vol 107 (2002). The statement asserts the irrationality of the sum of a series consisting of rational numbers defined using sequences that fulfill certain properties. Even though the statement is number-theoretic, the proof uses only arguments from introductory Analysis.\ text \We show the central result (theorem Hancl3) by proof by contradiction, by making use of some of the auxiliary lemmas. To this end, assuming that the sum is a rational number, for a quantity $\textrm{ALPHA}(n)$ we show that $\textrm{ALPHA}(n) \geq 1$ for all $n \in \mathbb{N}$. After that we show that we can find an $n \in \mathbb{N}$ for which $\textrm{ALPHA}(n) < 1$ which yields a contradiction and we thus conclude that the sum of the series is a rational number. We finally give an immediate application of theorem Hancl3 for a specific series (corollary Hancl3corollary, requiring lemma summable\_ln\_plus) which corresponds to Corollary 2 in the original paper by J. Hancl. \ hide_const floatarith.Max subsection \Misc\ lemma filterlim_sequentially_iff: "filterlim f F1 sequentially \ filterlim (\x. f (x+k)) F1 sequentially" unfolding filterlim_iff apply (subst eventually_sequentially_seg) by auto lemma filterlim_realpow_sequentially_at_top: "(x::real) > 1 \ filterlim ((^) x) at_top sequentially" apply (rule LIMSEQ_divide_realpow_zero[THEN filterlim_inverse_at_top,of _ 1,simplified]) by auto lemma filterlim_at_top_powr_real: fixes g::"'b \ real" assumes "filterlim f at_top F" "(g \ g') F" "g'>1" shows "filterlim (\x. g x powr f x) at_top F" proof - have "filterlim (\x. ((g'+1)/2) powr f x) at_top F" proof (subst filterlim_at_top_gt[of _ _ 1],rule+) fix Z assume "Z>(1::real)" have "\\<^sub>F x in F. ln Z \ ln (((g' + 1) / 2) powr f x)" using assms(1)[unfolded filterlim_at_top,rule_format,of "ln Z / ln ((g' + 1) / 2)"] apply (eventually_elim) using \g'>1\ by (auto simp:ln_powr divide_simps) then show "\\<^sub>F x in F. Z \ ((g' + 1) / 2) powr f x" apply (eventually_elim) apply (subst (asm) ln_le_cancel_iff) using \Z>1\ \g'>1\ by auto qed moreover have "\\<^sub>F x in F. ((g'+1)/2) powr f x \ g x powr f x" proof - have "\\<^sub>F x in F. g x > (g'+1)/2" apply (rule order_tendstoD[OF assms(2)]) using \g'>1\ by auto moreover have "\\<^sub>F x in F. f x>0" using assms(1)[unfolded filterlim_at_top_dense,rule_format,of 0] . ultimately show ?thesis apply eventually_elim using \g'>1\ by (auto intro!: powr_mono2) qed ultimately show ?thesis using filterlim_at_top_mono by fast qed lemma powrfinitesum: fixes a::real and s::nat assumes "s \ n" shows " (\j=s..(n::nat).(a powr (2^j))) = a powr (\j=s..(n::nat).(2^j)) " using \s \ n\ proof(induct n) case 0 then show ?case by auto next case (Suc n) have ?case when "s\n" using Suc.hyps by (metis Suc.prems add.commute linorder_not_le powr_add prod.nat_ivl_Suc' sum.cl_ivl_Suc that) moreover have ?case when "s=Suc n" proof- have "(\j = s..Suc n. a powr 2 ^ j) =(a powr 2 ^(Suc n)) " using \s=Suc n\ by simp also have "(a powr 2 ^(Suc n) ) = a powr sum ((^) 2) {s..Suc n} " using that by auto ultimately show " (\j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}" using \s\Suc n\ by linarith qed ultimately show ?case using \s\Suc n\ by linarith qed lemma summable_ratio_test_tendsto: fixes f :: "nat \ 'a::banach" assumes "c < 1" and "\n. f n\0" and "(\n. norm (f (Suc n)) / norm (f n)) \ c" shows "summable f" proof - obtain N where N_dist:"\n\N. dist (norm (f (Suc n)) / norm (f n)) c < (1-c)/2" using assms unfolding tendsto_iff eventually_sequentially by (meson diff_gt_0_iff_gt zero_less_divide_iff zero_less_numeral) have "norm (f (Suc n)) / norm (f n) \ (1+c)/2" when "n\N" for n using N_dist[rule_format,OF that] \c<1\ apply (auto simp add:field_simps dist_norm) by argo then have "norm (f (Suc n)) \ (1+c)/2 * norm (f n)" when "n\N" for n using that assms(2)[rule_format, of n] by (auto simp add:divide_simps) moreover have "(1+c)/2 < 1" using \c<1\ by auto ultimately show ?thesis using summable_ratio_test[of _ N f] by blast qed lemma summable_ln_plus: fixes f::"nat \ real" assumes "summable f" "\n. f n>0" shows "summable (\n. ln (1+f n))" proof (rule summable_comparison_test_ev[OF _ assms(1)]) have "ln (1 + f n) > 0" for n by (simp add: assms(2) ln_gt_zero) moreover have "ln (1 + f n) \ f n" for n apply (rule ln_add_one_self_le_self2) using assms(2)[rule_format,of n] by auto ultimately show "\\<^sub>F n in sequentially. norm (ln (1 + f n)) \ f n" by (auto intro!: eventuallyI simp add:less_imp_le) qed lemma suminf_real_offset_le: fixes f :: "nat \ real" assumes f: "\i. 0 \ f i" and "summable f" shows "(\i. f (i + k)) \ suminf f" proof - have "(\n. \i (\i. f (i + k))" using summable_sums[OF \summable f\] by (simp add: assms(2) summable_LIMSEQ summable_ignore_initial_segment) moreover have "(\n. \i (\i. f i)" using summable_sums[OF \summable f\] by (simp add: sums_def atLeast0LessThan f) then have "(\n. \i (\i. f i)" by (rule LIMSEQ_ignore_initial_segment) ultimately show ?thesis proof (rule LIMSEQ_le, safe intro!: exI[of _ k]) fix n assume "k \ n" have "(\ii (\i. i + k)) i)" by simp also have "\ = (\i\(\i. i + k) ` {.. \ sum f {..i sum f {.. n" shows " (\i=s..n. 2^i) < (2^(n+1) :: real) " using assms proof (induct n) case 0 show ?case by auto next case (Suc n) have ?case when "s=n+1" using that by auto moreover have ?case when "s \ n+1" proof - have"(\i=s..(n+1). 2^i ) = (\i=s..n. 2^i ) + (2::real)^(n+1) " using sum.cl_ivl_Suc \s \ Suc n \ by (auto simp add:add.commute) also have "... < (2) ^ (n +1) + (2)^(n+1)" proof - have "s \n" using that \s \ Suc n \ by auto then show ?thesis using Suc.hyps \s \ n\ by linarith qed also have "... = 2^(n+2)" by simp finally show "(\i=s..(Suc n). 2^i )< (2::real)^(Suc n+1)" by auto qed ultimately show ?case by blast qed subsection \Auxiliary lemmas and the main proof\ lemma showpre7: fixes a b ::"nat\int " and q p::int assumes "q>0" and "p>0"and a: "\n. a n>0" and "\n. b n>0" and assumerational:"(\ n. b (n+1) / a (n+1) ) sums (p/q)" shows "q*((\j=1..n. of_int( a j)))*(suminf (\(j::nat). (b (j+n+1)/ a (j+n+1 )))) = ((\j=1..n. of_int( a j)))*(p -q* (\j=1..n. b j / a j)) " proof - define aa where "aa=(\j = 1..n. real_of_int (a j))" define ff where "ff=(\i. real_of_int (b (i+1)) / real_of_int (a (i+1)))" have "(\j. ff (j+n)) = (\n. ff n) - sum ff {..j=1..n. ff (j-1))" proof - have "sum ff {..j=1..n. ff (j-1))" apply (subst sum_bounds_lt_plus1[symmetric]) by simp then show ?thesis unfolding ff_def by auto qed finally have "(\j. ff (j + n)) = p / q - (\j = 1..n. ff (j - 1))" . then have "q*(\j. ff (j + n)) = p - q*(\j = 1..n. ff (j - 1))" using \q>0\ by (auto simp add:field_simps) then have "aa*q*(\j. ff (j + n)) = aa*(p - q*(\j = 1..n. ff (j - 1)))" by auto then show ?thesis unfolding aa_def ff_def by auto qed lemma show7: fixes d::"nat\real" and a b::"nat\int " and q p::int assumes "q \1" and "p \ 1" and a: "\n. a n \ 1" and "\n. b n \ 1" and assumerational:"(\ n. b (n+1) / a (n+1) ) sums (p/q)" shows "q*((\j=1..n. of_int( a j)))*( suminf (\ (j::nat). (b (j+n+1)/ a (j+n+1 )))) \ 1 " (is "?L \ _") proof- define LL where "LL=?L" define aa where "aa=(\j = 1..n. real_of_int (a j))" define ff where "ff=(\i. real_of_int (b (i+1)) / real_of_int (a (i+1)))" have "?L > 0" proof - have "aa > 0" unfolding aa_def using a apply (induct n,auto) by (simp add: int_one_le_iff_zero_less prod_pos) moreover have "(\j. ff (j + n)) > 0" proof (rule suminf_pos) have "summable ff" unfolding ff_def using assumerational using summable_def by blast then show " summable (\j. ff (j + n))" using summable_iff_shift[of ff n] by auto show "\i. 0 < ff (i + n)" unfolding ff_def using a assms(4) int_one_le_iff_zero_less by auto qed ultimately show ?thesis unfolding aa_def ff_def using \q\1\ by auto qed moreover have "?L \ \" proof - have "?L = aa *(p -q* ( \j=1..n. b j / a j))" unfolding aa_def apply (rule showpre7) using assms int_one_le_iff_zero_less by auto also have "... = aa * p - q * (\j=1..n. aa * b j / a j)" by (auto simp add:algebra_simps sum_distrib_left) also have "... = prod a {1..n} * p - q * (\j = 1..n. b j * prod a ({1..n} - {j}))" proof - have "(\j=1..n. aa * b j / a j) = (\j=1..n. b j * prod a ({1..n} - {j}))" unfolding of_int_sum proof (rule sum.cong) fix x assume "x \ {1..n}" then have "(\i = 1..n. real_of_int (a i)) = a x * (\i\{1..n} - {x}. real_of_int (a i))" apply (rule_tac prod.remove) by auto then have "aa / real_of_int (a x) = prod a ({1..n} - {x})" unfolding aa_def using a[rule_format,of x] by (auto simp add:field_simps) then show "aa * b x / a x = b x * prod a ({1..n} - {x})" by (metis mult.commute of_int_mult times_divide_eq_right) qed simp moreover have "aa * p = (\j = 1..n. (a j)) * p" unfolding aa_def by auto ultimately show ?thesis by force qed also have "... \ \" using Ints_of_int by blast finally show ?thesis . qed ultimately show ?thesis apply (fold LL_def) by (metis Ints_cases int_one_le_iff_zero_less not_less of_int_0_less_iff of_int_less_1_iff) qed lemma show8: fixes d ::"nat\real " and a :: "nat\int" and s k::nat assumes "A > 1" and d: "\n. d n> 1" and a:"\n. a n>0" and "s>0" and "convergent_prod d" and assu2: "\n \ s. ( A/ (of_int (a n)) powr(1/of_int (2^n)))> prodinf (\j. d(n +j))" shows "\n\s. prodinf (\j. d(j+n)) < A/(Max ((\(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n}))" proof (intro strip) fix n assume "s \ n" define sp where "sp = (\n. prodinf (\j. d(j+n)))" define ff where "ff = (\(j::nat). (real_of_int (a j)) powr(1 /of_int (2^j)))" have "sp i \ sp n" when "i\n" for i proof - have "(\j. d (j + i)) = (\ia. d (ia + (n - i) + i)) * (\iaj. d (j + i))" using \convergent_prod d\ convergent_prod_iff_shift[of d i] by simp show "\j. j < n - i \ d (j + i) \ 0" by (metis d not_one_less_zero) qed then have "sp i = sp n * (\jn\i\ by (auto simp:algebra_simps) moreover have "sp i>1" "sp n>1" unfolding sp_def using convergent_prod_iff_shift \convergent_prod d\ d by (auto intro!:less_1_prodinf) moreover have "(\j 1" using d less_imp_le by (auto intro: prod_ge_1) ultimately show ?thesis by auto qed moreover have "\j\s. A / ff j > sp j" unfolding ff_def sp_def using assu2 by (auto simp:algebra_simps) ultimately have "\j. s\j \ j\n \ A / ff j > sp n" by force then show "sp n< A / Max (ff ` {s..n})" by (metis (mono_tags, hide_lams) Max_in \n\s\ atLeastAtMost_iff empty_iff finite_atLeastAtMost finite_imageI imageE image_is_empty order_refl) qed lemma auxiliary1_9: fixes d ::"nat\real" and a::"nat\int " and s m::nat assumes d: "\n. d n> 1" and a: "\n. a n>0" and "s>0" and "n \ m" and " m \ s" and auxifalse_assu: "\n\m. (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) < (d (n+1))* (Max ((\ (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} ))" shows "(of_int (a (n+1))) powr(1 /of_int (2^(n+1))) < (\j=(m+1)..(n+1). d j) * (Max ((\ (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..m}))" proof- define ff where "ff = (\(j::nat). (real_of_int (a j)) powr(1 /of_int (2^j)))" have [simp]:"ff j > 0" for j unfolding ff_def by (metis a less_numeral_extra(3) of_int_0_less_iff powr_gt_zero) have ff_asm:"ff (n+1) < d (n+1) * Max (ff ` {s..n})" when "n\m" for n using auxifalse_assu that unfolding ff_def by simp from \n\m\ have Q: "(Max( ff ` {s..n} )) \ (\j=(m+1)..n. d j)* (Max (ff ` {s..m}))" proof(induct n) case 0 then show ?case using \m\s\ by simp next case (Suc n) have ?case when "m=Suc n" using that by auto moreover have ?case when "m\Suc n" proof - have "m \ n" using that Suc(2) by simp then have IH:"Max (ff ` {s..n}) \ prod d {m + 1..n} * Max (ff ` {s..m})" using Suc(1) by linarith have "Max (ff ` {s..Suc n}) = Max (ff ` {s..n} \ {ff (Suc n)})" using Suc.prems assms(5) atLeastAtMostSuc_conv by auto also have "... = max (Max (ff ` {s..n})) (ff (Suc n))" using Suc.prems assms(5) max_def sup_assoc that by auto also have "... \ max (Max (ff ` {s..n})) (d (n+1) * Max (ff ` {s..n}))" using \m \ n\ ff_asm by fastforce also have "... \ Max (ff ` {s..n}) * max 1 (d (n+1))" proof - have "Max (ff ` {s..n}) \ 0" by (metis (mono_tags, hide_lams) Max_in \\j. 0 < ff j\ \m \ n\ assms(5) atLeastAtMost_iff empty_iff finite_atLeastAtMost finite_imageI imageE image_is_empty less_eq_real_def) then show ?thesis using max_mult_distrib_right by (simp add: max_mult_distrib_right mult.commute) qed also have "... = Max (ff ` {s..n}) * d (n+1)" using d[rule_format, of "n+1"] by auto also have "... \ prod d {m + 1..n} * Max (ff ` {s..m}) * d (n+1)" using IH d[rule_format, of "n+1"] by auto also have "... = prod d {m + 1..n+1} * Max (ff ` {s..m})" using \n\m\ by (simp add:prod.nat_ivl_Suc' algebra_simps) finally show ?case by simp qed ultimately show ?case by blast qed then have "d (n+1) * Max (ff ` {s..n} ) \ (\j=(m+1)..(n+1). d j)* (Max (ff ` {s..m}))" using \m\n\ d[rule_format,of "Suc n"] by (simp add:prod.nat_ivl_Suc') then show ?thesis using ff_asm[of n] \s\m\ \m\n\ unfolding ff_def by auto qed lemma show9: fixes d ::"nat\real " and a :: "nat\int " and s ::nat and A::real assumes "A > 1" and d: "\n. d n> 1" and a: "\n. a n>0" and "s>0" and assu1: "(( \ n. (of_int (a n)) powr(1 /of_int (2^n)))\ A) sequentially " and "convergent_prod d" and 8: "\n\s. prodinf (\j. d( n+j)) < A/(Max ((\(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n})) " shows "\m \s. \n\m. ( (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \ (d (n+1))* (Max ( ( \ (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))" proof (rule ccontr) define ff where "ff = (\(j::nat). (real_of_int (a j)) powr(1 /of_int (2^j)))" assume assumptioncontra: " \ (\m \s. \n\m. ( (ff (n+1)) \ (d (n+1))* (Max ( ff ` {s..n}))))" then obtain t where "t\s" and ttt: " \n\t. ( (ff (n+1)) < (d (n+1))* (Max ( ff ` {s..n} ) ))" by fastforce define B where "B=prodinf (\j. d(t+1+j))" have "B>0" unfolding B_def proof (rule less_0_prodinf) show "convergent_prod (\j. d (t + 1 + j))" using convergent_prod_iff_shift[of d "t+1"] \convergent_prod d\ by (auto simp: algebra_simps) show "\i. 0 < d (t + 1 + i)" using d le_less_trans zero_le_one by blast qed have "A \ B * Max ( ff ` {s..t})" proof (rule tendsto_le[of sequentially "\n. (\j=(t+1)..(n+1). d j) * Max ( ff ` {s..t})" _ "\n. ff (n+1)"]) show "(\n. ff (n + 1)) \ A" using assu1[folded ff_def] LIMSEQ_ignore_initial_segment by blast have "(\n. prod d {t + 1..n + 1}) \ B" proof - have "convergent_prod (\j. d (t + 1 + j))" using \convergent_prod d\ convergent_prod_iff_shift[of d "t+1"] by (simp add:algebra_simps) then have "(\n. \i\n. d (t + 1 + i)) \ B" using B_def convergent_prod_LIMSEQ by blast then have "(\n. \i\{0..n}. d (i+(t + 1))) \ B" using atLeast0AtMost by (auto simp:algebra_simps) then have "(\n. prod d {(t + 1)..n + (t + 1)}) \ B" apply (subst (asm) prod.shift_bounds_cl_nat_ivl[symmetric]) by simp from seq_offset_neg[OF this,of "t"] show "(\n. prod d {t + 1..n+1}) \ B" apply (elim Lim_transform) apply (rule LIMSEQ_I) apply (rule exI[where x="t+1"]) by auto qed then show "(\n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \ B * Max (ff ` {s..t})" by (auto intro:tendsto_eq_intros) have "\\<^sub>F n in sequentially. (ff (n+1)) < (\j=(t+1)..(n+1). d j) * (Max ( ff ` {s..t}))" unfolding eventually_sequentially ff_def using auxiliary1_9[OF d a \s>0\ _ \t\s\ ttt[unfolded ff_def]] by blast then show "\\<^sub>F n in sequentially. (ff (n+1)) \ (\j=(t+1)..(n+1). d j) * (Max ( ff ` {s..t}))" by (eventually_elim,simp) qed simp also have "... \ B * Max ( ff ` {s..t+1})" proof - have "Max (ff ` {s..t}) \ Max (ff ` {s..t + 1})" apply (rule Max_mono) using \t\s\ by auto then show ?thesis using \B>0\ by auto qed finally have "A \ B * Max (ff ` {s..t + 1})" unfolding B_def . moreover have "B < A / Max (ff ` {s..t + 1})" using 8[rule_format, of "t+1",folded ff_def B_def] \s\t\ by auto moreover have "Max (ff ` {s..t+1})>0" using \A \ B * Max (ff ` {s..t + 1})\ \B>0\ \A>1\ zero_less_mult_pos [of B "Max (ff ` {s..Suc t})"] by simp ultimately show False by (auto simp add:field_simps) qed lemma show10: fixes d ::"nat\real " and a ::"nat\int " and s::nat assumes d: "\n. d n> 1" and a: "\n. a n>0" and " s>0" and 9: "\m \s. \n\m. ((of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \ (d (n+1))* (Max ((\(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))" shows "\m\s. \n\m. (((d (n+1))powr(2^(n+1))) * (\j=1..n. of_int( a j)) * (1/ (\j=1..s-1. (of_int( a j) )))) \ (a (n+1)) " proof (rule,rule) fix m assume "s \ m" from 9[rule_format,OF this] obtain n where "n\m" and asm_9:"( (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \ (d (n+1))* (Max ( ( \ (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))" by auto with \s\m\ have "s\n" by auto have prod:"(\j=1..n. real_of_int( a j)) * ( 1/ (\j=1..s-1. (of_int( a j) ))) = (\j=s..n. of_int( a j))" proof - define f where "f= (\j. real_of_int( a j))" have "{Suc 0..n}= {Suc 0..s - Suc 0} \ {s..n}" using \n\s\ \s >0\ by auto then have "(\j=1..n. f j) = (\j=1..s-1. f j) * (\j=s..n. f j)" apply (subst prod.union_disjoint[symmetric]) by auto moreover have "(\j=1..s-1. f j) > 0 " by (metis a f_def of_int_0_less_iff prod_pos) then have "(\j=1..s-1. f j) \ 0" by argo ultimately show ?thesis unfolding f_def by auto qed then have "d (n+1) powr 2 ^ (n+1) * (\j = 1..n. of_int (a j)) * (1 / (\j = 1..s - 1. of_int (a j))) = d (n+1) powr 2 ^ (n+1) * (\j = s..n. of_int (a j))" by (metis mult.assoc prod) also have "... \ ((d (n+1))powr(2^(n+1) ) * (\i=s..n. (Max(( \ (j::nat). ( of_int( a j) powr(1 /real_of_int (2^j)) )) ` {s..n } )) powr(2^i)) )" proof (rule mult_left_mono) show "0 \ (d (n + 1)) powr 2 ^ (n + 1)" by auto show "(\j = s..n. real_of_int (a j)) \ (\i = s..n. Max ((\j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}) powr 2 ^ i)" proof (rule prod_mono) fix i assume i: "i \ {s..n}" have "real_of_int (a i) = (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i" unfolding powr_powr by (simp add: a less_eq_real_def) also have "\ \ (Max(( \ (j::nat). ( real_of_int( a j) powr(1 /real_of_int (2^j)))) ` {s..n}))powr(2^i)" proof (rule powr_mono2) show "real_of_int (a i) powr (1 / real_of_int (2 ^ i)) \ Max ((\j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n})" using i by force qed simp_all finally have "real_of_int (a i) \ Max ((\j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}) powr 2 ^ i" . then show "0 \ real_of_int (a i) \ real_of_int (a i) \ (MAX j\{s..n}. of_int (a j) powr (1 / of_int (2 ^ j))) powr 2 ^ i" using a i by (metis \real_of_int (a i) = (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i\ powr_ge_pzero) qed qed also have "... = ((d (n+1))powr(2^(n+1) )) * (Max(( \ (j::nat). ( of_int( a j) powr (1 /of_int (2^j)) )) ` {s..n } )) powr (\i=s..n. 2^i ) " proof- have "((d (n+1))powr(2^(n+1) ))\1 " by (metis Transcendental.log_one d le_powr_iff zero_le_numeral zero_le_power zero_less_one) moreover have "(\i=s..n. (Max(( \ (j::nat). ( of_int( a j) powr(1 /real_of_int (2^j)) )) ` {s..n } ) ) powr(2^i)) = (Max(( \ (j::nat). ( of_int( a j) powr(1 /of_int (2^j)) )) ` {s..n } )) powr (\i=s..n. 2^i ) " using \s\n\ powrfinitesum by auto ultimately show ?thesis by auto qed also have "... \ ((d (n+1))powr(2^(n+1) )) * (Max(( \ (j::nat).( of_int( a j) powr(1 /of_int (2^j)) )) ` {s..n })) powr(2^(n+1)) " proof - define ff where "ff \ (MAX j\{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))" have " sum ((^) 2) {s..n} < (2::real) ^ (n + 1)" using factt \s\n\ by auto moreover have "1 \ ff" proof - define S where "S=(\(j::nat). ( of_int( a j) powr(1 /real_of_int (2^j)) )) ` {s..n }" have "finite S" unfolding S_def by auto moreover have "S\{}" unfolding S_def using \s\n\ by auto moreover have "\x\S. x\1" proof- have "a s powr (1 / (2^s)) \ 1" proof (rule ge_one_powr_ge_zero) show "1 \ real_of_int (a s)" by (simp add: a int_one_le_iff_zero_less) qed auto moreover have "of_int( a s) powr(1 /real_of_int (2^s)) \ S" unfolding S_def using \s\n\ by auto ultimately show ?thesis by auto qed ultimately show ?thesis using Max_ge_iff[of S 1] unfolding S_def ff_def by blast qed moreover have "0 \ (d (n + 1)) powr 2 ^ (n + 1)" by auto ultimately show ?thesis by (simp add: mult_left_mono powr_mono ff_def) qed also have "... = ((d (n+1)) * (Max((\j. (of_int( a j) powr(1 /of_int (2^j)))) ` {s..n}))) powr(2^(n+1))" proof - define ss where "ss = (\j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}" have "d (n + 1) \0" using d[rule_format,of "n+1"] by argo moreover have "Max ss \0" proof - have "(a s) powr (1 / (2 ^ s)) \ 0" by auto moreover have "(a s) powr (1 / (2 ^ s)) \ ss" unfolding ss_def using \s\n\ by auto moreover have "finite ss" "ss \ {}" unfolding ss_def using \s\n\ by auto ultimately show ?thesis using Max_ge_iff[of ss 0] by blast qed ultimately show ?thesis unfolding ss_def using powr_mult by auto qed also have "... \ (real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1)" proof - define ss where "ss = (\j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}" show ?thesis proof (fold ss_def,rule powr_mono2) have "Max ss \0" \ \NOTE: we are repeating the same proof, so it may be a good idea to put this conclusion in an outer block so that it can be reused (without reproving).\ proof - have "(a s) powr (1 / (2 ^ s)) \ 0" by auto moreover have "(a s) powr (1 / (2 ^ s)) \ ss" unfolding ss_def using \s\n\ by auto moreover have "finite ss" "ss \ {}" unfolding ss_def using \s\n\ by auto ultimately show ?thesis using Max_ge_iff[of ss 0] by blast qed moreover have "d (n + 1) \0" using d[rule_format,of "n+1"] by argo ultimately show "0 \ (d (n + 1)) * Max ss" by auto show "(d (n + 1)) * Max ss \ real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))" using asm_9[folded ss_def] . qed simp qed also have "... = (of_int (a (n+1)))" by (simp add: a less_eq_real_def pos_add_strict powr_powr) finally show "\n\m. d (n + 1) powr 2 ^ (n + 1) * (\j = 1..n. real_of_int (a j)) * (1 / (\j = 1..s - 1. real_of_int (a j))) \ real_of_int (a (n + 1))" using \n\m\ \m\s\ by force qed lemma lasttoshow: fixes d ::"nat\real " and a b ::"nat\int " and q::int and s::nat assumes d: "\n. d n> 1" and a:"\n. a n>0" and "s>0" and "q>0" and "A > 1" and b:"\n. b n>0" and 9: "\m\s. \n\m. ((of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \ (d (n+1))* (Max ((\(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))" and assu3: "filterlim( \ n. (d n)^(2^n)/ b n) at_top sequentially " and 5: "\\<^sub>F n in sequentially. (\j. (b (n + j)) / (a (n + j))) \ 2 * b n / a n" shows "\n. q*((\j=1..n. real_of_int(a j))) * suminf (\(j::nat). (b (j+n+1)/ a (j+n+1)))<1" proof- define as where "as=(\j = 1..s - 1. real_of_int (a j))" obtain n where "n\s" and n_def1:"real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1" and n_def2:"d (n + 1) powr 2 ^ (n + 1) * (\j = 1..n. real_of_int (a j)) * (1 / as) \ real_of_int (a (n + 1))" and n_def3:"(\j. (b (n+1 + j)) / (a (n+1 + j))) \ 2 * b (n+1) / a (n+1)" proof - have *:"(\n. real_of_int (b n) / d n ^ 2 ^ n) \ 0" using tendsto_inverse_0_at_top[OF assu3] by auto then have "(\n. real_of_int (b n) / d n powr 2 ^ n) \ 0" proof - have "d n ^ 2 ^ n = d n powr (of_nat (2 ^ n))" for n apply (subst powr_realpow) using d[rule_format, of n] by auto then show ?thesis using * by auto qed from tendsto_mult_right_zero[OF this,of "q * as * 2"] have "(\n. q * as * 2 * b n / d n powr 2 ^ n) \ 0" by auto then have "\\<^sub>F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1" by (elim order_tendstoD) simp then have "\\<^sub>F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1 \ (\j. (b (n + j)) / (a (n + j))) \ 2 * b n / a n" using 5 by eventually_elim auto then obtain N where N_def:"\n\N. q * as * 2 * b n / d n powr 2 ^ n < 1 \ (\j. (b (n + j)) / (a (n + j))) \ 2 * b n / a n" unfolding eventually_sequentially by auto obtain n where "n\s" and "n\N" and n_def:"d (n + 1) powr 2 ^ (n + 1) * (\j = 1..n. of_int (a j)) * (1 / as) \ real_of_int (a (n + 1))" using show10[OF d a \s>0\ 9,folded as_def,rule_format,of "max s N"] by auto with N_def[rule_format, of "n+1"] that[of n] show ?thesis by auto qed define pa where "pa = (\j = 1..n. real_of_int (a j))" define dn where "dn = d (n + 1) powr 2 ^ (n + 1)" have [simp]:"dn >0" "as > 0" subgoal unfolding dn_def by (metis d not_le numeral_One powr_gt_zero zero_le_numeral) subgoal unfolding as_def by (simp add: a prod_pos) done have [simp]:"pa>0" unfolding pa_def using a by (simp add: prod_pos) have K: "q* (\j=1..n. real_of_int (a j)) * suminf (\ (j::nat). (b (j+n+1)/ a (j+n+1))) \q* (\j=1..n. real_of_int (a j)) *2* (b (n+1))/(a( n+1))" apply (fold pa_def) using mult_left_mono[OF n_def3,of "real_of_int q * pa"] \n\s\ \pa>0\ \q>0\ by (auto simp add:algebra_simps) also have KK:"... \ 2*q* (\j=1..n. real_of_int (a j)) * (b(n+1))* ((\j=1..s-1. real_of_int( a j))/((d (n+1))powr(2^(n+1)) * (\j=1..n. real_of_int ( a j))))" proof - have " dn * pa * (1 / as) \ real_of_int (a (n + 1))" using n_def2 unfolding dn_def pa_def . then show ?thesis apply (fold pa_def dn_def as_def) using \pa>0\ \q>0\ a[rule_format, of "Suc n"] b[rule_format, of "Suc n"] by (auto simp add:divide_simps algebra_simps) qed also have KKK: "... = (q* ((\j=1..(s-1). real_of_int( a j)))*2 * (b (n+1)))/ ((d (n+1))powr(2^(n+1)))" apply (fold as_def pa_def dn_def) apply simp using \0 < pa\ by blast also have KKKK: "... < 1" using n_def1 unfolding as_def by simp finally show ?thesis by auto qed lemma fixes d ::"nat\real " and a b ::"nat\int " and A::real assumes "A > 1" and d: "\n. d n> 1" and a: "\n. a n>0" and b:"\n. b n>0" and assu1: "(( \ n. (of_int (a n)) powr(1 /of_int (2^n)))\ A) sequentially " and assu3: "filterlim ( \ n. (d n)^(2^n)/ b n) at_top sequentially" and "convergent_prod d" shows issummable: "summable (\j. b j / a j)" and show5: "\\<^sub>F n in sequentially. (\j. (b (n + j)) / (a (n + j))) \ 2 * b n / a n" proof- define c where "c = (\j. b j / a j)" have c_pos:"c j>0" for j using a b unfolding c_def by simp have c_ratio_tendsto:"(\n. c (n+1) / c n ) \ 0" proof - define nn where "nn=(\n. (2::int)^ (Suc n))" define ff where "ff=(\ n. (a n / a (Suc n)) powr(1 /nn n)*(d(Suc n)))" have nn_pos:"nn n>0" and ff_pos:"ff n>0" for n subgoal unfolding nn_def by simp subgoal unfolding ff_def using d[rule_format, of "Suc n"] a[rule_format, of n] a[rule_format, of "Suc n"] by auto done have ff_tendsto:"ff \ 1/ sqrt A" proof - have "(of_int (a n)) powr(1 / (nn n)) = sqrt(of_int (a n) powr(1 /of_int (2^n)))" for n unfolding nn_def using a by (simp add: powr_half_sqrt [symmetric] powr_powr ac_simps) moreover have "(( \ n. sqrt(of_int (a n) powr(1 /of_int (2^n))))\ sqrt A) sequentially " using assu1 tendsto_real_sqrt by blast ultimately have "(( \ n. (of_int (a n)) powr(1 /of_int (nn n)))\ sqrt A) sequentially " by auto from tendsto_divide[OF this assu1[THEN LIMSEQ_ignore_initial_segment[where k=1]]] have "(\n. (a n / a (Suc n)) powr(1 /nn n)) \ 1/sqrt A" using \A>1\ a unfolding nn_def by (auto simp add:powr_divide less_imp_le inverse_eq_divide sqrt_divide_self_eq) moreover have "(\n. d (Suc n))\ 1" apply (rule convergent_prod_imp_LIMSEQ) using convergent_prod_iff_shift[of d 1] \convergent_prod d\ by auto ultimately show ?thesis unfolding ff_def by (auto intro:tendsto_eq_intros) qed have "(\n. (ff n) powr nn n) \ 0" proof - define aa where "aa=(1+1/sqrt A) / 2" have "eventually (\n. ff nA>1\ by (auto simp add:field_simps) moreover have "(\n. aa powr nn n) \ 0" proof - have "(\y. aa ^ (nat \ nn) y) \ 0" apply (rule tendsto_power_zero) subgoal unfolding nn_def comp_def apply (rule filterlim_subseq) by (auto intro:strict_monoI) subgoal unfolding aa_def using \A>1\ by auto done then show ?thesis proof (elim filterlim_mono_eventually) have "aa>0" unfolding aa_def using \A>1\ by (auto simp add:field_simps pos_add_strict) then show " \\<^sub>F x in sequentially. aa ^ (nat \ nn) x = aa powr real_of_int (nn x)" by (auto simp: powr_int order.strict_implies_order[OF nn_pos]) qed auto qed ultimately show ?thesis apply (elim metric_tendsto_imp_tendsto) apply (auto intro!:powr_mono2 elim!:eventually_mono) using nn_pos ff_pos by (meson le_cases not_le)+ qed then have "(\n. (d (Suc n))^(nat (nn n)) * (a n / a (Suc n))) \ 0" proof (elim filterlim_mono_eventually) show "\\<^sub>F x in sequentially. ff x powr (nn x) = d (Suc x) ^ nat (nn x) * (a x / a (Suc x))" apply (rule eventuallyI) subgoal for x unfolding ff_def using a[rule_format,of x] a[rule_format,of "Suc x"] d[rule_format,of "Suc x"] nn_pos[of x] apply (auto simp add:field_simps powr_divide powr_powr powr_mult ) by (simp add: powr_int) done qed auto moreover have "(\n. b (Suc n) / (d (Suc n))^(nat (nn n))) \ 0" using tendsto_inverse_0_at_top[OF assu3,THEN LIMSEQ_ignore_initial_segment[where k=1]] unfolding nn_def by (auto simp add:field_simps nat_mult_distrib nat_power_eq) ultimately have "(\n. b (Suc n) * (a n / a (Suc n))) \ 0" apply - subgoal premises asm using tendsto_mult[OF asm,simplified] apply (elim filterlim_mono_eventually) using d by (auto simp add:algebra_simps,metis (mono_tags, lifting) always_eventually not_one_less_zero) done then have "(\n. (b (Suc n) / b n) * (a n / a (Suc n))) \ 0" apply (elim Lim_transform_bound[rotated]) apply (rule eventuallyI) subgoal for x using a[rule_format, of x] a[rule_format, of "Suc x"] b[rule_format, of x] b[rule_format, of "Suc x"] by (auto simp add:field_simps) done then show ?thesis unfolding c_def by (auto simp add:algebra_simps) qed from c_ratio_tendsto have "(\n. norm (b (Suc n) / a (Suc n)) / norm (b n / a n)) \ 0" unfolding c_def using a b by (force simp add:divide_simps abs_of_pos intro: Lim_transform_eventually) from summable_ratio_test_tendsto[OF _ _ this] a b show "summable c" unfolding c_def by (metis c_def c_pos less_irrefl zero_less_one) have "\\<^sub>F n in sequentially. (\j. c (n + j)) \ 2 * c n" proof - obtain N where N_ratio:"\n\N. c (n + 1) / c n < 1 / 2" proof - have "eventually (\n. c (n+1) / c n < 1/2) sequentially" using c_ratio_tendsto[unfolded tendsto_iff,rule_format, of "1/2",simplified] apply eventually_elim subgoal for n using c_pos[of n] c_pos[of "Suc n"] by auto done then show ?thesis using that unfolding eventually_sequentially by auto qed have "(\j. c (j + n)) \ 2 * c n" when "n\N" for n proof - have "(\j 2*c n * (1 - 1 / 2^(m+1))" for m proof (induct m) case 0 then show ?case using c_pos[of n] by simp next case (Suc m) have "(\ji c n + (\i c (i + n) / 2" for i using N_ratio[rule_format,of "i+n"] \n\N\ c_pos[of "i+n"] by simp then show ?thesis by (auto intro:sum_mono) qed also have "... = c n + (\i c n + c n * (1 - 1 / 2 ^ (m + 1))" using Suc by auto also have "... = 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))" by (auto simp add:field_simps) finally show ?case . qed then have "(\j 2*c n" for m using c_pos[of n] by (smt divide_le_eq_1_pos divide_pos_pos nonzero_mult_div_cancel_left zero_less_power) moreover have "summable (\j. c (j + n))" using \summable c\ by (simp add: summable_iff_shift) ultimately show ?thesis using suminf_le_const[of "\j. c (j+n)" "2*c n"] by auto qed then show ?thesis unfolding eventually_sequentially by (auto simp add:algebra_simps) qed then show "\\<^sub>F n in sequentially. (\j. (b (n + j)) / (a (n + j))) \ 2 * b n / a n" unfolding c_def by simp qed theorem Hancl3: fixes d ::"nat\real " and a b ::"nat\int " - assumes "A > 1" and d:"\n. d n> 1" and a: "\n. a n>0" and b:"\n. b n>0" and "s>0" - and assu1: "(( \ n. (of_int (a n)) powr(1 /of_int (2^n)))\ A) sequentially " - and assu2: "\n \ s. (A/ (of_int (a n)) powr(1 /of_int (2^n)))> prodinf (\j. d(n +j))" - and assu3: "filterlim (\ n. (d n)^(2^n)/ b n) at_top sequentially" + assumes "A > 1" and d: "\n. d n > 1" and a: "\n. a n>0" and b: "\n. b n > 0" and "s>0" + and assu1: "(\n. (a n) powr(1 / of_int(2^n))) \ A" + and assu2: "\n \ s. A / (a n) powr (1 / of_int(2^n)) > (\j. d (n + j))" + and assu3: "LIM n sequentially. d n ^ 2 ^ n / b n :> at_top" and "convergent_prod d" - shows "suminf(\ n. b n / a n ) \ Rats" -proof(rule ccontr) + shows "(\n. b n / a n) \ Rats" +proof (rule ccontr) assume asm:"\ (suminf(\ n. b n / a n ) \ Rats)" - have ab_sum:"summable (\j. b j / a j)" + have ab_sum: "summable (\j. b j / a j)" using issummable[OF \A>1\ d a b assu1 assu3 \convergent_prod d\] . obtain p q ::int where "q>0" and pq_def:"(\ n. b (n+1) / a (n+1) ) sums (p/q)" proof - - from asm have "suminf(\ n. b n / a n ) \ Rats" by auto - then have "suminf(\ n. b (n+1) / a (n+1)) \ Rats" + from asm have "(\n. b n / a n) \ \" by auto + then have "(\n. b (n+1) / a (n+1)) \ \" apply (subst suminf_minus_initial_segment[OF ab_sum,of 1]) by auto - then obtain p' q' ::int where "q'\0" and pq_def:"(\ n. b (n+1) / a (n+1) ) sums (p'/q')" + then obtain p' q' ::int where "q'\0" and pq_def: "(\ n. b (n+1) / a (n+1) ) sums (p'/q')" unfolding Rats_eq_int_div_int using summable_ignore_initial_segment[OF ab_sum,of 1,THEN summable_sums] by force - define p q where "p=(if q'<0 then - p' else p')" and "q=(if q'<0 then - q' else q')" - have "p'/q'=p/q" "q>0" using \q'\0\ unfolding p_def q_def by auto + define p q where "p \ (if q'<0 then -p' else p')" and "q \ (if q'<0 then -q' else q')" + have "p'/q' = p/q" "q>0" + using \q'\0\ unfolding p_def q_def by auto then show ?thesis using that[of q p] pq_def by auto qed define ALPHA where - "ALPHA = (\n. (of_int q)*((\j=1..n. of_int(a j)))*(suminf (\ (j::nat). + "ALPHA = (\n. (of_int q) * ((\j=1..n. of_int(a j)))*(suminf (\ (j::nat). (b (j+n+1)/a (j+n+1)))))" have "ALPHA n \ 1" for n proof - - have "suminf(\ n. b (n+1) / a (n+1)) > 0" - apply (rule suminf_pos) - subgoal using summable_ignore_initial_segment[OF ab_sum,of 1] by auto - subgoal using a b by simp - done - then have "p/q > 0" using sums_unique[OF pq_def,symmetric] by auto + have "(\n. b (n+1) / a (n+1)) > 0" + proof (rule suminf_pos) + show "summable (\n. b (n + 1) / real_of_int (a (n + 1)))" + using summable_ignore_initial_segment[OF ab_sum,of 1] by auto + show "\n. 0 < b (n + 1) / a (n + 1)" + using a b by simp + qed + then have "p/q > 0" + using pq_def sums_unique by force then have "q\1" "p\1" using \q>0\ by (auto simp add:divide_simps) moreover have "\n. 1 \ a n" "\n. 1 \ b n" using a b by (auto simp add: int_one_le_iff_zero_less) ultimately show ?thesis unfolding ALPHA_def using show7[OF _ _ _ _ pq_def] by auto qed moreover have "\n. ALPHA n < 1" unfolding ALPHA_def proof (rule lasttoshow[OF d a \s>0\ \q>0\ \A>1\ b _ assu3]) show "\\<^sub>F n in sequentially. (\j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \ real_of_int (2 * b n) / real_of_int (a n)" using show5[OF \A>1\ d a b assu1 assu3 \convergent_prod d\] by simp show "\m\s. \n\m. d (n + 1) * Max ((\j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}) \ real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))" apply (rule show9[OF \A>1\ d a \s>0\ assu1 \convergent_prod d\]) using show8[OF \A>1\ d a \s>0\ \convergent_prod d\ assu2] by (simp add:algebra_simps) qed ultimately show False using not_le by blast qed corollary Hancl3corollary: fixes A::real and a b ::"nat\int " assumes "A > 1" and a: "\n. a n>0" and b:"\n. b n>0" and assu1: "((\ n. (of_int (a n)) powr(1 /of_int (2^n)))\ A) sequentially " and asscor2: "\n \6. (of_int (a n)) powr(1 /of_int (2^n ))*(1+ 4*(2/3)^n) \ A \ (b n \2 powr((4/3)^(n-1)) ) " shows "suminf(\ n. b n / a n ) \ Rats" proof- define d::"nat\real" where "d= (\ n. 1+(2/3)^(n+1))" have dgt1:"\n. 1 < d n " unfolding d_def by auto moreover have "convergent_prod d" unfolding d_def apply (rule abs_convergent_prod_imp_convergent_prod) apply (rule summable_imp_abs_convergent_prod) by simp moreover have "\n\6. (\j. d (n + j)) < A / real_of_int (a n) powr (1 / real_of_int (2 ^ n))" proof (intro strip) fix n::nat assume "6 \ n" have d_sum:"summable (\j. ln (d j))" unfolding d_def by (auto intro: summable_ln_plus) have "(\j. ln (d (n + j))) < ln (1+4 * (2 / 3) ^ n)" proof - define c::real where "c=(2 / 3) ^ n" have "0n\6\ apply (subst power_add[symmetric]) by auto also have "... \ (2 / 3)^6" by (auto intro:power_le_one) also have "... < 1/8" by (auto simp add:field_simps) finally show "c<1/8" . qed (simp add:c_def) have "(\j. ln (d (n + j))) \ (\j. (2 / 3) ^ (n + j + 1))" proof (rule suminf_le) show "\j. ln (d (n + j)) \ (2 / 3) ^ (n + j + 1)" unfolding d_def by (metis divide_pos_pos less_eq_real_def ln_add_one_self_le_self zero_less_numeral zero_less_power) show "summable (\j. ln (d (n + j)))" using summable_ignore_initial_segment[OF d_sum] by (force simp add: algebra_simps) show "summable (\j. (2 / 3::real) ^ (n + j + 1))" using summable_geometric[THEN summable_ignore_initial_segment,of "2/3" "n+1"] by (auto simp add:algebra_simps) qed also have "... = (\j. (2 / 3)^(n+1)*(2 / 3) ^ j)" by (auto simp add:algebra_simps power_add) also have "... = (2 / 3)^(n+1) * (\j. (2 / 3) ^ j)" by (force intro!: summable_geometric suminf_mult) also have "... = 2 * c" unfolding c_def apply (subst suminf_geometric) by auto also have "... < 4 * c - (4 * c)\<^sup>2" using \0 \c<1/8\ by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1/16 * [1]^2))))") also have "... \ ln (1 + 4 * c)" apply (rule ln_one_plus_pos_lower_bound) using \0 \c<1/8\ by auto finally show ?thesis unfolding c_def by simp qed then have "exp (\j. ln (d (n + j))) < 1 + 4 * (2 / 3) ^ n" by (metis Groups.mult_ac(2) add.right_neutral add_mono_thms_linordered_field(5) divide_inverse divide_less_eq_numeral1(1) divide_pos_pos exp_gt_zero less_eq_real_def ln_exp ln_less_cancel_iff mult_zero_left rel_simps(27) rel_simps(76) zero_less_one zero_less_power) moreover have "exp (\j. ln (d (n + j))) = (\j. d (n + j))" proof (subst exp_suminf_prodinf_real [symmetric]) show "\k. 0 \ ln (d (n + k))" using dgt1 by (simp add: less_imp_le) show "abs_convergent_prod (\na. exp (ln (d (n + na))))" apply (subst exp_ln) subgoal for j using dgt1[rule_format,of "n+j"] by auto subgoal unfolding abs_convergent_prod_def real_norm_def apply (subst abs_of_nonneg) using convergent_prod_iff_shift[of d n] \convergent_prod d\ by (auto simp add: dgt1 less_imp_le algebra_simps) done show "(\na. exp (ln (d (n + na)))) = (\j. d (n + j))" apply (subst exp_ln) subgoal using dgt1 le_less_trans zero_le_one by blast subgoal by simp done qed ultimately have "(\j. d (n + j)) < 1 + 4 * (2 / 3) ^ n" by simp also have "... \ A / (a n) powr (1 / of_int (2 ^ n))" proof - have "a n powr (1 / real_of_int (2 ^ n)) > 0" using a[rule_format,of n] by auto then show ?thesis using asscor2[rule_format,OF \6\n\] by (auto simp add:field_simps) qed finally show "(\j. d (n + j)) < A / real_of_int (a n) powr (1 / of_int (2 ^ n))" . qed moreover have "LIM n sequentially. d n ^ 2 ^ n / real_of_int (b n) :> at_top" proof - have "LIM n sequentially. d n ^ 2 ^ n / 2 powr((4/3)^(n-1)) :> at_top" proof - define n1 where "n1=(\n. (2::real)* (3/2)^(n-1))" define n2 where "n2=(\n. ((4::real)/3)^(n-1))" have "LIM n sequentially. (((1+(8/9)/(n1 n)) powr (n1 n))/2) powr (n2 n) :> at_top" proof (rule filterlim_at_top_powr_real[where g'="exp (8/9) / (2::real)"]) define e1 where "e1=exp (8/9) / (2::real)" show "e1>1" unfolding e1_def by (approximation 4) show "(\n. ((1+(8/9)/(n1 n)) powr (n1 n))/2) \ e1" proof - have "(\n. (1+(8/9)/(n1 n)) powr (n1 n)) \ exp (8/9)" apply (rule filterlim_compose[OF tendsto_exp_limit_at_top]) unfolding n1_def by (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_realpow_sequentially_at_top simp:filterlim_sequentially_iff[of "\x. (3 / 2) ^ (x - Suc 0)" _ 1]) then show ?thesis unfolding e1_def by (intro tendsto_intros,auto) qed show "filterlim n2 at_top sequentially" unfolding n2_def apply (subst filterlim_sequentially_iff[of "\n. (4 / 3) ^ (n - 1)" _ 1]) by (auto intro:filterlim_realpow_sequentially_at_top) qed moreover have "\\<^sub>F n in sequentially. (((1+(8/9)/(n1 n)) powr (n1 n))/2) powr (n2 n) = d n ^ 2 ^ n / 2 powr((4/3)^(n-1))" proof (rule eventually_sequentiallyI[of 1]) fix x assume "x\(1::nat)" have " ((1 + 8 / 9 / n1 x) powr n1 x / 2) powr n2 x = (((1 + 8 / 9 / n1 x) powr n1 x) powr n2 x) / 2 powr (4 / 3) ^ (x - 1)" by (simp add:n1_def n2_def powr_divide) also have "... = (1 + 8 / 9 / n1 x) powr (n1 x * n2 x) / 2 powr (4 / 3) ^ (x - 1)" by (simp add: powr_powr) also have "... = (1 + 8 / 9 / n1 x) powr (2 ^ x) / 2 powr (4 / 3) ^ (x - 1)" proof - have "n1 x * n2 x = 2 ^ x" unfolding n1_def n2_def apply (subst mult.assoc) apply (subst power_mult_distrib[symmetric]) using \x\1\ by (auto simp flip:power_Suc) then show ?thesis by simp qed also have "... = (1 + 8 / 9 / n1 x) ^ (2 ^ x) / 2 powr (4 / 3) ^ (x - 1)" apply (subst (3) powr_realpow[symmetric]) apply (simp_all add: n1_def) by (smt zero_le_divide_iff zero_le_power) also have "... = d x ^ 2 ^ x / 2 powr (4 / 3) ^ (x - 1)" proof - define x1 where "x1=x-1" have *:"x=x1+1" unfolding x1_def using \x\1\ by simp have **: "8 / 9 / n1 x = (2 / 3) ^ (x + 1)" unfolding n1_def using \x\1\ apply (fold x1_def *[symmetric]) by (auto simp add:divide_simps) then show ?thesis unfolding d_def apply (subst **) by auto qed finally show "((1 + 8 / 9 / n1 x) powr n1 x / 2) powr n2 x = d x ^ 2 ^ x / 2 powr (4 / 3) ^ (x - 1) " . qed ultimately show ?thesis using filterlim_cong by fast qed moreover have "\\<^sub>F n in sequentially. d n ^ 2 ^ n / 2 powr((4/3)^(n-1)) \ d n ^ 2 ^ n / real_of_int (b n)" apply (rule eventually_sequentiallyI[of 6]) - apply (rule divide_left_mono) - subgoal for x - using asscor2[rule_format,of x] by auto - subgoal for x - using \\n. 1 < d n\[rule_format, of x] by auto - subgoal for x - using b by auto - done + by (smt (verit, best) asscor2 b dgt1 frac_le of_int_0_less_iff zero_le_power) ultimately show ?thesis by (auto elim: filterlim_at_top_mono) qed ultimately show ?thesis using Hancl3[OF \A>1\ _ a b _ assu1,of d 6] by force qed end