Theory Akra_Bazzi.Akra_Bazzi_Asymptotics

(* File:   Akra_Bazzi_Asymptotics.thy
   Author: Manuel Eberl <manuel@pruvisto.org>

   Proofs for the four(ish) asymptotic inequalities required for proving the
   Akra Bazzi theorem with variation functions in the recursive calls.
*)

section ‹Asymptotic bounds›
theory Akra_Bazzi_Asymptotics
imports
  Complex_Main
  Akra_Bazzi_Library
  "HOL-Library.Landau_Symbols"
begin

locale akra_bazzi_asymptotics_bep =
  fixes b e p hb :: real
  assumes bep: "b > 0" "b < 1" "e > 0" "hb > 0"
begin

context
begin

text ‹
  Functions that are negligible w.r.t. @{term "ln (b*x) powr (e/2 + 1)"}.
›
private abbreviation (input) negl :: "(real  real)  bool" where
  "negl f  f  o(λx. ln (b*x) powr (-(e/2 + 1)))"

private lemma neglD: "negl f  c > 0  eventually (λx. ¦f x¦  c / ln (b*x) powr (e/2+1)) at_top"
  by (drule (1) landau_o.smallD, subst (asm) powr_minus) (simp add: field_simps)

private lemma negl_mult: "negl f  negl g  negl (λx. f x * g x)"
  by (erule landau_o.small_1_mult, rule landau_o.small_imp_big, erule landau_o.small_trans)
     (insert bep, simp)

private lemma ev4:
  assumes g: "negl g"
  shows   "eventually (λx. ln (b*x) powr (-e/2) - ln x powr (-e/2)  g x) at_top"
proof (rule smallo_imp_le_real)
  define h1 where [abs_def]:
    "h1 x = (1 + ln b/ln x) powr (-e/2) - 1 + e/2 * (ln b/ln x)" for x
  define h2 where [abs_def]:
    "h2 x = ln x powr (- e / 2) * ((1 + ln b / ln x) powr (- e / 2) - 1)" for x
  from bep have "((λx. ln b / ln x)  0) at_top"
    by (simp add: tendsto_0_smallo_1)
  note one_plus_x_powr_Taylor2_bigo[OF this, of "-e/2"]
  also have "(λx. (1 + ln b / ln x) powr (- e / 2) - 1 - - e / 2 * (ln b / ln x)) = h1"
    by (simp add: h1_def)
  finally have "h1  o(λx. 1 / ln x)"
    by (rule landau_o.big_small_trans) (insert bep, simp add: power2_eq_square)
  with bep have "(λx. h1 x - e/2 * (ln b / ln x))  Θ(λx. 1 / ln x)" by simp
  also have "(λx. h1 x - e/2 * (ln b/ln x)) = (λx. (1 + ln b/ ln x) powr (-e/2) - 1)"
    by (rule ext) (simp add: h1_def)
  finally have "h2  Θ(λx. ln x powr (-e/2) * (1 / ln x))" unfolding h2_def
    by (intro landau_theta.mult) simp_all
  also have "(λx. ln x powr (-e/2) * (1 / ln x))  Θ(λx. ln x powr (-(e/2+1)))" by simp
  also from g bep have "(λx. ln x powr (-(e/2+1)))  ω(g)" by (simp add: smallomega_iff_smallo)
  finally have "g  o(h2)" by (simp add: smallomega_iff_smallo)
  also have "eventually (λx. h2 x = ln (b*x) powr (-e/2) - ln x powr (-e/2)) at_top"
    using eventually_gt_at_top[of "1::real"] eventually_gt_at_top[of "1/b"]
    by eventually_elim (use bep in simp add: ln_mult powr_diff h2_def powr_minus powr_divide field_simps)
  hence "h2  Θ(λx. ln (b*x) powr (-e/2) - ln x powr (-e/2))" by (rule bigthetaI_cong)
  finally show "g  o(λx. ln (b * x) powr (- e / 2) - ln x powr (- e / 2))" .
