Theory Akra_Bazzi.Akra_Bazzi_Real

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

  The continuous version of the Akra-Bazzi theorem for functions on the reals.
*)

section ‹The continuous Akra-Bazzi theorem›
theory Akra_Bazzi_Real
imports
  Complex_Main
  Akra_Bazzi_Asymptotics
begin

text ‹
  We want to be generic over the integral definition used; we fix some arbitrary
  notions of integrability and integral and assume just the properties we need.
  The user can then instantiate the theorems with any desired integral definition.
›
locale akra_bazzi_integral =
  fixes integrable :: "(real  real)  real  real  bool"
    and integral   :: "(real  real)  real  real  real"
  assumes integrable_const: "c  0  integrable (λ_. c) a b"
      and integral_const:   "c  0  a  b  integral (λ_. c) a b = (b - a) * c"
      and integrable_subinterval:
            "integrable f a b  a  a'  b'  b  integrable f a' b'"
      and integral_le:
            "integrable f a b  integrable g a b  (x. x  {a..b}  f x  g x) 
                 integral f a b  integral g a b"
      and integral_combine:
            "a  c  c  b  integrable f a b 
                 integral f a c + integral f c b = integral f a b"
begin
lemma integral_nonneg:
  "a  b  integrable f a b  (x. x  {a..b}  f x  0)  integral f a b  0"
  using integral_le[OF integrable_const[of 0], of f a b]  by (simp add: integral_const)
end


declare sum.cong[fundef_cong]

lemma strict_mono_imp_ex1_real:
  fixes f :: "real  real"
  assumes lim_neg_inf: "LIM x at_bot. f x :> at_top"
  assumes lim_inf: "(f  z) at_top"
  assumes mono: "a b. a < b  f b < f a"
  assumes cont: "x. isCont f x"
  assumes y_greater_z: "z < y"
  shows   "∃!x. f x = y"
proof (rule ex_ex1I)
  fix a b assume "f a = y" "f b = y"
  thus "a = b" by (cases rule: linorder_cases[of a b]) (auto dest: mono)
next
  from lim_neg_inf have "eventually (λx. y  f x) at_bot" by (subst (asm) filterlim_at_top) simp
  then obtain l where l: "x. x  l  y  f x" by (subst (asm) eventually_at_bot_linorder) auto

  from order_tendstoD(2)[OF lim_inf y_greater_z]
    obtain u where u: "x. x  u  f x < y" by (subst (asm) eventually_at_top_linorder) auto
  define a where "a = min l u"
  define b where "b = max l u"
  have a: "f a  y" unfolding a_def by (intro l) simp
  moreover have b: "f b < y" unfolding b_def by (intro u) simp
  moreover have a_le_b: "a  b" by (simp add: a_def b_def)
  ultimately have "xa. x  b  f x = y" using cont by (intro IVT2) auto
  thus "x. f x = y" by blast
qed

text ‹The parameter @{term "p"} in the Akra-Bazzi theorem always exists and is unique.›

definition akra_bazzi_exponent :: "real list  real list  real" where
  "akra_bazzi_exponent as bs  (THE p. (i<length as. as!i * bs!i powr p) = 1)"

locale akra_bazzi_params =
  fixes k :: nat and as bs :: "real list"
  assumes length_as: "length as = k"
  and     length_bs: "length bs = k"
  and     k_not_0:   "k  0"
  and     a_ge_0:    "a  set as  a  0"
  and     b_bounds:  "b  set bs  b  {0<..<1}"
begin

abbreviation p :: real where "p  akra_bazzi_exponent as bs"

lemma p_def: "p = (THE p. (i<k. as!i * bs!i powr p) = 1)"
  by (simp add: akra_bazzi_exponent_def length_as)

lemma b_pos: "b  set bs  b > 0" and b_less_1: "b  set bs  b < 1"
  using b_bounds by simp_all

lemma as_nonempty [simp]: "as  []" and bs_nonempty [simp]: "bs  []"
  using length_as length_bs k_not_0 by auto

lemma a_in_as[intro, simp]: "i < k  as ! i  set as"
  by (rule nth_mem) (simp add: length_as)

lemma b_in_bs[intro, simp]: "i < k  bs ! i  set bs"
  by (rule nth_mem) (simp add: length_bs)

end


locale akra_bazzi_params_nonzero =
  fixes k :: nat and as bs :: "real list"
  assumes length_as: "length as = k"
  and     length_bs: "length bs = k"
  and     a_ge_0:    "a  set as  a  0"
  and     ex_a_pos:  "aset as. a > 0"
  and     b_bounds:  "b  set bs  b  {0<..<1}"
begin

sublocale akra_bazzi_params k as bs
 by unfold_locales (insert length_as length_bs a_ge_0 ex_a_pos b_bounds, auto)

lemma akra_bazzi_p_strict_mono:
  assumes "x < y"
  shows "(i<k. as!i * bs!i powr y) < (i<k. as!i * bs!i powr x)"
proof (intro sum_strict_mono_ex1 ballI)
  from ex_a_pos obtain a where "a  set as" "a > 0" by blast
  then obtain i where "i < k" "as!i > 0" by (force simp: in_set_conv_nth length_as)
  with b_bounds x < y have "as!i * bs!i powr y < as!i * bs!i powr x"
    by (intro mult_strict_left_mono powr_less_mono') auto
  with i < k show "i{..<k}. as!i * bs!i powr y < as!i * bs!i powr x" by blast
next
  fix i assume "i  {..<k}"
  with a_ge_0 b_bounds[of "bs!i"] x < y show "as!i * bs!i powr y  as!i * bs!i powr x"
    by (intro mult_left_mono powr_mono') simp_all
qed simp_all

lemma akra_bazzi_p_mono:
  assumes "x  y"
  shows "(i<k. as!i * bs!i powr y)  (i<k. as!i * bs!i powr x)"
apply (cases "x < y")
using akra_bazzi_p_strict_mono[of x y] assms apply simp_all
done


lemma akra_bazzi_p_unique:
  "∃!p. (i<k. as!i * bs!i powr p) = 1"
proof (rule strict_mono_imp_ex1_real)
  from as_nonempty have [simp]: "k > 0" by (auto simp: length_as[symmetric])
  have [simp]: "i. i < k  as!i  0" by (rule a_ge_0) simp
  from ex_a_pos obtain a where "a  set as" "a > 0" by blast
  then obtain i where i: "i < k" "as!i > 0" by (force simp: in_set_conv_nth length_as)

  hence "LIM p at_bot. as!i * bs!i powr p :> at_top" using b_bounds i
    by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] real_powr_at_bot_neg) simp_all
  moreover have "p. as!i*bs!i powr p  (i{..<k}. as ! i * bs ! i powr p)"
  proof
    fix p :: real
    from a_ge_0 b_bounds have "(i{..<k}-{i}. as ! i * bs ! i powr p)  0"
      by (intro sum_nonneg mult_nonneg_nonneg) simp_all
    also have "as!i * bs!i powr p + ... = (iinsert i {..<k}. as ! i * bs ! i powr p)"
      by (simp add: sum.insert_remove)
    also from i have "insert i {..<k} = {..<k}" by blast
    finally show "as!i*bs!i powr p  (i{..<k}. as ! i * bs ! i powr p)" by simp
  qed
  ultimately show "LIM p at_bot. i<k. as ! i * bs ! i powr p :> at_top"
    by (rule filterlim_at_top_mono[OF _ always_eventually])
next
  from b_bounds show "((λx. i<k. as ! i * bs ! i powr x)  (i<k. 0)) at_top"
    by (intro tendsto_sum tendsto_mult_right_zero real_powr_at_top_neg) simp_all
next
  fix x
  from b_bounds have A: "i. i < k  bs ! i > 0" by simp
  show "isCont (λx. i<k. as ! i * bs ! i powr x) x"
    using b_bounds[OF nth_mem] by (intro continuous_intros) (auto dest: A)
qed (simp_all add: akra_bazzi_p_strict_mono)

lemma p_props:  "(i<k. as!i * bs!i powr p) = 1"
  and p_unique: "(i<k. as!i * bs!i powr p') = 1  p = p'"
proof-
  from theI'[OF akra_bazzi_p_unique] the1_equality[OF akra_bazzi_p_unique]
    show "(i<k. as!i * bs!i powr p) = 1" "(i<k. as!i * bs!i powr p') = 1  p = p'"
    unfolding p_def by - blast+
qed

