Theory Akra_Bazzi.Akra_Bazzi

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

  The Akra-Bazzi theorem for functions on the naturals.
*)

section ‹The discrete Akra-Bazzi theorem›
theory Akra_Bazzi
imports
  Complex_Main
  "HOL-Library.Landau_Symbols"
  Akra_Bazzi_Real
begin

lemma ex_mono: "(x. P x)  (x. P x  Q x)  (x. Q x)" by blast

lemma x_over_ln_mono:
  assumes "(e::real) > 0"
  assumes "x > exp e"
  assumes "x  y"
  shows   "x / ln x powr e  y / ln y powr e"
proof (rule DERIV_nonneg_imp_mono[of _ _ "λx. x / ln x powr e"])
  fix t assume t: "t  {x..y}"
  from assms(1) have "1 < exp e" by simp
  from this and assms(2) have "x > 1" by (rule less_trans)
  with t have t': "t > 1" by simp
  from x > exp e and t have "t > exp e" by simp
  with t' have "ln t > ln (exp e)" by (subst ln_less_cancel_iff) simp_all
  hence t'': "ln t > e" by simp
  show "((λx. x / ln x powr e) has_real_derivative 
            (ln t - e) / ln t powr (e+1)) (at t)" using assms t t' t''
    by (force intro!: derivative_eq_intros simp: powr_diff field_simps powr_add)
  from t'' show "(ln t - e) / ln t powr (e + 1)  0" by (intro divide_nonneg_nonneg) simp_all
qed (simp_all add: assms)


definition akra_bazzi_term :: "nat  nat  real  (nat  nat)  bool" where
  "akra_bazzi_term x0 x1 b t = 
    (e h. e > 0  (λx. h x)  O(λx. real x / ln (real x) powr (1+e)) 
               (xx1. t x  x0  t x < x  b*x + h x = real (t x)))"

lemma akra_bazzi_termI [intro?]:
  assumes "e > 0" "(λx. h x)  O(λx. real x / ln (real x) powr (1+e))"
          "x. x  x1  t x  x0" "x. x  x1  t x < x"
          "x. x  x1  b*x + h x = real (t x)"
  shows "akra_bazzi_term x0 x1 b t"
  using assms unfolding akra_bazzi_term_def by blast

lemma akra_bazzi_term_imp_less:
  assumes "akra_bazzi_term x0 x1 b t" "x  x1"
  shows   "t x < x"
  using assms unfolding akra_bazzi_term_def by blast

lemma akra_bazzi_term_imp_less':
  assumes "akra_bazzi_term x0 (Suc x1) b t" "x > x1"
  shows   "t x < x"
  using assms unfolding akra_bazzi_term_def by force


locale akra_bazzi_recursion =
  fixes x0 x1 k :: nat and as bs :: "real list" and ts :: "(nat  nat) list" and  f :: "nat  real"  
  assumes k_not_0:   "k  0"
  and     length_as: "length as = k"
  and     length_bs: "length bs = k"
  and     length_ts: "length ts = k"
  and     a_ge_0:    "a  set as  a  0"
  and     b_bounds:  "b  set bs  b  {0<..<1}"
  and     ts:        "i < length bs  akra_bazzi_term x0 x1 (bs!i) (ts!i)"
begin

sublocale akra_bazzi_params k as bs
  using length_as length_bs k_not_0 a_ge_0 b_bounds by unfold_locales

lemma ts_nonempty: "ts  []" using length_ts k_not_0 by (cases ts) simp_all

definition e_hs :: "real × (nat  real) list" where
  "e_hs = (SOME (e,hs). 
     e > 0  length hs = k  (hset hs. (λx. h x)  O(λx. real x / ln (real x) powr (1+e))) 
     (tset ts. xx1. t x  x0  t x < x)  
     (i<k. xx1. (bs!i)*x + (hs!i) x = real ((ts!i) x))
   )"

definition "e = (case e_hs of (e,_)  e)"
definition "hs = (case e_hs of (_,hs)  hs)"

lemma filterlim_powr_zero_cong: 
  "filterlim (λx. P (x::real) (x powr (0::real))) F at_top = filterlim (λx. P x 1) F at_top"
  apply (rule filterlim_cong[OF refl refl])
  using eventually_gt_at_top[of "0::real"] by eventually_elim simp_all
  

lemma e_hs_aux:
  "0 < e  length hs = k 
  (hset hs. (λx. h x)  O(λx. real x / ln (real x) powr (1 + e))) 
  (tset ts. xx1. x0  t x  t x < x)  
  (i<k. xx1. (bs!i)*x + (hs!i) x = real ((ts!i) x))"
proof-
  have "Ex (λ(e,hs). e > 0  length hs = k  
    (hset hs. (λx. h x)  O(λx. real x / ln (real x) powr (1+e))) 
    (tset ts. xx1. t x  x0  t x < x)  
    (i<k. xx1. (bs!i)*x + (hs!i) x = real ((ts!i) x)))"
  proof-
    from ts have A: "i{..<k}. akra_bazzi_term x0 x1 (bs!i) (ts!i)" by (auto simp: length_bs)
    hence "e h. (i<k. e i > 0  
             (λx. h i x)  O(λx. real x / ln (real x) powr (1+e i)) 
             (xx1. (ts!i) x  x0  (ts!i) x < x)  
             (i<k. xx1. (bs!i)*real x + h i x = real ((ts!i) x)))"
             unfolding akra_bazzi_term_def
      by (subst (asm) bchoice_iff, subst (asm) bchoice_iff) blast
    then guess ee :: "_  real" and hh :: "_  nat  real" 
      by (elim exE conjE) note eh = this
    define e where "e = Min {ee i |i. i < k}"
    define hs where "hs = map hh (upt 0 k)"
    have e_pos: "e > 0" unfolding e_def using eh k_not_0 by (subst Min_gr_iff) auto
    moreover have "length hs = k" unfolding hs_def by (simp_all add: length_ts)
    moreover have hs_growth: "hset hs. (λx. h x)  O(λx. real x / ln (real x) powr (1+e))"
    proof
      fix h assume "h  set hs"
      then obtain i where t: "i < k" "h = hh i" unfolding hs_def by force
      hence "(λx. h x)  O(λx. real x / ln (real x) powr (1+ee i))" using eh by blast
      also from t k_not_0 have "e  ee i" unfolding e_def by (subst Min_le_iff) auto
      hence "(λx::nat. real x / ln (real x) powr (1+ee i))  O(λx. real x / ln (real x) powr (1+e))"
        by (intro bigo_real_nat_transfer) auto
      finally show "(λx. h x)  O(λx. real x / ln (real x) powr (1+e))" .
    qed
    moreover have "tset ts. (xx1. t x  x0  t x < x)"
    proof (rule ballI)
      fix t assume "t  set ts"
      then obtain i where "i < k" "t = ts!i" using length_ts by (subst (asm) in_set_conv_nth) auto
      with eh show "xx1. t x  x0  t x < x" unfolding hs_def by force
    qed
    moreover have "i<k. xx1. (bs!i)*x + (hs!i) x = real ((ts!i) x)"
    proof (rule allI, rule impI)
      fix i assume i: "i < k"
      with eh show "xx1. (bs!i)*x + (hs!i) x = real ((ts!i) x)"
        using length_ts unfolding hs_def by fastforce
    qed
    ultimately show ?thesis by blast
  qed
  from someI_ex[OF this, folded e_hs_def] show ?thesis
    unfolding e_def hs_def by (intro conjI) fastforce+