next
  show "eventually (λx. ln (b*x) powr (-e/2) - ln x powr (-e/2)  0) at_top"
    using eventually_gt_at_top[of "1/b"] eventually_gt_at_top[of "1::real"]
    by eventually_elim (use bep in auto intro!: powr_mono2' simp: field_simps simp flip: ln_mult)
qed

private lemma ev1:
  "negl (λx. (1 + c * inverse b * ln x powr (-(1+e))) powr p - 1)"
proof-
  from bep have "((λx. c * inverse b * ln x powr (-(1+e)))  0) at_top"
    by (simp add: tendsto_0_smallo_1)
  have "(λx. (1 + c * inverse b * ln x powr (-(1+e))) powr p - 1)
            O(λx. c * inverse b * ln x powr - (1 + e))"
    using bep by (intro one_plus_x_powr_Taylor1_bigo) (simp add: tendsto_0_smallo_1)
  also from bep have "negl (λx. c * inverse b * ln x powr - (1 + e))" by simp
  finally show ?thesis .
qed

private lemma ev2_aux:
  defines "f  λx. (1 + 1/ln (b*x) * ln (1 + hb / b * ln x powr (-1-e))) powr (-e/2)"
  obtains h where "eventually (λx. f x  1 + h x) at_top" "h  o(λx. 1 / ln x)"
proof (rule that[of "λx. f x - 1"])
  define g where [abs_def]: "g x = 1/ln (b*x) * ln (1 + hb / b * ln x powr (-1-e))" for x
  have lim: "((λx. ln (1 + hb / b * ln x powr (- 1 - e)))  0) at_top"
    by (rule tendsto_eq_rhs[OF tendsto_ln[OF tendsto_add[OF tendsto_const, of _ 0]]])
       (insert bep, simp_all add: tendsto_0_smallo_1)
  hence lim': "(g  0) at_top" unfolding g_def
    by (intro tendsto_mult_zero) (insert bep, simp add: tendsto_0_smallo_1)
  from one_plus_x_powr_Taylor2_bigo[OF this, of "-e/2"]
    have "(λx. (1 + g x) powr (-e/2) - 1 - - e/2 * g x)  O(λx. (g x)2)" .
  also from lim' have "(λx. g x ^ 2)  o(λx. g x * 1)" unfolding power2_eq_square
    by (intro landau_o.big_small_mult smalloI_tendsto) simp_all
  also have "o(λx. g x * 1) = o(g)" by simp
  also have "(λx. (1 + g x) powr (-e/2) - 1 - - e/2 * g x) = (λx. f x - 1 + e/2 * g x)"
    by (simp add: f_def g_def)
  finally have A: "(λx. f x - 1 + e / 2 * g x)  O(g)" by (rule landau_o.small_imp_big)
  hence "(λx. f x - 1 + e/2 * g x - e/2 * g x)  O(g)"
    by (rule sum_in_bigo) (insert bep, simp)
  also have "(λx. f x - 1 + e/2 * g x - e/2 * g x) = (λx. f x - 1)" by simp
  finally have "(λx. f x - 1)  O(g)" .
  also from bep lim have "g  o(λx. 1 / ln x)" unfolding g_def
    by (auto intro!: smallo_1_tendsto_0)
  finally show "(λx. f x - 1)  o(λx. 1 / ln x)" .
qed simp_all

private lemma ev2:
  defines "f  λx. ln (b * x + hb * x / ln x powr (1 + e)) powr (-e/2)"
  obtains h where
    "negl h"
    "eventually (λx. f x  ln (b * x) powr (-e/2) + h x) at_top"
    "eventually (λx. ¦ln (b * x) powr (-e/2) + h x¦ < 1) at_top"
proof -
  define f'
    where "f' x = (1 + 1 / ln (b*x) * ln (1 + hb / b * ln x powr (-1-e))) powr (-e/2)" for x
  from ev2_aux obtain g where g: "eventually (λx. 1 + g x  f' x) at_top" "g  o(λx. 1 / ln x)"
    unfolding f'_def .
  define h where [abs_def]: "h x = ln (b*x) powr (-e/2) * g x" for x
  show ?thesis
  proof (rule that[of h])
    from bep g show "negl h" unfolding h_def
      by (auto simp: powr_diff elim: landau_o.small_big_trans)
  next
    from g(2) have "g  o(λx. 1)" by (rule landau_o.small_big_trans) simp
    with bep have "eventually (λx. ¦ln (b*x) powr (-e/2) * (1 + g x)¦ < 1) at_top"
      by (intro smallo_imp_abs_less_real) simp_all
    thus "eventually (λx. ¦ln (b*x) powr (-e/2) + h x¦ < 1) at_top"
      by (simp add: algebra_simps h_def)
  next
    from eventually_gt_at_top[of "1/b"] and g(1)
      show "eventually (λx. f x  ln (b*x) powr (-e/2) + h x) at_top"
    proof eventually_elim
      case (elim x)
      from bep have "b * x + hb * x / ln x powr (1 + e) = b*x * (1 + hb / b * ln x powr (-1 - e))"
        by (simp add: field_simps powr_diff powr_add powr_minus)
      also from elim(1) bep
        have "ln  = ln (b*x) * (1 + 1/ln (b*x) * ln (1 + hb / b * ln x powr (-1-e)))"
        by (subst ln_mult_pos) (simp_all add: add_pos_nonneg field_simps)
      also from elim(1) bep have " powr (-e/2) = ln (b*x) powr (-e/2) * f' x"
        by (subst powr_mult) (simp_all add: field_simps f'_def)
      also from elim have "  ln (b*x) powr (-e/2) * (1 + g x)"
        by (intro mult_left_mono) simp_all
      finally show "f x  ln (b*x) powr (-e/2) + h x"
        by (simp add: f_def h_def algebra_simps)
    qed
  qed
qed

private lemma ev21:
  obtains g where
    "negl g"
    "eventually (λx. 1 + ln (b * x + hb * x / ln x powr (1 + e)) powr (-e/2) 
         1 + ln (b * x) powr (-e/2) + g x) at_top"
    "eventually (λx. 1 + ln (b * x) powr (-e/2) + g x > 0) at_top"
proof-
  from ev2 guess g . note g = this
  from g(3) have "eventually (λx. 1 + ln (b * x) powr (-e/2) + g x > 0) at_top"
    by eventually_elim simp
  with g(1,2) show ?thesis by (intro that[of g]) simp_all
qed

private lemma ev22:
  obtains g where
    "negl g"
    "eventually (λx. 1 - ln (b * x + hb * x / ln x powr (1 + e)) powr (-e/2) 
         1 - ln (b * x) powr (-e/2) - g x) at_top"
    "eventually (λx. 1 - ln (b * x) powr (-e/2) - g x > 0) at_top"
