Theory Akra_Bazzi.Akra_Bazzi_Asymptotics
section ‹Asymptotic bounds›
theory Akra_Bazzi_Asymptotics
imports
Complex_Main
Akra_Bazzi_Library
"HOL-Library.Landau_Symbols"
begin
locale akra_bazzi_asymptotics_bep =
fixes b e p hb :: real
assumes bep: "b > 0" "b < 1" "e > 0" "hb > 0"
begin
context
begin
text ‹
Functions that are negligible w.r.t. @{term "ln (b*x) powr (e/2 + 1)"}.
›
private abbreviation (input) negl :: "(real ⇒ real) ⇒ bool" where
"negl f ≡ f ∈ o(λx. ln (b*x) powr (-(e/2 + 1)))"
private lemma neglD: "negl f ⟹ c > 0 ⟹ eventually (λx. ¦f x¦ ≤ c / ln (b*x) powr (e/2+1)) at_top"
by (drule (1) landau_o.smallD, subst (asm) powr_minus) (simp add: field_simps)
private lemma negl_mult: "negl f ⟹ negl g ⟹ negl (λx. f x * g x)"
by (erule landau_o.small_1_mult, rule landau_o.small_imp_big, erule landau_o.small_trans)
(insert bep, simp)
private lemma ev4:
assumes g: "negl g"
shows "eventually (λx. ln (b*x) powr (-e/2) - ln x powr (-e/2) ≥ g x) at_top"
proof (rule smallo_imp_le_real)
define h1 where [abs_def]:
"h1 x = (1 + ln b/ln x) powr (-e/2) - 1 + e/2 * (ln b/ln x)" for x
define h2 where [abs_def]:
"h2 x = ln x powr (- e / 2) * ((1 + ln b / ln x) powr (- e / 2) - 1)" for x
from bep have "((λx. ln b / ln x) ⤏ 0) at_top"
by (simp add: tendsto_0_smallo_1)
note one_plus_x_powr_Taylor2_bigo[OF this, of "-e/2"]
also have "(λx. (1 + ln b / ln x) powr (- e / 2) - 1 - - e / 2 * (ln b / ln x)) = h1"
by (simp add: h1_def)
finally have "h1 ∈ o(λx. 1 / ln x)"
by (rule landau_o.big_small_trans) (insert bep, simp add: power2_eq_square)
with bep have "(λx. h1 x - e/2 * (ln b / ln x)) ∈ Θ(λx. 1 / ln x)" by simp
also have "(λx. h1 x - e/2 * (ln b/ln x)) = (λx. (1 + ln b/ ln x) powr (-e/2) - 1)"
by (rule ext) (simp add: h1_def)
finally have "h2 ∈ Θ(λx. ln x powr (-e/2) * (1 / ln x))" unfolding h2_def
by (intro landau_theta.mult) simp_all
also have "(λx. ln x powr (-e/2) * (1 / ln x)) ∈ Θ(λx. ln x powr (-(e/2+1)))" by simp
also from g bep have "(λx. ln x powr (-(e/2+1))) ∈ ω(g)" by (simp add: smallomega_iff_smallo)
finally have "g ∈ o(h2)" by (simp add: smallomega_iff_smallo)
also have "eventually (λx. h2 x = ln (b*x) powr (-e/2) - ln x powr (-e/2)) at_top"
using eventually_gt_at_top[of "1::real"] eventually_gt_at_top[of "1/b"]
by eventually_elim (use bep in ‹simp add: ln_mult powr_diff h2_def powr_minus powr_divide field_simps›)
hence "h2 ∈ Θ(λx. ln (b*x) powr (-e/2) - ln x powr (-e/2))" by (rule bigthetaI_cong)
finally show "g ∈ o(λx. ln (b * x) powr (- e / 2) - ln x powr (- e / 2))" .
next
show "eventually (λx. ln (b*x) powr (-e/2) - ln x powr (-e/2) ≥ 0) at_top"
using eventually_gt_at_top[of "1/b"] eventually_gt_at_top[of "1::real"]
by eventually_elim (use bep in ‹auto intro!: powr_mono2' simp: field_simps simp flip: ln_mult›)
qed
private lemma ev1:
"negl (λx. (1 + c * inverse b * ln x powr (-(1+e))) powr p - 1)"
proof-
from bep have "((λx. c * inverse b * ln x powr (-(1+e))) ⤏ 0) at_top"
by (simp add: tendsto_0_smallo_1)
have "(λx. (1 + c * inverse b * ln x powr (-(1+e))) powr p - 1)
∈ O(λx. c * inverse b * ln x powr - (1 + e))"
using bep by (intro one_plus_x_powr_Taylor1_bigo) (simp add: tendsto_0_smallo_1)
also from bep have "negl (λx. c * inverse b * ln x powr - (1 + e))" by simp
finally show ?thesis .
qed
private lemma ev2_aux:
defines "f ≡ λx. (1 + 1/ln (b*x) * ln (1 + hb / b * ln x powr (-1-e))) powr (-e/2)"
obtains h where "eventually (λx. f x ≥ 1 + h x) at_top" "h ∈ o(λx. 1 / ln x)"
proof (rule that[of "λx. f x - 1"])
define g where [abs_def]: "g x = 1/ln (b*x) * ln (1 + hb / b * ln x powr (-1-e))" for x
have lim: "((λx. ln (1 + hb / b * ln x powr (- 1 - e))) ⤏ 0) at_top"
by (rule tendsto_eq_rhs[OF tendsto_ln[OF tendsto_add[OF tendsto_const, of _ 0]]])
(insert bep, simp_all add: tendsto_0_smallo_1)
hence lim': "(g ⤏ 0) at_top" unfolding g_def
by (intro tendsto_mult_zero) (insert bep, simp add: tendsto_0_smallo_1)
from one_plus_x_powr_Taylor2_bigo[OF this, of "-e/2"]
have "(λx. (1 + g x) powr (-e/2) - 1 - - e/2 * g x) ∈ O(λx. (g x)⇧2)" .
also from lim' have "(λx. g x ^ 2) ∈ o(λx. g x * 1)" unfolding power2_eq_square
by (intro landau_o.big_small_mult smalloI_tendsto) simp_all
also have "o(λx. g x * 1) = o(g)" by simp
also have "(λx. (1 + g x) powr (-e/2) - 1 - - e/2 * g x) = (λx. f x - 1 + e/2 * g x)"
by (simp add: f_def g_def)
finally have A: "(λx. f x - 1 + e / 2 * g x) ∈ O(g)" by (rule landau_o.small_imp_big)
hence "(λx. f x - 1 + e/2 * g x - e/2 * g x) ∈ O(g)"
by (rule sum_in_bigo) (insert bep, simp)
also have "(λx. f x - 1 + e/2 * g x - e/2 * g x) = (λx. f x - 1)" by simp
finally have "(λx. f x - 1) ∈ O(g)" .
also from bep lim have "g ∈ o(λx. 1 / ln x)" unfolding g_def
by (auto intro!: smallo_1_tendsto_0)
finally show "(λx. f x - 1) ∈ o(λx. 1 / ln x)" .
qed simp_all
private lemma ev2:
defines "f ≡ λx. ln (b * x + hb * x / ln x powr (1 + e)) powr (-e/2)"
obtains h where
"negl h"
"eventually (λx. f x ≥ ln (b * x) powr (-e/2) + h x) at_top"
"eventually (λx. ¦ln (b * x) powr (-e/2) + h x¦ < 1) at_top"
proof -
define f'
where "f' x = (1 + 1 / ln (b*x) * ln (1 + hb / b * ln x powr (-1-e))) powr (-e/2)" for x
from ev2_aux obtain g where g: "eventually (λx. 1 + g x ≤ f' x) at_top" "g ∈ o(λx. 1 / ln x)"
unfolding f'_def .
define h where [abs_def]: "h x = ln (b*x) powr (-e/2) * g x" for x
show ?thesis
proof (rule that[of h])
from bep g show "negl h" unfolding h_def
by (auto simp: powr_diff elim: landau_o.small_big_trans)
next
from g(2) have "g ∈ o(λx. 1)" by (rule landau_o.small_big_trans) simp
with bep have "eventually (λx. ¦ln (b*x) powr (-e/2) * (1 + g x)¦ < 1) at_top"
by (intro smallo_imp_abs_less_real) simp_all
thus "eventually (λx. ¦ln (b*x) powr (-e/2) + h x¦ < 1) at_top"
by (simp add: algebra_simps h_def)
next
from eventually_gt_at_top[of "1/b"] and g(1)
show "eventually (λx. f x ≥ ln (b*x) powr (-e/2) + h x) at_top"
proof eventually_elim
case (elim x)
from bep have "b * x + hb * x / ln x powr (1 + e) = b*x * (1 + hb / b * ln x powr (-1 - e))"
by (simp add: field_simps powr_diff powr_add powr_minus)
also from elim(1) bep
have "ln … = ln (b*x) * (1 + 1/ln (b*x) * ln (1 + hb / b * ln x powr (-1-e)))"
by (subst ln_mult_pos) (simp_all add: add_pos_nonneg field_simps)
also from elim(1) bep have "… powr (-e/2) = ln (b*x) powr (-e/2) * f' x"
by (subst powr_mult) (simp_all add: field_simps f'_def)
also from elim have "… ≥ ln (b*x) powr (-e/2) * (1 + g x)"
by (intro mult_left_mono) simp_all
finally show "f x ≥ ln (b*x) powr (-e/2) + h x"
by (simp add: f_def h_def algebra_simps)
qed
qed
qed
private lemma ev21:
obtains g where
"negl g"
"eventually (λx. 1 + ln (b * x + hb * x / ln x powr (1 + e)) powr (-e/2) ≥
1 + ln (b * x) powr (-e/2) + g x) at_top"
"eventually (λx. 1 + ln (b * x) powr (-e/2) + g x > 0) at_top"
proof-
from ev2 guess g . note g = this
from g(3) have "eventually (λx. 1 + ln (b * x) powr (-e/2) + g x > 0) at_top"
by eventually_elim simp
with g(1,2) show ?thesis by (intro that[of g]) simp_all
qed
private lemma ev22:
obtains g where
"negl g"
"eventually (λx. 1 - ln (b * x + hb * x / ln x powr (1 + e)) powr (-e/2) ≤
1 - ln (b * x) powr (-e/2) - g x) at_top"
"eventually (λx. 1 - ln (b * x) powr (-e/2) - g x > 0) at_top"
proof-
from ev2 guess g . note g = this
from g(2) have "eventually (λx. 1 - ln (b * x + hb * x / ln x powr (1 + e)) powr (-e/2) ≤
1 - ln (b * x) powr (-e/2) - g x) at_top"
by eventually_elim simp
moreover from g(3) have "eventually (λx. 1 - ln (b * x) powr (-e/2) - g x > 0) at_top"
by eventually_elim simp
ultimately show ?thesis using g(1) by (intro that[of g]) simp_all
qed
lemma asymptotics1:
shows "eventually (λx.
(1 + c * inverse b * ln x powr -(1+e)) powr p *
(1 + ln (b * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) ≥
1 + (ln x powr (-e/2))) at_top"
proof-
let ?f = "λx. (1 + c * inverse b * ln x powr -(1+e)) powr p"
let ?g = "λx. 1 + ln (b * x + hb * x / ln x powr (1 + e)) powr (- e / 2)"
define f where [abs_def]: "f x = 1 - ?f x" for x
from ev1[of c] have "negl f" unfolding f_def
by (subst landau_o.small.uminus_in_iff [symmetric]) simp
from landau_o.smallD[OF this zero_less_one]
have f: "eventually (λx. f x ≤ ln (b*x) powr -(e/2+1)) at_top"
by eventually_elim (simp add: f_def)
from ev21 guess g . note g = this
define h where [abs_def]: "h x = -g x + f x + f x * ln (b*x) powr (-e/2) + f x * g x" for x
have A: "eventually (λx. ?f x * ?g x ≥ 1 + ln (b*x) powr (-e/2) - h x) at_top"
using g(2,3) f
proof eventually_elim
case (elim x)
let ?t = "ln (b*x) powr (-e/2)"
have "1 + ?t - h x = (1 - f x) * (1 + ln (b*x) powr (-e/2) + g x)"
by (simp add: algebra_simps h_def)
also from elim have "?f x * ?g x ≥ (1 - f x) * (1 + ln (b*x) powr (-e/2) + g x)"
by (intro mult_mono[OF _ elim(1)]) (simp_all add: algebra_simps f_def)
finally show "?f x * ?g x ≥ 1 + ln (b*x) powr (-e/2) - h x" .
qed
from bep ‹negl f› g(1) have "negl h" unfolding h_def
by (fastforce intro!: sum_in_smallo landau_o.small.mult simp: powr_diff
intro: landau_o.small_trans)+
from ev4[OF this] A show ?thesis by eventually_elim simp
qed
lemma asymptotics2:
shows "eventually (λx.
(1 + c * inverse b * ln x powr -(1+e)) powr p *
(1 - ln (b * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) ≤
1 - (ln x powr (-e/2))) at_top"
proof-
let ?f = "λx. (1 + c * inverse b * ln x powr -(1+e)) powr p"
let ?g = "λx. 1 - ln (b * x + hb * x / ln x powr (1 + e)) powr (- e / 2)"
define f where [abs_def]: "f x = 1 - ?f x" for x
from ev1[of c] have "negl f" unfolding f_def
by (subst landau_o.small.uminus_in_iff [symmetric]) simp
from landau_o.smallD[OF this zero_less_one]
have f: "eventually (λx. f x ≤ ln (b*x) powr -(e/2+1)) at_top"
by eventually_elim (simp add: f_def)
from ev22 guess g . note g = this
define h where [abs_def]: "h x = -g x - f x + f x * ln (b*x) powr (-e/2) + f x * g x" for x
have "((λx. ln (b * x + hb * x / ln x powr (1 + e)) powr - (e / 2)) ⤏ 0) at_top"
apply (insert bep, intro tendsto_neg_powr, simp)
apply (rule filterlim_compose[OF ln_at_top])
apply (rule filterlim_at_top_smallomega_1, simp)
using eventually_gt_at_top[of "max 1 (1/b)"]
apply (auto elim!: eventually_mono intro!: add_pos_nonneg simp: field_simps)
apply (smt (z3) divide_nonneg_nonneg mult_neg_pos mult_nonneg_nonneg powr_non_neg)
done
hence ev_g: "eventually (λx. ¦1 - ?g x¦ < 1) at_top"
by (intro smallo_imp_abs_less_real smalloI_tendsto) simp_all
have A: "eventually (λx. ?f x * ?g x ≤ 1 - ln (b*x) powr (-e/2) + h x) at_top"
using g(2,3) ev_g f
proof eventually_elim
case (elim x)
let ?t = "ln (b*x) powr (-e/2)"
from elim have "?f x * ?g x ≤ (1 - f x) * (1 - ln (b*x) powr (-e/2) - g x)"
by (intro mult_mono) (simp_all add: f_def)
also have "... = 1 - ?t + h x" by (simp add: algebra_simps h_def)
finally show "?f x * ?g x ≤ 1 - ln (b*x) powr (-e/2) + h x" .
qed
from bep ‹negl f› g(1) have "negl h" unfolding h_def
by (fastforce intro!: sum_in_smallo landau_o.small.mult simp: powr_diff
intro: landau_o.small_trans)+
from ev4[OF this] A show ?thesis by eventually_elim simp
qed
lemma asymptotics3: "eventually (λx. (1 + (ln x powr (-e/2))) / 2 ≤ 1) at_top"
(is "eventually (λx. ?f x ≤ 1) _")
proof (rule eventually_mp[OF always_eventually], clarify)
from bep have "(?f ⤏ 1/2) at_top"
by (force intro: tendsto_eq_intros tendsto_neg_powr ln_at_top)
hence "⋀e. e>0 ⟹ eventually (λx. ¦?f x - 0.5¦ < e) at_top"
by (subst (asm) tendsto_iff) (simp add: dist_real_def)
from this[of "0.5"] show "eventually (λx. ¦?f x - 0.5¦ < 0.5) at_top" by simp
fix x assume "¦?f x - 0.5¦ < 0.5"
thus "?f x ≤ 1" by simp
qed
lemma asymptotics4: "eventually (λx. (1 - (ln x powr (-e/2))) * 2 ≥ 1) at_top"
(is "eventually (λx. ?f x ≥ 1) _")
proof (rule eventually_mp[OF always_eventually], clarify)
from bep have "(?f ⤏ 2) at_top"
by (force intro: tendsto_eq_intros tendsto_neg_powr ln_at_top)
hence "⋀e. e>0 ⟹ eventually (λx. ¦?f x - 2¦ < e) at_top"
by (subst (asm) tendsto_iff) (simp add: dist_real_def)
from this[of 1] show "eventually (λx. ¦?f x - 2¦ < 1) at_top" by simp
fix x assume "¦?f x - 2¦ < 1"
thus "?f x ≥ 1" by simp
qed
lemma asymptotics5: "eventually (λx. ln (b*x - hb*x*ln x powr -(1+e)) powr (-e/2) < 1) at_top"
proof-
from bep have "((λx. b - hb * ln x powr -(1+e)) ⤏ b - 0) at_top"
by (intro tendsto_intros tendsto_mult_right_zero tendsto_neg_powr ln_at_top) simp_all
hence "LIM x at_top. (b - hb * ln x powr -(1+e)) * x :> at_top"
by (rule filterlim_tendsto_pos_mult_at_top[OF _ _ filterlim_ident], insert bep) simp_all
also have "(λx. (b - hb * ln x powr -(1+e)) * x) = (λx. b*x - hb*x*ln x powr -(1+e))"
by (intro ext) (simp add: algebra_simps)
finally have "filterlim ... at_top at_top" .
with bep have "((λx. ln (b*x - hb*x*ln x powr -(1+e)) powr -(e/2)) ⤏ 0) at_top"
by (intro tendsto_neg_powr filterlim_compose[OF ln_at_top]) simp_all
hence "eventually (λx. ¦ln (b*x - hb*x*ln x powr -(1+e)) powr (-e/2)¦ < 1) at_top"
by (subst (asm) tendsto_iff) (simp add: dist_real_def)
thus ?thesis by simp
qed
lemma asymptotics6: "eventually (λx. hb / ln x powr (1 + e) < b/2) at_top"
and asymptotics7: "eventually (λx. hb / ln x powr (1 + e) < (1 - b) / 2) at_top"
and asymptotics8: "eventually (λx. x*(1 - b - hb / ln x powr (1 + e)) > 1) at_top"
proof-
from bep have A: "(λx. hb / ln x powr (1 + e)) ∈ o(λ_. 1)" by simp
from bep have B: "b/3 > 0" and C: "(1 - b)/3 > 0" by simp_all
from landau_o.smallD[OF A B] show "eventually (λx. hb / ln x powr (1+e) < b/2) at_top"
by eventually_elim (insert bep, simp)
from landau_o.smallD[OF A C] show "eventually (λx. hb / ln x powr (1 + e) < (1 - b)/2) at_top"
by eventually_elim (insert bep, simp)
from bep have "(λx. hb / ln x powr (1 + e)) ∈ o(λ_. 1)" "(1 - b) / 2 > 0" by simp_all
from landau_o.smallD[OF this] eventually_gt_at_top[of "1::real"]
have A: "eventually (λx. 1 - b - hb / ln x powr (1 + e) > 0) at_top"
by eventually_elim (insert bep, simp add: field_simps)
from bep have "(λx. x * (1 - b - hb / ln x powr (1+e))) ∈ ω(λ_. 1)" "(0::real) < 2" by simp_all
from landau_omega.smallD[OF this] A eventually_gt_at_top[of "0::real"]
show "eventually (λx. x*(1 - b - hb / ln x powr (1 + e)) > 1) at_top"
by eventually_elim (simp_all add: abs_mult)
qed
end
end
definition "akra_bazzi_asymptotic1 b hb e p x ⟷
(1 - hb * inverse b * ln x powr -(1+e)) powr p * (1 + ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
≥ 1 + (ln x powr (-e/2) :: real)"
definition "akra_bazzi_asymptotic1' b hb e p x ⟷
(1 + hb * inverse b * ln x powr -(1+e)) powr p * (1 + ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
≥ 1 + (ln x powr (-e/2) :: real)"
definition "akra_bazzi_asymptotic2 b hb e p x ⟷
(1 + hb * inverse b * ln x powr -(1+e)) powr p * (1 - ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
≤ 1 - ln x powr (-e/2 :: real)"
definition "akra_bazzi_asymptotic2' b hb e p x ⟷
(1 - hb * inverse b * ln x powr -(1+e)) powr p * (1 - ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
≤ 1 - ln x powr (-e/2 :: real)"
definition "akra_bazzi_asymptotic3 e x ⟷ (1 + (ln x powr (-e/2))) / 2 ≤ (1::real)"
definition "akra_bazzi_asymptotic4 e x ⟷ (1 - (ln x powr (-e/2))) * 2 ≥ (1::real)"
definition "akra_bazzi_asymptotic5 b hb e x ⟷
ln (b*x - hb*x*ln x powr -(1+e)) powr (-e/2::real) < 1"
definition "akra_bazzi_asymptotic6 b hb e x ⟷ hb / ln x powr (1 + e :: real) < b/2"
definition "akra_bazzi_asymptotic7 b hb e x ⟷ hb / ln x powr (1 + e :: real) < (1 - b) / 2"
definition "akra_bazzi_asymptotic8 b hb e x ⟷ x*(1 - b - hb / ln x powr (1 + e :: real)) > 1"
definition "akra_bazzi_asymptotics b hb e p x ⟷
akra_bazzi_asymptotic1 b hb e p x ∧ akra_bazzi_asymptotic1' b hb e p x ∧
akra_bazzi_asymptotic2 b hb e p x ∧ akra_bazzi_asymptotic2' b hb e p x ∧
akra_bazzi_asymptotic3 e x ∧ akra_bazzi_asymptotic4 e x ∧ akra_bazzi_asymptotic5 b hb e x ∧
akra_bazzi_asymptotic6 b hb e x ∧ akra_bazzi_asymptotic7 b hb e x ∧
akra_bazzi_asymptotic8 b hb e x"
lemmas akra_bazzi_asymptotic_defs =
akra_bazzi_asymptotic1_def akra_bazzi_asymptotic1'_def
akra_bazzi_asymptotic2_def akra_bazzi_asymptotic2'_def akra_bazzi_asymptotic3_def
akra_bazzi_asymptotic4_def akra_bazzi_asymptotic5_def akra_bazzi_asymptotic6_def
akra_bazzi_asymptotic7_def akra_bazzi_asymptotic8_def akra_bazzi_asymptotics_def
lemma akra_bazzi_asymptotics:
assumes "⋀b. b ∈ set bs ⟹ b ∈ {0<..<1}"
assumes "hb > 0" "e > 0"
shows "eventually (λx. ∀b∈set bs. akra_bazzi_asymptotics b hb e p x) at_top"
proof (intro eventually_ball_finite ballI)
fix b assume "b ∈ set bs"
with assms interpret akra_bazzi_asymptotics_bep b e p hb by unfold_locales auto
show "eventually (λx. akra_bazzi_asymptotics b hb e p x) at_top"
unfolding akra_bazzi_asymptotic_defs
using asymptotics1[of "-c" for c] asymptotics2[of "-c" for c]
by (intro eventually_conj asymptotics1 asymptotics2 asymptotics3
asymptotics4 asymptotics5 asymptotics6 asymptotics7 asymptotics8) simp_all
qed simp
end