lemma p_greaterI: "1 < (i<k. as!i * bs!i powr p')  p' < p"
  by (rule disjE[OF le_less_linear, of p p'], drule akra_bazzi_p_mono, subst (asm) p_props, simp_all)

lemma p_lessI: "1 > (i<k. as!i * bs!i powr p')  p' > p"
  by (rule disjE[OF le_less_linear, of p' p], drule akra_bazzi_p_mono, subst (asm) p_props, simp_all)

lemma p_geI: "1  (i<k. as!i * bs!i powr p')  p'  p"
  by (rule disjE[OF le_less_linear, of p' p], simp, drule akra_bazzi_p_strict_mono,
      subst (asm) p_props, simp_all)

lemma p_leI: "1  (i<k. as!i * bs!i powr p')  p'  p"
  by (rule disjE[OF le_less_linear, of p p'], simp, drule akra_bazzi_p_strict_mono,
      subst (asm) p_props, simp_all)

lemma p_boundsI: "(i<k. as!i * bs!i powr x)  1  (i<k. as!i * bs!i powr y)  1  p  {y..x}"
  by (elim conjE, drule p_leI, drule p_geI, simp)

lemma p_boundsI': "(i<k. as!i * bs!i powr x) < 1  (i<k. as!i * bs!i powr y) > 1  p  {y<..<x}"
  by (elim conjE, drule p_lessI, drule p_greaterI, simp)

lemma p_nonneg: "sum_list as  1  p  0"
proof (rule p_geI)
  assume "sum_list as  1"
  also have "... = (i<k. as!i)" by (simp add: sum_list_sum_nth length_as atLeast0LessThan)
  also {
    fix i assume "i < k"
    with b_bounds have "bs!i > 0" by simp
    hence "as!i * bs!i powr 0 = as!i" by simp
  }
  hence "(i<k. as!i) = (i<k. as!i * bs!i powr 0)" by (intro sum.cong) simp_all
  finally show "1  (i<k. as ! i * bs ! i powr 0)" .
qed

end


locale akra_bazzi_real_recursion =
  fixes as bs :: "real list" and hs :: "(real  real) list" and k :: nat and x0 x1 hb e p :: real
  assumes length_as: "length as = k"
  and     length_bs: "length bs = k"
  and     length_hs: "length hs = k"
  and     k_not_0:   "k  0"
  and     a_ge_0:    "a  set as  a  0"
  and     b_bounds:  "b  set bs  b  {0<..<1}"

  (* The recursively-defined function *)
  and     x0_ge_1:      "x0  1"
  and     x0_le_x1:     "x0  x1"
  and     x1_ge:        "b  set bs  x1  2 * x0 * inverse b"
  (* Bounds on the variation functions *)
  and     e_pos:        "e > 0"
  and     h_bounds:     "x  x1  h  set hs  ¦h x¦  hb * x / ln x powr (1 + e)"
  (* Asymptotic inequalities *)
  and     asymptotics:  "x  x0  b  set bs  akra_bazzi_asymptotics b hb e p x"
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 h_in_hs[intro, simp]: "i < k  hs ! i  set hs"
  by (rule nth_mem) (simp add: length_hs)

lemma x1_gt_1: "x1 > 1"
proof-
  from bs_nonempty obtain b where "b  set bs" by (cases bs) auto
  from b_pos[OF this] b_less_1[OF this] x0_ge_1 have "1 < 2 * x0 * inverse b"
    by (simp add: field_simps)
  also from x1_ge and b  set bs have "...  x1" by simp
  finally show ?thesis .
qed

lemma x1_ge_1: "x1  1" using x1_gt_1 by simp

lemma x1_pos: "x1 > 0" using x1_ge_1 by simp

lemma bx_le_x: "x  0  b  set bs   b * x  x"
  using b_pos[of b] b_less_1[of b] by (intro mult_left_le_one_le) (simp_all)

lemma x0_pos: "x0 > 0" using x0_ge_1 by simp

lemma
  assumes "x  x0" "b  set bs"
  shows x0_hb_bound0: "hb / ln x powr (1 + e) < b/2"
  and   x0_hb_bound1: "hb / ln x powr (1 + e) < (1 - b) / 2"
  and   x0_hb_bound2: "x*(1 - b - hb / ln x powr (1 + e)) > 1"
using asymptotics[OF assms] unfolding akra_bazzi_asymptotic_defs by blast+

lemma step_diff:
  assumes "i < k" "x  x1"
  shows   "bs ! i * x + (hs ! i) x + 1 < x"
proof-
  have "bs ! i * x + (hs ! i) x + 1  bs ! i * x + ¦(hs ! i) x¦ + 1" by simp
  also from assms have "¦(hs ! i) x¦  hb * x / ln x powr (1 + e)" by (simp add: h_bounds)
  also from assms x0_le_x1 have "x*(1 - bs ! i - hb / ln x powr (1 + e)) > 1"
    by (simp add: x0_hb_bound2)
  hence "bs ! i * x + hb * x / ln x powr (1 + e) + 1 < x" by (simp add: algebra_simps)
  finally show ?thesis by simp
qed

lemma step_le_x: "i < k  x  x1  bs ! i * x + (hs ! i) x  x"
  by (drule (1) step_diff) simp

lemma x0_hb_bound0': "x b. x  x0  b  set bs  hb / ln x powr (1 + e) < b"
  by (drule (1) x0_hb_bound0, erule less_le_trans) (simp add: b_pos)

lemma step_pos:
  assumes "i < k" "x  x1"
  shows   "bs ! i * x + (hs ! i) x > 0"
proof-
  from assms x0_le_x1 have "hb / ln x powr (1 + e) < bs ! i" by (simp add: x0_hb_bound0')
  with assms x0_pos x0_le_x1 have "x * 0 < x * (bs ! i - hb / ln x powr (1 + e))" by simp
  also have "... = bs ! i * x - hb * x / ln x powr (1 + e)"
    by (simp add: algebra_simps)
  also from assms have "-hb * x / ln x powr (1 + e)  -¦(hs ! i) x¦" by (simp add: h_bounds)
  hence "bs ! i * x - hb * x / ln x powr (1 + e)  bs ! i * x + -¦(hs ! i) x¦" by simp
  also have "-¦(hs ! i) x¦  (hs ! i) x" by simp
  finally show "bs ! i * x + (hs ! i) x > 0" by simp
qed

lemma step_nonneg: "i < k  x  x1  bs ! i * x + (hs ! i) x  0"
  by (drule (1) step_pos) simp

lemma step_nonneg': "i < k  x  x1  bs ! i + (hs ! i) x / x  0"
  by (frule (1) step_nonneg, insert x0_pos x0_le_x1) (simp_all add: field_simps)

lemma hb_nonneg: "hb  0"
proof-
  from k_not_0 and length_hs have "hs  []" by auto
  then obtain h where h: "h  set hs" by (cases hs) auto
  have "0  ¦h x1¦" by simp
  also from h have "¦h x1¦  hb * x1 / ln x1 powr (1+e)" by (intro h_bounds) simp_all
  finally have "0  hb * x1 / ln x1 powr (1 + e)" .
  hence "0  ... * (ln x1 powr (1 + e) / x1)"
    by (rule mult_nonneg_nonneg) (intro divide_nonneg_nonneg, insert x1_pos, simp_all)
  also have "... = hb" using x1_gt_1 by (simp add: field_simps)
  finally show ?thesis .
qed

lemma x0_hb_bound3:
  assumes "x  x1" "i < k"
  shows   "x - (bs ! i * x + (hs ! i) x)  x"
proof-
  have "-(hs ! i) x  ¦(hs ! i) x¦" by simp
  also from assms have "...  hb * x / ln x powr (1 + e)" by (simp add: h_bounds)
  also have "... = x * (hb / ln x powr (1 + e))" by simp
  also from assms x0_pos x0_le_x1 have "... < x * bs ! i"
    by (intro mult_strict_left_mono x0_hb_bound0') simp_all
  finally show ?thesis by (simp add: algebra_simps)
qed

lemma x0_hb_bound4:
  assumes "x  x1" "i < k"
  shows   "(bs ! i + (hs ! i) x / x) > bs ! i / 2"
proof-
  from assms x0_le_x1 have "hb / ln x powr (1 + e) < bs ! i / 2" by (intro x0_hb_bound0) simp_all
  with assms x0_pos x0_le_x1 have "(-bs ! i / 2) * x < (-hb / ln x powr (1 + e)) * x"
    by (intro mult_strict_right_mono) simp_all
  also from assms x0_pos have "...  -¦(hs ! i) x¦" using h_bounds by simp
  also have "...  (hs ! i) x" by simp
  finally show ?thesis using assms x1_pos by (simp add: field_simps)
qed

lemma x0_hb_bound4': "x  x1  i < k  (bs ! i + (hs ! i) x / x)  bs ! i / 2"
  by (drule (1) x0_hb_bound4) simp

lemma x0_hb_bound5:
  assumes "x  x1" "i < k"
  shows   "(bs ! i + (hs ! i) x / x)  bs ! i * 3/2"
proof-
  have "(hs ! i) x  ¦(hs ! i) x¦" by simp
  also from assms have "...  hb * x / ln x powr (1 + e)" by (simp add: h_bounds)
  also have "... = x * (hb / ln x powr (1 + e))" by simp
  also from assms x0_pos x0_le_x1 have "... < x * (bs ! i / 2)"
    by (intro mult_strict_left_mono x0_hb_bound0) simp_all
  finally show ?thesis using assms x1_pos by (simp add: field_simps)
qed

lemma x0_hb_bound6:
  assumes "x  x1" "i < k"
  shows   "x * ((1 - bs ! i) / 2)  x - (bs ! i * x + (hs ! i) x)"
proof-
  from assms x0_le_x1 have "hb / ln x powr (1 + e) < (1 - bs ! i) / 2" using x0_hb_bound1 by simp
  with assms x1_pos have "x * ((1 - bs ! i) / 2)  x * (1 - (bs ! i + hb / ln x powr (1 + e)))"
    by (intro mult_left_mono) (simp_all add: field_simps)
  also have "... = x - bs ! i * x + -hb * x / ln x powr (1 + e)" by (simp add: algebra_simps)
  also from h_bounds assms have "-hb * x / ln x powr (1 + e)  -¦(hs ! i) x¦"
    by (simp add: length_hs)
  also have "...  -(hs ! i) x" by simp
  finally show ?thesis by (simp add: algebra_simps)
qed

lemma x0_hb_bound7:
  assumes "x  x1" "i < k"
  shows   "bs!i*x + (hs!i) x > x0"
proof-
  from assms x0_le_x1 have x': "x  x0" by simp
  from x1_ge assms have "2 * x0 * inverse (bs!i)  x1" by simp
  with assms b_pos have "x0  x1 * (bs!i / 2)" by (simp add: field_simps)
  also from assms x' have "bs!i/2 < bs!i + (hs!i) x / x" by (intro x0_hb_bound4)
  also from assms step_nonneg' x' have "x1 * ...  x * ..." by (intro mult_right_mono) (simp_all)
  also from assms x1_pos have "x * (bs!i + (hs!i) x / x) = bs!i*x + (hs!i) x"
    by (simp add: field_simps)
  finally show ?thesis using x1_pos by simp
qed

lemma x0_hb_bound7': "x  x1  i < k  bs!i*x + (hs!i) x > 1"
  by (rule le_less_trans[OF _ x0_hb_bound7]) (insert x0_le_x1 x0_ge_1, simp_all)

lemma x0_hb_bound8:
  assumes "x  x1" "i < k"
  shows   "bs!i*x - hb * x / ln x powr (1+e) > x0"
proof-
  from assms have "2 * x0 * inverse (bs!i)  x1" by (intro x1_ge) simp_all
  with b_pos assms have "x0  x1 * (bs!i/2)" by (simp add: field_simps)
  also from assms b_pos have "...  x * (bs!i/2)" by simp
  also from assms x0_le_x1 have "hb / ln x powr (1+e) < bs!i/2" by (intro x0_hb_bound0) simp_all
  with assms have "bs!i/2 < bs!i - hb / ln x powr (1+e)" by (simp add: field_simps)
  also have "x * ... = bs!i*x - hb * x / ln x powr (1+e)" by (simp add: algebra_simps)
  finally show ?thesis using assms x1_pos by (simp add: field_simps)
qed

lemma x0_hb_bound8':
  assumes "x  x1" "i < k"
  shows   "bs!i*x + hb * x / ln x powr (1+e) > x0"
proof-
  from assms have "x0 < bs!i*x - hb * x / ln x powr (1+e)" by (rule x0_hb_bound8)
  also from assms hb_nonneg x1_pos have "hb * x / ln x powr (1+e)  0"
    by (intro mult_nonneg_nonneg divide_nonneg_nonneg) simp_all
  hence "bs!i*x - hb * x / ln x powr (1+e)  bs!i*x + hb * x / ln x powr (1+e)" by simp
  finally show ?thesis .
qed

lemma
  assumes "x  x0"
  shows   asymptotics1: "i < k  1 + ln x powr (- e / 2) 
             (1 - hb * inverse (bs!i) * ln x powr -(1+e)) powr p *
             (1 + ln (bs!i*x + hb*x/ln x powr (1+e)) powr (-e/2))"
  and     asymptotics2: "i < k  1 - ln x powr (- e / 2) 
             (1 + hb * inverse (bs!i) * ln x powr -(1+e)) powr p *
             (1 - ln (bs!i*x + hb*x/ln x powr (1+e)) powr (-e/2))"
  and     asymptotics1': "i < k  1 + ln x powr (- e / 2) 
             (1 + hb * inverse (bs!i) * ln x powr -(1+e)) powr p *
             (1 + ln (bs!i*x + hb*x/ln x powr (1+e)) powr (-e/2))"
  and     asymptotics2': "i < k  1 - ln x powr (- e / 2) 
             (1 - hb * inverse (bs!i) * ln x powr -(1+e)) powr p *
             (1 - ln (bs!i*x + hb*x/ln x powr (1+e)) powr (-e/2))"
  and     asymptotics3: "(1 + ln x powr (- e / 2)) / 2  1"
  and     asymptotics4: "(1 - ln x powr (- e / 2)) * 2  1"
  and     asymptotics5: "i < k  ln (bs!i*x - hb*x*ln x powr -(1+e)) powr (-e/2) < 1"
apply -
using assms asymptotics[of x "bs!i"] unfolding akra_bazzi_asymptotic_defs
apply simp_all[4]
using assms asymptotics[of x "bs!0"] unfolding akra_bazzi_asymptotic_defs
apply simp_all[2]
using assms asymptotics[of x "bs!i"] unfolding akra_bazzi_asymptotic_defs
apply simp_all
done


lemma x0_hb_bound9:
  assumes "x  x1" "i < k"
  shows   "ln (bs!i*x + (hs!i) x) powr -(e/2) < 1"
proof-
  from b_pos assms have "0 < bs!i/2" by simp
  also from assms x0_le_x1 have "... < bs!i + (hs!i) x / x" by (intro x0_hb_bound4) simp_all
  also from assms x1_pos have "x * ... = bs!i*x + (hs!i) x" by (simp add: field_simps)
  finally have pos: "bs!i*x + (hs!i) x > 0" using assms x1_pos by simp
  from x0_hb_bound8[OF assms] x0_ge_1 have pos': "bs!i*x - hb * x / ln x powr (1+e) > 1" by simp

  from assms have "-(hb * x / ln x powr (1+e))  -¦(hs!i) x¦"
    by (intro le_imp_neg_le h_bounds) simp_all
  also have "...  (hs!i) x" by simp
  finally have "ln (bs!i*x - hb * x / ln x powr (1+e))  ln (bs!i*x + (hs!i) x)"
    using assms b_pos x0_pos pos' by (intro ln_mono mult_pos_pos pos) simp_all
  hence "ln (bs!i*x + (hs!i) x) powr -(e/2)  ln (bs!i*x - hb * x / ln x powr (1+e)) powr -(e/2)"
    using assms e_pos asymptotics5[of x] pos' by (intro powr_mono2' ln_gt_zero) simp_all
  also have "... < 1" using asymptotics5[of x i] assms x0_le_x1
    by (subst (asm) powr_minus) (simp_all add: field_simps)
  finally show ?thesis .
qed


definition akra_bazzi_measure :: "real  nat" where
  "akra_bazzi_measure x = nat x"

lemma akra_bazzi_measure_decreases:
  assumes "x  x1" "i < k"
  shows   "akra_bazzi_measure (bs!i*x + (hs!i) x) < akra_bazzi_measure x"
proof-
  from step_diff assms have "(bs!i * x + (hs!i) x) + 1 < x" by (simp add: algebra_simps)
  hence "(bs!i * x + (hs!i) x) + 1  x" by (intro ceiling_mono) simp
  hence "(bs!i * x + (hs!i) x) < x" by simp
  with assms x1_pos have "nat (bs!i * x + (hs!i) x) < nat x" by (subst nat_mono_iff) simp_all
  thus ?thesis unfolding akra_bazzi_measure_def .
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  (i. i < k  P (bs!i*x + (hs!i) x))  P x"
  shows   "P x"
proof (insert x  x0, induction "akra_bazzi_measure x" arbitrary: x rule: less_induct)
  case less
  show ?case
  proof (cases "x  x1")
    case True
    with base and x  x0 show ?thesis .
  next
    case False
    hence x: "x > x1" by simp
    thus ?thesis
    proof (rule rec)
      fix i assume i: "i < k"
      from x0_hb_bound7[OF _ i, of x] x have "bs!i*x + (hs!i) x  x0" by simp
      with i x show "P (bs ! i * x + (hs ! i) x)"
        by (intro less akra_bazzi_measure_decreases) simp_all
    qed
  qed
qed

end


locale akra_bazzi_real = akra_bazzi_real_recursion +
  fixes integrable integral
  assumes integral: "akra_bazzi_integral integrable integral"
  fixes f :: "real  real"
  and   g :: "real  real"
  and   C :: real
  assumes p_props:      "(i<k. as!i * bs!i powr p) = 1"
  and     f_base:       "x  x0  x  x1  f x  0"
  and     f_rec:        "x > x1  f x = g x + (i<k. as!i * f (bs!i * x + (hs!i) x))"
  and     g_nonneg:     "x  x0  g x  0"
  and     C_bound:      "b  set bs  x  x1  C*x  b*x - hb*x/ln x powr (1+e)"
  and     g_integrable: "x  x0  integrable (λu. g u / u powr (p + 1)) x0 x"
begin

interpretation akra_bazzi_integral integrable integral by (rule integral)

lemma akra_bazzi_integrable:
  "a  x0  a  b  integrable (λx. g x / x powr (p + 1)) a b"
  by (rule integrable_subinterval[OF g_integrable, of b]) simp_all

definition g_approx :: "nat  real  real" where
  "g_approx i x = x powr p * integral (λu. g u / u powr (p + 1)) (bs!i * x + (hs!i) x) x"

lemma f_nonneg: "x  x0  f x  0"
proof (induction x rule: akra_bazzi_induct)
  case (base x)
  with f_base[of x] show ?case by simp
next
  case (rec x)
  with x0_le_x1 have "g x  0" by (intro g_nonneg) simp_all
  moreover {
    fix i assume i: "i < k"
    with rec.IH have "f (bs!i*x + (hs!i) x)  0" by simp
    with i have "as!i * f (bs!i*x + (hs!i) x)  0"
        by (intro mult_nonneg_nonneg[OF a_ge_0]) simp_all
  }
  hence "(i<k. as!i * f (bs!i*x + (hs!i) x))  0" by (intro sum_nonneg) blast
  ultimately show "f x  0" using rec.hyps by (subst f_rec) simp_all
qed


definition f_approx :: "real  real" where
  "f_approx x = x powr p * (1 + integral (λu. g u / u powr (p + 1)) x0 x)"

lemma f_approx_aux:
  assumes "x  x0"
  shows   "1 + integral (λu. g u / u powr (p + 1)) x0 x  1"
proof-
  from assms have "integral (λu. g u / u powr (p + 1)) x0 x  0"
    by (intro integral_nonneg ballI g_nonneg divide_nonneg_nonneg g_integrable) simp_all
  thus ?thesis by simp
qed

lemma f_approx_pos: "x  x0  f_approx x > 0"
  unfolding f_approx_def by (intro mult_pos_pos, insert x0_pos, simp, drule f_approx_aux, simp)

lemma f_approx_nonneg: "x  x0  f_approx x  0"
  using f_approx_pos[of x] by simp


lemma f_approx_bounded_below:
  obtains c where "x. x  x0  x  x1  f_approx x  c" "c > 0"
proof-
  {
    fix x assume x: "x  x0" "x  x1"
    with x0_pos have "x powr p  min (x0 powr p) (x1 powr p)"
      by (intro powr_lower_bound) simp_all
    with x have "f_approx x  min (x0 powr p) (x1 powr p) * 1"
      unfolding f_approx_def by (intro mult_mono f_approx_aux) simp_all
  }
  from this x0_pos x1_pos show ?thesis by (intro that[of "min (x0 powr p) (x1 powr p)"]) auto
qed


lemma asymptotics_aux:
  assumes "x  x1" "i < k"
  assumes "s  (if p  0 then 1 else -1)"
  shows "(bs!i*x - s*hb*x*ln x powr -(1+e)) powr p  (bs!i*x + (hs!i) x) powr p" (is "?thesis1")
  and   "(bs!i*x + (hs!i) x) powr p  (bs!i*x + s*hb*x*ln x powr -(1+e)) powr p" (is "?thesis2")
proof-
  from assms x1_gt_1 have ln_x_pos: "ln x > 0" by simp
  from assms x1_pos have x_pos: "x > 0" by simp
  from assms x0_le_x1 have *: "hb / ln x powr (1+e) < bs!i/2" by (intro x0_hb_bound0) simp_all
  with hb_nonneg ln_x_pos have "(bs!i - hb * ln x powr -(1+e)) > 0"
    by (subst powr_minus) (simp_all add: field_simps)
  with * have "0 < x * (bs!i - hb * ln x powr -(1+e))" using x_pos
    by (subst (asm) powr_minus, intro mult_pos_pos)
  hence A: "0 < bs!i*x - hb * x * ln x powr -(1+e)" by (simp add: algebra_simps)

  from assms have "-(hb*x*ln x powr -(1+e))  -¦(hs!i) x¦"
    using h_bounds[of x "hs!i"] by (subst neg_le_iff_le, subst powr_minus) (simp add: field_simps)
  also have "...  (hs!i) x" by simp
  finally have B: "bs!i*x - hb*x*ln x powr -(1+e)  bs!i*x + (hs!i) x" by simp

  have "(hs!i) x  ¦(hs!i) x¦" by simp
  also from assms have "...  (hb*x*ln x powr -(1+e))"
     using h_bounds[of x "hs!i"] by (subst powr_minus) (simp_all add: field_simps)
  finally have C: "bs!i*x + hb*x*ln x powr -(1+e)  bs!i*x + (hs!i) x" by simp

  from A B C show ?thesis1
    by (cases "p  0") (auto intro: powr_mono2 powr_mono2' simp: assms(3))
  from A B C show ?thesis2
    by (cases "p  0") (auto intro: powr_mono2 powr_mono2' simp: assms(3))
qed

lemma asymptotics1':
  assumes "x  x1" "i < k"
  shows   "(bs!i*x) powr p * (1 + ln x powr (-e/2)) 
           (bs!i*x + (hs!i) x) powr p * (1 + ln (bs!i*x + (hs!i) x) powr (-e/2))"
proof-
  from assms x0_le_x1 have x: "x  x0" by simp
  from b_pos[of "bs!i"] assms have b_pos: "bs!i > 0" "bs!i  0" by simp_all
  from b_less_1[of "bs!i"] assms have b_less_1: "bs!i < 1" by simp
  from x1_gt_1 assms have ln_x_pos: "ln x > 0" by simp
  have mono: "a b. a  b  (bs!i*x) powr p * a  (bs!i*x) powr p * b"
    by (rule mult_left_mono) simp_all

  define s :: real where [abs_def]: "s = (if p  0 then 1 else -1)"
  have "1 + ln x powr (-e/2) 
          (1 - s*hb*inverse(bs!i)*ln x powr -(1+e)) powr p *
          (1 + ln (bs!i*x + hb * x / ln x powr (1+e)) powr (-e/2))" (is "_  ?A * ?B")
    using assms x unfolding s_def using asymptotics1[OF x assms(2)] asymptotics1'[OF x assms(2)]
    by simp
  also have "(bs!i*x) powr p * ... = (bs!i*x) powr p * ?A * ?B" by simp
  also from x0_hb_bound0'[OF x, of "bs!i"] hb_nonneg x ln_x_pos assms
    have "s*hb * ln x powr -(1 + e) < bs ! i"
    by (subst powr_minus) (simp_all add: field_simps s_def)
  hence "(bs!i*x) powr p * ?A = (bs!i*x*(1 - s*hb*inverse (bs!i)*ln x powr -(1+e))) powr p"
    using b_pos assms x x0_pos b_less_1 ln_x_pos
    by (subst powr_mult[symmetric]) (simp_all add: s_def field_simps)
  also have "bs!i*x*(1 - s*hb*inverse (bs!i)*ln x powr -(1+e)) = bs!i*x - s*hb*x*ln x powr -(1+e)"
    using b_pos assms by (simp add: algebra_simps)
  also have "?B = 1 + ln (bs!i*x + hb*x*ln x powr -(1+e)) powr (-e/2)"
    by (subst powr_minus) (simp add: field_simps)

  also {
    from x assms have "(bs!i*x - s*hb*x*ln x powr -(1+e)) powr p  (bs!i*x + (hs!i) x) powr p"
      using asymptotics_aux(1)[OF assms(1,2) s_def] by blast
    moreover {
      have "(hs!i) x  ¦(hs!i) x¦" by simp
      also from assms have "¦(hs!i) x¦  hb * x / ln x powr (1+e)" by (intro h_bounds) simp_all
      finally have "(hs ! i) x  hb * x * ln x powr -(1 + e)"
        by (subst powr_minus) (simp_all add: field_simps)
      moreover from x hb_nonneg x0_pos have "hb * x * ln x powr -(1+e)  0"
        by (intro mult_nonneg_nonneg) simp_all
      ultimately have "1 + ln (bs!i*x + hb * x * ln x powr -(1+e)) powr (-e/2) 
                       1 + ln (bs!i*x + (hs!i) x) powr (-e/2)" using assms x e_pos b_pos x0_pos
      by (intro add_left_mono powr_mono2' ln_mono ln_gt_zero step_pos x0_hb_bound7'
                add_pos_nonneg mult_pos_pos) simp_all
    }
    ultimately have "(bs!i*x - s*hb*x*ln x powr -(1+e)) powr p *
                         (1 + ln (bs!i*x + hb * x * ln x powr -(1+e)) powr (-e/2))
                      (bs!i*x + (hs!i) x) powr p * (1 + ln (bs!i*x + (hs!i) x) powr (-e/2))"
      by (rule mult_mono) simp_all
  }
  finally show ?thesis by (simp_all add: mono)
qed

lemma asymptotics2':
  assumes "x  x1" "i < k"
  shows   "(bs!i*x + (hs!i) x) powr p * (1 - ln (bs!i*x + (hs!i) x) powr (-e/2)) 
           (bs!i*x) powr p * (1 - ln x powr (-e/2))"
proof-
  define s :: real where "s = (if p  0 then 1 else -1)"
  from assms x0_le_x1 have x: "x  x0" by simp
  from assms x1_gt_1 have ln_x_pos: "ln x > 0" by simp
  from b_pos[of "bs!i"] assms have b_pos: "bs!i > 0" "bs!i  0" by simp_all
  from b_pos hb_nonneg have pos: "1 + s * hb * (inverse (bs!i) * ln x powr -(1+e)) > 0"
    using x0_hb_bound0'[OF x, of "bs!i"] b_pos assms ln_x_pos
    by (subst powr_minus) (simp add: field_simps s_def)
  have mono: "a b. a  b  (bs!i*x) powr p * a  (bs!i*x) powr p * b"
    by (rule mult_left_mono) simp_all

  let ?A = "(1 + s*hb*inverse(bs!i)*ln x powr -(1+e)) powr p"
  let ?B = "1 - ln (bs!i*x + (hs!i) x) powr (-e/2)"
  let ?B' = "1 - ln (bs!i*x + hb * x / ln x powr (1+e)) powr (-e/2)"

  from assms x have "(bs!i*x + (hs!i) x) powr p  (bs!i*x + s*hb*x*ln x powr -(1+e)) powr p"
    by (intro asymptotics_aux(2)) (simp_all add: s_def)
  moreover from x0_hb_bound9[OF assms(1,2)] have "?B  0" by (simp add: field_simps)
  ultimately have "(bs!i*x + (hs!i) x) powr p * ?B 
                   (bs!i*x + s*hb*x*ln x powr -(1+e)) powr p * ?B" by (rule mult_right_mono)
  also from assms e_pos pos have "?B  ?B'"
  proof -
    from x0_hb_bound8'[OF assms(1,2)] x0_hb_bound8[OF assms(1,2)] x0_ge_1
    have *: "bs ! i * x + s*hb * x / ln x powr (1 + e) > 1" by (simp add: s_def)
    moreover from * have "... > 0" by simp
    moreover from x0_hb_bound7[OF assms(1,2)] x0_ge_1 have "bs ! i * x + (hs ! i) x > 1" by simp
    moreover {
      have "(hs!i) x  ¦(hs!i) x¦" by simp
      also from assms x0_le_x1 have "...  hb*x/ln x powr (1+e)" by (intro h_bounds) simp_all
      finally have "bs!i*x + (hs!i) x  bs!i*x + hb*x/ln x powr (1+e)" by simp
    }
    ultimately show "?B  ?B'" using assms e_pos x step_pos
      by (intro diff_left_mono powr_mono2' ln_mono ln_gt_zero) simp_all
  qed
  hence "(bs!i*x + s*hb*x*ln x powr -(1+e)) powr p * ?B 
             (bs!i*x + s*hb*x*ln x powr -(1+e)) powr p * ?B'" by (intro mult_left_mono) simp_all
  also have "bs!i*x + s*hb*x*ln x powr -(1+e) = bs!i*x*(1 + s*hb*inverse (bs!i)*ln x powr -(1+e))"
    using b_pos by (simp_all add: field_simps)
  also have "... powr p = (bs!i*x) powr p * ?A"
    using powr_mult by force
  also have "(bs!i*x) powr p * ?A * ?B' = (bs!i*x) powr p * (?A * ?B')" by simp
  also have "?A * ?B'  1 - ln x powr (-e/2)" using assms x
    using asymptotics2[OF x assms(2)] asymptotics2'[OF x assms(2)] by (simp add: s_def)
  finally show ?thesis by (simp_all add: mono)
qed

lemma Cx_le_step:
  assumes "i < k" "x  x1"
  shows   "C*x  bs!i*x + (hs!i) x"
proof-
  from assms have "C*x  bs!i*x - hb*x/ln x powr (1+e)" by (intro C_bound) simp_all
  also from assms have "-(hb*x/ln x powr (1+e))  -¦(hs!i) x¦"
    by (subst neg_le_iff_le, intro h_bounds) simp_all
  hence "bs!i*x - hb*x/ln x powr (1+e)  bs!i*x + -¦(hs!i) x¦" by simp
  also have "-¦(hs!i) x¦  (hs!i) x" by simp
  finally show ?thesis by simp
qed

end


locale akra_bazzi_nat_to_real = akra_bazzi_real_recursion +
  fixes f :: "nat  real"
  and   g :: "real  real"
  assumes f_base: "real x  x0  real x  x1  f x  0"
  and     f_rec:  "real x > x1 
                          f x = g (real x) + (i<k. as!i * f (nat bs!i * x + (hs!i) (real x)))"
  and     x0_int: "real (nat x0) = x0"
begin

function f' :: "real  real" where
  "x  x1  f' x = f (nat x)"
| "x > x1  f' x = g x + (i<k. as!i * f' (bs!i * x + (hs!i) x))"
by (force, simp_all)
termination by (relation "Wellfounded.measure akra_bazzi_measure")
               (simp_all add: akra_bazzi_measure_decreases)

lemma f'_base: "x  x0  x  x1  f' x  0"
  apply (subst f'.simps(1), assumption)
  apply (rule f_base)
  apply (rule order.trans[of _ "real (nat x0)"], simp add: x0_int)
  apply (subst of_nat_le_iff, intro nat_mono floor_mono, assumption)
  using x0_pos apply linarith
  done

lemmas f'_rec = f'.simps(2)

end


locale akra_bazzi_real_lower = akra_bazzi_real +
  fixes fb2 gb2 c2 :: real
  assumes f_base2:   "x  x0  x  x1  f x  fb2"
  and     fb2_pos:   "fb2 > 0"
  and     g_growth2: "xx1. u{C*x..x}. c2 * g x  g u"
  and     c2_pos:    "c2 > 0"
  and     g_bounded: "x  x0  x  x1  g x  gb2"
begin

interpretation akra_bazzi_integral integrable integral by (rule integral)

lemma gb2_nonneg: "gb2  0" using g_bounded[of x0] x0_le_x1 x0_pos g_nonneg[of x0] by simp

lemma g_growth2':
  assumes "x  x1" "i < k" "u  {bs!i*x+(hs!i) x..x}"
  shows   "c2 * g x  g u"
proof-
  from assms have "C*x  bs!i*x+(hs!i) x" by (intro Cx_le_step)
  with assms have "u  {C*x..x}" by auto
  with assms g_growth2 show ?thesis by simp
qed

lemma g_bounds2:
  obtains c4 where "x i. x  x1  i < k  g_approx i x  c4 * g x" "c4 > 0"
proof-
  define c4
    where "c4 = Max {c2 / min 1 (min ((b/2) powr (p+1)) ((b*3/2) powr (p+1))) |b. b  set bs}"

  {
    from bs_nonempty obtain b where b: "b  set bs" by (cases bs) auto
    let ?m = "min 1 (min ((b/2) powr (p+1)) ((b*3/2) powr (p+1)))"
    from b b_pos have "?m > 0" unfolding min_def by (auto simp: not_le)
    with b b_pos c2_pos have "c2 / ?m > 0" by (simp_all add: field_simps)
    with b have "c4 > 0" unfolding c4_def by (subst Max_gr_iff) (simp, simp, blast)
  }

  {
    fix x i assume i: "i < k" and x: "x  x1"
    have powr_negD: "a powr b  0  a = 0"
      for a b :: real unfolding powr_def by (simp split: if_split_asm)
    let ?m = "min 1 (min ((bs!i/2) powr (p+1)) ((bs!i*3/2) powr (p+1)))"
    have "min 1 ((bs!i + (hs ! i) x / x) powr (p+1))  min 1 (min ((bs!i/2) powr (p+1)) ((bs!i*3/2) powr (p+1)))"
      apply (insert x i x0_le_x1 x1_pos step_pos b_pos[OF b_in_bs[OF i]],
             rule min.mono, simp, cases "p + 1  0")
      apply (rule order.trans[OF min.cobounded1 powr_mono2[OF _ _ x0_hb_bound4']], simp_all add: field_simps) []
      apply (rule order.trans[OF min.cobounded2 powr_mono2'[OF _ _ x0_hb_bound5]], simp_all add: field_simps) []
      done
    with i b_pos[of "bs!i"] have "c2 / min 1 ((bs!i + (hs ! i) x / x) powr (p+1))  c2 / ?m" using c2_pos
      unfolding min_def by (intro divide_left_mono) (auto intro!: mult_pos_pos dest!: powr_negD)

    also from i x have "...  c4" unfolding c4_def by (intro Max.coboundedI) auto
    finally have "c2 / min 1 ((bs!i + (hs ! i) x / x) powr (p+1))  c4" .
  } note c4 = this

  {
    fix x :: real and i :: nat
    assume x: "x  x1" and i: "i < k"
    from x x1_pos have x_pos: "x > 0" by simp
    let ?x' = "bs ! i * x + (hs ! i) x"
    let ?x'' = "bs ! i + (hs ! i) x / x"
    from x x1_ge_1 i g_growth2' x0_le_x1 c2_pos
      have c2: "c2 > 0" "u{?x'..x}. g u  c2 * g x" by auto

    from x0_le_x1 x i have x'_le_x: "?x'  x" by (intro step_le_x) simp_all
    let ?m = "min (?x' powr (p + 1)) (x powr (p + 1))"
    define m' where "m' = min 1 (?x'' powr (p + 1))"
    have [simp]: "bs ! i > 0" by (intro b_pos nth_mem) (simp add: i length_bs)
    from x0_le_x1 x i have [simp]: "?x' > 0" by (intro step_pos) simp_all


    {
      fix u assume u: "u  ?x'" "u  x"
      have "?m  u powr (p + 1)" using x u by (intro powr_lower_bound mult_pos_pos) simp_all
      moreover from c2 and u have "g u  c2 * g x" by simp
      ultimately have "g u * ?m  c2 * g x * u powr (p + 1)" using c2 x x1_pos x0_le_x1
        by (intro mult_mono mult_nonneg_nonneg g_nonneg) auto
    }
    hence "integral (λu. g u / u powr (p+1)) ?x' x  integral (λu. c2 * g x / ?m) ?x' x"
      using x_pos step_pos[OF i x] x0_hb_bound7[OF x i] c2 x x0_le_x1
      by (intro integral_le x'_le_x akra_bazzi_integrable ballI integrable_const)
         (auto simp: field_simps intro!: mult_nonneg_nonneg g_nonneg)

    also from x0_pos x x0_le_x1 x'_le_x c2 have "... = (x - ?x') * (c2 * g x / ?m)"
      by (subst integral_const) (simp_all add: g_nonneg)
    also from c2 x_pos x x0_le_x1 have "c2 * g x  0"
      by (intro mult_nonneg_nonneg g_nonneg) simp_all
    with x i x0_le_x1 have "(x - ?x') * (c2 * g x / ?m)  x * (c2 * g x / ?m)"
      by (intro x0_hb_bound3 mult_right_mono) (simp_all add: field_simps)

    also have "x powr (p + 1) = x powr (p + 1) * 1" by simp
    also have "(bs ! i * x + (hs ! i) x) powr (p + 1) =
               (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)"
      using x x1_pos step_pos[OF i x] 
      by (simp add: ring_class.ring_distribs flip: powr_mult)
    also have "... = x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)" by simp
    also have "min ... (x powr (p + 1) * 1) = x powr (p + 1) * m'" unfolding m'_def using x_pos
      by (subst min.commute, intro min_mult_left[symmetric]) simp

    also from x_pos have "x * (c2 * g x / (x powr (p + 1) * m')) = (c2/m') * (g x / x powr p)"
      by (simp add: field_simps powr_add)
    also from x i g_nonneg x0_le_x1 x1_pos have "...  c4 * (g x / x powr p)" unfolding m'_def
      by (intro mult_right_mono c4) (simp_all add: field_simps)
    finally have "g_approx i x  c4 * g x"
      unfolding g_approx_def using x_pos by (simp add: field_simps)
  }
  thus ?thesis using that c4 > 0 by blast
qed

lemma f_approx_bounded_above:
  obtains c where "x. x  x0  x  x1  f_approx x  c" "c > 0"
proof-
  let ?m1 = "max (x0 powr p) (x1 powr p)"
  let ?m2 = "max (x0 powr (-(p+1))) (x1 powr (-(p+1)))"
  let ?m3 = "gb2 * ?m2"
  let ?m4 = "1 + (x1 - x0) * ?m3"
  let ?int = "λx. integral (λu. g u / u powr (p + 1)) x0 x"
  {
    fix x assume x: "x  x0" "x  x1"
    with x0_pos have "x powr p  ?m1" "?m1  0" by (intro powr_upper_bound) (simp_all add: max_def)
    moreover {
      fix u assume u: "u  {x0..x}"
      have "g u / u powr (p + 1) = g u * u powr (-(p+1))"
        by (subst powr_minus) (simp add: field_simps)
      also from u x x0_pos have "u powr (-(p+1))  ?m2"
        by (intro powr_upper_bound) simp_all
      hence "g u * u powr (-(p+1))  g u * ?m2"
        using u g_nonneg x0_pos by (intro mult_left_mono) simp_all
      also from x u x0_pos have "g u  gb2" by (intro g_bounded) simp_all
      hence "g u * ?m2  gb2 * ?m2" by (intro mult_right_mono) (simp_all add: max_def)
      finally have "g u / u powr (p + 1)  ?m3" .
    } note A = this
    {
      from A x gb2_nonneg have "?int x  integral (λ_. ?m3) x0 x"
        by (intro integral_le akra_bazzi_integrable integrable_const mult_nonneg_nonneg)
           (simp_all add: le_max_iff_disj)
      also from x gb2_nonneg have "...  (x - x0) * ?m3"
        by (subst integral_const) (simp_all add: le_max_iff_disj)
      also from x gb2_nonneg have "...  (x1 - x0) * ?m3"
        by (intro mult_right_mono mult_nonneg_nonneg) (simp_all add: max_def)
      finally have "1 + ?int x  ?m4" by simp
    }
    moreover from x g_nonneg x0_pos have "?int x  0"
      by (intro integral_nonneg akra_bazzi_integrable) (simp_all add: powr_def field_simps)
    hence "1 + ?int x  0" by simp
    ultimately have "f_approx x  ?m1 * ?m4"
      unfolding f_approx_def by (intro mult_mono)
    hence "f_approx x  max 1 (?m1 * ?m4)" by simp
  }
  from that[OF this] show ?thesis by auto
qed

lemma f_bounded_below:
  assumes c': "c' > 0"
  obtains c where "x. x  x0  x  x1  2 * (c * f_approx x)  f x" "c  c'" "c > 0"
proof-
  obtain c where c: "x. x0  x  x  x1  f_approx x  c" "c > 0"
    by (rule f_approx_bounded_above) blast
  {
    fix x assume x: "x0  x" "x  x1"
    with c have "inverse c * f_approx x  1" by (simp add: field_simps)
    moreover from x f_base2 x0_pos have "f x  fb2" by auto
    ultimately have "inverse c * f_approx x * fb2  1 * f x" using fb2_pos
      by (intro mult_mono) simp_all
    hence "inverse c * fb2 * f_approx x  f x" by (simp add: field_simps)
    moreover have "min c' (inverse c * fb2) * f_approx x  inverse c * fb2 * f_approx x"
      using f_approx_nonneg x c
      by (intro mult_right_mono f_approx_nonneg) (simp_all add: field_simps)
    ultimately have "2 * (min c' (inverse c * fb2) / 2 * f_approx x)  f x" by simp
  }
  moreover from c' have "min c' (inverse c * fb2) / 2  c'" by simp
  moreover have "min c' (inverse c * fb2) / 2 > 0"
    using c fb2_pos c' by simp
  ultimately show ?thesis by (rule that)
qed

lemma akra_bazzi_lower:
  obtains c5 where "x. x  x0  f x  c5 * f_approx x" "c5 > 0"
proof-
  obtain c4 where c4: "x i. x  x1  i < k  g_approx i x  c4 * g x" "c4 > 0"
    by (rule g_bounds2) blast
  hence "inverse c4 / 2 > 0" by simp
  then obtain c5 where c5: "x. x  x0  x  x1  2 * (c5 * f_approx x)  f x"
                           "c5  inverse c4 / 2" "c5 > 0"
    by (rule f_bounded_below) blast

  {
  fix x :: real assume x: "x  x0"
  from c5 x have  " c5 * 1 * f_approx x  c5 * (1 + ln x powr (- e / 2)) * f_approx x"
    by (intro mult_right_mono mult_left_mono f_approx_nonneg) simp_all
  also from x have "c5 * (1 + ln x powr (-e/2)) * f_approx x  f x"
  proof (induction x rule: akra_bazzi_induct)
    case (base x)
    have "1 + ln x powr (-e/2)  2" using asymptotics3 base by simp
    hence "(1 + ln x powr (-e/2)) * (c5 * f_approx x)  2 * (c5 * f_approx x)"
      using c5 f_approx_nonneg base x0_ge_1 by (intro mult_right_mono mult_nonneg_nonneg) simp_all
    also from base have "2 * (c5 * f_approx x)  f x"  by (intro c5) simp_all
    finally show ?case by (simp add: algebra_simps)
  next
    case (rec x)
    let ?a = "λi. as!i" and ?b = "λi. bs!i" and ?h = "λi. hs!i"
    let ?int = "integral (λu. g u / u powr (p+1)) x0 x"
    let ?int1 = "λi. integral (λu. g u / u powr (p+1)) x0 (?b i*x+?h i x)"
    let ?int2 = "λi. integral (λu. g u / u powr (p+1)) (?b i*x+?h i x) x"
    let ?l = "ln x powr (-e/2)" and ?l' = "λi. ln (?b i*x + ?h i x) powr (-e/2)"

    from rec and x0_le_x1 x0_ge_1 have x: "x  x0" and x_gt_1: "x > 1" by simp_all
    with x0_pos have x_pos: "x > 0" and x_nonneg: "x  0" by simp_all
    from c5 c4 have "c5 * c4  1/2" by (simp add: field_simps)
    moreover from asymptotics3 x have "(1 + ?l)  2" by (simp add: field_simps)
    ultimately have "(c5*c4)*(1 + ?l)  (1/2) * 2" by (rule mult_mono) simp_all
    hence "0  1 - c5*c4*(1 + ?l)" by simp
    with g_nonneg[OF x] have "0  g x * ..." by (intro mult_nonneg_nonneg) simp_all
    hence "c5 * (1 + ?l) * f_approx x  c5 * (1 + ?l) * f_approx x + g x - c5*c4*(1 + ?l) * g x"
      by (simp add: algebra_simps)
    also from x_gt_1 have "... = c5 * x powr p * (1 + ?l) * (1 + ?int - c4*g x/x powr p) + g x"
      by (simp add: field_simps f_approx_def powr_minus)
    also have "c5 * x powr p * (1 + ?l) * (1 + ?int - c4*g x/x powr p) =
                 (i<k. (?a i * ?b i powr p) * (c5 * x powr p * (1 + ?l) * (1 + ?int - c4*g x/x powr p)))"
      by (subst sum_distrib_right[symmetric]) (simp add: p_props)
    also have "...  (i<k. ?a i * f (?b i*x + ?h i x))"
    proof (intro sum_mono, clarify)
      fix i assume i: "i < k"
      let ?f = "c5 * ?a i * (?b i * x) powr p"
      from rec.hyps i have "x0 < bs ! i * x + (hs ! i) x" by (intro x0_hb_bound7) simp_all
      hence "1 + ?int1 i  1" by (intro f_approx_aux x0_hb_bound7) simp_all
      hence int_nonneg: "1 + ?int1 i  0" by simp

      have "(?a i * ?b i powr p) * (c5 * x powr p * (1 + ?l) * (1 + ?int - c4*g x/x powr p)) =
            ?f * (1 + ?l) * (1 + ?int - c4*g x/x powr p)" (is "?expr = ?A * ?B")
            using x_pos b_pos[of "bs!i"] i by (subst powr_mult) simp_all
      also from rec.hyps i have "g_approx i x  c4 * g x" by (intro c4) simp_all
      hence "c4*g x/x powr p  ?int2 i" unfolding g_approx_def using x_pos
        by (simp add: field_simps)
      hence "?A * ?B  ?A * (1 + (?int - ?int2 i))" using i c5 a_ge_0
        by (intro mult_left_mono mult_nonneg_nonneg) simp_all
      also from rec.hyps i have "x0 < bs ! i * x + (hs ! i) x" by (intro x0_hb_bound7) simp_all
      hence "?int - ?int2 i = ?int1 i"
        apply (subst diff_eq_eq, subst eq_commute)
        apply (intro integral_combine akra_bazzi_integrable)
        apply (insert rec.hyps step_le_x[OF i, of x], simp_all)
        done
      also have "?A * (1 + ?int1 i) = (c5*?a i*(1 + ?int1 i)) * ((?b i*x) powr p * (1 + ?l))"
        by (simp add: algebra_simps)
      also have "...  (c5*?a i*(1 + ?int1 i)) * ((?b i*x + ?h i x) powr p * (1 + ?l' i))"
        using rec.hyps i c5 a_ge_0 int_nonneg
        by (intro mult_left_mono asymptotics1' mult_nonneg_nonneg) simp_all
      also have "... = ?a i*(c5*(1 + ?l' i)*f_approx (?b i*x + ?h i x))"
        by (simp add: algebra_simps f_approx_def)
      also from i have "...  ?a i * f (?b i*x + ?h i x)"
        by (intro mult_left_mono a_ge_0 rec.IH) simp_all
      finally show "?expr  ?a i * f (?b i*x + ?h i x)" .
    qed
    also have "... + g x = f x" using f_rec[of x] rec.hyps x0_le_x1 by simp
    finally show ?case by simp
  qed
  finally have "c5 * f_approx x  f x" by simp
  }
  from this and c5(3) show ?thesis by (rule that)
qed

lemma akra_bazzi_bigomega:
  "f  Ω(λx. x powr p * (1 + integral (λu. g u / u powr (p + 1)) x0 x))"
apply (fold f_approx_def, rule akra_bazzi_lower, erule landau_omega.bigI)
apply (subst eventually_at_top_linorder, rule exI[of _ x0])
apply (simp add: f_nonneg f_approx_nonneg)
done

end


locale akra_bazzi_real_upper = akra_bazzi_real +
  fixes fb1 c1 :: real
  assumes f_base1:   "x  x0  x  x1  f x  fb1"
  and     g_growth1: "xx1. u{C*x..x}. c1 * g x  g u"
  and     c1_pos:    "c1 > 0"
begin

interpretation akra_bazzi_integral integrable integral by (rule integral)

lemma g_growth1':
  assumes "x  x1" "i < k" "u  {bs!i*x+(hs!i) x..x}"
  shows   "c1 * g x  g u"
proof-
  from assms have "C*x  bs!i*x+(hs!i) x" by (intro Cx_le_step)
  with assms have "u  {C*x..x}" by auto
  with assms g_growth1 show ?thesis by simp
qed

lemma g_bounds1:
  obtains c3 where
    "x i. x  x1  i < k  c3 * g x  g_approx i x" "c3 > 0"
proof-
  define c3 where "c3 =
    Min {c1*((1-b)/2) / max 1 (max ((b/2) powr (p+1)) ((b*3/2) powr (p+1))) |b. b  set bs}"

  {
    fix b assume b: "b  set bs"
    let ?x = "max 1 (max ((b/2) powr (p+1)) ((b*3/2) powr (p+1)))"
    have "?x  1" by simp
    hence "?x > 0" by (rule less_le_trans[OF zero_less_one])
    with b b_less_1 c1_pos have "c1*((1-b)/2) / ?x > 0"
      by (intro divide_pos_pos mult_pos_pos) (simp_all add: algebra_simps)
  }
  hence "c3 > 0" unfolding c3_def by (subst Min_gr_iff) auto

  {
    fix x i assume i: "i < k" and x: "x  x1"
    with b_less_1 have b_less_1': "bs ! i < 1" by simp
    let ?m = "max 1 (max ((bs!i/2) powr (p+1)) ((bs!i*3/2) powr (p+1)))"
    from i x have "c3  c1*((1-bs!i)/2) / ?m" unfolding c3_def by (intro Min.coboundedI) auto
    also have "max 1 ((bs!i + (hs ! i) x / x) powr (p+1))  max 1 (max ((bs!i/2) powr (p+1)) ((bs!i*3/2) powr (p+1)))"
      apply (insert x i x0_le_x1 x1_pos step_pos[OF i x] b_pos[OF b_in_bs[OF i]],
             rule max.mono, simp, cases "p + 1  0")
      apply (rule order.trans[OF powr_mono2[OF _ _ x0_hb_bound5] max.cobounded2], simp_all add: field_simps) []
      apply (rule order.trans[OF powr_mono2'[OF _ _ x0_hb_bound4'] max.cobounded1], simp_all add: field_simps) []
      done
    with b_less_1' c1_pos have "c1*((1-bs!i)/2) / ?m 
          c1*((1-bs!i)/2) / max 1 ((bs!i + (hs ! i) x / x) powr (p+1))"
      by (intro divide_left_mono mult_nonneg_nonneg) (simp_all add: algebra_simps)
    finally have "c3  c1*((1-bs!i)/2) / max 1 ((bs!i + (hs ! i) x / x) powr (p+1))" .
  } note c3 = this

  {
    fix x :: real and i :: nat
    assume x: "x  x1" and i: "i < k"
    from x x1_pos have x_pos: "x > 0" by simp
    let ?x' = "bs ! i * x + (hs ! i) x"
    let ?x'' = "bs ! i + (hs ! i) x / x"
    from x x1_ge_1 x0_le_x1 i c1_pos g_growth1'
      have c1: "c1 > 0" "u{?x'..x}. g u  c1 * g x" by auto
    define b' where "b' = (1 - bs!i)/2"

    from x x0_le_x1 i have x'_le_x: "?x'  x" by (intro step_le_x) simp_all
    let ?m = "max (?x' powr (p + 1)) (x powr (p + 1))"
    define m' where "m' = max 1 (?x'' powr (p + 1))"
    have [simp]: "bs ! i > 0" by (intro b_pos nth_mem) (simp add: i length_bs)
    from x x0_le_x1 i have x'_pos: "?x' > 0" by (intro step_pos) simp_all
    have m_pos: "?m > 0" unfolding max_def using x_pos step_pos[OF i x] by auto
    with x x0_le_x1 c1 have c1_g_m_nonneg: "c1 * g x / ?m  0"
      by (intro mult_nonneg_nonneg divide_nonneg_pos g_nonneg) simp_all

    from x i g_nonneg x0_le_x1 have "c3 * (g x / x powr p)  (c1*b'/m') * (g x / x powr p)"
      unfolding m'_def b'_def by (intro mult_right_mono c3) (simp_all add: field_simps)
    also from x_pos have "... = (x * b') * (c1 * g x / (x powr (p + 1) * m'))"
      by (simp add: field_simps powr_add)
    also from x i c1_pos x1_pos x0_le_x1
      have "...  (x - ?x') * (c1 * g x / (x powr (p + 1) * m'))"
      unfolding b'_def m'_def by (intro x0_hb_bound6 mult_right_mono mult_nonneg_nonneg
                                        divide_nonneg_nonneg g_nonneg) simp_all
    also have "x powr (p + 1) * m' =
                 max (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1)"
      unfolding m'_def using x_pos by (subst max.commute, intro max_mult_left) simp
    also have "(x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) =
                 (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)" by simp
    also have "... = (bs ! i * x + (hs ! i) x) powr (p + 1)"
      using x x1_pos by (simp add: ring_class.ring_distribs flip: powr_mult)
    also have "x powr (p + 1) * 1 = x powr (p + 1)" by simp
    also have "(x - ?x') * (c1 * g x / ?m) = integral (λ_. c1 * g x / ?m) ?x' x"
      using x'_le_x by (subst integral_const[OF c1_g_m_nonneg]) auto
    also {
      fix u assume u: "u  ?x'" "u  x"
      have "u powr (p + 1)  ?m" using x u x'_pos by (intro powr_upper_bound mult_pos_pos) simp_all
      moreover from x'_pos u have "u  0" by simp
      moreover from c1 and u have "c1 * g x  g u" by simp
      ultimately have "c1 * g x * u powr (p + 1)  g u * ?m" using c1 x u x0_hb_bound7[OF x i]
        by (intro mult_mono g_nonneg) auto
      with m_pos u step_pos[OF i x]
        have "c1 * g x / ?m  g u / u powr (p + 1)" by (simp add: field_simps)
    }
    hence "integral (λ_. c1 * g x / ?m) ?x' x  integral (λu. g u / u powr (p + 1)) ?x' x"
      using x0_hb_bound7[OF x i] x'_le_x
      by (intro integral_le ballI akra_bazzi_integrable integrable_const c1_g_m_nonneg) simp_all
    finally have "c3 * g x  g_approx i x" using x_pos
      unfolding g_approx_def by (simp add: field_simps)
  }
  thus ?thesis using that c3 > 0 by blast
qed


lemma f_bounded_above:
  assumes c': "c' > 0"
  obtains c where "x. x  x0  x  x1  f x  (1/2) * (c * f_approx x)" "c  c'" "c > 0"
proof-
  obtain c where c: "x. x0  x  x  x1  f_approx x  c" "c > 0"
    by (rule f_approx_bounded_below) blast
  have fb1_nonneg: "fb1  0" using f_base1[of "x0"] f_nonneg[of x0] x0_le_x1 by simp
  {
    fix x assume x: "x  x0" "x  x1"
    with f_base1 x0_pos have "f x  fb1" by simp
    moreover from c and x have "f_approx x  c" by blast
    ultimately have "f x * c  fb1 * f_approx x" using c fb1_nonneg by (intro mult_mono) simp_all
    also from f_approx_nonneg x have "...  (fb1 + 1) * f_approx x" by (simp add: algebra_simps)
    finally have "f x  ((fb1+1) / c) * f_approx x" by (simp add: field_simps c)
    also have "...  max ((fb1+1) / c) c' * f_approx x"
      by (intro mult_right_mono) (simp_all add: f_approx_nonneg x)
    finally have "f x  1/2 * (max ((fb1+1) / c) c' * 2 * f_approx x)" by simp
  }
  moreover have "max ((fb1+1) / c) c' * 2  max ((fb1+1) / c) c'"
    by (subst mult_le_cancel_left1) (insert c', simp)
  hence "max ((fb1+1) / c) c' * 2  c'" by (rule order.trans[OF max.cobounded2])
  moreover from fb1_nonneg and c have "(fb1+1) / c > 0" by simp
  hence "max ((fb1+1) / c) c' * 2 > 0" by simp
  ultimately show ?thesis by (rule that)
qed


lemma akra_bazzi_upper:
  obtains c6 where "x. x  x0  f x  c6 * f_approx x" "c6 > 0"
proof-
  obtain c3 where c3: "x i. x  x1  i < k  c3 * g x  g_approx i x" "c3 > 0"
    by (rule g_bounds1) blast
  hence "2 / c3 > 0" by simp
  then obtain c6 where c6: "x. x  x0  x  x1  f x  1/2 * (c6 * f_approx x)"
                           "c6  2 / c3" "c6 > 0"
    by (rule f_bounded_above) blast

  {
  fix x :: real assume x: "x  x0"
  hence "f x  c6 * (1 - ln x powr (-e/2)) * f_approx x"
  proof (induction x rule: akra_bazzi_induct)
    case (base x)
    from base have "f x  1/2 * (c6 * f_approx x)"  by (intro c6) simp_all
    also have "1 - ln x powr (-e/2)  1/2" using asymptotics4 base by simp
    hence "(1 - ln x powr (-e/2)) * (c6 * f_approx x)  1/2 * (c6 * f_approx x)"
      using c6 f_approx_nonneg base x0_ge_1 by (intro mult_right_mono mult_nonneg_nonneg) simp_all
    finally show ?case by (simp add: algebra_simps)
  next
    case (rec x)
    let ?a = "λi. as!i" and ?b = "λi. bs!i" and ?h = "λi. hs!i"
    let ?int = "integral (λu. g u / u powr (p+1)) x0 x"
    let ?int1 = "λi. integral (λu. g u / u powr (p+1)) x0 (?b i*x+?h i x)"
    let ?int2 = "λi. integral (λu. g u / u powr (p+1)) (?b i*x+?h i x) x"
    let ?l = "ln x powr (-e/2)" and ?l' = "λi. ln (?b i*x + ?h i x) powr (-e/2)"

    from rec and x0_le_x1 have x: "x  x0" by simp
    with x0_pos have x_pos: "x > 0" and x_nonneg: "x  0" by simp_all
    from c6 c3 have "c6 * c3  2" by (simp add: field_simps)
    have "f x = (i<k. ?a i * f (?b i*x + ?h i x)) + g x" (is "_ = ?sum + _")
      using f_rec[of x] rec.hyps x0_le_x1 by simp
    also have "?sum  (i<k. (?a i*?b i powr p) * (c6*x powr p*(1 - ?l)*(1 + ?int - c3*g x/x powr p)))" (is "_  ?sum'")
    proof (rule sum_mono, clarify)
      fix i assume i: "i < k"
      from rec.hyps i have "x0 < bs ! i * x + (hs ! i) x" by (intro x0_hb_bound7) simp_all
      hence "1 + ?int1 i  1" by (intro f_approx_aux x0_hb_bound7) simp_all
      hence int_nonneg: "1 + ?int1 i  0" by simp
      have l_le_1: "ln x powr -(e/2)  1" using asymptotics3[OF x] by (simp add: field_simps)

      from i have "f (?b i*x + ?h i x)  c6 * (1 - ?l' i) * f_approx (?b i*x + ?h i x)"
        by (rule rec.IH)
      hence "?a i * f (?b i*x + ?h i x)  ?a i * ..." using a_ge_0 i
        by (intro mult_left_mono) simp_all
      also have "... = (c6*?a i*(1 + ?int1 i)) * ((?b i*x + ?h i x) powr p * (1 - ?l' i))"
        unfolding f_approx_def by (simp add: algebra_simps)
      also from i rec.hyps c6 a_ge_0
        have "...  (c6*?a i*(1 + ?int1 i)) * ((?b i*x) powr p * (1 - ?l))"
        by (intro mult_left_mono asymptotics2' mult_nonneg_nonneg int_nonneg) simp_all
      also have "... = (1 + ?int1 i) * (c6*?a i*(?b i*x) powr p * (1 - ?l))"
        by (simp add: algebra_simps)
      also from rec.hyps i have "x0 < bs ! i * x + (hs ! i) x" by (intro x0_hb_bound7) simp_all
      hence "?int1 i = ?int - ?int2 i"
        apply (subst eq_diff_eq)
        apply (intro integral_combine akra_bazzi_integrable)
        apply (insert rec.hyps step_le_x[OF i, of x], simp_all)
        done
      also from rec.hyps i have "c3 * g x  g_approx i x" by (intro c3) simp_all
      hence "?int2 i  c3*g x/x powr p" unfolding g_approx_def using x_pos
        by (simp add: field_simps)
      hence "(1 + (?int - ?int2 i)) * (c6*?a i*(?b i*x) powr p * (1 - ?l)) 
             (1 + ?int - c3*g x/x powr p) * (c6*?a i*(?b i*x) powr p * (1 - ?l))"
             using i c6 a_ge_0 l_le_1
             by (intro mult_right_mono mult_nonneg_nonneg) (simp_all add: field_simps)
      also have "... = (?a i*?b i powr p) * (c6*x powr p*(1 - ?l) * (1 + ?int - c3*g x/x powr p))"
        using b_pos[of "bs!i"] x x0_pos i by (subst powr_mult) (simp_all add: algebra_simps)
      finally show "?a i * f (?b i*x + ?h i x)  ..." .
    qed

    hence "?sum + g x  ?sum' + g x" by simp
    also have "... = c6 * x powr p * (1 - ?l) * (1 + ?int - c3*g x/x powr p) + g x"
      by (simp add: sum_distrib_right[symmetric] p_props)
    also have "... = c6 * (1 - ?l) * f_approx x - (c6*c3*(1 - ?l) - 1) * g x"
      unfolding f_approx_def using x_pos by (simp add: field_simps)
    also {
       from c6 c3 have "c6*c3  2" by (simp add: field_simps)
       moreover have "(1 - ?l)  1/2" using asymptotics4[OF x] by simp
       ultimately have "c6*c3*(1 - ?l)  2 * (1/2)" by (intro mult_mono) simp_all
       with x x_pos have "(c6*c3*(1 - ?l) - 1) * g x  0"
         by (intro mult_nonneg_nonneg g_nonneg) simp_all
       hence "c6 * (1 - ?l) * f_approx x - (c6*c3*(1 - ?l) - 1) * g x 
                  c6 * (1 - ?l) * f_approx x" by (simp add: algebra_simps)
    }
    finally show ?case .
  qed
  also from x c6 have "...  c6 * 1 * f_approx x"
    by (intro mult_left_mono mult_right_mono f_approx_nonneg) simp_all
  finally have "f x  c6 * f_approx x" by simp
  }
  from this and c6(3) show ?thesis by (rule that)
qed

lemma akra_bazzi_bigo:
  "f  O(λx. x powr p *(1 + integral (λu. g u / u powr (p + 1)) x0 x))"
apply (fold f_approx_def, rule akra_bazzi_upper, erule landau_o.bigI)
apply (subst eventually_at_top_linorder, rule exI[of _ x0])
apply (simp add: f_nonneg f_approx_nonneg)
done

end

end