proof-
  from ev2 guess g . note g = this
  from g(2) have "eventually (λx. 1 - ln (b * x + hb * x / ln x powr (1 + e)) powr (-e/2) 
                                      1 - ln (b * x) powr (-e/2) - g x) at_top"
    by eventually_elim simp
  moreover from g(3) have "eventually (λx. 1 - ln (b * x) powr (-e/2) - g x > 0) at_top"
    by eventually_elim simp
  ultimately show ?thesis using g(1) by (intro that[of g]) simp_all
qed


lemma asymptotics1:
  shows "eventually (λx.
             (1 + c * inverse b * ln x powr -(1+e)) powr p *
             (1 + ln (b * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) 
             1 + (ln x powr (-e/2))) at_top"
proof-
  let ?f = "λx. (1 + c * inverse b * ln x powr -(1+e)) powr p"
  let ?g = "λx. 1 + ln (b * x + hb * x / ln x powr (1 + e)) powr (- e / 2)"
  define f where [abs_def]: "f x = 1 - ?f x" for x
  from ev1[of c] have "negl f" unfolding f_def
    by (subst landau_o.small.uminus_in_iff [symmetric]) simp
  from landau_o.smallD[OF this zero_less_one]
    have f: "eventually (λx. f x  ln (b*x) powr -(e/2+1)) at_top"
    by eventually_elim (simp add: f_def)

  from ev21 guess g . note g = this
  define h where [abs_def]: "h x = -g x + f x + f x * ln (b*x) powr (-e/2) + f x * g x" for x

  have A: "eventually (λx. ?f x * ?g x  1 + ln (b*x) powr (-e/2) - h x) at_top"
    using g(2,3) f
  proof eventually_elim
    case (elim x)
    let ?t = "ln (b*x) powr (-e/2)"
    have "1 + ?t - h x = (1 - f x) * (1 + ln (b*x) powr (-e/2) + g x)"
      by (simp add: algebra_simps h_def)
    also from elim have "?f x * ?g x  (1 - f x) * (1 + ln (b*x) powr (-e/2) + g x)"
      by (intro mult_mono[OF _ elim(1)]) (simp_all add: algebra_simps f_def)
    finally show "?f x * ?g x  1 + ln (b*x) powr (-e/2) - h x" .
  qed
  from bep negl f g(1) have "negl h" unfolding h_def
    by (fastforce intro!: sum_in_smallo landau_o.small.mult simp: powr_diff
                  intro: landau_o.small_trans)+
  from ev4[OF this] A show ?thesis by eventually_elim simp
