Theory Akra_Bazzi
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 x⇩0 x⇩1 b t =
(∃e h. e > 0 ∧ (λx. h x) ∈ O(λx. real x / ln (real x) powr (1+e)) ∧
(∀x≥x⇩1. t x ≥ x⇩0 ∧ 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 ≥ x⇩1 ⟹ t x ≥ x⇩0" "⋀x. x ≥ x⇩1 ⟹ t x < x"
"⋀x. x ≥ x⇩1 ⟹ b*x + h x = real (t x)"
shows "akra_bazzi_term x⇩0 x⇩1 b t"
using assms unfolding akra_bazzi_term_def by blast
lemma akra_bazzi_term_imp_less:
assumes "akra_bazzi_term x⇩0 x⇩1 b t" "x ≥ x⇩1"
shows "t x < x"
using assms unfolding akra_bazzi_term_def by blast
lemma akra_bazzi_term_imp_less':
assumes "akra_bazzi_term x⇩0 (Suc x⇩1) b t" "x > x⇩1"
shows "t x < x"
using assms unfolding akra_bazzi_term_def by force
locale akra_bazzi_recursion =
fixes x⇩0 x⇩1 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 x⇩0 x⇩1 (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 ∧ (∀h∈set hs. (λx. h x) ∈ O(λx. real x / ln (real x) powr (1+e))) ∧
(∀t∈set ts. ∀x≥x⇩1. t x ≥ x⇩0 ∧ t x < x) ∧
(∀i<k. ∀x≥x⇩1. (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 ∧
(∀h∈set hs. (λx. h x) ∈ O(λx. real x / ln (real x) powr (1 + e))) ∧
(∀t∈set ts. ∀x≥x⇩1. x⇩0 ≤ t x ∧ t x < x) ∧
(∀i<k. ∀x≥x⇩1. (bs!i)*x + (hs!i) x = real ((ts!i) x))"
proof-
have "Ex (λ(e,hs). e > 0 ∧ length hs = k ∧
(∀h∈set hs. (λx. h x) ∈ O(λx. real x / ln (real x) powr (1+e))) ∧
(∀t∈set ts. ∀x≥x⇩1. t x ≥ x⇩0 ∧ t x < x) ∧
(∀i<k. ∀x≥x⇩1. (bs!i)*x + (hs!i) x = real ((ts!i) x)))"
proof-
from ts have A: "∀i∈{..<k}. akra_bazzi_term x⇩0 x⇩1 (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)) ∧
(∀x≥x⇩1. (ts!i) x ≥ x⇩0 ∧ (ts!i) x < x) ∧
(∀i<k. ∀x≥x⇩1. (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: "∀h∈set 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 "∀t∈set ts. (∀x≥x⇩1. t x ≥ x⇩0 ∧ 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 "∀x≥x⇩1. t x ≥ x⇩0 ∧ t x < x" unfolding hs_def by force
qed
moreover have "∀i<k. ∀x≥x⇩1. (bs!i)*x + (hs!i) x = real ((ts!i) x)"
proof (rule allI, rule impI)
fix i assume i: "i < k"
with eh show "∀x≥x⇩1. (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 ≥ x⇩1 ⟹ x⇩0 ≤ t x" and
step_less: "⋀t x. t ∈ set ts ⟹ x ≥ x⇩1 ⟹ t x < x" and
decomp: "⋀i x. i < k ⟹ x ≥ x⇩1 ⟹ (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: "x⇩0 < x⇩1" and x0_le_x1: "x⇩0 ≤ x⇩1"
proof-
from ts_nonempty have "x⇩0 ≤ hd ts x⇩1" using step_ge_x0[of "hd ts" x⇩1] by simp
also from ts_nonempty have "... < x⇩1" by (intro step_less) simp_all
finally show "x⇩0 < x⇩1" by simp
thus "x⇩0 ≤ x⇩1" by simp
qed
lemma akra_bazzi_induct [consumes 1, case_names base rec]:
assumes "x ≥ x⇩0"
assumes base: "⋀x. x ≥ x⇩0 ⟹ x < x⇩1 ⟹ P x"
assumes rec: "⋀x. x ≥ x⇩1 ⟹ (⋀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 < x⇩1") 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 ≥ 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
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 ≥ x⇩0 ⟹ 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. ∀h∈set hs'. ¦h x¦ ≤ hb * x / ln x powr (1 + e)) at_top"
proof-
have "∀h∈set 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:
"∀h∈set 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 "∀h∈set 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 "∀h∈set hs'. eventually (λx. ¦h x¦ ≤ hb' * x / ln x powr (1 + e)) at_top"
by (auto simp: hs'_def)
hence "eventually (λx. ∀h∈set 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. ∀b∈set 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 "∀b∈set bs. eventually (λx. ¦hb * ln x powr -(1+e)¦ < b - C) at_top"
by (force simp: tendsto_iff dist_real_def)
hence "eventually (λx. ∀b∈set 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: "∀b∈set 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. ∀b≥a. 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 x⇩1] 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 x⇩1 (SOME gx0. ∀x≥gx0. g x ≥ gc2 * g' (real x) ∧ f x > 0 ∧ g' (real x) ≥ 0)"
definition "gx1 ≡ max gx0 (SOME gx1. ∀x≥gx1. ∀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. ∀x≥gx0. 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. ∀x≥gx0. 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: "∀h∈set 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 ≥ x⇩1"
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. ∀x≥gx1. ∀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 ≥ x⇩1" 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 ≥ x⇩0 ⟹ 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 ⟹ x⇩0 ≤ (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. ∀b∈set 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. ∀b∈set 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. (∀h∈set hs'. ¦h x¦ ≤ hb*x/ln x powr (1+e)) ∧
(∀b∈set bs. C*x ≤ b*x - hb*x/ln x powr (1+e)) ∧
(∀b∈set 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. (∀x≥X. (∀h∈set hs'. ¦h x¦ ≤ hb*x/ln x powr (1+e)) ∧
(∀b∈set bs. C*x ≤ b*x - hb*x/ln x powr (1+e)) ∧
(∀b∈set 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 x⇩0'_min where "x⇩0'_min = max A (max X (max a0 (max gx1 (max 1 (real x⇩1 + 1)))))"
{
fix x⇩0' :: real assume x0'_props: "x⇩0' ≥ x⇩0'_min" "x⇩0' ∈ ℕ"
hence x0'_ge_x1: "x⇩0' ≥ real (x⇩1+1)" and x0'_ge_1: "x⇩0' ≥ 1" and x0'_ge_X: "x⇩0' ≥ X"
unfolding x⇩0'_min_def by linarith+
hence x0'_pos: "x⇩0' > 0" and x0'_nonneg: "x⇩0' ≥ 0" by simp_all
have x0': "∀x≥x⇩0'. (∀h∈set hs'. ¦h x¦ ≤ hb*x/ln x powr (1+e))"
"∀x≥x⇩0'. (∀b∈set bs. C*x ≤ b*x - hb*x/ln x powr (1+e))"
"∀x≥x⇩0'. (∀b∈set bs. akra_bazzi_asymptotics b hb e p x)"
"∀a≥x⇩0'. ∀b>a. ∃c. ∀x∈{a..b}. g' x ≤ c"
"∀x≥x⇩0'. ∀u∈{C * x..x}. g' u ≤ c2 * g' x"
"∀x≥x⇩0'. f2' (nat ⌊x⌋) > 0" "∀x≥x⇩0'. g' x ≥ 0"
using X x0'_ge_X by auto
from x0'_props(2) have x0'_int: "real (nat ⌊x⇩0'⌋) = x⇩0'" by (rule real_natfloor_nat)
from x0'_props have x0'_ge_gx1: "x⇩0' ≥ gx1" and x0'_ge_a0: "x⇩0' ≥ a0"
unfolding x⇩0'_min_def by simp_all
with gx0_le_gx1 have f2'_nonneg: "⋀x. x ≥ x⇩0' ⟹ f2' x ≥ 0" by (force intro!: f2'_nonneg)
define bm where "bm = Min (set bs)"
define x⇩1' where "x⇩1' = 2 * x⇩0' * inverse bm"
define fb2 where "fb2 = Min {f2' x |x. x ∈ {x⇩0'..x⇩1'}}"
define gb2 where "gb2 = (SOME c. ∀x∈{x⇩0'..x⇩1'}. 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': "x⇩0' < x⇩1'" and x0'_le_x1': "x⇩0' ≤ x⇩1'" unfolding x⇩1'_def by simp_all
from x0_le_x1 x0'_ge_x1 have ge_x0'D: "⋀x. x⇩0' ≤ real x ⟹ x⇩0 ≤ x" by simp
from x0'_ge_x1 x0'_le_x1' have gt_x1'D: "⋀x. x⇩1' < real x ⟹ x⇩1 ≤ x" by simp
have x0'_x1': "∀b∈set bs. 2 * x⇩0' * inverse b ≤ x⇩1'"
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 * x⇩0' * inverse b ≤ x⇩1'"
unfolding x⇩1'_def by (intro mult_left_mono) simp_all
qed
note f_nonneg' = f_nonneg
have "⋀x. real x ≥ x⇩0' ⟹ x ≥ nat ⌊x⇩0'⌋" "⋀x. real x ≤ x⇩1' ⟹ x ≤ nat ⌈x⇩1'⌉" by linarith+
hence "{x |x. real x ∈ {x⇩0'..x⇩1'}} ⊆ {x |x. x ∈ {nat ⌊x⇩0'⌋..nat ⌈x⇩1'⌉}}" by auto
hence "finite {x |x::nat. real x ∈ {x⇩0'..x⇩1'}}" by (rule finite_subset) auto
hence fin: "finite {f2' x |x::nat. real x ∈ {x⇩0'..x⇩1'}}" 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 x⇩0' x⇩1' 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 x⇩0' x⇩1' hb e p
integrable integral abr.f' g' C fb2 gb2 c2
proof unfold_locales
fix x assume "x ≥ x⇩0'" "x ≤ x⇩1'"
thus "abr.f' x ≥ 0" by (intro abr.f'_base) simp_all
next
fix x assume x:"x ≥ x⇩0'"
show "integrable (λx. g' x / x powr (p + 1)) x⇩0' x"
by (rule integrable_subinterval[of _ a0 x]) (insert a0 x0'_ge_a0 x, auto)
next
fix x assume x: "x ≥ x⇩0'" "x ≤ x⇩1'"
have "x⇩0' = real (nat ⌊x⇩0'⌋)" by (simp add: x0'_int)
also from x have "... ≤ real (nat ⌊x⌋)" by (auto intro!: nat_mono floor_mono)
finally have "x⇩0' ≤ real (nat ⌊x⌋)" .
moreover have "real (nat ⌊x⌋) ≤ x⇩1'" using x x0'_ge_1 by linarith
ultimately have "f2' (nat ⌊x⌋) ∈ {f2' x |x. real x ∈ {x⇩0'..x⇩1'}}" 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 ≥ x⇩0' ∧ real x ≤ x⇩1'"
by (intro exI[of _ "nat ⌊x⇩0'⌋"]) simp_all
moreover {
fix x :: nat assume "real x ≥ x⇩0' ∧ real x ≤ x⇩1'"
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: "x⇩0' ≤ x" "x ≤ x⇩1'"
with x0'(4) x0'_lt_x1' have "∃c. ∀x∈{x⇩0'..x⇩1'}. 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 ⌈x⇩0'⌉"
hence x: "real x ≥ x⇩0'" 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 "x⇩0'_min ≥ A" unfolding x⇩0'_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. ∀b≥a. 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 x⇩1] 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 x⇩1 (SOME gx0. ∀x≥gx0. g x ≤ gc1 * g' (real x))"
lemma gx3:
assumes "x ≥ gx3"
shows "g x ≤ gc1 * g' (real x)"
proof-
from gc1(2) have "∃gx3. ∀x≥gx3. g x ≤ gc1 * g' (real x)" by (simp add: eventually_at_top_linorder)
note someI_ex[OF this]
moreover have "x ≥ (SOME gx0. ∀x≥gx0. 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 ≥ x⇩1" 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 ≥ x⇩0 ⟹ 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 ⟹ x⇩0 ≤ 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. ∀b∈set 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. ∀b∈set 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. (∀h∈set hs'. ¦h x¦ ≤ hb*x/ln x powr (1+e)) ∧
(∀b∈set bs. C*x ≤ b*x - hb*x/ln x powr (1+e)) ∧
(∀b∈set 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. (∀x≥X. (∀h∈set hs'. ¦h x¦ ≤ hb*x/ln x powr (1+e)) ∧
(∀b∈set bs. C*x ≤ b*x - hb*x/ln x powr (1+e)) ∧
(∀b∈set 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 x⇩0'_min where "x⇩0'_min = max A (max X (max 1 (max a0 (max gx3 (real x⇩1 + 1)))))"
{
fix x⇩0' :: real assume x0'_props: "x⇩0' ≥ x⇩0'_min" "x⇩0' ∈ ℕ"
hence x0'_ge_x1: "x⇩0' ≥ real (x⇩1+1)" and x0'_ge_1: "x⇩0' ≥ 1" and x0'_ge_X: "x⇩0' ≥ X"
unfolding x⇩0'_min_def by linarith+
hence x0'_pos: "x⇩0' > 0" and x0'_nonneg: "x⇩0' ≥ 0" by simp_all
have x0': "∀x≥x⇩0'. (∀h∈set hs'. ¦h x¦ ≤ hb*x/ln x powr (1+e))"
"∀x≥x⇩0'. (∀b∈set bs. C*x ≤ b*x - hb*x/ln x powr (1+e))"
"∀x≥x⇩0'. (∀b∈set bs. akra_bazzi_asymptotics b hb e p x)"
"∀x≥x⇩0'. ∀u∈{C*x..x}. g' u ≥ c1 * g' x" "∀x≥x⇩0'. g' x ≥ 0"
using X x0'_ge_X by auto
from x0'_props(2) have x0'_int: "real (nat ⌊x⇩0'⌋) = x⇩0'" by (rule real_natfloor_nat)
from x0'_props have x0'_ge_gx0: "x⇩0' ≥ gx3" and x0'_ge_a0: "x⇩0' ≥ a0"
unfolding x⇩0'_min_def by simp_all
hence f'_nonneg: "⋀x. x ≥ x⇩0' ⟹ 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 x⇩1' where "x⇩1' = 2 * x⇩0' * inverse bm"
define fb1 where "fb1 = Max {f' x |x. x ∈ {x⇩0'..x⇩1'}}"
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': "x⇩0' < x⇩1'" and x0'_le_x1': "x⇩0' ≤ x⇩1'" unfolding x⇩1'_def by simp_all
from x0_le_x1 x0'_ge_x1 have ge_x0'D: "⋀x. x⇩0' ≤ real x ⟹ x⇩0 ≤ x" by simp
from x0'_ge_x1 x0'_le_x1' have gt_x1'D: "⋀x. x⇩1' < real x ⟹ x⇩1 ≤ x" by simp
have x0'_x1': "∀b∈set bs. 2 * x⇩0' * inverse b ≤ x⇩1'"
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 * x⇩0' * inverse b ≤ x⇩1'"
unfolding x⇩1'_def by (intro mult_left_mono) simp_all
qed
note f_nonneg' = f_nonneg
have "⋀x. real x ≥ x⇩0' ⟹ x ≥ nat ⌊x⇩0'⌋" "⋀x. real x ≤ x⇩1' ⟹ x ≤ nat ⌈x⇩1'⌉" by linarith+
hence "{x |x. real x ∈ {x⇩0'..x⇩1'}} ⊆ {x |x. x ∈ {nat ⌊x⇩0'⌋..nat ⌈x⇩1'⌉}}" by auto
hence "finite {x |x::nat. real x ∈ {x⇩0'..x⇩1'}}" by (rule finite_subset) auto
hence fin: "finite {f' x |x::nat. real x ∈ {x⇩0'..x⇩1'}}" 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 x⇩0' x⇩1' 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 x⇩0' x⇩1' hb e p integrable integral abr.f' g' C fb1 c1
proof (unfold_locales)
fix x assume "x ≥ x⇩0'" "x ≤ x⇩1'"
thus "abr.f' x ≥ 0" by (intro abr.f'_base) simp_all
next
fix x assume x:"x ≥ x⇩0'"
show "integrable (λx. g' x / x powr (p + 1)) x⇩0' x"
by (rule integrable_subinterval[of _ a0 x]) (insert a0 x0'_ge_a0 x, auto)
next
fix x assume x: "x ≥ x⇩0'" "x ≤ x⇩1'"
have "x⇩0' = real (nat ⌊x⇩0'⌋)" by (simp add: x0'_int)
also from x have "... ≤ real (nat ⌊x⌋)" by (auto intro!: nat_mono floor_mono)
finally have "x⇩0' ≤ real (nat ⌊x⌋)" .
moreover have "real (nat ⌊x⌋) ≤ x⇩1'" using x x0'_ge_1 by linarith
ultimately have "f' (nat ⌊x⌋) ∈ {f' x |x. real x ∈ {x⇩0'..x⇩1'}}" 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 ⌈x⇩0'⌉"
hence x: "real x ≥ x⇩0'" 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 ⌈x⇩0'⌉"] 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 "x⇩0'_min ≥ A" unfolding x⇩0'_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. ∀b≥a. 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 x⇩0 ≤ b * real x⇩1 + c" "c < (1 - b) * real x⇩1" "x⇩1 > 0"
shows "akra_bazzi_term x⇩0 x⇩1 b (λx. nat ⌊b*real x + c⌋)"
proof (rule akra_bazzi_termI[OF zero_less_one])
fix x assume x: "x ≥ x⇩1"
from assms x have "real x⇩0 ≤ b * real x⇩1 + c" by simp
also from x assms have "... ≤ b * real x + c" by auto
finally have step_ge_x0: "b * real x + c ≥ real x⇩0" by simp
thus "nat ⌊b * real x + c⌋ ≥ x⇩0" by (subst le_nat_iff) (simp_all add: le_floor_iff)
from assms x have "c < (1 - b) * real x⇩1" 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 x⇩0 ≤ b * real x⇩1 + real c" "real c < (1 - b) * real x⇩1" "x⇩1 > 0"
shows "akra_bazzi_term x⇩0 x⇩1 b (λx. nat ⌊b*real x⌋ + c)"
proof-
from assms have "akra_bazzi_term x⇩0 x⇩1 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 x⇩0 ≤ b * real x⇩1 - c" "0 < c + (1 - b) * real x⇩1" "x⇩1 > 0"
shows "akra_bazzi_term x⇩0 x⇩1 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 x⇩0 ≤ b * real x⇩1 - real c" "0 < real c + (1 - b) * real x⇩1" "x⇩1 > 0"
shows "akra_bazzi_term x⇩0 x⇩1 b (λx. nat ⌊b*real x⌋ - c)"
proof-
from assms have "akra_bazzi_term x⇩0 x⇩1 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 x⇩0 ≤ b * real x⇩1" "0 < (1 - b) * real x⇩1" "x⇩1 > 0"
shows "akra_bazzi_term x⇩0 x⇩1 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 x⇩0 ≤ b * real x⇩1 + c" "c + 1 ≤ (1 - b) * x⇩1"
shows "akra_bazzi_term x⇩0 x⇩1 b (λx. nat ⌈b*real x + c⌉)"
proof (rule akra_bazzi_termI[OF zero_less_one])
fix x assume x: "x ≥ x⇩1"
have "0 ≤ real x⇩0" by simp
also from assms have "real x⇩0 ≤ b * real x⇩1 + c" by simp
also from assms x have "b * real x⇩1 ≤ b * real x" by (intro mult_left_mono) simp_all
hence "b * real x⇩1 + 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) * x⇩1" by fact
also have "(1 - b) * x⇩1 ≤ (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 x⇩0 ≤ b * real x⇩1 + c" by fact
also have "... ≤ real_of_int ⌈...⌉" by linarith
also have "x⇩1 ≤ x" by fact
finally show "x⇩0 ≤ 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 x⇩0 ≤ b * real x⇩1 + real c" "real c + 1 ≤ (1 - b) * x⇩1"
shows "akra_bazzi_term x⇩0 x⇩1 b (λx. nat ⌈b*real x⌉ + c)"
proof-
from assms have "akra_bazzi_term x⇩0 x⇩1 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 x⇩0 ≤ b * real x⇩1 - c" "1 ≤ c + (1 - b) * x⇩1"
shows "akra_bazzi_term x⇩0 x⇩1 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 x⇩0 ≤ b * real x⇩1 - real c" "1 ≤ real c + (1 - b) * x⇩1"
shows "akra_bazzi_term x⇩0 x⇩1 b (λx. nat ⌈b*real x⌉ - c)"
proof-
from assms have "akra_bazzi_term x⇩0 x⇩1 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 x⇩0 ≤ b * real x⇩1" "1 ≤ (1 - b) * x⇩1"
shows "akra_bazzi_term x⇩0 x⇩1 b (λx. nat ⌈b*real x⌉)"
using assms akra_bazzi_term_ceiling_add[where c = 0] by simp
end