qed

lemma
  e_pos: "e > 0" and length_hs: "length hs = k" and 
  hs_growth:  "h. h  set hs  (λx. h x)  O(λx. real x / ln (real x) powr (1 + e))" and
  step_ge_x0: "t x. t  set ts  x  x1  x0  t x" and
  step_less:  "t x. t  set ts  x  x1  t x < x" and
  decomp:     "i x. i < k  x  x1  (bs!i)*x + (hs!i) x = real ((ts!i) x)"
by (insert e_hs_aux) simp_all

lemma h_in_hs [intro, simp]: "i < k  hs ! i  set hs"
  by (rule nth_mem) (simp add: length_hs)

lemma t_in_ts [intro, simp]: "i < k  ts ! i  set ts"
  by (rule nth_mem) (simp add: length_ts)

lemma x0_less_x1: "x0 < x1" and x0_le_x1: "x0  x1"
proof-
  from ts_nonempty have "x0  hd ts x1" using step_ge_x0[of "hd ts" x1] by simp
  also from ts_nonempty have "... < x1" by (intro step_less) simp_all
  finally show "x0 < x1" by simp
  thus "x0  x1" by simp
qed

lemma akra_bazzi_induct [consumes 1, case_names base rec]:
  assumes "x  x0"
  assumes base: "x. x  x0  x < x1  P x"
  assumes rec:  "x. x  x1  (t. t  set ts  P (t x))  P x"
  shows   "P x"
proof (insert assms(1), induction x rule: less_induct)
  case (less x)
  with assms step_less step_ge_x0 show "P x" by (cases "x < x1") auto
qed

end

locale akra_bazzi_function = akra_bazzi_recursion +
  fixes integrable integral 
  assumes integral: "akra_bazzi_integral integrable integral"
  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

lemma ex_pos_a': "i<k. as!i > 0"
  using ex_pos_a by (auto simp: in_set_conv_nth length_as)

sublocale akra_bazzi_params_nonzero
  using length_as length_bs ex_pos_a a_ge_0 b_bounds by unfold_locales


definition g_real :: "real  real" where "g_real x = g (nat x)"

lemma g_real_real[simp]: "g_real (real x) = g x" unfolding g_real_def by simp

lemma f_nonneg: "x  x0  f x  0"
proof (induction x rule: akra_bazzi_induct)
  case (base x)
  with f_nonneg_base show "f x  0" by simp
next
  case (rec x)
  from rec.hyps have "g x  0" by (intro g_nonneg) simp
  moreover have "(i<k. as!i*f ((ts!i) x))  0" using rec.hyps length_ts length_as
    by (intro sum_nonneg ballI mult_nonneg_nonneg[OF a_ge_0 rec.IH]) simp_all
  ultimately show "f x  0" using rec.hyps by (simp add: f_rec)
qed  

definition "hs' = map (λh x. h (nat x::real)) hs"

lemma length_hs': "length hs' = k" unfolding hs'_def by (simp add: length_hs)

lemma hs'_real: "i < k  (hs'!i) (real x) = (hs!i) x"
  unfolding hs'_def by (simp add: length_hs)

lemma h_bound:
  obtains hb where "hb > 0" and
      "eventually (λx. hset hs'. ¦h x¦  hb * x / ln x powr (1 + e)) at_top"
proof-
  have "hset hs. c>0. eventually (λx. ¦h x¦  c * real x / ln (real x) powr (1 + e)) at_top"
  proof
    fix h assume h: "h  set hs"
    hence "(λx. h x)  O(λx. real x / ln (real x) powr (1 + e))" by (rule hs_growth)
    thus "c>0. eventually (λx. ¦h x¦  c * x / ln x powr (1 + e)) at_top"
     unfolding bigo_def by auto
  qed
  from bchoice[OF this] obtain hb where hb:
      "hset hs. hb h > 0  eventually (λx. ¦h x¦  hb h * real x / ln (real x) powr (1 + e)) at_top" by blast
  define hb' where "hb' = max 1 (Max {hb h |h. h  set hs})"
  have "hb' > 0" unfolding hb'_def by simp
  moreover have "hset hs. eventually (λx. ¦h (nat x)¦  hb' * x / ln x powr (1 + e)) at_top"
  proof (intro ballI, rule eventually_mp[OF always_eventually eventually_conj], clarify)
    fix h assume h: "h  set hs"
    with hb have hb_pos: "hb h > 0" by auto
    
    show "eventually (λx. x > exp (1 + e) + 1) at_top" by (rule eventually_gt_at_top)
    from h hb have e: "eventually (λx. ¦h (nat x :: real)¦  
        hb h * real (nat x) / ln (real (nat x)) powr (1 + e)) at_top" 
      by (intro eventually_natfloor) blast
    show "eventually (λx. ¦h (nat x :: real)¦  hb' * x / ln x powr (1 + e)) at_top"
      using e eventually_gt_at_top
    proof eventually_elim      
      fix x :: real assume x: "x > exp (1 + e) + 1"
 
      have x': "x > 0" by (rule le_less_trans[OF _ x]) simp_all
      assume "¦h (nat x)¦  hb h*real (nat x)/ln (real (nat x)) powr (1 + e)"
      also {
        from x have "exp (1 + e) < real (nat x)" by linarith
        moreover have "x > 0" by (rule le_less_trans[OF _ x]) simp_all
        hence "real (nat x)  x" by simp
        ultimately have "real (nat x)/ln (real (nat x)) powr (1+e)  x/ln x powr (1+e)"
          using e_pos by (intro x_over_ln_mono) simp_all
        from hb_pos mult_left_mono[OF this, of "hb h"]
          have "hb h * real (nat x)/ln (real (nat x)) powr (1+e)  hb h * x / ln x powr (1+e)"
          by (simp add: algebra_simps)
      }
      also from h have "hb h  hb'"
        unfolding hb'_def f_rec by (intro order.trans[OF Max.coboundedI max.cobounded2]) auto
      with x' have "hb h*x/ln x powr (1+e)  hb'*x/ln x powr (1+e)"
        by (intro mult_right_mono divide_right_mono) simp_all
      finally show "¦h (nat x)¦  hb' * x / ln x powr (1 + e)" .
    qed
  qed
  hence "hset hs'. eventually (λx. ¦h x¦  hb' * x / ln x powr (1 + e)) at_top"
    by (auto simp: hs'_def)
  hence "eventually (λx. hset hs'. ¦h x¦  hb' * x / ln x powr (1 + e)) at_top"
    by (intro eventually_ball_finite) simp_all
  ultimately show ?thesis by (rule that)
qed

lemma C_bound:
  assumes "b. b  set bs  C < b" "hb > 0"
  shows   "eventually (λx::real. bset bs. C*x  b*x - hb*x/ln x powr (1+e)) at_top"
proof-
  from e_pos have "((λx. hb * ln x powr -(1+e))  0) at_top"
    by (intro tendsto_mult_right_zero tendsto_neg_powr ln_at_top) simp_all
  with assms have "bset bs. eventually (λx. ¦hb * ln x powr -(1+e)¦ < b - C) at_top"
    by (force simp: tendsto_iff dist_real_def)
  hence "eventually (λx. bset bs. ¦hb * ln x powr -(1+e)¦ < b - C) at_top"
    by (intro eventually_ball_finite) simp_all
  note A = eventually_conj[OF this eventually_gt_at_top]
  show ?thesis using A apply eventually_elim
  proof clarify
    fix x b :: real assume x: "x > 0" and b: "b  set bs"
    assume A: "bset bs. ¦hb * ln x powr -(1+e)¦ < b - C"
    from b A assms have "hb * ln x powr -(1+e) < b - C" by simp
    with x have "x * (hb * ln x powr -(1+e)) < x * (b - C)" by (intro mult_strict_left_mono)
    thus "C*x  b*x - hb*x / ln x powr (1+e)"
      by (subst (asm) powr_minus) (simp_all add: field_simps)
  qed
qed

end



locale akra_bazzi_lower = akra_bazzi_function +
  fixes   g' :: "real  real"
  assumes f_pos:      "eventually (λx. f x > 0) at_top"
  and     g_growth2:  "C c2. c2 > 0  C < Min (set bs)  
                           eventually (λx. u{C*x..x}. g' u  c2 * g' x) at_top"
  and     g'_integrable:  "a. ba. integrable (λu. g' u / u powr (p + 1)) a b"
  and     g'_bounded:  "eventually (λa::real. (b>a. c. x{a..b}. g' x  c)) at_top"
  and     g_bigomega: "g  Ω(λx. g' (real x))"
  and     g'_nonneg:  "eventually (λx. g' x  0) at_top"
