Theory Irrationality_J_Hancl
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. Hančl, 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 prove the central result (theorem Hancl3) 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 rational. 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. Hančl.
›
hide_const floatarith.Max
subsection ‹Misc›
lemma filterlim_sequentially_iff:
"filterlim f F1 sequentially ⟷ filterlim (λx. f (x+k)) F1 sequentially"
unfolding filterlim_iff
by (metis eventually_at_top_linorder eventually_sequentially_seg)
lemma filterlim_realpow_sequentially_at_top:
"(x::real) > 1 ⟹ filterlim (power 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 "LIM x F. g x powr f x :> at_top"
proof -
have "LIM x F. ((g' + 1) / 2) powr f x :> at_top"
proof (subst filterlim_at_top_gt[of _ _ 1],rule+)
fix Z::real assume "Z > 1"
have "∀⇩F x in F. ln Z / ln ((g' + 1) / 2) ≤ f x"
using assms(1) filterlim_at_top by blast
then have "∀⇩F x in F. ln Z ≤ ln (((g' + 1) / 2) powr f x)"
proof (eventually_elim)
case (elim x)
then show ?case
using ‹g'>1› by (auto simp:ln_powr divide_simps)
qed
then show "∀⇩F x in F. Z ≤ ((g' + 1) / 2) powr f x"
proof (eventually_elim)
case (elim x)
then show ?case
using ‹1 < Z› ‹g'>1› by auto
qed
qed
moreover have "∀⇩F x in F. ((g'+1)/2) powr f x ≤ g x powr f x"
proof -
have "∀⇩F x in F. g x > (g'+1)/2"
apply (rule order_tendstoD[OF assms(2)])
using ‹g'>1› by auto
moreover have "∀⇩F x in F. f x>0"
using assms(1) filterlim_at_top_dense by blast
ultimately show ?thesis
proof eventually_elim
case (elim x)
then show ?case
using ‹g'>1› by (auto intro!: powr_mono2)
qed
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 (power 2) {s..Suc n}" using that by auto
ultimately show "(∏j = s..Suc n. a powr 2 ^ j) = a powr sum (power 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 "∀⇩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<n. f (i + k)) ⇢ (∑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<n. f i) ⇢ (∑i. f i)"
using summable_sums[OF ‹summable f›] by (simp add: sums_def atLeast0LessThan f)
then have "(λn. ∑i<n + k. f 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 "(∑i<n. f (i + k)) = (∑i<n. (f ∘ (λi. i + k)) i)"
by simp
also have "… = (∑i∈(λi. i + k) ` {..<n}. f i)"
by (subst sum.reindex) auto
also have "… ≤ sum f {..<n + k}"
by (intro sum_mono2) (auto simp: f)
finally show "(∑i<n. f (i + k)) ≤ sum f {..<n + k}" .
qed
qed
lemma factt:
fixes s n ::nat assumes "s ≤ 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 {..<n}"
apply (rule suminf_minus_initial_segment)
using assumerational unfolding ff_def by (simp add: sums_summable)
also have "... = p/q - sum ff {..<n}"
using assumerational unfolding ff_def by (simp add: sums_iff)
also have "... = p/q - (∑j=1..n. ff (j-1))"
proof -
have "sum ff {..<n} = (∑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
by (induction n) (simp_all 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
using a assms assumerational int_one_le_iff_zero_less showpre7 by force
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 j assume "j ∈ {1..n}"
then have "(∏i = 1..n. real_of_int (a i)) = a j * (∏i∈{1..n} - {j}. real_of_int (a i))"
by (meson finite_atLeastAtMost prod.remove)
then have "aa / real_of_int (a j) = prod a ({1..n} - {j})"
unfolding aa_def using a[rule_format,of j] by (auto simp add:field_simps)
then show "aa * b j / a j = b j * prod a ({1..n} - {j})"
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)) > (∏j. d (n + j))"
shows "∀n≥s. (∏j. d (j+n)) < A / (MAX j∈{s..n}. of_int (a j) powr (1 / of_int (2 ^ j)))"
proof (intro strip)
fix n assume "s ≤ n"
define sp where "sp ≡ (λn. ∏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)) * (∏ia<n - i. d (ia + i))"
proof (rule prodinf_split_initial_segment)
show "convergent_prod (λj. 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 * (∏j<n - i. d (i + j))"
unfolding sp_def using ‹n≥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<n - i. d (i + 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, opaque_lifting) 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. 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, opaque_lifting) 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)"
by (metis d max.commute max.strict_order_iff)
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. 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 ≡ ∏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 "∀⇩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 "∀⇩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})"
using ‹t≥s› by (auto intro: Max_mono)
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 fastforce
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 [rule_format]: "∀n. d n> 1"
and a [rule_format]: "∀n. a n>0" and " s>0"
and 9: "∀m ≥s. ∃n≥m. a (n+1) powr(1 / of_int (2^(n+1))) ≥
d (n+1) * (Max ((λj. (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 (intro strip)
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
define M where "M ≡ λs. MAX j∈{s..n}. a j powr (1 / real_of_int (2 ^ j))"
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. M s 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. M s powr 2 ^ i)"
proof (intro prod_mono conjI)
fix i assume i: "i ∈ {s..n}"
have "a i = (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 "… ≤ M s powr(2^i)"
unfolding M_def using i by (force intro: powr_mono2)
finally show "a i ≤ M s powr 2 ^ i" .
show "⋀i. i ∈ {s..n} ⟹ 0 ≤ real_of_int (a i)"
by (meson a less_imp_le of_int_0_le_iff)
qed
qed
also have "... = d(n+1) powr (2^(n+1)) * M s 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. M s powr(2^i)) = M s 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) * M s powr(2^(n+1))"
proof -
have "sum (power 2) {s..n} < (2::real) ^ (n + 1)" using factt ‹s≤n› by auto
moreover have "1 ≤ M s"
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 M_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 M_def)
qed
also have "... = (d (n+1) * M s) powr(2^(n+1))"
proof -
have "d (n + 1) ≥ 0" using d[of "n+1"] by argo
moreover have "M s ≥ 0"
using ‹s≤n› by (auto simp: M_def Max_ge_iff)
ultimately show ?thesis
unfolding M_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 (rule powr_mono2)
have "M s ≥ 0"
using ‹s≤n› by (auto simp: M_def Max_ge_iff)
moreover have "d (n + 1) ≥0"
using d[of "n+1"] by argo
ultimately show "0 ≤ (d (n + 1)) * M s" by auto
show "(d (n + 1)) * M s ≤ real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))"
using M_def asm_9 by presburger
qed simp
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: "∀⇩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
by (metis d le_less_trans powr_realpow zero_le_one)
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 "∀⇩F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1"
by (elim order_tendstoD) simp
then have "∀⇩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: field_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: "∀⇩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 n<aa) sequentially"
apply (rule order_tendstoD[OF ff_tendsto])
unfolding aa_def using ‹A>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 " ∀⇩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 "∀⇩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 "∀⇩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<m. c (j + n)) ≤ 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 "(∑j<Suc m. c (j + n)) = c n + (∑i<m. c (Suc i + n)) "
unfolding sum.lessThan_Suc_shift by simp
also have "... ≤ c n + (∑i<m. c (i + n) / 2)"
proof -
have "c (Suc i + n) ≤ 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<m. c (i + n)) / 2"
unfolding sum_divide_distrib by simp
also have "... ≤ 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<m. c (j + n)) ≤ 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 "∀⇩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. (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 "(∑n. b n / a n) ∉ ℚ"
proof (rule ccontr)
assume asm: "¬ ((∑n. b n / a n) ∉ ℚ)"
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 "(∑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')"
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
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)) * (∑j. (b (j+n+1)/a (j+n+1))))"
have "ALPHA n ≥ 1" for n
proof -
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 "∀⇩F n in sequentially. (∑j. b (n+j) / a (n+j)) ≤ (2 * b n) / 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∈{s..n}. a j powr (1 / of_int (2 ^ j)))
≤ a (n+1) powr (1 / 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. (a n) powr(1 / of_int(2^n))) ⇢ A"
and asscor2: "∀n ≥ 6. a n powr(1 / of_int (2^n)) * (1 + 4*(2/3)^n) ≤ A
∧ b n ≤ 2 powr (4/3)^(n-1)"
shows "(∑n. b n / a n) ∉ ℚ"
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
by (simp add: abs_convergent_prod_imp_convergent_prod summable_imp_abs_convergent_prod)
moreover have "∀n≥6. (∏j. d (n+j)) < A / a n powr (1 / 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 "0<c" "c<1/8"
proof -
have "c = (2/3)^6 * (2/3) ^ (n-6)"
unfolding c_def using ‹n≥6›
by (metis le_add_diff_inverse power_add)
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
by (simp add: suminf_geometric)
also have "... < 4 * c - (4 * c)⇧2"
using ‹0<c› ‹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› ‹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 (smt (z3) divide_pos_pos ln_exp ln_ge_iff 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))))"
proof (subst exp_ln)
show "⋀j. 0 < d (n + j)"
using dgt1 le_less_trans zero_le_one by blast
show "abs_convergent_prod (λj. d (n + j))"
unfolding abs_convergent_prod_def
using ‹convergent_prod d›
by (simp add: dgt1 convergent_prod_iff_shift less_imp_le algebra_simps)
qed
show "(∏j. exp (ln (d (n + j)))) = (∏j. d (n + j))"
by (meson dgt1 exp_ln not_less not_one_less_zero order_trans)
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"])
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 "∀⇩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)
fix k::nat assume "k ≥ 1"
have "((1 + 8 / 9 / n1 k) powr n1 k / 2) powr n2 k
= (((1 + 8 / 9 / n1 k) powr n1 k) powr n2 k) / 2 powr (4 / 3) ^ (k - 1)"
by (simp add: n1_def n2_def powr_divide)
also have "... = (1 + 8 / 9 / n1 k) powr (n1 k * n2 k) / 2 powr (4 / 3) ^ (k - 1)"
by (simp add: powr_powr)
also have "... = (1 + 8 / 9 / n1 k) powr (2 ^ k) / 2 powr (4 / 3) ^ (k - 1)"
proof -
have "n1 k * n2 k = 2 ^ k"
unfolding n1_def n2_def
using ‹k≥1› by (simp add: mult_ac flip:power_mult_distrib power_Suc)
then show ?thesis by simp
qed
also have "... = (1 + 8 / 9 / n1 k) ^ (2 ^ k) / 2 powr (4 / 3) ^ (k - 1)"
unfolding n1_def
by (smt (verit, best) powr_realpow divide_pos_pos numeral_plus_numeral numeral_plus_one of_nat_numeral of_nat_power semiring_norm(2) zero_less_power)
also have "... = d k ^ 2 ^ k / 2 powr (4 / 3) ^ (k - 1)"
proof -
have **: "8 / 9 / n1 k = (2/3) ^ (k+1)"
unfolding n1_def using ‹k≥1›
by (simp add: divide_simps split: nat_diff_split)
then show ?thesis
unfolding d_def by presburger
qed
finally show "((1 + 8 / 9 / n1 k) powr n1 k / 2) powr n2 k
= d k ^ 2 ^ k / 2 powr (4 / 3) ^ (k - 1)" .
qed
ultimately show ?thesis using filterlim_cong by fast
qed
moreover have "∀⇩F n in sequentially. d n ^ 2 ^ n / 2 powr((4/3)^(n-1))
≤ d n ^ 2 ^ n / real_of_int (b n)"
using eventually_sequentiallyI[of 6]
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