Theory Akra_Bazzi.Master_Theorem

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

  The Master theorem in a generalised form as derived from the Akra-Bazzi theorem.
*)
section ‹The Master theorem›
theory Master_Theorem
imports
  "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
  Akra_Bazzi_Library
  Akra_Bazzi
begin

lemma fundamental_theorem_of_calculus_real:
  "a  b  x{a..b}. (f has_real_derivative f' x) (at x within {a..b}) 
      (f' has_integral (f b - f a)) {a..b}"
  by (intro fundamental_theorem_of_calculus ballI)
     (simp_all add: has_real_derivative_iff_has_vector_derivative[symmetric])

lemma integral_powr:
  "y  -1  a  b  a > 0  integral {a..b} (λx. x powr y :: real) =
     inverse (y + 1) * (b powr (y + 1) - a powr (y + 1))"
  by (subst right_diff_distrib, intro integral_unique fundamental_theorem_of_calculus_real)
     (auto intro!: derivative_eq_intros)

lemma integral_ln_powr_over_x:
  "y  -1  a  b  a > 1  integral {a..b} (λx. ln x powr y / x :: real) =
     inverse (y + 1) * (ln b powr (y + 1) - ln a powr (y + 1))"
  by (subst right_diff_distrib, intro integral_unique fundamental_theorem_of_calculus_real)
     (auto intro!: derivative_eq_intros)

lemma integral_one_over_x_ln_x:
  "a  b  a > 1  integral {a..b} (λx. inverse (x * ln x) :: real) = ln (ln b) - ln (ln a)"
  by (intro integral_unique fundamental_theorem_of_calculus_real)
     (auto intro!: derivative_eq_intros simp: field_simps)

lemma akra_bazzi_integral_kurzweil_henstock:
  "akra_bazzi_integral (λf a b. f integrable_on {a..b}) (λf a b. integral {a..b} f)"
apply unfold_locales
apply (rule integrable_const_ivl)
apply simp
apply (erule integrable_subinterval_real, simp)
apply (blast intro!: integral_le)
apply (rule integral_combine, simp_all) []
done


locale master_theorem_function = akra_bazzi_recursion +
  fixes g :: "nat  real"
  assumes f_nonneg_base: "x  x0  x < x1  f x  0"
  and     f_rec:         "x  x1  f x = g x + (i<k. as!i * f ((ts!i) x))"
  and     g_nonneg:      "x  x1  g x  0"
  and     ex_pos_a:      "aset as. a > 0"
begin

interpretation akra_bazzi_integral "λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f"
  by (rule akra_bazzi_integral_kurzweil_henstock)

sublocale akra_bazzi_function x0 x1 k as bs ts f "λf a b. f integrable_on {a..b}"
            "λf a b. integral {a..b} f" g
  using f_nonneg_base f_rec g_nonneg ex_pos_a by unfold_locales

context
begin

private lemma g_nonneg': "eventually (λx. g x  0) at_top"
  using g_nonneg by (force simp: eventually_at_top_linorder)

private lemma g_pos:
  assumes "g  Ω(h)"
  assumes "eventually (λx. h x > 0) at_top"
  shows   "eventually (λx. g x > 0) at_top"
proof-
  from landau_omega.bigE_nonneg_real[OF assms(1) g_nonneg'] guess c . note c = this
  from assms(2) c(2) show ?thesis
    by eventually_elim (rule less_le_trans[OF mult_pos_pos[OF c(1)]], simp_all)
qed

private lemma f_pos:
  assumes "g  Ω(h)"
  assumes "eventually (λx. h x > 0) at_top"
  shows   "eventually (λx. f x > 0) at_top"
  using g_pos[OF assms(1,2)] eventually_ge_at_top[of x1]
  by (eventually_elim) (subst f_rec, insert step_ge_x0,
         auto intro!: add_pos_nonneg sum_nonneg mult_nonneg_nonneg[OF a_ge_0] f_nonneg)

lemma bs_lower_bound: "C>0. bset bs. C < b"
proof (intro exI conjI ballI)
  from b_pos show A: "Min (set bs) / 2 > 0" by auto
  fix b assume b: "b  set bs"
  from A have "Min (set bs) / 2 < Min (set bs)" by simp
  also from b have "...  b" by simp
  finally show "Min (set bs) / 2 < b" .
qed

private lemma powr_growth2:
  "C c2. 0 < c2  C < Min (set bs) 
      eventually (λx. u{C * x..x}. c2 * x powr p'  u powr p') at_top"
proof (intro exI conjI allI ballI)
  define C where "C = Min (set bs) / 2"
  from b_bounds bs_nonempty have C_pos: "C > 0" unfolding C_def by auto
  thus "C < Min (set bs)" unfolding C_def by simp
  show "max (C powr p') 1 > 0" by simp
  show "eventually (λx. u{C * x..x}.
    max ((Min (set bs)/2) powr p') 1 * x powr p'  u powr p') at_top"
    using eventually_gt_at_top[of "0::real"] apply eventually_elim
  proof clarify
    fix x u assume x: "x > 0" and "u  {C*x..x}"
    hence u: "u  C*x" "u  x" unfolding C_def by  simp_all
    from u have "u powr p'  max ((C*x) powr p') (x powr p')" using C_pos x
      by (intro powr_upper_bound mult_pos_pos) simp_all
    also from u x C_pos have "max ((C*x) powr p') (x powr p') = x powr p' * max (C powr p') 1"
      by (subst max_mult_left) (simp_all add: powr_mult algebra_simps)
    finally show "u powr p'  max ((Min (set bs)/2) powr p') 1 * x powr p'"
      by (simp add: C_def algebra_simps)
  qed
qed

private lemma powr_growth1:
  "C c1. 0 < c1  C < Min (set bs) 
      eventually (λx. u{C * x..x}. c1 * x powr p'  u powr p') at_top"
proof (intro exI conjI allI ballI)
  define C where "C = Min (set bs) / 2"
  from b_bounds bs_nonempty have C_pos: "C > 0" unfolding C_def by auto
  thus "C < Min (set bs)" unfolding C_def by simp
  from C_pos show "min (C powr p') 1 > 0" by simp
  show "eventually (λx. u{C * x..x}.
          min ((Min (set bs)/2) powr p') 1 * x powr p'  u powr p') at_top"
    using eventually_gt_at_top[of "0::real"] apply eventually_elim
  proof clarify
    fix x u assume x: "x > 0" and "u  {C*x..x}"
    hence u: "u  C*x" "u  x" unfolding C_def by  simp_all
    from u x C_pos have "x powr p' * min (C powr p') 1 = min ((C*x) powr p') (x powr p')"
      by (subst min_mult_left) (simp_all add: powr_mult algebra_simps)
    also from u have "u powr p'  min ((C*x) powr p') (x powr p')" using C_pos x
      by (intro powr_lower_bound mult_pos_pos) simp_all
    finally show "u powr p'  min ((Min (set bs)/2) powr p') 1 * x powr p'"
      by (simp add: C_def algebra_simps)
  qed
qed

private lemma powr_ln_powr_lower_bound:
  "a > 1  a  x  x  b 
     min (a powr p) (b powr p) * min (ln a powr p') (ln b powr p')  x powr p * ln x powr p'"
  by (intro mult_mono powr_lower_bound) (auto intro: min.coboundedI1)

private lemma powr_ln_powr_upper_bound:
  "a > 1  a  x  x  b 
     max (a powr p) (b powr p) * max (ln a powr p') (ln b powr p')  x powr p * ln x powr p'"
  by (intro mult_mono powr_upper_bound) (auto intro: max.coboundedI1)

private lemma powr_ln_powr_upper_bound':
  "eventually (λa. b>a. c. x{a..b}. x powr p * ln x powr p'  c) at_top"
  by (subst eventually_at_top_dense) (force intro: powr_ln_powr_upper_bound)

private lemma powr_upper_bound':
  "eventually (λa::real. b>a. c. x{a..b}. x powr p'  c) at_top"
  by (subst eventually_at_top_dense) (force intro: powr_upper_bound)

lemmas bounds =
  powr_ln_powr_lower_bound powr_ln_powr_upper_bound powr_ln_powr_upper_bound' powr_upper_bound'


private lemma eventually_ln_const:
  assumes "(C::real) > 0"
  shows   "eventually (λx. ln (C*x) / ln x > 1/2) at_top"
proof-
  from tendstoD[OF tendsto_ln_over_ln[of C 1], of "1/2"] assms
    have "eventually (λx. ¦ln (C*x) / ln x - 1¦ < 1/2) at_top" by (simp add: dist_real_def)
  thus ?thesis by eventually_elim linarith
qed

private lemma powr_ln_powr_growth1: "C c1. 0 < c1  C < Min (set bs) 
  eventually (λx. u{C * x..x}. c1 * (x powr r * ln x powr r')  u powr r * ln u powr r') at_top"
proof (intro exI conjI)
  let ?C = "Min (set bs) / 2" and ?f = "λx. x powr r * ln x powr r'"
  define C where "C = ?C"
  from b_bounds have C_pos: "C > 0" unfolding C_def by simp
  let ?T = "min (C powr r) (1 powr r) * min ((1/2) powr r') (1 powr r')"
  from C_pos show "?T > 0" unfolding min_def by (auto split: if_split)
  from bs_nonempty b_bounds have C_pos: "C > 0" unfolding C_def by simp
  thus "C < Min (set bs)" by (simp add: C_def)

  show "eventually (λx. u{C*x..x}. ?T * ?f x  ?f u) at_top"
    using eventually_gt_at_top[of "max 1 (inverse C)"] eventually_ln_const[OF C_pos]
    apply eventually_elim
  proof clarify
    fix x u assume x: "x > max 1 (inverse C)" and u: "u  {C*x..x}"
    hence x': "x > 1" by (simp add: field_simps)
    with C_pos have x_pos: "x > 0" by (simp add: field_simps)
    from x u C_pos have u': "u > 1" by (simp add: field_simps)
    assume A: "ln (C*x) / ln x > 1/2"
    have "min (C powr r) (1 powr r)  (u/x) powr r"
      using x u u' C_pos by (intro powr_lower_bound) (simp_all add: field_simps)
    moreover {
      note A
      also from C_pos x' u u' have "ln (C*x)  ln u" by (subst ln_le_cancel_iff) simp_all
      with x' have "ln (C*x) / ln x  ln u / ln x" by (simp add: field_simps)
      finally have "min ((1/2) powr r') (1 powr r')  (ln u / ln x) powr r'"
        using x u u' C_pos A by (intro powr_lower_bound) simp_all
    }
    ultimately have "?T  (u/x) powr r * (ln u / ln x) powr r'"
      using x_pos by (intro mult_mono) simp_all
    also from x u u' have "... = ?f u / ?f x" by (simp add: powr_divide)
    finally show "?T * ?f x  ?f u" using x' by (simp add: field_simps)
  qed
qed

private lemma powr_ln_powr_growth2: "C c1. 0 < c1  C < Min (set bs) 
  eventually (λx. u{C * x..x}. c1 * (x powr r * ln x powr r')  u powr r * ln u powr r') at_top"
proof (intro exI conjI)
  let ?C = "Min (set bs) / 2" and ?f = "λx. x powr r * ln x powr r'"
  define C where "C = ?C"
  let ?T = "max (C powr r) (1 powr r) * max ((1/2) powr r') (1 powr r')"
  show "?T > 0" by simp
  from b_bounds bs_nonempty have C_pos: "C > 0" unfolding C_def by simp
  thus "C < Min (set bs)" by (simp add: C_def)

  show "eventually (λx. u{C*x..x}. ?T * ?f x  ?f u) at_top"
    using eventually_gt_at_top[of "max 1 (inverse C)"] eventually_ln_const[OF C_pos]
    apply eventually_elim
  proof clarify
    fix x u assume x: "x > max 1 (inverse C)" and u: "u  {C*x..x}"
    hence x': "x > 1" by (simp add: field_simps)
    with C_pos have x_pos: "x > 0" by (simp add: field_simps)
    from x u C_pos have u': "u > 1" by (simp add: field_simps)
    assume A: "ln (C*x) / ln x > 1/2"
    from x u u' have "?f u / ?f x = (u/x) powr r * (ln u/ln x) powr r'" by (simp add: powr_divide)
    also {
      have "(u/x) powr r  max (C powr r) (1 powr r)"
        using x u u' C_pos by (intro powr_upper_bound) (simp_all add: field_simps)
      moreover {
        note A
        also from C_pos x' u u' have "ln (C*x)  ln u" by (subst ln_le_cancel_iff) simp_all
        with x' have "ln (C*x) / ln x  ln u / ln x" by (simp add: field_simps)
        finally have "(ln u / ln x) powr r'  max ((1/2) powr r') (1 powr r')"
          using x u u' C_pos A by (intro powr_upper_bound) simp_all
      } ultimately have "(u/x) powr r * (ln u / ln x) powr r'  ?T"
        using x_pos by (intro mult_mono) simp_all
    }
    finally show "?T * ?f x  ?f u" using x' by (simp add: field_simps)
  qed
qed

lemmas growths = powr_growth1 powr_growth2 powr_ln_powr_growth1 powr_ln_powr_growth2


private lemma master_integrable:
  "a::real. ba. (λu. u powr r * ln u powr s / u powr t) integrable_on {a..b}"
  "a::real. ba. (λu. u powr r / u powr s) integrable_on {a..b}"
  by (rule exI[of _ 2], force intro!: integrable_continuous_real continuous_intros)+

private lemma master_integral:
  fixes a p p' :: real
  assumes p: "p  p'" and a: "a > 0"
  obtains c d where "c  0" "p > p'  d  0"
    "(λx::nat. x powr p * (1 + integral {a..x} (λu. u powr p' / u powr (p+1)))) 
             Θ(λx::nat. d * x powr p + c * x powr p')"
proof-
  define e where "e = a powr (p' - p)"
  from assms have e: "e  0" by (simp add: e_def)
  define c where "c = inverse (p' - p)"
  define d where "d = 1 - inverse (p' - p) * e"
  have "c  0" and "p > p'  d  0"
    using e p a unfolding c_def d_def by (auto simp: field_simps)
  thus ?thesis
    apply (rule that) apply (rule bigtheta_real_nat_transfer, rule bigthetaI_cong)
    using eventually_ge_at_top[of a]
  proof eventually_elim
    fix x assume x: "x  a"
    hence "integral {a..x} (λu. u powr p' / u powr (p+1)) =
               integral {a..x} (λu. u powr (p' - (p + 1)))"
      by (intro Henstock_Kurzweil_Integration.integral_cong) (simp_all add: powr_diff [symmetric] )
    also have "... = inverse (p' - p) * (x powr (p' - p) - a powr (p' - p))"
      using p x0_less_x1 a x by (simp add: integral_powr)
    also have "x powr p * (1 + ...) = d * x powr p + c * x powr p'"
      using p unfolding c_def d_def by (simp add: algebra_simps powr_diff e_def)
    finally show "x powr p * (1 + integral {a..x} (λu. u powr p' / u powr (p+1))) =
                      d * x powr p + c * x powr p'" .
  qed
qed

private lemma master_integral':
  fixes a p p' :: real
  assumes p': "p'  0" and a: "a > 1"
  obtains c d :: real where "p' < 0  c  0" "d  0"
    "(λx::nat. x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr (p'-1) / u powr (p+1)))) 
       Θ(λx::nat. c * x powr p + d * x powr p * ln x powr p')"
proof-
  define e where "e = ln a powr p'"
  from assms have e: "e > 0" by (simp add: e_def)
  define c where "c = 1 - inverse p' * e"
  define d where "d = inverse p'"
  from assms e have "p' < 0  c  0" "d  0" unfolding c_def d_def by (auto simp: field_simps)
  thus ?thesis
    apply (rule that) apply (rule landau_real_nat_transfer, rule bigthetaI_cong)
    using eventually_ge_at_top[of a]
  proof eventually_elim
    fix x :: real assume x: "x  a"
    have "integral {a..x} (λu. u powr p * ln u powr (p' - 1) / u powr (p + 1)) =
          integral {a..x} (λu. ln u powr (p' - 1) / u)" using x a x0_less_x1
      by (intro Henstock_Kurzweil_Integration.integral_cong) (simp_all add: powr_add)
    also have "... = inverse p' * (ln x powr p' - ln a powr p')"
      using p' x0_less_x1 a(1) x by (simp add: integral_ln_powr_over_x)
    also have "x powr p * (1 + ...) = c * x powr p + d * x powr p * ln x powr p'"
      using p' by (simp add: algebra_simps c_def d_def e_def)
    finally show "x powr p * (1+integral {a..x} (λu. u powr p * ln u powr (p'-1) / u powr (p+1))) =
                  c * x powr p + d * x powr p * ln x powr p'" .
  qed
qed

private lemma master_integral'':
  fixes a p p' :: real
  assumes a: "a > 1"
  shows "(λx::nat. x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr - 1/u powr (p+1)))) 
           Θ(λx::nat. x powr p * ln (ln x))"
proof (rule landau_real_nat_transfer)
  have "(λx::real. x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr - 1/u powr (p+1)))) 
          Θ(λx::real. (1 - ln (ln a)) * x powr p + x powr p * ln (ln x))" (is "?f  _")
    apply (rule bigthetaI_cong) using eventually_ge_at_top[of a]
  proof eventually_elim
    fix x assume x: "x  a"
    have "integral {a..x} (λu. u powr p * ln u powr -1 / u powr (p + 1)) =
          integral {a..x} (λu. inverse (u * ln u))" using x a x0_less_x1
      by (intro Henstock_Kurzweil_Integration.integral_cong) (simp_all add: powr_add powr_minus field_simps)
    also have "... = ln (ln x) - ln (ln a)"
      using x0_less_x1 a(1) x by (subst integral_one_over_x_ln_x) simp_all
    also have "x powr p * (1 + ...) = (1 - ln (ln a)) * x powr p + x powr p * ln (ln x)"
      by (simp add: algebra_simps)
    finally show "x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr - 1 / u powr (p+1))) =
                    (1 - ln (ln a)) * x powr p + x powr p * ln (ln x)" .
  qed
  also have "(λx. (1 - ln (ln a)) * x powr p + x powr p * ln (ln x)) 
                Θ(λx. x powr p * ln (ln x))" by simp
  finally show "?f  Θ(λa. a powr p * ln (ln a))" .
qed



lemma master1_bigo:
  assumes g_bigo: "g  O(λx. real x powr p')"
  assumes less_p': "(i<k. as!i * bs!i powr p') > 1"
  shows "f  O(λx. real x powr p)"
proof-
  interpret akra_bazzi_upper x0 x1 k as bs ts f
    "λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p'"
    using assms growths g_bigo master_integrable by unfold_locales (assumption | simp)+
  from less_p' have less_p: "p' < p" by (rule p_greaterI)
  from bigo_f[of "0"] guess a . note a = this
  note a(2)
  also from a(1) less_p x0_less_x1 have "p  p'" by simp_all
  from master_integral[OF this a(1)] guess c d . note cd = this
  note cd(3)
  also from cd(1,2) less_p
    have "(λx::nat. d * real x powr p + c * real x powr p')  Θ(λx. real x powr p)" by force
  finally show "f  O(λx::nat. x powr p)" .
qed


lemma master1:
  assumes g_bigo: "g  O(λx. real x powr p')"
  assumes less_p': "(i<k. as!i * bs!i powr p') > 1"
  assumes f_pos:  "eventually (λx. f x > 0) at_top"
  shows "f  Θ(λx. real x powr p)"
proof (rule bigthetaI)
  interpret akra_bazzi_lower x0 x1 k as bs ts f
    "λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λ_. 0"
    using assms(1,3) bs_lower_bound by unfold_locales (auto intro: always_eventually)
  from bigomega_f show "f  Ω(λx. real x powr p)" by force
qed (fact master1_bigo[OF g_bigo less_p'])

lemma master2_3:
  assumes g_bigtheta: "g  Θ(λx. real x powr p * ln (real x) powr (p' - 1))"
  assumes p': "p' > 0"
  shows "f  Θ(λx. real x powr p * ln (real x) powr p')"
proof-
  have "eventually (λx::real. x powr p * ln x powr (p' - 1) > 0) at_top"
    using eventually_gt_at_top[of "1::real"] by eventually_elim simp
  hence "eventually (λx. f x > 0) at_top"
    by (rule f_pos[OF bigthetaD2[OF g_bigtheta] eventually_nat_real])
  then interpret akra_bazzi x0 x1 k as bs ts f
    "λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p * ln x powr (p' - 1)"
    using assms growths bounds master_integrable by unfold_locales (assumption | simp)+
  from bigtheta_f[of "1"] guess a . note a = this
  note a(2)
  also from a(1) p' have "p'  0" by simp_all
  from master_integral'[OF this a(1), of p] guess c d . note cd = this
  note cd(3)
  also have "(λx::nat. c * real x powr p + d * real x powr p * ln (real x) powr p') 
                 Θ(λx::nat. x powr p * ln x powr p')" using cd(1,2) p' by force
  finally show "f  Θ(λx. real x powr p * ln (real x) powr p')" .
qed

lemma master2_1:
  assumes g_bigtheta: "g  Θ(λx. real x powr p * ln (real x) powr p')"
  assumes p': "p' < -1"
  shows "f  Θ(λx. real x powr p)"
proof-
  have "eventually (λx::real. x powr p * ln x powr p' > 0) at_top"
    using eventually_gt_at_top[of "1::real"] by eventually_elim simp
  hence "eventually (λx. f x > 0) at_top"
    by (rule f_pos[OF bigthetaD2[OF g_bigtheta] eventually_nat_real])
  then interpret akra_bazzi x0 x1 k as bs ts f
    "λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p * ln x powr p'"
    using assms growths bounds master_integrable by unfold_locales (assumption | simp)+
  from bigtheta_f[of "1"] guess a . note a = this
  note a(2)
  also from a(1) p' have A: "p' + 1  0" by simp_all
  obtain c d :: real where cd: "c  0" "d  0" and
    "(λx::nat. x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr p'/ u powr (p+1)))) 
       Θ(λx::nat. c * x powr p + d * x powr p * ln x powr (p' + 1))"
    by (rule master_integral'[OF A a(1), of p]) (insert p', simp)
  note this(3)
  also have "(λx::nat. c * real x powr p + d * real x powr p * ln (real x) powr (p' + 1)) 
                 Θ(λx::nat. x powr p)" using cd(1,2) p' by force
  finally show "f  Θ(λx::nat. x powr p)" .
qed

lemma master2_2:
  assumes g_bigtheta: "g  Θ(λx. real x powr p / ln (real x))"
  shows "f  Θ(λx. real x powr p * ln (ln (real x)))"
proof-
  have "eventually (λx::real. x powr p / ln x > 0) at_top"
    using eventually_gt_at_top[of "1::real"] by eventually_elim simp
  hence "eventually (λx. f x > 0) at_top"
    by (rule f_pos[OF bigthetaD2[OF g_bigtheta] eventually_nat_real])
  moreover from g_bigtheta have g_bigtheta': "g  Θ(λx. real x powr p * ln (real x) powr -1)"
    by (rule landau_theta.trans, intro landau_real_nat_transfer) simp
  ultimately interpret akra_bazzi x0 x1 k as bs ts f
    "λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p * ln x powr -1"
    using assms growths bounds master_integrable by unfold_locales (assumption | simp)+
  from bigtheta_f[of 1] guess a . note a = this
  note a(2)
  also note master_integral''[OF a(1)]
  finally show "f  Θ(λx::nat. x powr p * ln (ln x))" .
qed

lemma master3:
  assumes g_bigtheta: "g  Θ(λx. real x powr p')"
  assumes p'_greater': "(i<k. as!i * bs!i powr p') < 1"
  shows "f  Θ(λx. real x powr p')"
proof-
  have "eventually (λx::real. x powr p' > 0) at_top"
    using eventually_gt_at_top[of "1::real"] by eventually_elim simp
  hence "eventually (λx. f x > 0) at_top"
    by (rule f_pos[OF bigthetaD2[OF g_bigtheta] eventually_nat_real])
  then interpret akra_bazzi x0 x1 k as bs ts f
    "λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p'"
    using assms growths bounds master_integrable by unfold_locales (assumption | simp)+
  from p'_greater' have p'_greater: "p' > p" by (rule p_lessI)
  from bigtheta_f[of 0] guess a . note a = this
  note a(2)
  also from p'_greater have "p  p'" by simp
  from master_integral[OF this a(1)] guess c d . note cd = this
  note cd(3)
  also have "(λx::nat. d * x powr p + c * x powr p')  Θ(λx::real. x powr p')"
    using p'_greater cd(1,2) by force
  finally show "f  Θ(λx. real x powr p')" .
qed

end
end

end