begin

definition "gc2  SOME gc2. gc2 > 0  eventually (λx. g x  gc2 * g' (real x)) at_top"

lemma gc2: "gc2 > 0" "eventually (λx. g x  gc2 * g' (real x)) at_top"
proof-
  from g_bigomega guess c by (elim landau_omega.bigE) note c = this
  from g'_nonneg have "eventually (λx::nat. g' (real x)  0) at_top" by (rule eventually_nat_real)
  with c(2) have "eventually (λx. g x  c * g' (real x)) at_top" 
    using eventually_ge_at_top[of x1] by eventually_elim (insert g_nonneg, simp_all)
  with c(1) have "gc2. gc2 > 0  eventually (λx. g x  gc2 * g' (real x)) at_top" by blast
  from someI_ex[OF this] show "gc2 > 0" "eventually (λx. g x  gc2 * g' (real x)) at_top"
    unfolding gc2_def by blast+
qed

definition "gx0  max x1 (SOME gx0. xgx0. g x  gc2 * g' (real x)  f x > 0  g' (real x)  0)"
definition "gx1  max gx0 (SOME gx1. xgx1. i<k. (ts!i) x  gx0)"

lemma gx0:
  assumes "x  gx0"
  shows   "g x  gc2 * g' (real x)" "f x > 0" "g' (real x)  0"
