Theory Master_Theorem
section ‹The Master theorem›
theory Master_Theorem
imports
"HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
Akra_Bazzi_Library
Akra_Bazzi
begin
lemma fundamental_theorem_of_calculus_real:
"a ≤ b ⟹ ∀x∈{a..b}. (f has_real_derivative f' x) (at x within {a..b}) ⟹
(f' has_integral (f b - f a)) {a..b}"
by (intro fundamental_theorem_of_calculus ballI)
(simp_all add: has_real_derivative_iff_has_vector_derivative[symmetric])
lemma integral_powr:
"y ≠ -1 ⟹ a ≤ b ⟹ a > 0 ⟹ integral {a..b} (λx. x powr y :: real) =
inverse (y + 1) * (b powr (y + 1) - a powr (y + 1))"
by (subst right_diff_distrib, intro integral_unique fundamental_theorem_of_calculus_real)
(auto intro!: derivative_eq_intros)
lemma integral_ln_powr_over_x:
"y ≠ -1 ⟹ a ≤ b ⟹ a > 1 ⟹ integral {a..b} (λx. ln x powr y / x :: real) =
inverse (y + 1) * (ln b powr (y + 1) - ln a powr (y + 1))"
by (subst right_diff_distrib, intro integral_unique fundamental_theorem_of_calculus_real)
(auto intro!: derivative_eq_intros)
lemma integral_one_over_x_ln_x:
"a ≤ b ⟹ a > 1 ⟹ integral {a..b} (λx. inverse (x * ln x) :: real) = ln (ln b) - ln (ln a)"
by (intro integral_unique fundamental_theorem_of_calculus_real)
(auto intro!: derivative_eq_intros simp: field_simps)
lemma akra_bazzi_integral_kurzweil_henstock:
"akra_bazzi_integral (λf a b. f integrable_on {a..b}) (λf a b. integral {a..b} f)"
apply unfold_locales
apply (rule integrable_const_ivl)
apply simp
apply (erule integrable_subinterval_real, simp)
apply (blast intro!: integral_le)
apply (rule integral_combine, simp_all) []
done
locale master_theorem_function = akra_bazzi_recursion +
fixes g :: "nat ⇒ real"
assumes f_nonneg_base: "x ≥ x⇩0 ⟹ x < x⇩1 ⟹ f x ≥ 0"
and f_rec: "x ≥ x⇩1 ⟹ f x = g x + (∑i<k. as!i * f ((ts!i) x))"
and g_nonneg: "x ≥ x⇩1 ⟹ g x ≥ 0"
and ex_pos_a: "∃a∈set as. a > 0"
begin
interpretation akra_bazzi_integral "λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f"
by (rule akra_bazzi_integral_kurzweil_henstock)
sublocale akra_bazzi_function x⇩0 x⇩1 k as bs ts f "λf a b. f integrable_on {a..b}"
"λf a b. integral {a..b} f" g
using f_nonneg_base f_rec g_nonneg ex_pos_a by unfold_locales
context
begin
private lemma g_nonneg': "eventually (λx. g x ≥ 0) at_top"
using g_nonneg by (force simp: eventually_at_top_linorder)
private lemma g_pos:
assumes "g ∈ Ω(h)"
assumes "eventually (λx. h x > 0) at_top"
shows "eventually (λx. g x > 0) at_top"
proof-
from landau_omega.bigE_nonneg_real[OF assms(1) g_nonneg'] guess c . note c = this
from assms(2) c(2) show ?thesis
by eventually_elim (rule less_le_trans[OF mult_pos_pos[OF c(1)]], simp_all)
qed
private lemma f_pos:
assumes "g ∈ Ω(h)"
assumes "eventually (λx. h x > 0) at_top"
shows "eventually (λx. f x > 0) at_top"
using g_pos[OF assms(1,2)] eventually_ge_at_top[of x⇩1]
by (eventually_elim) (subst f_rec, insert step_ge_x0,
auto intro!: add_pos_nonneg sum_nonneg mult_nonneg_nonneg[OF a_ge_0] f_nonneg)
lemma bs_lower_bound: "∃C>0. ∀b∈set bs. C < b"
proof (intro exI conjI ballI)
from b_pos show A: "Min (set bs) / 2 > 0" by auto
fix b assume b: "b ∈ set bs"
from A have "Min (set bs) / 2 < Min (set bs)" by simp
also from b have "... ≤ b" by simp
finally show "Min (set bs) / 2 < b" .
qed
private lemma powr_growth2:
"∃C c2. 0 < c2 ∧ C < Min (set bs) ∧
eventually (λx. ∀u∈{C * x..x}. c2 * x powr p' ≥ u powr p') at_top"
proof (intro exI conjI allI ballI)
define C where "C = Min (set bs) / 2"
from b_bounds bs_nonempty have C_pos: "C > 0" unfolding C_def by auto
thus "C < Min (set bs)" unfolding C_def by simp
show "max (C powr p') 1 > 0" by simp
show "eventually (λx. ∀u∈{C * x..x}.
max ((Min (set bs)/2) powr p') 1 * x powr p' ≥ u powr p') at_top"
using eventually_gt_at_top[of "0::real"] apply eventually_elim
proof clarify
fix x u assume x: "x > 0" and "u ∈ {C*x..x}"
hence u: "u ≥ C*x" "u ≤ x" unfolding C_def by simp_all
from u have "u powr p' ≤ max ((C*x) powr p') (x powr p')" using C_pos x
by (intro powr_upper_bound mult_pos_pos) simp_all
also from u x C_pos have "max ((C*x) powr p') (x powr p') = x powr p' * max (C powr p') 1"
by (subst max_mult_left) (simp_all add: powr_mult algebra_simps)
finally show "u powr p' ≤ max ((Min (set bs)/2) powr p') 1 * x powr p'"
by (simp add: C_def algebra_simps)
qed
qed
private lemma powr_growth1:
"∃C c1. 0 < c1 ∧ C < Min (set bs) ∧
eventually (λx. ∀u∈{C * x..x}. c1 * x powr p' ≤ u powr p') at_top"
proof (intro exI conjI allI ballI)
define C where "C = Min (set bs) / 2"
from b_bounds bs_nonempty have C_pos: "C > 0" unfolding C_def by auto
thus "C < Min (set bs)" unfolding C_def by simp
from C_pos show "min (C powr p') 1 > 0" by simp
show "eventually (λx. ∀u∈{C * x..x}.
min ((Min (set bs)/2) powr p') 1 * x powr p' ≤ u powr p') at_top"
using eventually_gt_at_top[of "0::real"] apply eventually_elim
proof clarify
fix x u assume x: "x > 0" and "u ∈ {C*x..x}"
hence u: "u ≥ C*x" "u ≤ x" unfolding C_def by simp_all
from u x C_pos have "x powr p' * min (C powr p') 1 = min ((C*x) powr p') (x powr p')"
by (subst min_mult_left) (simp_all add: powr_mult algebra_simps)
also from u have "u powr p' ≥ min ((C*x) powr p') (x powr p')" using C_pos x
by (intro powr_lower_bound mult_pos_pos) simp_all
finally show "u powr p' ≥ min ((Min (set bs)/2) powr p') 1 * x powr p'"
by (simp add: C_def algebra_simps)
qed
qed
private lemma powr_ln_powr_lower_bound:
"a > 1 ⟹ a ≤ x ⟹ x ≤ b ⟹
min (a powr p) (b powr p) * min (ln a powr p') (ln b powr p') ≤ x powr p * ln x powr p'"
by (intro mult_mono powr_lower_bound) (auto intro: min.coboundedI1)
private lemma powr_ln_powr_upper_bound:
"a > 1 ⟹ a ≤ x ⟹ x ≤ b ⟹
max (a powr p) (b powr p) * max (ln a powr p') (ln b powr p') ≥ x powr p * ln x powr p'"
by (intro mult_mono powr_upper_bound) (auto intro: max.coboundedI1)
private lemma powr_ln_powr_upper_bound':
"eventually (λa. ∀b>a. ∃c. ∀x∈{a..b}. x powr p * ln x powr p' ≤ c) at_top"
by (subst eventually_at_top_dense) (force intro: powr_ln_powr_upper_bound)
private lemma powr_upper_bound':
"eventually (λa::real. ∀b>a. ∃c. ∀x∈{a..b}. x powr p' ≤ c) at_top"
by (subst eventually_at_top_dense) (force intro: powr_upper_bound)
lemmas bounds =
powr_ln_powr_lower_bound powr_ln_powr_upper_bound powr_ln_powr_upper_bound' powr_upper_bound'
private lemma eventually_ln_const:
assumes "(C::real) > 0"
shows "eventually (λx. ln (C*x) / ln x > 1/2) at_top"
proof-
from tendstoD[OF tendsto_ln_over_ln[of C 1], of "1/2"] assms
have "eventually (λx. ¦ln (C*x) / ln x - 1¦ < 1/2) at_top" by (simp add: dist_real_def)
thus ?thesis by eventually_elim linarith
qed
private lemma powr_ln_powr_growth1: "∃C c1. 0 < c1 ∧ C < Min (set bs) ∧
eventually (λx. ∀u∈{C * x..x}. c1 * (x powr r * ln x powr r') ≤ u powr r * ln u powr r') at_top"
proof (intro exI conjI)
let ?C = "Min (set bs) / 2" and ?f = "λx. x powr r * ln x powr r'"
define C where "C = ?C"
from b_bounds have C_pos: "C > 0" unfolding C_def by simp
let ?T = "min (C powr r) (1 powr r) * min ((1/2) powr r') (1 powr r')"
from C_pos show "?T > 0" unfolding min_def by (auto split: if_split)
from bs_nonempty b_bounds have C_pos: "C > 0" unfolding C_def by simp
thus "C < Min (set bs)" by (simp add: C_def)
show "eventually (λx. ∀u∈{C*x..x}. ?T * ?f x ≤ ?f u) at_top"
using eventually_gt_at_top[of "max 1 (inverse C)"] eventually_ln_const[OF C_pos]
apply eventually_elim
proof clarify
fix x u assume x: "x > max 1 (inverse C)" and u: "u ∈ {C*x..x}"
hence x': "x > 1" by (simp add: field_simps)
with C_pos have x_pos: "x > 0" by (simp add: field_simps)
from x u C_pos have u': "u > 1" by (simp add: field_simps)
assume A: "ln (C*x) / ln x > 1/2"
have "min (C powr r) (1 powr r) ≤ (u/x) powr r"
using x u u' C_pos by (intro powr_lower_bound) (simp_all add: field_simps)
moreover {
note A
also from C_pos x' u u' have "ln (C*x) ≤ ln u" by (subst ln_le_cancel_iff) simp_all
with x' have "ln (C*x) / ln x ≤ ln u / ln x" by (simp add: field_simps)
finally have "min ((1/2) powr r') (1 powr r') ≤ (ln u / ln x) powr r'"
using x u u' C_pos A by (intro powr_lower_bound) simp_all
}
ultimately have "?T ≤ (u/x) powr r * (ln u / ln x) powr r'"
using x_pos by (intro mult_mono) simp_all
also from x u u' have "... = ?f u / ?f x" by (simp add: powr_divide)
finally show "?T * ?f x ≤ ?f u" using x' by (simp add: field_simps)
qed
qed
private lemma powr_ln_powr_growth2: "∃C c1. 0 < c1 ∧ C < Min (set bs) ∧
eventually (λx. ∀u∈{C * x..x}. c1 * (x powr r * ln x powr r') ≥ u powr r * ln u powr r') at_top"
proof (intro exI conjI)
let ?C = "Min (set bs) / 2" and ?f = "λx. x powr r * ln x powr r'"
define C where "C = ?C"
let ?T = "max (C powr r) (1 powr r) * max ((1/2) powr r') (1 powr r')"
show "?T > 0" by simp
from b_bounds bs_nonempty have C_pos: "C > 0" unfolding C_def by simp
thus "C < Min (set bs)" by (simp add: C_def)
show "eventually (λx. ∀u∈{C*x..x}. ?T * ?f x ≥ ?f u) at_top"
using eventually_gt_at_top[of "max 1 (inverse C)"] eventually_ln_const[OF C_pos]
apply eventually_elim
proof clarify
fix x u assume x: "x > max 1 (inverse C)" and u: "u ∈ {C*x..x}"
hence x': "x > 1" by (simp add: field_simps)
with C_pos have x_pos: "x > 0" by (simp add: field_simps)
from x u C_pos have u': "u > 1" by (simp add: field_simps)
assume A: "ln (C*x) / ln x > 1/2"
from x u u' have "?f u / ?f x = (u/x) powr r * (ln u/ln x) powr r'" by (simp add: powr_divide)
also {
have "(u/x) powr r ≤ max (C powr r) (1 powr r)"
using x u u' C_pos by (intro powr_upper_bound) (simp_all add: field_simps)
moreover {
note A
also from C_pos x' u u' have "ln (C*x) ≤ ln u" by (subst ln_le_cancel_iff) simp_all
with x' have "ln (C*x) / ln x ≤ ln u / ln x" by (simp add: field_simps)
finally have "(ln u / ln x) powr r' ≤ max ((1/2) powr r') (1 powr r')"
using x u u' C_pos A by (intro powr_upper_bound) simp_all
} ultimately have "(u/x) powr r * (ln u / ln x) powr r' ≤ ?T"
using x_pos by (intro mult_mono) simp_all
}
finally show "?T * ?f x ≥ ?f u" using x' by (simp add: field_simps)
qed
qed
lemmas growths = powr_growth1 powr_growth2 powr_ln_powr_growth1 powr_ln_powr_growth2
private lemma master_integrable:
"∃a::real. ∀b≥a. (λu. u powr r * ln u powr s / u powr t) integrable_on {a..b}"
"∃a::real. ∀b≥a. (λu. u powr r / u powr s) integrable_on {a..b}"
by (rule exI[of _ 2], force intro!: integrable_continuous_real continuous_intros)+
private lemma master_integral:
fixes a p p' :: real
assumes p: "p ≠ p'" and a: "a > 0"
obtains c d where "c ≠ 0" "p > p' ⟶ d ≠ 0"
"(λx::nat. x powr p * (1 + integral {a..x} (λu. u powr p' / u powr (p+1)))) ∈
Θ(λx::nat. d * x powr p + c * x powr p')"
proof-
define e where "e = a powr (p' - p)"
from assms have e: "e ≥ 0" by (simp add: e_def)
define c where "c = inverse (p' - p)"
define d where "d = 1 - inverse (p' - p) * e"
have "c ≠ 0" and "p > p' ⟶ d ≠ 0"
using e p a unfolding c_def d_def by (auto simp: field_simps)
thus ?thesis
apply (rule that) apply (rule bigtheta_real_nat_transfer, rule bigthetaI_cong)
using eventually_ge_at_top[of a]
proof eventually_elim
fix x assume x: "x ≥ a"
hence "integral {a..x} (λu. u powr p' / u powr (p+1)) =
integral {a..x} (λu. u powr (p' - (p + 1)))"
by (intro Henstock_Kurzweil_Integration.integral_cong) (simp_all add: powr_diff [symmetric] )
also have "... = inverse (p' - p) * (x powr (p' - p) - a powr (p' - p))"
using p x0_less_x1 a x by (simp add: integral_powr)
also have "x powr p * (1 + ...) = d * x powr p + c * x powr p'"
using p unfolding c_def d_def by (simp add: algebra_simps powr_diff e_def)
finally show "x powr p * (1 + integral {a..x} (λu. u powr p' / u powr (p+1))) =
d * x powr p + c * x powr p'" .
qed
qed
private lemma master_integral':
fixes a p p' :: real
assumes p': "p' ≠ 0" and a: "a > 1"
obtains c d :: real where "p' < 0 ⟶ c ≠ 0" "d ≠ 0"
"(λx::nat. x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr (p'-1) / u powr (p+1)))) ∈
Θ(λx::nat. c * x powr p + d * x powr p * ln x powr p')"
proof-
define e where "e = ln a powr p'"
from assms have e: "e > 0" by (simp add: e_def)
define c where "c = 1 - inverse p' * e"
define d where "d = inverse p'"
from assms e have "p' < 0 ⟶ c ≠ 0" "d ≠ 0" unfolding c_def d_def by (auto simp: field_simps)
thus ?thesis
apply (rule that) apply (rule landau_real_nat_transfer, rule bigthetaI_cong)
using eventually_ge_at_top[of a]
proof eventually_elim
fix x :: real assume x: "x ≥ a"
have "integral {a..x} (λu. u powr p * ln u powr (p' - 1) / u powr (p + 1)) =
integral {a..x} (λu. ln u powr (p' - 1) / u)" using x a x0_less_x1
by (intro Henstock_Kurzweil_Integration.integral_cong) (simp_all add: powr_add)
also have "... = inverse p' * (ln x powr p' - ln a powr p')"
using p' x0_less_x1 a(1) x by (simp add: integral_ln_powr_over_x)
also have "x powr p * (1 + ...) = c * x powr p + d * x powr p * ln x powr p'"
using p' by (simp add: algebra_simps c_def d_def e_def)
finally show "x powr p * (1+integral {a..x} (λu. u powr p * ln u powr (p'-1) / u powr (p+1))) =
c * x powr p + d * x powr p * ln x powr p'" .
qed
qed
private lemma master_integral'':
fixes a p p' :: real
assumes a: "a > 1"
shows "(λx::nat. x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr - 1/u powr (p+1)))) ∈
Θ(λx::nat. x powr p * ln (ln x))"
proof (rule landau_real_nat_transfer)
have "(λx::real. x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr - 1/u powr (p+1)))) ∈
Θ(λx::real. (1 - ln (ln a)) * x powr p + x powr p * ln (ln x))" (is "?f ∈ _")
apply (rule bigthetaI_cong) using eventually_ge_at_top[of a]
proof eventually_elim
fix x assume x: "x ≥ a"
have "integral {a..x} (λu. u powr p * ln u powr -1 / u powr (p + 1)) =
integral {a..x} (λu. inverse (u * ln u))" using x a x0_less_x1
by (intro Henstock_Kurzweil_Integration.integral_cong) (simp_all add: powr_add powr_minus field_simps)
also have "... = ln (ln x) - ln (ln a)"
using x0_less_x1 a(1) x by (subst integral_one_over_x_ln_x) simp_all
also have "x powr p * (1 + ...) = (1 - ln (ln a)) * x powr p + x powr p * ln (ln x)"
by (simp add: algebra_simps)
finally show "x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr - 1 / u powr (p+1))) =
(1 - ln (ln a)) * x powr p + x powr p * ln (ln x)" .
qed
also have "(λx. (1 - ln (ln a)) * x powr p + x powr p * ln (ln x)) ∈
Θ(λx. x powr p * ln (ln x))" by simp
finally show "?f ∈ Θ(λa. a powr p * ln (ln a))" .
qed
lemma master1_bigo:
assumes g_bigo: "g ∈ O(λx. real x powr p')"
assumes less_p': "(∑i<k. as!i * bs!i powr p') > 1"
shows "f ∈ O(λx. real x powr p)"
proof-
interpret akra_bazzi_upper x⇩0 x⇩1 k as bs ts f
"λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p'"
using assms growths g_bigo master_integrable by unfold_locales (assumption | simp)+
from less_p' have less_p: "p' < p" by (rule p_greaterI)
from bigo_f[of "0"] guess a . note a = this
note a(2)
also from a(1) less_p x0_less_x1 have "p ≠ p'" by simp_all
from master_integral[OF this a(1)] guess c d . note cd = this
note cd(3)
also from cd(1,2) less_p
have "(λx::nat. d * real x powr p + c * real x powr p') ∈ Θ(λx. real x powr p)" by force
finally show "f ∈ O(λx::nat. x powr p)" .
qed
lemma master1:
assumes g_bigo: "g ∈ O(λx. real x powr p')"
assumes less_p': "(∑i<k. as!i * bs!i powr p') > 1"
assumes f_pos: "eventually (λx. f x > 0) at_top"
shows "f ∈ Θ(λx. real x powr p)"
proof (rule bigthetaI)
interpret akra_bazzi_lower x⇩0 x⇩1 k as bs ts f
"λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λ_. 0"
using assms(1,3) bs_lower_bound by unfold_locales (auto intro: always_eventually)
from bigomega_f show "f ∈ Ω(λx. real x powr p)" by force
qed (fact master1_bigo[OF g_bigo less_p'])
lemma master2_3:
assumes g_bigtheta: "g ∈ Θ(λx. real x powr p * ln (real x) powr (p' - 1))"
assumes p': "p' > 0"
shows "f ∈ Θ(λx. real x powr p * ln (real x) powr p')"
proof-
have "eventually (λx::real. x powr p * ln x powr (p' - 1) > 0) at_top"
using eventually_gt_at_top[of "1::real"] by eventually_elim simp
hence "eventually (λx. f x > 0) at_top"
by (rule f_pos[OF bigthetaD2[OF g_bigtheta] eventually_nat_real])
then interpret akra_bazzi x⇩0 x⇩1 k as bs ts f
"λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p * ln x powr (p' - 1)"
using assms growths bounds master_integrable by unfold_locales (assumption | simp)+
from bigtheta_f[of "1"] guess a . note a = this
note a(2)
also from a(1) p' have "p' ≠ 0" by simp_all
from master_integral'[OF this a(1), of p] guess c d . note cd = this
note cd(3)
also have "(λx::nat. c * real x powr p + d * real x powr p * ln (real x) powr p') ∈
Θ(λx::nat. x powr p * ln x powr p')" using cd(1,2) p' by force
finally show "f ∈ Θ(λx. real x powr p * ln (real x) powr p')" .
qed
lemma master2_1:
assumes g_bigtheta: "g ∈ Θ(λx. real x powr p * ln (real x) powr p')"
assumes p': "p' < -1"
shows "f ∈ Θ(λx. real x powr p)"
proof-
have "eventually (λx::real. x powr p * ln x powr p' > 0) at_top"
using eventually_gt_at_top[of "1::real"] by eventually_elim simp
hence "eventually (λx. f x > 0) at_top"
by (rule f_pos[OF bigthetaD2[OF g_bigtheta] eventually_nat_real])
then interpret akra_bazzi x⇩0 x⇩1 k as bs ts f
"λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p * ln x powr p'"
using assms growths bounds master_integrable by unfold_locales (assumption | simp)+
from bigtheta_f[of "1"] guess a . note a = this
note a(2)
also from a(1) p' have A: "p' + 1 ≠ 0" by simp_all
obtain c d :: real where cd: "c ≠ 0" "d ≠ 0" and
"(λx::nat. x powr p * (1 + integral {a..x} (λu. u powr p * ln u powr p'/ u powr (p+1)))) ∈
Θ(λx::nat. c * x powr p + d * x powr p * ln x powr (p' + 1))"
by (rule master_integral'[OF A a(1), of p]) (insert p', simp)
note this(3)
also have "(λx::nat. c * real x powr p + d * real x powr p * ln (real x) powr (p' + 1)) ∈
Θ(λx::nat. x powr p)" using cd(1,2) p' by force
finally show "f ∈ Θ(λx::nat. x powr p)" .
qed
lemma master2_2:
assumes g_bigtheta: "g ∈ Θ(λx. real x powr p / ln (real x))"
shows "f ∈ Θ(λx. real x powr p * ln (ln (real x)))"
proof-
have "eventually (λx::real. x powr p / ln x > 0) at_top"
using eventually_gt_at_top[of "1::real"] by eventually_elim simp
hence "eventually (λx. f x > 0) at_top"
by (rule f_pos[OF bigthetaD2[OF g_bigtheta] eventually_nat_real])
moreover from g_bigtheta have g_bigtheta': "g ∈ Θ(λx. real x powr p * ln (real x) powr -1)"
by (rule landau_theta.trans, intro landau_real_nat_transfer) simp
ultimately interpret akra_bazzi x⇩0 x⇩1 k as bs ts f
"λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p * ln x powr -1"
using assms growths bounds master_integrable by unfold_locales (assumption | simp)+
from bigtheta_f[of 1] guess a . note a = this
note a(2)
also note master_integral''[OF a(1)]
finally show "f ∈ Θ(λx::nat. x powr p * ln (ln x))" .
qed
lemma master3:
assumes g_bigtheta: "g ∈ Θ(λx. real x powr p')"
assumes p'_greater': "(∑i<k. as!i * bs!i powr p') < 1"
shows "f ∈ Θ(λx. real x powr p')"
proof-
have "eventually (λx::real. x powr p' > 0) at_top"
using eventually_gt_at_top[of "1::real"] by eventually_elim simp
hence "eventually (λx. f x > 0) at_top"
by (rule f_pos[OF bigthetaD2[OF g_bigtheta] eventually_nat_real])
then interpret akra_bazzi x⇩0 x⇩1 k as bs ts f
"λf a b. f integrable_on {a..b}" "λf a b. integral {a..b} f" g "λx. x powr p'"
using assms growths bounds master_integrable by unfold_locales (assumption | simp)+
from p'_greater' have p'_greater: "p' > p" by (rule p_lessI)
from bigtheta_f[of 0] guess a . note a = this
note a(2)
also from p'_greater have "p ≠ p'" by simp
from master_integral[OF this a(1)] guess c d . note cd = this
note cd(3)
also have "(λx::nat. d * x powr p + c * x powr p') ∈ Θ(λx::real. x powr p')"
using p'_greater cd(1,2) by force
finally show "f ∈ Θ(λx. real x powr p')" .
qed
end
end
end