Theory Irrationality_J_Hancl

(*
  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. 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" and g': "(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: 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
        by (smt (verit, best) g'>1 ln_le_cancel_iff divide_le_eq_1_pos powr_nonneg_iff)
    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"
      by (metis add.commute g' gt_half_sum one_add_one order_tendsto_iff)
    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 "sn" 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 sSuc n by linarith
  qed
  ultimately show ?case using sSuc n by linarith
qed

lemma summable_ratio_test_tendsto:
  fixes f :: "nat  'a::banach"
  assumes "c < 1" and "n. f n0" and "(λn. norm (f (Suc n)) / norm (f n))  c"
  shows "summable f"
proof -
  obtain N where N_dist:"nN. 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 "nN" 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 "nN" 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 ::"natint " 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::"natreal" and a b::"natint " 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 q1 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 ::"natreal " and a :: "natint" 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 "ns. (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 "in" 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 ni 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 "js. A / ff j > sp j" 
    unfolding ff_def sp_def using assu2 by (auto simp:algebra_simps)
  ultimately have "j. sj  jn  A / ff j > sp n" by force
  then show "sp n< A / Max (ff ` {s..n})" 
    by (metis (mono_tags, opaque_lifting) Max_in ns atLeastAtMost_iff empty_iff 
        finite_atLeastAtMost finite_imageI imageE image_is_empty order_refl)
qed

lemma auxiliary1_9:
  fixes d ::"natreal" and a::"natint " 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: "nm. (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 "nm" for n
    using auxifalse_assu that unfolding ff_def by simp
  from nm
  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 ms by simp 
  next
    case (Suc n)
    have ?case when "m=Suc n"
      using that by auto
    moreover have ?case when "mSuc 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 nm 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 mn d[rule_format,of "Suc n"] by (simp add:prod.nat_ivl_Suc')
  then show ?thesis using ff_asm[of n] sm mn unfolding ff_def by auto
qed

lemma show9:
  fixes d ::"natreal " and a :: "natint " 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: "ns. prodinf (λj. d( n+j)) 
                  < A/(Max ((λ(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n})) "
  shows "m s. nm.  ( (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. nm. ff(n+1)  d(n+1) * Max (ff  ` {s..n}))"

  then obtain t where "ts" and
    ttt: "nt. 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. in. 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 _ ts 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 ts 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] st 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 ::"natreal " and  a ::"natint " 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. nm. 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 "ms. nm. 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 "nm" 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 sm have "sn" 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 ns  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 sn 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 sn 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 sn  by auto
      moreover have "xS. x1"
      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 sn 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 sn 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 sn 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 "nm. 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 nm ms 
    by force
qed

lemma lasttoshow:
  fixes d ::"natreal " and a b ::"natint " 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:
    "ms. nm. ((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 "ns" 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:"nN. 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 "ns" and "nN" 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"] 
      ns 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 ::"natreal " and  a b ::"natint " 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:"nN. 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 "nN" 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"] nN 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 ::"natreal" and  a b :: "natint"
  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 "q1" "p1" 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 "ms. nm. 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 :: "natint"
  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::"natreal" 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 "n6. (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 n6
          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 6n] 
        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 k1 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 k1
            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