qed

lemma asymptotics2:
  shows "eventually (λx.
             (1 + c * inverse b * ln x powr -(1+e)) powr p *
             (1 - ln (b * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) 
             1 - (ln x powr (-e/2))) at_top"
proof-
  let ?f = "λx. (1 + c * inverse b * ln x powr -(1+e)) powr p"
  let ?g = "λx. 1 - ln (b * x + hb * x / ln x powr (1 + e)) powr (- e / 2)"

  define f where [abs_def]: "f x = 1 - ?f x" for x
  from ev1[of c] have "negl f" unfolding f_def
    by (subst landau_o.small.uminus_in_iff [symmetric]) simp
  from landau_o.smallD[OF this zero_less_one]
    have f: "eventually (λx. f x  ln (b*x) powr -(e/2+1)) at_top"
    by eventually_elim (simp add: f_def)

  from ev22 guess g . note g = this
  define h where [abs_def]: "h x = -g x - f x + f x * ln (b*x) powr (-e/2) + f x * g x" for x
  have "((λx. ln (b * x + hb * x / ln x powr (1 + e)) powr - (e / 2))  0) at_top"
    apply (insert bep, intro tendsto_neg_powr, simp)
    apply (rule filterlim_compose[OF ln_at_top])
    apply (rule filterlim_at_top_smallomega_1, simp)
    using eventually_gt_at_top[of "max 1 (1/b)"]
    apply (auto elim!: eventually_mono intro!: add_pos_nonneg simp: field_simps)
    apply (smt (z3) divide_nonneg_nonneg mult_neg_pos mult_nonneg_nonneg powr_non_neg)
    done
  hence ev_g: "eventually (λx. ¦1 - ?g x¦ < 1) at_top"
    by (intro smallo_imp_abs_less_real smalloI_tendsto) simp_all

  have A: "eventually (λx. ?f x * ?g x  1 - ln (b*x) powr (-e/2) + h x) at_top"
    using g(2,3) ev_g f
  proof eventually_elim
    case (elim x)
    let ?t = "ln (b*x) powr (-e/2)"
    from elim have "?f x * ?g x  (1 - f x) * (1 - ln (b*x) powr (-e/2) - g x)"
      by (intro mult_mono) (simp_all add: f_def)
    also have "... = 1 - ?t + h x" by (simp add: algebra_simps h_def)
    finally show "?f x * ?g x  1 - ln (b*x) powr (-e/2) + h x" .
  qed
  from bep negl f g(1) have "negl h" unfolding h_def
    by (fastforce intro!: sum_in_smallo landau_o.small.mult simp: powr_diff
                  intro: landau_o.small_trans)+
  from ev4[OF this] A show ?thesis by eventually_elim simp