proof-
  from eventually_conj[OF gc2(2) eventually_conj[OF f_pos eventually_nat_real[OF g'_nonneg]]]
    have "gx0. xgx0. g x  gc2 * g' (real x)  f x > 0  g' (real x)  0" 
    by (simp add: eventually_at_top_linorder)
  note someI_ex[OF this]
  moreover have "x  (SOME gx0. xgx0. g x  gc2 * g' (real x) f x > 0  g' (real x)  0)"
    using assms unfolding gx0_def by simp
  ultimately show "g x  gc2 * g' (real x)" "f x > 0" "g' (real x)  0" unfolding gx0_def by blast+
qed

lemma gx1:
  assumes "x  gx1" "i < k"
  shows  "(ts!i) x  gx0"
proof-
  define mb where "mb = Min (set bs)/2"
  from b_bounds bs_nonempty have mb_pos: "mb > 0" unfolding mb_def by simp
  from h_bound guess hb . note hb = this
  from e_pos have "((λx. hb * ln x powr -(1 + e))  0) at_top"
    by (intro tendsto_mult_right_zero tendsto_neg_powr ln_at_top) simp_all
  moreover note mb_pos
  ultimately have "eventually (λx. hb * ln x powr -(1 + e) < mb) at_top" using hb(1)
    by (subst (asm) tendsto_iff) (simp_all add: dist_real_def)

  from eventually_nat_real[OF hb(2)] eventually_nat_real[OF this]
       eventually_ge_at_top eventually_ge_at_top
  have "eventually (λx. i<k. (ts!i) x  gx0) at_top" apply eventually_elim
  proof clarify
    fix i x :: nat assume A: "hb * ln (real x) powr -(1+e) < mb" and i: "i < k"
    assume B: "hset hs'. ¦h (real x)¦  hb * real x / ln (real x) powr (1+e)"
    with i have B': "¦(hs'!i) (real x)¦  hb * real x / ln (real x) powr (1+e)"
      using length_hs'[symmetric] by auto
    assume C: "x  nat gx0/mb"
    hence C': "real gx0/mb  real x" by linarith
    assume D: "x  x1"
      
    from mb_pos have "real gx0 = mb * (real gx0/mb)" by simp
    also from i bs_nonempty have "mb  bs!i/2" unfolding mb_def by simp
    hence "mb * (real gx0/mb)  bs!i/2 * x" 
      using C' i b_bounds[of "bs!i"] mb_pos by (intro mult_mono) simp_all
    also have "... = bs!i*x + -bs!i/2 * x" by simp
    also {
      have "-(hs!i) x  ¦(hs!i) x¦" by simp
      also from i B' length_hs have "¦(hs!i) x¦  hb * real x / ln (real x) powr (1+e)" 
        by (simp add: hs'_def)
      also from A have "hb / ln x powr (1+e)  mb" 
        by (subst (asm) powr_minus) (simp add: field_simps)
      hence "hb / ln x powr (1+e) * x  mb * x" by (intro mult_right_mono) simp_all
      hence "hb * x / ln x powr (1+e)  mb * x" by simp
      also from i have "...  (bs!i/2) * x" unfolding mb_def by (intro mult_right_mono) simp_all
      finally have "-bs!i/2 * x  (hs!i) x" by simp
    }
    also have "bs!i*real x + (hs!i) x = real ((ts!i) x)" using i D decomp by simp
    finally show "(ts!i) x  gx0" by simp
  qed
  hence "gx1. xgx1. i<k. gx0  (ts!i) x" (is "Ex ?P")
    by (simp add: eventually_at_top_linorder)
  from someI_ex[OF this] have "?P (SOME x. ?P x)" .
  moreover have "x. x  gx1  x  (SOME x. ?P x)" unfolding gx1_def by simp
  ultimately have "?P gx1" by blast
  with assms show ?thesis by blast
qed

lemma gx0_ge_x1: "gx0  x1" unfolding gx0_def by simp
lemma gx0_le_gx1: "gx0  gx1" unfolding gx1_def by simp

function f2' :: "nat  real" where
  "x < gx1  f2' x = max 0 (f x / gc2)"
| "x  gx1  f2' x = g' (real x) + (i<k. as!i*f2' ((ts!i) x))"
using le_less_linear by (blast, simp_all)
termination by (relation "Wellfounded.measure (λx. x)") 
               (insert gx0_le_gx1 gx0_ge_x1, simp_all add: step_less)

lemma f2'_nonneg: "x  gx0  f2' x  0"
by (induction x rule: f2'.induct)
   (auto intro!: add_nonneg_nonneg sum_nonneg gx0 gx1  mult_nonneg_nonneg[OF a_ge_0])
               
lemma f2'_le_f: "x  x0  gc2 * f2' x  f x"
proof (induction rule: f2'.induct)
  case (1 x)
  with gc2 f_nonneg show ?case by (simp add: max_def field_simps)
next
  case prems: (2 x)
  with gx0 gx0_le_gx1 have "gc2 * g' (real x)  g x" by force
  moreover from step_ge_x0 prems(1) gx0_ge_x1 gx0_le_gx1
    have "i. i < k  x0  (ts!i) x" by simp
  hence "i. i < k  as!i * (gc2 * f2' ((ts!i) x))  as!i * f ((ts!i) x)"
    using prems(1) by (intro mult_left_mono a_ge_0 prems(2)) auto
  hence "gc2 * (i<k. as!i*f2' ((ts!i) x))  (i<k. as!i*f ((ts!i) x))"
    by (subst sum_distrib_left, intro sum_mono) (simp_all add: algebra_simps)
  ultimately show ?case using prems(1) gx0_ge_x1 gx0_le_gx1
    by (simp_all add: algebra_simps f_rec)
qed

lemma f2'_pos: "eventually (λx. f2' x > 0) at_top"
proof (subst eventually_at_top_linorder, intro exI allI impI)
  fix x :: nat assume "x  gx0"
  thus "f2' x > 0"
  proof (induction x rule: f2'.induct)
    case (1 x)
    with gc2 gx0(2)[of x] show ?case by (simp add: max_def field_simps)
  next
    case prems: (2 x)
    have "(i<k. as!i*f2' ((ts!i) x)) > 0"
    proof (rule sum_pos')
      from ex_pos_a' guess i by (elim exE conjE) note i = this
      with prems(1) gx0 gx1 have "as!i * f2' ((ts!i) x) > 0"
        by (intro mult_pos_pos prems(2)) simp_all
      with i show "i{..<k}. as!i * f2' ((ts!i) x) > 0" by blast
    next
      fix i assume i: "i  {..<k}"
      with prems(1) have "f2' ((ts!i) x) > 0" by (intro prems(2) gx1) simp_all
      with i show "as!i * f2' ((ts!i) x)  0" by (intro mult_nonneg_nonneg[OF a_ge_0]) simp_all
    qed simp_all
    with prems(1) gx0_le_gx1 show ?case by (auto intro!: add_nonneg_pos gx0)
  qed
qed


lemma bigomega_f_aux: 
  obtains a where "a  A" "a'a. a'    
    f  Ω(λx. x powr p *(1 + integral (λu. g' u / u powr (p + 1)) a' x))"
proof-
  from g'_integrable guess a0 by (elim exE) note a0 = this
  from h_bound guess hb . note hb = this
  moreover from g_growth2 guess C c2 by (elim conjE exE) note C = this
  hence "eventually (λx. bset bs. C*x  b*x - hb*x/ln x powr (1 + e)) at_top"
    using hb(1) bs_nonempty by (intro C_bound) simp_all
  moreover from b_bounds hb(1) e_pos 
    have "eventually (λx. bset bs. akra_bazzi_asymptotics b hb e p x) at_top"
    by (rule akra_bazzi_asymptotics)
  moreover note g'_bounded C(3) g'_nonneg eventually_natfloor[OF f2'_pos] eventually_natfloor[OF gc2(2)]
  ultimately have "eventually (λx. (hset hs'. ¦h x¦  hb*x/ln x powr (1+e)) 
                     (bset bs. C*x  b*x - hb*x/ln x powr (1+e)) 
                     (bset bs. akra_bazzi_asymptotics b hb e p x) 
                     (b>x. c. x{x..b}. g' x  c)  f2' (nat x) > 0  
                     (u{C * x..x}. g' u  c2 * g' x) 
                     g' x  0) at_top"
    by (intro eventually_conj) (force elim!: eventually_conjE)+
  then have "X. (xX. (hset hs'. ¦h x¦  hb*x/ln x powr (1+e)) 
                        (bset bs. C*x  b*x - hb*x/ln x powr (1+e)) 
                        (bset bs. akra_bazzi_asymptotics b hb e p x) 
                        (b>x. c. x{x..b}. g' x  c)  
                        (u{C * x..x}. g' u  c2 * g' x) 
                        f2' (nat x) > 0  g' x  0)"
    by (subst (asm) eventually_at_top_linorder) (erule ex_mono, blast)
  then guess X by (elim exE conjE) note X = this

  define x0'_min where "x0'_min = max A (max X (max a0 (max gx1 (max 1 (real x1 + 1)))))"
  {
  fix x0' :: real assume x0'_props: "x0'  x0'_min" "x0'  "
  hence x0'_ge_x1: "x0'  real (x1+1)" and x0'_ge_1: "x0'  1" and x0'_ge_X: "x0'  X" 
    unfolding x0'_min_def by linarith+
  hence x0'_pos: "x0' > 0" and  x0'_nonneg: "x0'  0" by simp_all
  have x0': "xx0'. (hset hs'. ¦h x¦  hb*x/ln x powr (1+e))"
            "xx0'. (bset bs. C*x  b*x - hb*x/ln x powr (1+e))"
            "xx0'. (bset bs. akra_bazzi_asymptotics b hb e p x)"
            "ax0'. b>a. c. x{a..b}. g' x  c"
            "xx0'. u{C * x..x}. g' u  c2 * g' x"
            "xx0'. f2' (nat x) > 0" "xx0'. g' x  0"
    using X x0'_ge_X by auto
  from x0'_props(2) have x0'_int: "real (nat x0') = x0'" by (rule real_natfloor_nat)
  from x0'_props have x0'_ge_gx1: "x0'  gx1" and x0'_ge_a0: "x0'  a0" 
    unfolding x0'_min_def by simp_all
  with gx0_le_gx1 have f2'_nonneg: "x. x  x0'  f2' x  0" by (force intro!: f2'_nonneg)
           
  define bm where "bm = Min (set bs)"
  define x1' where "x1' = 2 * x0' * inverse bm"
  define fb2 where "fb2 = Min {f2' x |x. x  {x0'..x1'}}"
  define gb2 where "gb2 = (SOME c. x{x0'..x1'}. g' x  c)"
  
  from b_bounds bs_nonempty have "bm > 0" "bm < 1" unfolding bm_def by auto
  hence "1 < 2 * inverse bm" by (simp add: field_simps)
  from mult_strict_left_mono[OF this x0'_pos] 
    have x0'_lt_x1': "x0' < x1'" and x0'_le_x1': "x0'  x1'" unfolding x1'_def by simp_all 
    
  from x0_le_x1 x0'_ge_x1 have ge_x0'D: "x. x0'  real x  x0  x" by simp
  from x0'_ge_x1 x0'_le_x1' have gt_x1'D: "x. x1' < real x  x1  x" by simp
  
  have x0'_x1': "bset bs. 2 * x0' * inverse b  x1'"
  proof
    fix b assume b: "b  set bs"
    hence "bm  b" by (simp add: bm_def)
    moreover from b bs_nonempty b_bounds have "bm > 0" "b > 0" unfolding bm_def by auto
    ultimately have "inverse b  inverse bm" by simp
    with x0'_nonneg show "2 * x0' * inverse b  x1'" 
      unfolding x1'_def by (intro mult_left_mono) simp_all
  qed
  
  note f_nonneg' = f_nonneg
  have "x. real x  x0'  x  nat x0'" "x. real x  x1'  x  nat x1'" by linarith+  
  hence "{x |x. real x  {x0'..x1'}}  {x |x. x  {nat x0'..nat x1'}}" by auto
  hence "finite {x |x::nat. real x  {x0'..x1'}}" by (rule finite_subset) auto
  hence fin: "finite {f2' x |x::nat. real x  {x0'..x1'}}" by force

  note facts = hs'_real e_pos length_hs' length_as length_bs k_not_0 a_ge_0 p_props x0'_ge_1
               f2'_nonneg f_rec[OF gt_x1'D] x0' x0'_int x0'_x1' gc2(1) decomp
  from b_bounds x0'_le_x1' x0'_ge_gx1 gx0_le_gx1 x0'_ge_x1
    interpret abr: akra_bazzi_nat_to_real as bs hs' k x0' x1' hb e p f2' g'
    by (unfold_locales) (auto simp: facts simp del: f2'.simps intro!: f2'.simps(2))
  
  have f'_nat: "x::nat. abr.f' (real x) = f2' x"
  proof-
    fix x :: nat show "abr.f' (real (x::nat)) = f2' x"
    proof (induction "real x" arbitrary: x rule: abr.f'.induct)
      case (2 x)
      note x = this(1) and IH = this(2)
      from x have "abr.f' (real x) = g' (real x) + (i<k. as!i*abr.f' (bs!i*real x + (hs!i) x))"
        by (auto simp: gt_x1'D hs'_real g_real_def intro!: sum.cong)
      also have "(i<k. as!i*abr.f' (bs!i*real x + (hs!i) x)) = 
                 (i<k. as!i*f2' ((ts!i) x))"
      proof (rule sum.cong, simp, clarify)
        fix i assume i: "i < k"
        from i x x0'_le_x1' x0'_ge_x1 have *: "bs!i * real x + (hs!i) x = real ((ts!i) x)"
          by (intro decomp) simp_all
        also from i * have "abr.f' ... = f2' ((ts!i) x)"
          by (subst IH[of i]) (simp_all add: hs'_real)
        finally show "as!i*abr.f' (bs!i*real x+(hs!i) x) = as!i*f2' ((ts!i) x)" by simp
      qed
      also have "g' x + ... = f2' x" using x x0'_ge_gx1 x0'_le_x1' 
        by (intro f2'.simps(2)[symmetric] gt_x1'D) simp_all
      finally show ?case .
    qed simp
  qed
  interpret akra_bazzi_integral integrable integral by (rule integral) 
  interpret akra_bazzi_real_lower as bs hs' k x0' x1' hb e p 
      integrable integral abr.f' g' C fb2 gb2 c2
  proof unfold_locales
    fix x assume "x  x0'" "x  x1'"
    thus "abr.f' x  0" by (intro abr.f'_base) simp_all
  next
    fix x assume x:"x  x0'"
    show "integrable (λx. g' x / x powr (p + 1)) x0' x"
      by (rule integrable_subinterval[of _ a0 x]) (insert a0 x0'_ge_a0 x, auto)
  next
    fix x assume x: "x  x0'" "x  x1'"
    have "x0' = real (nat x0')" by (simp add: x0'_int)
    also from x have "...  real (nat x)" by (auto intro!: nat_mono floor_mono)
    finally have "x0'  real (nat x)" .
    moreover have "real (nat x)  x1'" using x x0'_ge_1 by linarith
    ultimately have "f2' (nat x)  {f2' x |x. real x  {x0'..x1'}}" by force
    from fin and this have "f2' (nat x)  fb2" unfolding fb2_def by (rule Min_le)
    with x show "abr.f' x  fb2" by simp
  next
    from x0'_int x0'_le_x1' have "x::nat. real x  x0'  real x  x1'" 
        by (intro exI[of _ "nat x0'"]) simp_all
    moreover {
      fix x :: nat assume "real x  x0'  real x  x1'"
      with x0'(6) have "f2' (nat real x) > 0" by blast
      hence "f2' x > 0" by simp
    }
    ultimately show "fb2 > 0" unfolding fb2_def using fin by (subst Min_gr_iff) auto 
  next
    fix x assume x: "x0'  x" "x  x1'"
    with x0'(4) x0'_lt_x1' have "c. x{x0'..x1'}. g' x  c" by force
    from someI_ex[OF this] x show "g' x  gb2" unfolding gb2_def by simp
  qed (insert g_nonneg integral x0'(2) C x0'_le_x1' x0'_ge_x1, simp_all add: facts)
  
  from akra_bazzi_lower guess c5 . note c5 = this
  have "eventually (λx. ¦f x¦  gc2 * c5 * ¦f_approx (real x)¦) at_top"
  proof (unfold eventually_at_top_linorder, intro exI allI impI)
    fix x :: nat assume "x  nat x0'"
    hence x: "real x  x0'" by linarith
    note c5(1)[OF x]
    also have "abr.f' (real x) = f2' x" by (rule f'_nat)
    also have "gc2 * ...  f x" using x x0'_ge_x1 x0_le_x1 by (intro f2'_le_f) simp_all
    also have "f x = ¦f x¦" using x f_nonneg' x0'_ge_x1 x0_le_x1 by simp
    finally show "gc2 * c5 * ¦f_approx (real x)¦  ¦f x¦" 
      using gc2 f_approx_nonneg[OF x] by (simp add: algebra_simps)
  qed
  hence "f  Ω(λx. f_approx (real x))" using gc2(1) f_nonneg' f_approx_nonneg
    by (intro landau_omega.bigI[of "gc2 * c5"] eventually_conj 
        mult_pos_pos c5 eventually_nat_real) (auto simp: eventually_at_top_linorder)
  note this[unfolded f_approx_def]
  }
  moreover have "x0'_min  A" unfolding x0'_min_def gx0_ge_x1 by simp
  ultimately show ?thesis by (intro that) auto
qed

lemma bigomega_f: 
  obtains a where "a  A" "f  Ω(λx. x powr p *(1 + integral (λu. g' u / u powr (p+1)) a x))"
proof-
  from bigomega_f_aux[of A] guess a . note a = this
  define a' where "a' = real (max (nat a) 0) + 1"
  note a
  moreover have "a'  " by (auto simp: max_def a'_def)
  moreover have *: "a'  a + 1" unfolding a'_def by linarith
  moreover from * and a have "a'  A" by simp
  ultimately show ?thesis by (intro that[of a']) auto
qed

end



locale akra_bazzi_upper = akra_bazzi_function +
  fixes   g' :: "real  real"
  assumes g'_integrable:  "a. ba. integrable (λu. g' u / u powr (p + 1)) a b"
  and     g_growth1: "C c1. c1 > 0  C < Min (set bs)  
                          eventually (λx. u{C*x..x}. g' u  c1 * g' x) at_top"
  and     g_bigo:    "g  O(g')"
  and     g'_nonneg: "eventually (λx. g' x  0) at_top"
begin


definition "gc1  SOME gc1. gc1 > 0  eventually (λx. g x  gc1 * g' (real x)) at_top"

lemma gc1: "gc1 > 0" "eventually (λx. g x  gc1 * g' (real x)) at_top"
proof-
  from g_bigo guess c by (elim landau_o.bigE) note c = this
  from g'_nonneg have "eventually (λx::nat. g' (real x)  0) at_top" by (rule eventually_nat_real)
  with c(2) have "eventually (λx. g x  c * g' (real x)) at_top" 
    using eventually_ge_at_top[of x1] by eventually_elim (insert g_nonneg, simp_all)
  with c(1) have "gc1. gc1 > 0  eventually (λx. g x  gc1 * g' (real x)) at_top" by blast
  from someI_ex[OF this] show "gc1 > 0" "eventually (λx. g x  gc1 * g' (real x)) at_top"
    unfolding gc1_def by blast+
qed

definition "gx3  max x1 (SOME gx0. xgx0. g x  gc1 * g' (real x))"

lemma gx3:
  assumes "x  gx3"
  shows   "g x  gc1 * g' (real x)"
proof-
  from gc1(2) have "gx3. xgx3. g x  gc1 * g' (real x)" by (simp add: eventually_at_top_linorder)
  note someI_ex[OF this]
  moreover have "x  (SOME gx0. xgx0. g x  gc1 * g' (real x))"
    using assms unfolding gx3_def by simp
  ultimately show "g x  gc1 * g' (real x)" unfolding gx3_def by blast
qed

lemma gx3_ge_x1: "gx3  x1" unfolding gx3_def by simp

function f' :: "nat  real" where
  "x < gx3  f' x = max 0 (f x / gc1)"
| "x  gx3  f' x = g' (real x) + (i<k. as!i*f' ((ts!i) x))"
using le_less_linear by (blast, simp_all)
termination by (relation "Wellfounded.measure (λx. x)") 
               (insert gx3_ge_x1, simp_all add: step_less)

lemma f'_ge_f: "x  x0  gc1 * f' x  f x"
proof (induction rule: f'.induct)
  case (1 x)
  with gc1 f_nonneg show ?case by (simp add: max_def field_simps)
next
  case prems: (2 x)
  with gx3 have "gc1 * g' (real x)  g x" by force
  moreover from step_ge_x0 prems(1) gx3_ge_x1
    have "i. i < k  x0  nat (ts!i) x" by (intro le_nat_floor) simp
  hence "i. i < k  as!i * (gc1 * f' ((ts!i) x))  as!i * f ((ts!i) x)"
    using prems(1) by (intro mult_left_mono a_ge_0 prems(2)) auto
  hence "gc1 * (i<k. as!i*f' ((ts!i) x))  (i<k. as!i*f ((ts!i) x))"
    by (subst sum_distrib_left, intro sum_mono) (simp_all add: algebra_simps)
  ultimately show ?case using prems(1) gx3_ge_x1
    by (simp_all add: algebra_simps f_rec)
qed

lemma bigo_f_aux:
  obtains a where "a  A" "a'a. a'    
    f  O(λx. x powr p *(1 + integral (λu. g' u / u powr (p + 1)) a' x))"
proof-
  from g'_integrable guess a0 by (elim exE) note a0 = this
  from h_bound guess hb . note hb = this
  moreover from g_growth1 guess C c1 by (elim conjE exE) note C = this
  hence "eventually (λx. bset bs. C*x  b*x - hb*x/ln x powr (1 + e)) at_top"
    using hb(1) bs_nonempty by (intro C_bound) simp_all
  moreover from b_bounds hb(1) e_pos 
    have "eventually (λx. bset bs. akra_bazzi_asymptotics b hb e p x) at_top"
    by (rule akra_bazzi_asymptotics)
  moreover note gc1(2) C(3) g'_nonneg
  ultimately have "eventually (λx. (hset hs'. ¦h x¦  hb*x/ln x powr (1+e)) 
                     (bset bs. C*x  b*x - hb*x/ln x powr (1+e)) 
                     (bset bs. akra_bazzi_asymptotics b hb e p x)  
                     (u{C*x..x}. g' u  c1 * g' x)  g' x  0) at_top"
    by (intro eventually_conj) (force elim!: eventually_conjE)+
  then have "X. (xX. (hset hs'. ¦h x¦  hb*x/ln x powr (1+e)) 
                        (bset bs. C*x  b*x - hb*x/ln x powr (1+e)) 
                        (bset bs. akra_bazzi_asymptotics b hb e p x)  
                        (u{C*x..x}. g' u  c1 * g' x)  g' x  0)"
    by (subst (asm) eventually_at_top_linorder) fast
  then guess X by (elim exE conjE) note X = this
  
  define x0'_min where "x0'_min = max A (max X (max 1 (max a0 (max gx3 (real x1 + 1)))))"
  {
  fix x0' :: real assume x0'_props: "x0'  x0'_min" "x0'  "
  hence x0'_ge_x1: "x0'  real (x1+1)" and x0'_ge_1: "x0'  1" and x0'_ge_X: "x0'  X" 
    unfolding x0'_min_def by linarith+
  hence x0'_pos: "x0' > 0" and  x0'_nonneg: "x0'  0" by simp_all
  have x0': "xx0'. (hset hs'. ¦h x¦  hb*x/ln x powr (1+e))"
            "xx0'. (bset bs. C*x  b*x - hb*x/ln x powr (1+e))"
            "xx0'. (bset bs. akra_bazzi_asymptotics b hb e p x)" 
            "xx0'. u{C*x..x}. g' u  c1 * g' x" "xx0'. g' x  0"
            using X x0'_ge_X by auto
  from x0'_props(2) have x0'_int: "real (nat x0') = x0'" by (rule real_natfloor_nat)
  from x0'_props have x0'_ge_gx0: "x0'  gx3" and x0'_ge_a0: "x0'  a0" 
    unfolding x0'_min_def by simp_all
  hence f'_nonneg: "x. x  x0'  f' x  0"
    using order.trans[OF f_nonneg f'_ge_f] gc1(1) x0'_ge_x1 x0_le_x1
    by (simp add: zero_le_mult_iff del: f'.simps)
  
  define bm where "bm = Min (set bs)"
  define x1' where "x1' = 2 * x0' * inverse bm"
  define fb1 where "fb1 = Max {f' x |x. x  {x0'..x1'}}"
  
from b_bounds bs_nonempty have "bm > 0" "bm < 1" unfolding bm_def by auto
  hence "1 < 2 * inverse bm" by (simp add: field_simps)
  from mult_strict_left_mono[OF this x0'_pos] 
    have x0'_lt_x1': "x0' < x1'" and x0'_le_x1': "x0'  x1'" unfolding x1'_def by simp_all 
    
  from x0_le_x1 x0'_ge_x1 have ge_x0'D: "x. x0'  real x  x0  x" by simp
  from x0'_ge_x1 x0'_le_x1' have gt_x1'D: "x. x1' < real x  x1  x" by simp
  
  have x0'_x1': "bset bs. 2 * x0' * inverse b  x1'"
  proof
    fix b assume b: "b  set bs"
    hence "bm  b" by (simp add: bm_def)
    moreover from b b_bounds bs_nonempty have "bm > 0" "b > 0" unfolding bm_def by auto
    ultimately have "inverse b  inverse bm" by simp
    with x0'_nonneg show "2 * x0' * inverse b  x1'" 
      unfolding x1'_def by (intro mult_left_mono) simp_all
  qed
  
  note f_nonneg' = f_nonneg
  have "x. real x  x0'  x  nat x0'" "x. real x  x1'  x  nat x1'" by linarith+  
  hence "{x |x. real x  {x0'..x1'}}  {x |x. x  {nat x0'..nat x1'}}" by auto
  hence "finite {x |x::nat. real x  {x0'..x1'}}" by (rule finite_subset) auto
  hence fin: "finite {f' x |x::nat. real x  {x0'..x1'}}" by force

  note facts = hs'_real e_pos length_hs' length_as length_bs k_not_0 a_ge_0 p_props x0'_ge_1
               f'_nonneg f_rec[OF gt_x1'D] x0' x0'_int x0'_x1' gc1(1) decomp
  from b_bounds x0'_le_x1' x0'_ge_gx0 x0'_ge_x1 
  interpret abr: akra_bazzi_nat_to_real as bs hs' k x0' x1' hb e p f' g'
    by (unfold_locales) (auto simp add: facts simp del: f'.simps intro!: f'.simps(2))
  
  have f'_nat: "x::nat. abr.f' (real x) = f' x"
  proof-
    fix x :: nat show "abr.f' (real (x::nat)) = f' x"
    proof (induction "real x" arbitrary: x rule: abr.f'.induct)
      case (2 x)
      note x = this(1) and IH = this(2)
      from x have "abr.f' (real x) = g' (real x) + (i<k. as!i*abr.f' (bs!i*real x + (hs!i) x))"
        by (auto simp: gt_x1'D hs'_real intro!: sum.cong)
      also have "(i<k. as!i*abr.f' (bs!i*real x + (hs!i) x)) = (i<k. as!i*f' ((ts!i) x))"
      proof (rule sum.cong, simp, clarify)
        fix i assume i: "i < k"
        from i x x0'_le_x1' x0'_ge_x1 have *: "bs!i * real x + (hs!i) x = real ((ts!i) x)"
          by (intro decomp) simp_all
        also from i * have "abr.f' ... = f' ((ts!i) x)"
          by (subst IH[of i]) (simp_all add: hs'_real)
        finally show "as!i*abr.f' (bs!i*real x+(hs!i) x) = as!i*f' ((ts!i) x)" by simp
      qed
      also from x have "g' x + ... = f' x" using x0'_le_x1' x0'_ge_gx0 by simp
      finally show ?case .
    qed simp
  qed
  
  interpret akra_bazzi_integral integrable integral by (rule integral)
  interpret akra_bazzi_real_upper as bs hs' k x0' x1' hb e p integrable integral abr.f' g' C fb1 c1
  proof (unfold_locales)
    fix x assume "x  x0'" "x  x1'"
    thus "abr.f' x  0" by (intro abr.f'_base) simp_all
  next
    fix x assume x:"x  x0'"
    show "integrable (λx. g' x / x powr (p + 1)) x0' x"
      by (rule integrable_subinterval[of _ a0 x]) (insert a0 x0'_ge_a0 x, auto)
  next
    fix x assume x: "x  x0'" "x  x1'"
    have "x0' = real (nat x0')" by (simp add: x0'_int)
    also from x have "...  real (nat x)" by (auto intro!: nat_mono floor_mono)
    finally have "x0'  real (nat x)" .
    moreover have "real (nat x)  x1'" using x x0'_ge_1 by linarith
    ultimately have "f' (nat x)  {f' x |x. real x  {x0'..x1'}}" by force
    from fin and this have "f' (nat x)  fb1" unfolding fb1_def by (rule Max_ge)
    with x show "abr.f' x  fb1" by simp
  qed (insert x0'(2) x0'_le_x1' x0'_ge_x1 C, simp_all add: facts)

  from akra_bazzi_upper guess c6 . note c6 = this
  { 
    fix x :: nat assume "x  nat x0'"
    hence x: "real x  x0'" by linarith
    have "f x  gc1 * f' x" using x x0'_ge_x1 x0_le_x1 by (intro f'_ge_f) simp_all
    also have "f' x = abr.f' (real x)" by (simp add: f'_nat)
    also note c6(1)[OF x]
    also from f_nonneg' x x0'_ge_x1 x0_le_x1 have "f x = ¦f x¦" by simp
    also from f_approx_nonneg x have "f_approx (real x) = ¦f_approx (real x)¦" by simp
    finally have "gc1 * c6 * ¦f_approx (real x)¦  ¦f x¦" using gc1 by (simp add: algebra_simps)
  }
  hence "eventually (λx. ¦f x¦  gc1 * c6 * ¦f_approx (real x)¦) at_top"
    using eventually_ge_at_top[of "nat x0'"] by (auto elim!: eventually_mono)
  hence "f  O(λx. f_approx (real x))" using gc1(1) f_nonneg' f_approx_nonneg
    by (intro landau_o.bigI[of "gc1 * c6"] eventually_conj 
        mult_pos_pos c6 eventually_nat_real) (auto simp: eventually_at_top_linorder)
  note this[unfolded f_approx_def]
  }
  moreover have "x0'_min  A" unfolding x0'_min_def gx3_ge_x1 by simp
  ultimately show ?thesis by (intro that) auto
qed

lemma bigo_f: 
  obtains a where "a > A" "f  O(λx. x powr p *(1 + integral (λu. g' u / u powr (p + 1)) a x))"
proof-
  from bigo_f_aux[of A] guess a . note a = this
  define a' where "a' = real (max (nat a) 0) + 1"
  note a
  moreover have "a'  " by (auto simp: max_def a'_def)
  moreover have *: "a'  a + 1" unfolding a'_def by linarith
  moreover from * and a have "a' > A" by simp
  ultimately show ?thesis by (intro that[of a']) auto
qed

end

locale akra_bazzi = akra_bazzi_function +
  fixes   g' :: "real  real"
  assumes f_pos:         "eventually (λx. f x > 0) at_top"
  and     g'_nonneg:     "eventually (λx. g' x  0) at_top"
  assumes g'_integrable:  "a. ba. integrable (λu. g' u / u powr (p + 1)) a b"
  and     g_growth1:  "C c1. c1 > 0  C < Min (set bs)  
                           eventually (λx. u{C*x..x}. g' u  c1 * g' x) at_top"
  and     g_growth2:  "C c2. c2 > 0  C < Min (set bs)  
                           eventually (λx. u{C*x..x}. g' u  c2 * g' x) at_top"
  and     g_bounded:  "eventually (λa::real. (b>a. c. x{a..b}. g' x  c)) at_top"
  and     g_bigtheta: "g  Θ(g')"
begin

sublocale akra_bazzi_lower using f_pos g_growth2 g_bounded 
  bigthetaD2[OF g_bigtheta] g'_nonneg g'_integrable by unfold_locales 
sublocale akra_bazzi_upper using g_growth1 bigthetaD1[OF g_bigtheta] 
  g'_nonneg g'_integrable by unfold_locales

lemma bigtheta_f: 
  obtains a where "a > A" "f  Θ(λx. x powr p *(1 + integral (λu. g' u / u powr (p + 1)) a x))"
proof-
  from bigo_f_aux[of A] guess a . note a = this
  moreover from bigomega_f_aux[of A] guess b . note b = this
  let ?a = "real (max (max (nat a) (nat b)) 0) + 1"
  have "?a  " by (auto simp: max_def)
  moreover have "?a  a" "?a  b" by linarith+
  ultimately have "f  Θ(λx. x powr p *(1 + integral (λu. g' u / u powr (p + 1)) ?a x))" 
    using a b by (intro bigthetaI) blast+
  moreover from a b have "?a > A" by linarith
  ultimately show ?thesis by (intro that[of ?a]) simp_all
qed

end


named_theorems akra_bazzi_term_intros "introduction rules for Akra-Bazzi terms"

lemma akra_bazzi_term_floor_add [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1 + c" "c < (1 - b) * real x1" "x1 > 0"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x + c)"
proof (rule akra_bazzi_termI[OF zero_less_one])
  fix x assume x: "x  x1"
  from assms x have "real x0  b * real x1 + c" by simp
  also from x assms have "...  b * real x + c" by auto
  finally have step_ge_x0: "b * real x + c  real x0" by simp
  thus "nat b * real x + c  x0" by (subst le_nat_iff) (simp_all add: le_floor_iff)

  from assms x have "c < (1 - b) * real x1" by simp
  also from assms x have "...  (1 - b) * real x" by (intro mult_left_mono) simp_all
  finally show "nat b * real x + c < x" using assms step_ge_x0 
    by (subst nat_less_iff) (simp_all add: floor_less_iff algebra_simps)
  
  from step_ge_x0 have "real_of_int c + b * real x = real_of_int (nat c + b * real x)" by linarith
  thus "(b * real x) + (b * real x + c - (b * real x)) = 
          real (nat b * real x + c)" by linarith
next
  have "(λx::nat. real_of_int b * real x + c - b * real x)  O(λ_. ¦c¦ + 1)"
    by (intro landau_o.big_mono always_eventually allI, unfold real_norm_def) linarith
  also have "(λ_::nat. ¦c¦ + 1)  O(λx. real x / ln (real x) powr (1 + 1))" by force
  finally show "(λx::nat. real_of_int b * real x + c - b * real x)  
                    O(λx. real x / ln (real x) powr (1+1))" .
qed

lemma akra_bazzi_term_floor_add' [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1 + real c" "real c < (1 - b) * real x1" "x1 > 0"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x + c)"
proof-
  from assms have "akra_bazzi_term x0 x1 b (λx. nat b*real x + real c)" 
    by (rule akra_bazzi_term_floor_add)
  also have "(λx. nat b*real x + real c) = (λx::nat. nat b*real x + c)"
  proof
    fix x :: nat 
    have "b * real x + real c = b * real x + int c" by linarith
    also from assms have "nat ... = nat b * real x + c" by (simp add: nat_add_distrib)
    finally show "nat b * real x + real c = nat b * real x + c" .
  qed
  finally show ?thesis .
qed

lemma akra_bazzi_term_floor_subtract [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1 - c" "0 < c + (1 - b) * real x1" "x1 > 0"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x - c)"
  by (subst diff_conv_add_uminus, rule akra_bazzi_term_floor_add, insert assms) simp_all

lemma akra_bazzi_term_floor_subtract' [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1 - real c" "0 < real c + (1 - b) * real x1" "x1 > 0"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x - c)"
proof-
  from assms have "akra_bazzi_term x0 x1 b (λx. nat b*real x - real c)" 
    by (intro akra_bazzi_term_floor_subtract) simp_all
  also have "(λx. nat b*real x - real c) = (λx::nat. nat b*real x - c)"
  proof
    fix x :: nat 
    have "b * real x - real c = b * real x - int c" by linarith
    also from assms have "nat ... = nat b * real x - c" by (simp add: nat_diff_distrib)
    finally show "nat b * real x - real c = nat b * real x - c" .
  qed
  finally show ?thesis .
qed


lemma akra_bazzi_term_floor [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1" "0 < (1 - b) * real x1" "x1 > 0"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x)"
  using assms akra_bazzi_term_floor_add[where c = 0] by simp



lemma akra_bazzi_term_ceiling_add [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1 + c" "c + 1  (1 - b) * x1"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x + c)"
proof (rule akra_bazzi_termI[OF zero_less_one])
  fix x assume x: "x  x1"
  have "0  real x0" by simp
  also from assms have "real x0  b * real x1 + c" by simp
  also from assms x have "b * real x1  b * real x" by (intro mult_left_mono) simp_all
  hence "b * real x1 + c  b * real x + c" by simp
  also have "b * real x + c  real_of_int b * real x + c" by linarith
  finally have bx_nonneg: "real_of_int b * real x + c  0" .
  
  have "c + 1  (1 - b) * x1" by fact
  also have "(1 - b) * x1  (1 - b) * x" using assms x by (intro mult_left_mono) simp_all
  finally have "b * real x + c + 1  real x" using assms by (simp add: algebra_simps)
  with bx_nonneg show "nat b * real x + c < x" by (subst nat_less_iff) (simp_all add: ceiling_less_iff)
  
  have "real x0  b * real x1 + c" by fact
  also have "...  real_of_int ..." by linarith
  also have "x1  x" by fact
  finally show "x0  nat b * real x + c" using assms by (force simp: ceiling_mono)
  
  show "b * real x + (b * real x + c - b * real x) = real (nat b * real x + c)"
    using assms bx_nonneg by simp
next
  have "(λx::nat. real_of_int b * real x + c - b * real x)  O(λ_. ¦c¦ + 1)"
    by (intro landau_o.big_mono always_eventually allI, unfold real_norm_def) linarith
  also have "(λ_::nat. ¦c¦ + 1)  O(λx. real x / ln (real x) powr (1 + 1))" by force
  finally show "(λx::nat. real_of_int b * real x + c - b * real x)  
                    O(λx. real x / ln (real x) powr (1+1))" .
qed

lemma akra_bazzi_term_ceiling_add' [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1 + real c" "real c + 1  (1 - b) * x1"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x + c)"
proof-
  from assms have "akra_bazzi_term x0 x1 b (λx. nat b*real x + real c)" 
    by (rule akra_bazzi_term_ceiling_add)
  also have "(λx. nat b*real x + real c) = (λx::nat. nat b*real x + c)"
  proof
    fix x :: nat 
    from assms have "0  b * real x" by simp
    also have "b * real x  real_of_int b * real x" by linarith
    finally have bx_nonneg: "b * real x  0" by simp

    have "b * real x + real c = b * real x + int c" by linarith
    also from assms bx_nonneg have "nat ... = nat b * real x + c" 
      by (subst nat_add_distrib) simp_all
    finally show "nat b * real x + real c = nat b * real x + c" .
  qed
  finally show ?thesis .
qed

lemma akra_bazzi_term_ceiling_subtract [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1 - c" "1  c + (1 - b) * x1"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x - c)"
  by (subst diff_conv_add_uminus, rule akra_bazzi_term_ceiling_add, insert assms) simp_all

lemma akra_bazzi_term_ceiling_subtract' [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1 - real c" "1  real c + (1 - b) * x1"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x - c)"
proof-
  from assms have "akra_bazzi_term x0 x1 b (λx. nat b*real x - real c)" 
    by (intro akra_bazzi_term_ceiling_subtract) simp_all
  also have "(λx. nat b*real x - real c) = (λx::nat. nat b*real x - c)"
  proof
    fix x :: nat 
    from assms have "0  b * real x" by simp
    also have "b * real x  real_of_int b * real x" by linarith
    finally have bx_nonneg: "b * real x  0" by simp

    have "b * real x - real c = b * real x - int c" by linarith
    also from assms bx_nonneg have "nat ... = nat b * real x - c" by simp
    finally show "nat b * real x - real c = nat b * real x - c" .
  qed
  finally show ?thesis .
qed

lemma akra_bazzi_term_ceiling [akra_bazzi_term_intros]:
  assumes "(b::real) > 0" "b < 1" "real x0  b * real x1" "1  (1 - b) * x1"
  shows   "akra_bazzi_term x0 x1 b (λx. nat b*real x)"
  using assms akra_bazzi_term_ceiling_add[where c = 0] by simp


end