qed

lemma asymptotics3: "eventually (λx. (1 + (ln x powr (-e/2))) / 2  1) at_top"
  (is "eventually (λx. ?f x  1) _")
proof (rule eventually_mp[OF always_eventually], clarify)
  from bep have "(?f  1/2) at_top"
    by (force intro: tendsto_eq_intros tendsto_neg_powr ln_at_top)
  hence "e. e>0  eventually (λx. ¦?f x - 0.5¦ < e) at_top"
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  from this[of "0.5"] show "eventually (λx. ¦?f x - 0.5¦ < 0.5) at_top" by simp
  fix x assume "¦?f x - 0.5¦ < 0.5"
  thus "?f x  1" by simp
qed

lemma asymptotics4: "eventually (λx. (1 - (ln x powr (-e/2))) * 2  1) at_top"
  (is "eventually (λx. ?f x  1) _")
proof (rule eventually_mp[OF always_eventually], clarify)
  from bep have "(?f  2) at_top"
    by (force intro: tendsto_eq_intros tendsto_neg_powr ln_at_top)
  hence "e. e>0  eventually (λx. ¦?f x - 2¦ < e) at_top"
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  from this[of 1] show "eventually (λx. ¦?f x - 2¦ < 1) at_top" by simp
  fix x assume "¦?f x - 2¦ < 1"
  thus "?f x  1" by simp
qed

lemma asymptotics5: "eventually (λx. ln (b*x - hb*x*ln x powr -(1+e)) powr (-e/2) < 1) at_top"
proof-
  from bep have "((λx. b - hb * ln x powr -(1+e))  b - 0) at_top"
    by (intro tendsto_intros tendsto_mult_right_zero tendsto_neg_powr ln_at_top) simp_all
  hence "LIM x at_top. (b - hb * ln x powr -(1+e)) * x :> at_top"
    by (rule filterlim_tendsto_pos_mult_at_top[OF _ _ filterlim_ident], insert bep) simp_all
  also have "(λx. (b - hb * ln x powr -(1+e)) * x) = (λx. b*x - hb*x*ln x powr -(1+e))"
    by (intro ext) (simp add: algebra_simps)
  finally have "filterlim ... at_top at_top" .
  with bep have "((λx. ln (b*x - hb*x*ln x powr -(1+e)) powr -(e/2))  0) at_top"
    by (intro tendsto_neg_powr filterlim_compose[OF ln_at_top]) simp_all
  hence "eventually (λx. ¦ln (b*x - hb*x*ln x powr -(1+e)) powr (-e/2)¦ < 1) at_top"
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  thus ?thesis by simp
qed

lemma asymptotics6: "eventually (λx. hb / ln x powr (1 + e) < b/2) at_top"
  and asymptotics7: "eventually (λx. hb / ln x powr (1 + e) < (1 - b) / 2) at_top"
  and asymptotics8: "eventually (λx. x*(1 - b - hb / ln x powr (1 + e)) > 1) at_top"
proof-
  from bep have A: "(λx. hb / ln x powr (1 + e))  o(λ_. 1)" by simp
  from bep have B: "b/3 > 0" and C: "(1 - b)/3 > 0" by simp_all
  from landau_o.smallD[OF A B] show "eventually (λx. hb / ln x powr (1+e) < b/2) at_top"
    by eventually_elim (insert bep, simp)
  from landau_o.smallD[OF A C] show "eventually (λx. hb / ln x powr (1 + e) < (1 - b)/2) at_top"
    by eventually_elim (insert bep, simp)

  from bep have "(λx. hb / ln x powr (1 + e))  o(λ_. 1)" "(1 - b) / 2 > 0" by simp_all
  from landau_o.smallD[OF this] eventually_gt_at_top[of "1::real"]
    have A: "eventually (λx. 1 - b - hb / ln x powr (1 + e) > 0) at_top"
    by eventually_elim (insert bep, simp add: field_simps)
  from bep have "(λx. x * (1 - b - hb / ln x powr (1+e)))  ω(λ_. 1)" "(0::real) < 2" by simp_all
  from landau_omega.smallD[OF this] A eventually_gt_at_top[of "0::real"]
    show "eventually (λx. x*(1 - b - hb / ln x powr (1 + e)) > 1) at_top"
    by eventually_elim (simp_all add: abs_mult)
qed

end
end


definition "akra_bazzi_asymptotic1 b hb e p x 
  (1 - hb * inverse b * ln x powr -(1+e)) powr p * (1 + ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
   1 + (ln x powr (-e/2) :: real)"
definition "akra_bazzi_asymptotic1' b hb e p x 
  (1 + hb * inverse b * ln x powr -(1+e)) powr p * (1 + ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
   1 + (ln x powr (-e/2) :: real)"
definition "akra_bazzi_asymptotic2 b hb e p x 
  (1 + hb * inverse b * ln x powr -(1+e)) powr p * (1 - ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
       1 - ln x powr (-e/2 :: real)"
definition "akra_bazzi_asymptotic2' b hb e p x 
  (1 - hb * inverse b * ln x powr -(1+e)) powr p * (1 - ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
       1 - ln x powr (-e/2 :: real)"
definition "akra_bazzi_asymptotic3 e x  (1 + (ln x powr (-e/2))) / 2  (1::real)"
definition "akra_bazzi_asymptotic4 e x  (1 - (ln x powr (-e/2))) * 2  (1::real)"
definition "akra_bazzi_asymptotic5 b hb e x 
  ln (b*x - hb*x*ln x powr -(1+e)) powr (-e/2::real) < 1"

definition "akra_bazzi_asymptotic6 b hb e x  hb / ln x powr (1 + e :: real) < b/2"
definition "akra_bazzi_asymptotic7 b hb e x  hb / ln x powr (1 + e :: real) < (1 - b) / 2"
definition "akra_bazzi_asymptotic8 b hb e x  x*(1 - b - hb / ln x powr (1 + e :: real)) > 1"

definition "akra_bazzi_asymptotics b hb e p x 
  akra_bazzi_asymptotic1 b hb e p x  akra_bazzi_asymptotic1' b hb e p x 
  akra_bazzi_asymptotic2 b hb e p x  akra_bazzi_asymptotic2' b hb e p x 
  akra_bazzi_asymptotic3 e x  akra_bazzi_asymptotic4 e x  akra_bazzi_asymptotic5 b hb e x 
  akra_bazzi_asymptotic6 b hb e x  akra_bazzi_asymptotic7 b hb e x 
  akra_bazzi_asymptotic8 b hb e x"

lemmas akra_bazzi_asymptotic_defs =
  akra_bazzi_asymptotic1_def akra_bazzi_asymptotic1'_def
  akra_bazzi_asymptotic2_def akra_bazzi_asymptotic2'_def akra_bazzi_asymptotic3_def
  akra_bazzi_asymptotic4_def akra_bazzi_asymptotic5_def akra_bazzi_asymptotic6_def
  akra_bazzi_asymptotic7_def akra_bazzi_asymptotic8_def akra_bazzi_asymptotics_def

lemma akra_bazzi_asymptotics:
  assumes "b. b  set bs  b  {0<..<1}"
  assumes "hb > 0" "e > 0"
  shows "eventually (λx. bset bs. akra_bazzi_asymptotics b hb e p x) at_top"
proof (intro eventually_ball_finite ballI)
  fix b assume "b  set bs"
  with assms interpret akra_bazzi_asymptotics_bep b e p hb by unfold_locales auto
  show "eventually (λx. akra_bazzi_asymptotics b hb e p x) at_top"
    unfolding akra_bazzi_asymptotic_defs
    using asymptotics1[of "-c" for c] asymptotics2[of "-c" for c]
    by (intro eventually_conj asymptotics1 asymptotics2 asymptotics3
              asymptotics4 asymptotics5 asymptotics6 asymptotics7 asymptotics8) simp_all
qed simp

end