Theory Asymptotics_1D
theory Asymptotics_1D
imports Akra_Bazzi.Akra_Bazzi_Method Auto2_HOL.Auto2_Main
begin
section ‹Eventually nonneg›
lemma event_nonneg_real: "eventually_nonneg F (λx. real (f x))"
by (simp add: eventually_nonneg_def)
lemma event_nonneg_ln: "eventually_nonneg at_top (λx. ln (real x))"
unfolding eventually_nonneg_def apply(rule eventually_sequentiallyI[where c=1])
using ln_ge_zero real_of_nat_ge_one_iff by blast
lemma event_nonneg_ln_pow: "eventually_nonneg at_top (λx. ln (real x) ^ m)"
using event_nonneg_ln by (simp add: eventually_mono eventually_nonneg_def)
lemma event_nonneg_add':
"eventually_nonneg F f ⟹ eventually_nonneg F g ⟹ eventually_nonneg F (f + g)"
by (subst plus_fun_def) (rule eventually_nonneg_add)
lemma event_nonneg_mult':
"eventually_nonneg F f ⟹ eventually_nonneg F g ⟹ eventually_nonneg F (f * g)"
apply (subst times_fun_def) by (rule eventually_nonneg_mult)
section ‹Normal form in one variale›
definition polylog :: "nat ⇒ nat ⇒ nat ⇒ real" where
"polylog a b x = real (x^a) * (ln x)^b"
lemma event_nonneg_polylog: "eventually_nonneg at_top (λx. polylog a b x)"
apply (simp only: polylog_def)
apply (rule eventually_nonneg_mult)
apply (rule event_nonneg_real)
apply (rule event_nonneg_ln_pow)
done
lemma poly_log_compare:
"(a1<a2 ∨ (a1=a2 ∧ b1<b2)) ⟹ (λx. polylog a1 b1 x) ∈ o(λx. polylog a2 b2 x)"
unfolding polylog_def by auto
section ‹Stability in one variable›
definition stablebigO :: "(nat ⇒ real) ⇒ bool" where
"stablebigO f = (∀c>0. (λx. f (c * x)) ∈ O(f))"
lemma stablebiOI: assumes "⋀c. 0 < c ⟹ (λx. f (c * x)) ∈ O(f)"
shows "stablebigO f"
unfolding stablebigO_def using assms by blast
lemma stablebigOD: assumes "stablebigO f" "d>0"
obtains c where "c>0" "eventually (λx. norm (f (d*x)) ≤ c * norm (f x)) at_top"
proof -
from assms have "(λx. f (d * x)) ∈ O(f)" unfolding stablebigO_def by auto
then obtain c where "c>0" "eventually (λx. norm (f (d * x)) ≤ c * norm (f x)) at_top"
using landau_o.bigE by blast
then show ?thesis by (rule that)
qed
lemma stablebigO_linear: "stablebigO (λn::nat. n)"
unfolding stablebigO_def by auto
lemma stablebigO_poly: "stablebigO (λn::nat. n^m)"
unfolding stablebigO_def by auto
lemma stablebigO_ln: "stablebigO (λx. ln (real x))"
unfolding stablebigO_def by auto
lemma stablebigO_lnpower: "stablebigO (λx. (ln (real x))^m)"
unfolding stablebigO_def by auto
lemma stablebigO_mult:
fixes f g :: "nat ⇒ real"
assumes f: "stablebigO f" and g: "stablebigO g" and
evf: "eventually_nonneg at_top f" and
evg: "eventually_nonneg at_top g"
shows "stablebigO (f * g)"
proof (rule stablebiOI)
fix d :: nat
assume d: "d>0"
from f d obtain cf where cf: "cf>0" and f: "eventually (λx. norm (f (d * x)) ≤ cf * norm (f x)) at_top"
using stablebigOD by blast
from g d obtain cg where cg: "cg>0" and g: "eventually (λx. norm (g (d * x)) ≤ cg * norm (g x)) at_top"
using stablebigOD by blast
have evf: "eventually (λx. f x ≥ 0) at_top" using evf by (simp add: eventually_nonneg_def)
have evg: "eventually (λx. g x ≥ 0) at_top" using evg by (simp add: eventually_nonneg_def)
let ?c = "cf * cg"
note prem = f evf[unfolded eventually_nonneg_def] g evg[unfolded eventually_nonneg_def]
show "(λx. (f * g) (d * x)) ∈ O(f * g)"
apply(rule bigoI[where c="?c"])
using prem
proof eventually_elim
case (elim x)
have "norm ((f*g)(d*x)) = norm(f (d*x)*g (d*x))" by auto
also have "… = norm(f (d*x)) * norm (g (d*x))"
by (metis norm_mult)
also have "… ≤ (cf * norm (f x)) * norm (g (d*x))" using elim(1) by (auto intro!: mult_right_mono)
also have "… ≤ (cf * norm (f x)) * (cg * norm (g x))" using cf elim(2,3) by (auto intro!: mult_left_mono)
also have "… = ?c * (norm (f x * g x))" using cg cf
by (metis mult.commute mult.left_commute norm_mult)
finally show ?case by auto
qed
qed
lemma stablebigO_mult':
fixes f g :: "nat ⇒ real"
assumes "stablebigO f" "stablebigO g"
"eventually_nonneg at_top f" "eventually_nonneg at_top g"
shows "stablebigO (%x. f x * g x)"
proof -
have "(λx. f x * g x) = f * g" by auto
with stablebigO_mult[OF assms] show ?thesis by simp
qed
lemma stable_polylog: "stablebigO (λx. polylog a b x)"
apply (simp only: polylog_def)
apply (rule stablebigO_mult')
apply (rule stablebigO_poly)
apply (rule stablebigO_lnpower)
apply (rule event_nonneg_real)
apply (rule event_nonneg_ln_pow)
done
lemma stablebigO_plus:
fixes f g :: "nat ⇒ real"
assumes f: "stablebigO f" and g: "stablebigO g" and
evf: "eventually_nonneg at_top f" and
evg: "eventually_nonneg at_top g"
shows "stablebigO (f + g)"
proof (rule stablebiOI)
fix d :: nat
assume d: "d>0"
from f d obtain cf where f: "eventually (λx. norm (f (d * x)) ≤ cf * norm (f x)) at_top"
using stablebigOD by blast
from g d obtain cg where g: "eventually (λx. norm (g (d * x)) ≤ cg * norm (g x)) at_top"
using stablebigOD by blast
have evf: "eventually (λx. f x ≥ 0) at_top" using evf by (simp add: eventually_nonneg_def)
have evg: "eventually (λx. g x ≥ 0) at_top" using evg by (simp add: eventually_nonneg_def)
let ?c = "(max cf cg)"
note prem = f evf[unfolded eventually_nonneg_def] g evg[unfolded eventually_nonneg_def]
show "(λx. (f + g) (d * x)) ∈ O(f + g)"
apply(rule bigoI[where c="?c"])
using prem
proof eventually_elim
case (elim x)
have "norm ((f+g)(d*x)) = norm(f (d*x)+g (d*x))" by auto
also have "… ≤ norm(f (d*x)) + norm (g (d*x))" by (simp add: norm_triangle_ineq)
also have "… ≤ cf * norm (f x) + cg * norm (g x)" using elim(1,3) by auto
also have "… ≤ ?c * norm (f x) + ?c * norm (g x)" by (simp add: max_def mult_right_mono)
also have "… = ?c * (norm (f x)+ norm (g x))" by (simp add: distrib_left)
also have "… = ?c * norm (f x + g x)" using elim(2,4) by auto
finally show ?case by auto
qed
qed
section ‹Eventual monotonicity in one variable›
definition event_mono :: "(nat ⇒ real) ⇒ bool" where
"event_mono g1 = eventually (λx1. ∀x2≥x1. norm (g1 x1) ≤ norm (g1 x2)) at_top"
lemma event_mono_linear: "event_mono (λn::nat. n)"
unfolding event_mono_def by auto
lemma event_mono_poly: "event_mono (λn::nat. n^m)"
unfolding event_mono_def apply (auto simp: eventually_sequentially)
apply(rule exI[where x=1]) apply auto apply(rule power_mono) by auto
lemma event_mono_ln: "event_mono (λx. ln (real x))"
unfolding event_mono_def apply (auto simp: eventually_sequentially)
apply(rule exI[where x=1]) by auto
lemma event_mono_lnpower: "event_mono (λx. (ln (real x))^m)"
unfolding event_mono_def apply (auto simp: eventually_sequentially)
apply(rule exI[where x=1]) apply(auto) apply(rule power_mono) by auto
lemma assumes f : "event_mono f" and g: "event_mono g" and
evf: "eventually_nonneg at_top f" and
evg: "eventually_nonneg at_top g"
shows event_mono_plus: "event_mono (λx. f x + g x)"
proof -
from evf have evf': "eventually (λx. ∀x'≥x. f x' ≥ 0) at_top"
using eventually_all_ge_at_top eventually_nonneg_def by blast
from evg have evg': "eventually (λx. ∀x'≥x. g x' ≥ 0) at_top"
using eventually_all_ge_at_top eventually_nonneg_def by blast
note prem = evf' f[unfolded event_mono_def] g[unfolded event_mono_def] evg'
show ?thesis
unfolding event_mono_def
using prem
proof eventually_elim
case (elim x1)
show "∀x2≥x1. norm (f x1 + g x1) ≤ norm (f x2 + g x2)"
proof safe
fix x2 assume x2: "x2≥x1"
with elim have e: "f x2 ≥ 0" "g x2 ≥ 0" by auto
have "norm (f x1 + g x1) ≤ norm (f x1) + norm (g x1)" by (simp add: norm_triangle_ineq)
also have "… ≤ norm (f x2) + norm (g x2)" using elim(2,3) x2 by force
also have "… = norm (f x2 + g x2)" using e by simp
finally show "norm (f x1 + g x1) ≤ norm (f x2 + g x2)" .
qed
qed
qed
lemma assumes f : "event_mono f" and g: "event_mono g"
shows event_mono_mult: "event_mono (λx. f x * g x)"
proof -
note B=eventually_conj[OF f[unfolded event_mono_def] g[unfolded event_mono_def]]
show ?thesis unfolding event_mono_def
proof(rule eventually_mono[OF B], safe, simp )
fix x1 x2
assume a: "∀x2≥x1. ¦f x1¦ ≤ ¦f x2¦"
assume b: "∀x2≥x1. ¦g x1¦ ≤ ¦g x2¦"
assume c: "x1 ≤ x2"
have "¦f x1 * g x1¦ = ¦f x1¦ * ¦g x1¦" by (metis abs_mult)
also have "… ≤ ¦f x2¦ * ¦g x1¦" using a c by (auto intro: mult_right_mono)
also have "… ≤ ¦f x2¦ * ¦g x2¦" using b c by (auto intro: mult_left_mono)
also have "… = ¦f x2 * g x2¦" by (metis abs_mult)
finally show "¦f x1 * g x1¦ ≤ ¦f x2 * g x2¦" .
qed
qed
lemma event_mono_polylog: "event_mono (λx. polylog a b x)"
apply (simp only: polylog_def)
apply (rule event_mono_mult)
apply (rule event_mono_poly)
apply (rule event_mono_lnpower)
done
section ‹Auxiliary basics about Landau symbols›
lemma bigomegaI [intro]:
assumes "∀⇩F x in F. norm (g x) ≤ c * (norm (f x))"
shows "f ∈ Ω[F](g)"
proof (rule landau_omega.bigI)
show "1 / max 1 c > 0" by simp
note assms
have *: "⋀x. c * norm (f x) ≤ max 1 c * norm (f x)" by (simp add: mult_right_mono)
show "∀⇩F x in F. (1 / max 1 c) * norm (g x) ≤ norm (f x)"
apply(rule eventually_mono)
apply(fact)
using *
by (metis ‹0 < 1 / max 1 c› mult.commute mult.left_neutral order_trans pos_divide_le_eq times_divide_eq_right zero_less_divide_1_iff)
qed
lemma bigOmegaE:
fixes f :: "nat ⇒ real"
assumes "f ∈ Ω(g)"
obtains c n where "c > 0" "∀x≥n. norm (f x) ≥ c * norm (g x)"
proof -
from assms obtain c where c1: "c>0" and
"∀⇩F x in at_top. norm (f x) ≥ c * norm (g x)" using landau_omega.bigE by blast
then obtain n where f1: "∀x≥n. norm (f x) ≥ c * norm (g x)"
by (meson eventually_at_top_linorder)
from c1 and f1 show ?thesis by (rule that)
qed
lemma bigOE:
fixes f :: "nat⇒real"
assumes "f ∈ O(g)"
obtains c n where "c > 0" "∀x≥n. norm (f x) ≤ c * norm (g x)"
proof -
from assms obtain c where c1: "c>0" and
"∀⇩F x in at_top. norm (f x) ≤ c * norm (g x)" using landau_o.bigE by blast
then obtain n where f1: "∀x≥n. norm (f x) ≤ c * norm (g x)"
by (meson eventually_at_top_linorder)
from c1 and f1 show ?thesis by (rule that)
qed
lemma bigOE_nat:
fixes f :: "nat ⇒ nat"
assumes "f ∈ O(g)"
obtains c n :: nat where "c > 0" "∀x≥n. f x ≤ c * g x"
proof -
from assms obtain c where c1: "c>0" and
"∀⇩F x in at_top. norm (f x) ≤ c * norm (g x)" using landau_o.bigE by blast
then obtain n where f1: "∀x≥n. norm (f x) ≤ c * norm (g x)"
by (meson eventually_at_top_linorder)
have c1': "(nat ⌈c⌉) > 0" using c1 by auto
{fix x assume "x≥n"
with f1 have f1': "f x ≤ c * g x" by auto
then have "f x ≤ (nat ⌈c⌉) * g x" using c1
by (smt mult_right_mono of_nat_0_le_iff of_nat_ceiling of_nat_le_iff of_nat_mult)
} then have "∀x≥n. f x ≤ (nat ⌈c⌉) * g x" by auto
from c1' and this show ?thesis by (rule that)
qed
lemma bigOmegaE_nat:
fixes f :: "nat ⇒ nat"
assumes "f ∈ Ω(g)"
obtains c n :: nat where "c>0" "∀x≥n. g x ≤ c * f x"
proof -
from assms obtain c where c1: "c>0" and
"∀⇩F x in at_top. norm (f x) ≥ c * norm (g x)" using landau_omega.bigE by blast
then obtain n where f1: "∀x≥n. norm (f x) ≥ c * norm (g x)"
by (meson eventually_at_top_linorder)
from c1 have ic: "1/c ≤ (nat ⌈1/c⌉)" by linarith
have 1: "(nat ⌈1/c⌉) > 0 "using c1
by simp
{fix x assume "x≥n"
with f1 have f1': "f x ≥ c * g x" by auto
with c1 have "g x ≤ f x / c"
by (simp add: mult.commute mult_imp_le_div_pos)
also have "… ≤ (nat ⌈1/c⌉) * f x" using ic
using mult_right_mono by fastforce
finally have "real (g x) ≤ real ((nat ⌈1/c⌉) * f x)" .
then have "g x ≤ (nat ⌈1/c⌉) * f x"
by linarith
} then have "∀x≥n. g x ≤ (nat ⌈1/c⌉) * f x" by auto
from 1 and this show ?thesis by (rule that)
qed
lemma fsmall': "⋀(f::nat⇒real) c::real. f ∈ ω(λn::real. 1::real) ⟹ c≥0 ⟹ (∃n. ∀x≥n. c ≤ norm (f x))"
proof -
fix f::"nat⇒real" and c :: real
assume c: "c≥0" and w: " f ∈ ω(λn::real. 1::real)"
then have "c+1 > 0" by auto
from landau_omega.smallD[OF w this]
have "∀⇩F x in at_top. norm (f x) ≥ (c+1) * norm (1::real)" by auto
then obtain N where "⋀x. x≥N ⟹ norm (f x) ≥ c+1 "
unfolding eventually_at_top_linorder by fastforce
then have "⋀x. x≥N ⟹ norm (f x) ≥ c" by force
then show "∃n. ∀x≥n. c ≤ norm (f x)" by auto
qed
lemma fsmall_ev: "⋀(f::nat⇒nat) (c::nat). f ∈ ω(λn::real. 1::real) ⟹
eventually (λx. c ≤ f x) at_top"
proof -
fix f::"nat⇒nat" and c :: nat
assume w: " f ∈ ω(λn::real. 1::real)"
then have "real (c+1) > 0" by auto
from landau_omega.smallD[OF w this]
have "∀⇩F x in at_top. norm (f x) ≥ (real (c+1)) * norm (1::real)" by auto
then obtain N where "⋀x. x≥N ⟹ f x ≥ c+1 "
unfolding eventually_at_top_linorder by fastforce
then have "⋀x. x≥N ⟹ f x ≥ c" by force
then have "∃n. ∀x≥n. c ≤ f x" by auto
then show "eventually (λx. c ≤ f x) at_top" unfolding eventually_sequentially
by blast
qed
lemma fsmall: "⋀(f::nat⇒nat) (c::nat). f ∈ ω(λn::real. 1::real) ⟹ (∃n. ∀x≥n. c ≤ f x)"
proof -
fix f::"nat⇒nat" and c :: nat
assume w: " f ∈ ω(λn::real. 1::real)"
then have "real (c+1) > 0" by auto
from landau_omega.smallD[OF w this]
have "∀⇩F x in at_top. norm (f x) ≥ (real (c+1)) * norm (1::real)" by auto
then obtain N where "⋀x. x≥N ⟹ f x ≥ c+1 "
unfolding eventually_at_top_linorder by fastforce
then have "⋀x. x≥N ⟹ f x ≥ c" by force
then show "∃n. ∀x≥n. c ≤ f x" by auto
qed
lemma fbig: "⋀(f::nat⇒nat) (c::nat). f ∈ Ω(λn. n) ⟹ (∃n. ∀x≥n. c ≤ f x)"
proof -
fix f::"nat⇒nat" and c :: nat
assume " f ∈ Ω(λn. n)"
then obtain c1 where c1: "c1>0" and
"∀⇩F x in at_top. norm (f x) ≥ c1 * norm (x)" using landau_omega.bigE by blast
then obtain n where f: "∀x≥n. norm (f x) ≥ c1 * norm (x)"
by (meson eventually_at_top_linorder)
{ fix x :: nat
assume "x≥max (nat ⌈c/c1⌉) n"
then have xn: "x≥n" and xc: "real x≥(real c/c1)" by auto
from xc have "real c ≤ c1 * x" using c1
using divide_le_cancel by fastforce
also have "c1 * x ≤ f x" using f xn by auto
finally have "c ≤ f x" by auto
}
then have "∀x≥max (nat ⌈c/c1⌉) n. c ≤ f x" by auto
then show "∃n. ∀x≥n. c ≤ f x" by blast
qed
section ‹Composition in 1 variable case›
lemma bigOmega_compose:
fixes f1 g1 :: "nat⇒real" and f2 g2:: "nat ⇒ nat"
assumes "stablebigO g1"
and "f1 ∈ Ω(g1)" "f2 ∈ Ω(g2)"
and "f2 ∈ ω(λn. 1)" "g2 ∈ ω(λn. 1)"
and monog1: "event_mono g1"
shows "f1 o f2 ∈ Ω(g1 o g2)"
proof -
from assms(2) obtain c1 and n1 :: nat where c1: "c1>0" and
"⋀x. x ≥ n1 ⟹ c1 * norm (g1 x) ≤norm (f1 x)" using bigOmegaE by blast
then have f1: "⋀x. x ≥ n1 ⟹ norm (g1 x) ≤norm (f1 x) / c1" using c1
by (simp add: le_divide_eq mult.commute pos_le_divide_eq)
from assms(3) obtain c2 n2 :: nat where c2: "c2>0" and
f2: "⋀x. x ≥ n2 ⟹ g2 x ≤ c2 * f2 x" using bigOmegaE_nat by blast
from assms(1)[unfolded stablebigO_def] c2
obtain c3 :: real and n3 :: nat where c3: "c3>0" and
f3: "⋀x. x≥n3 ⟹ norm (g1 (c2 * x)) ≤ c3 * norm (g1 x)" using bigOE by blast
from monog1[unfolded event_mono_def] obtain nM
where g1: "⋀x y. x ≥ nM ⟹ y≥x ⟹ norm (g1 x) ≤ norm (g1 y)"
unfolding eventually_sequentially by blast
from assms(4) fsmall_ev have 1: "∀⇩F x in sequentially. n1 ≤ f2 x" by force
from assms(4) fsmall_ev have 2: "∀⇩F x in sequentially. n3 ≤ f2 x" by force
from assms(5) fsmall_ev have 3: "∀⇩F x in sequentially. nM ≤ g2 x" by force
have "∀⇩F x in sequentially. n2 ≤ x" by simp
from 1 2 3 this have "∀⇩F x in sequentially. norm ((g1 ∘ g2) x) ≤ c3 / c1 * norm ((f1 ∘ f2) x)"
proof eventually_elim
case (elim x)
with g1 have g1: "⋀y. y≥g2 x ⟹ norm (g1 (g2 x)) ≤ norm (g1 y)" by auto
have "g2 x ≤ c2 * f2 x" using f2 elim by auto
then have "norm (g1 (g2 x)) ≤ norm(g1 (c2 * f2 x))" by(rule g1)
also have "… ≤ c3 * norm (g1 (f2 x))" using f3 elim by simp
also have "… ≤ c3 * (norm (f1 (f2 x))/c1)" apply(rule mult_left_mono) using c3 f1 elim by auto
also have "… = (c3/c1) * norm (f1 (f2 x))" by auto
finally show ?case by auto
qed
thus ?thesis by(rule bigomegaI[where c="c3/c1"])
qed
lemma bigO_compose:
fixes f1 g1 :: "nat ⇒ real" and f2 g2:: "nat ⇒ nat"
assumes "stablebigO g1"
and "f1 ∈ O(g1)" and 2: "f2 ∈ O(g2)"
and "f2 ∈ ω(λn. 1)" and "g2 ∈ ω(λn. 1)"
and monog1: "event_mono g1"
shows "f1 o f2 ∈ O(g1 o g2)"
proof -
from assms(2) obtain c1 :: real and n1 :: nat where c1: "c1>0" and
f1: "⋀x. x≥n1 ⟹ norm (f1 x) ≤ c1 * norm (g1 x)" using bigOE by blast
from 2 obtain c2 n2 :: nat where c2: "c2>0" and
f2: "⋀x. x≥n2 ⟹ f2 x ≤ c2 * g2 x" using bigOE_nat by blast
from assms(1)[unfolded stablebigO_def] c2
obtain c3 ::real and n3 :: nat where c3: "c3>0" and
f3: "⋀x. x≥n3 ⟹ norm (g1 (c2 * x)) ≤ c3 * norm (g1 x)" using bigOE by blast
from monog1[unfolded event_mono_def] obtain nM
where g1: "⋀x y. x ≥ nM ⟹ y≥x ⟹ norm (g1 x) ≤ norm (g1 y)"
unfolding eventually_sequentially by blast
from assms(4) fsmall_ev have 1: "∀⇩F x in sequentially. n1 ≤ f2 x" by fast
from assms(5) fsmall_ev have 2: "∀⇩F x in sequentially. n3 ≤ g2 x" by fast
from assms(4) fsmall_ev have 3: "∀⇩F x in sequentially. nM ≤ f2 x" by fast
have "∀⇩F x in sequentially. n2 ≤ x" by simp
from 1 2 3 this have "∀⇩F x in sequentially. norm ((f1 ∘ f2) x) ≤ c1 * c3 * norm ((g1 ∘ g2) x)"
proof eventually_elim
case (elim x)
have "norm (f1 (f2 x)) ≤ c1 * norm (g1 (f2 x))" using f1[where x="f2 x"] elim
by blast
also { have "norm (g1 (f2 x)) ≤ norm (g1 (c2 * g2 x))"
apply(rule g1) using f2 elim by auto
also have "… ≤ c3 * norm (g1 (g2 x))" using elim f3 by auto
finally have " c1 * norm (g1 (f2 x)) ≤ c1 * (c3 * norm (g1 (g2 x)))"
using c1 by auto }
finally have "norm ((f1 ∘ f2) x) ≤ (c1 * c3) * (norm (g1 (g2 x)))" by auto
then show "norm (((f1 ∘ f2) x)) ≤ (c1 * c3) * norm ((g1 ∘ g2) x) "
using of_nat_mono by fastforce
qed
thus ?thesis by(rule bigoI[where c="c1 * c3"])
qed
lemma bigTheta_compose:
fixes f1 g1 :: "nat⇒real" and f2 g2:: "nat ⇒ nat"
assumes "stablebigO g1"
and "f1 ∈ Θ(g1)" "f2 ∈ Θ(g2)"
and "f2 ∈ ω(λn. 1)"
and "event_mono g1"
shows "f1 o f2 ∈ Θ(g1 o g2)"
proof -
from assms(3,4) have z: "g2 ∈ ω(λn. 1)"
using landau_omega.small.in_cong_bigtheta by blast
have "f1 o f2 ∈ O(g1 o g2)" apply(rule bigO_compose) using z assms by auto
moreover have "f1 o f2 ∈ Ω(g1 o g2)" apply(rule bigOmega_compose) using assms z by auto
ultimately show ?thesis by auto
qed
lemma polylog_power_compose:
"polylog a b o (λn. n ^ c) ∈ Θ(polylog (c * a) b)"
unfolding polylog_def unfolding comp_def
proof -
fix x::nat assume "x > 0"
then have "ln (real (x ^ c)) = c * ln (real x)"
using ln_realpow by auto
then have "ln (real (x ^ c)) ^ b = c ^ b * ln (real x) ^ b"
by (simp add: semiring_normalization_rules(30))
oops
lemma bigTheta_compose_linear:
fixes f1 g1 :: "nat⇒real" and f2 :: "nat ⇒ nat"
assumes "stablebigO g1" "event_mono g1"
and "f1 ∈ Θ(g1)" "f2 ∈ Θ(%n. n)"
shows "(λn. f1 (f2 n)) ∈ Θ(g1)"
proof -
from assms(4) have g: "(λx. real (f2 x)) ∈ ω(λn. 1)"
by (metis (full_types) eventually_at_top_linorder eventually_nat_real filterlim_at_top filterlim_at_top_iff_smallomega landau_omega.small.in_cong_bigtheta)
have z: "g1 o (λn. n) = g1" by auto
have "f1 o f2 ∈ Θ(g1 o (%n. n))"
apply(rule bigTheta_compose)
using assms g by auto
thus ?thesis unfolding z comp_def .
qed
lemma bigTheta_compose_linear':
fixes f1 g1 :: "nat⇒real" and f2 :: "nat ⇒ nat"
assumes "stablebigO g1" "event_mono g1" "f1 ∈ Θ(g1)" "f2 ∈ Θ(polylog 1 0)"
shows "(λx. f1 (f2 x)) ∈ Θ(g1)"
proof -
show ?thesis
apply (rule bigTheta_compose_linear)
using assms unfolding polylog_def by auto
qed
section ‹Asymptotic behaviour of arithmetic operations›
lemma asym_bound_div:
fixes c :: nat and f :: "nat ⇒ nat"
shows "c > 0 ⟹ f ∈ Ω(λn. n) ⟹ f ∈ Θ(g) ⟹ (λn. (f n) div c) ∈ Θ(g)"
proof -
have estim: "⋀x. x > c ⟹ c>0 ⟹ real (c*2) * real (x div c) ≥ real (x)"
proof -
fix x::nat assume "x>c" "c>0"
have "1 = c div c" using ‹c>0› by auto
also have "… ≤ x div c" using ‹x>c› by(auto intro!: div_le_mono)
finally have i: "1≤x div c" .
have "real x = real (x mod c + c * (x div c))" by simp
also have "… = real (x mod c) + real (c * (x div c))" using of_nat_add by blast
also have "… ≤ real c + real c * real (x div c)" using ‹c>0› by auto
also have "… ≤ real c * real (x div c) + real c * real (x div c)" using i ‹0 < c› by auto
also have "… = real (c*2) * real (x div c)" by auto
finally show "real x ≤ real (c * 2) * real (x div c)" .
qed
have r: "⋀a b c. c > 0 ⟹ (a::real) ≥ b / c ⟹ b ≤ c * a"
by (simp add: mult.commute pos_divide_le_eq)
assume c0: "c>0"
assume Om: "f ∈ Ω(λn. n)"
assume "f ∈ Θ(g)"
then have O: "f ∈ O(g)" and Omega: "f ∈ Ω(g)" by auto
then obtain c1 n where c1: "c1>0" and "∀x≥n. norm (f x) ≤ c1 * norm (g x)" using bigOE by blast
then have f1: "⋀x. x≥n ⟹ f x ≤ c1 * norm (g x)" by auto
have O: "(λn. (f n) div c) ∈ O(g)"
apply(rule bigoI[where c="c1"])
apply(rule eventually_sequentiallyI[where c="n"])
proof -
fix x assume a: "n≤x"
have "norm (real (f x div c)) ≤ real (f x) " by simp
also have "… ≤ c1 * norm (g x) " using f1[OF a] by (simp add: divide_right_mono)
finally show "norm (real (f x div c)) ≤ (c1 ) * norm (g x)" by auto
qed
from Omega obtain c1 n where c1: "c1>0" and "∀x≥n. norm (f x) ≥ c1 * norm (g x)" using bigOmegaE by blast
then have f1: "⋀x. x≥n ⟹ f x ≥ c1 * norm (g x)" by auto
from Om fbig obtain n3 where P: "∀x≥n3. c+1 ≤ f x" by blast
let ?n = "max n3 n"
have Omega: "(λn. (f n) div c) ∈ Ω(g)"
apply(rule bigomegaI[where c="real (c*2) / c1"])
apply(rule eventually_sequentiallyI[where c="?n"])
proof -
fix x assume a: "?n≤x"
from a P have z1: "f x > c" by auto
have "norm (g x) ≤ f x / c1" using f1 a
by (simp add: c1 mult_imp_le_div_pos le_divide_eq mult.commute)
also have "… ≤ real (c*2) * real (f x div c) /c1" using estim z1 c0 by (simp add: c1 frac_le)
also have "… = ( real (c*2) / c1) * (f x div c)" by auto
also have "… = ( real (c*2) / c1) * norm (real (f x div c))" by auto
finally show "norm (g x) ≤ (real (c*2) / c1) * norm (real (f x div c))" .
qed
from Omega O show ?thesis by auto
qed
lemma asym_bound_div_linear:
fixes c :: nat and f :: "nat ⇒ nat"
shows "c > 0 ⟹ f ∈ Θ(λn. real n) ⟹ (λn. real ((f n) div c)) ∈ Θ(λn. real n)"
using asym_bound_div by auto
lemma asym_bound_diff:
fixes f :: "nat ⇒ nat" and g :: "nat ⇒ nat"
assumes "f ∈ Θ(λn. n)" "g ∈ Θ(λn. 1)"
shows "(λn. f n - g n) ∈ Θ(λn. n)"
proof -
from assms(1) obtain c n where "c>0" and P: "∀x≥n. norm (f x) ≤ c * norm (x)" using bigOE by blast
have O: "(λn. f n - g n) ∈ O(λn. n)"
apply(rule bigoI[where c=c])
apply(rule eventually_sequentiallyI[where c="n"])
using P by auto
from assms(2) have "g ∈ O(λn. 1)" by auto
from bigOE[OF this] obtain cg ng where "cg>0" and P: "∀x≥ng. norm (real (g x)) ≤ cg * norm ((λn. 1::real) ng)" by blast
then have g: "⋀x. x≥ng ⟹ g x ≤ cg" by auto
from assms(1) have fOm: "f ∈ Ω(λn. n)" by auto
from bigOmegaE[OF this] obtain cf nf where cf: "cf>0" and "∀x≥nf. cf * norm (real x) ≤ norm (real (f x))" by blast
then have f: "⋀x. x≥nf ⟹ cf * x ≤ f x" by auto
then have f: "⋀x. x≥nf ⟹ x ≤ f x / cf" using cf
by (simp add: mult.commute pos_le_divide_eq)
let ?n = "max (max nf ng) (nat ⌈2*cg/cf⌉)"
have Om: "(λn. f n - g n) ∈ Ω(λn. n)"
apply(rule bigomegaI[where c="(2/cf)"])
apply(rule eventually_sequentiallyI[where c="?n"])
proof -
fix x assume n: "?n≤x"
have z1: "x≥ng" using n by auto
with g have "g x ≤ cg" by auto
then have g': "real (f x) - cg ≤ real (f x) - g x" by auto
have z3: "x≥nf" using n by auto
have "x≥2*cg/cf" using n by auto
then have "x ≤ 2*(real x) - (2*cg/cf)" by linarith
also have "… ≤ 2*(f x/cf) - (2*cg/cf)" using f[OF z3] by auto
also have "… = 2/cf * (f x) - (2/cf)*cg" by auto
also have "… = (2/cf) * (f x - cg)" by (simp add: right_diff_distrib')
also have "… ≤ (2/cf) * (f x - g x)" apply(rule mult_left_mono) using g' cf by auto
also have "… = (2/cf) * norm (real (f x - g x)) " by auto
finally
show "norm (real x) ≤ (2/cf) * norm (real (f x - g x)) " by auto
qed
from O Om show ?thesis by auto
qed
section ‹Asymptotic behaviour of ceiling and log›
lemma fixes f:: "nat⇒real" and g :: "nat ⇒ real"
shows ceiling_Theta: "eventually_nonneg at_top f ⟹ (λn. g n) ∈ ω(λx. 1::real) ⟹ (λn. f n) ∈ Θ(g) ⟹ (λn. real (nat ⌈f n⌉)) ∈ Θ(g)"
proof
assume "(λn. (g n)) ∈ ω(λx. 1::real)"
from fsmall'[OF this,of 1] obtain ng where ng: "∀x≥ng. 1 ≤ norm (g x)" by auto
assume Th:"(λn. f n) ∈ Θ(g)"
from Th have "(λn. f n) ∈ O(g)" by auto
then obtain n c where "c>0" and O: "∀x≥n. norm (f x) ≤ c * norm (g x)" using bigOE by blast
let ?n = "max (nat⌈ng⌉) n"
show "(λn. real (nat ⌈f n⌉)) ∈ O(g)"
proof (rule bigoI[where c="c+1"], rule eventually_sequentiallyI[where c="?n"])
fix x assume "?n≤x"
then have xn: "x≥n" and xng: "x≥ng" by auto
have "norm (real (nat ⌈f x⌉)) = real (nat ⌈f x⌉)" by auto
also have "… ≤ real (nat ⌈norm (f x)⌉)"
by (smt of_nat_0_less_iff real_norm_def zero_less_ceiling zero_less_nat_eq)
also have "… = of_int ⌈norm (f x)⌉" by auto
also have "… ≤ norm (f x) + 1" by(rule of_int_ceiling_le_add_one)
also have "… ≤ c * norm (g x) + 1 " using O xn by auto
also have "… ≤ c * norm (g x) + norm (g x)" using ng xng by auto
also have "… ≤ (c+1) * norm (g x)" by argo
finally
show "norm (real (nat ⌈f x⌉)) ≤ (c+1) * norm (g x)" .
qed
assume "eventually_nonneg at_top f"
then have "∀⇩F n in at_top. f n ≥ 0" unfolding eventually_nonneg_def by auto
then obtain N where fpos: "⋀n. n≥N ⟹ f n ≥ 0" unfolding eventually_sequentially by auto
from Th have "(λn. f n) ∈ Ω(g)" by auto
then obtain n ::nat and c where c: "c>0" and "∀x≥n. c * norm (g x) ≤ norm (f x)" using bigOmegaE by blast
then have Om: "⋀x. x≥n ⟹ norm (g x) ≤ norm (f x) / c "
by (simp add: le_divide_eq mult.commute)
let ?n = "max N n"
show "(λn. real (nat ⌈f n⌉)) ∈ Ω(g)"
proof (rule bigomegaI[where c="(1/c)"], rule eventually_sequentiallyI[where c="?n"])
fix x assume x: "x≥?n"
with Om have "norm (g x) ≤ (1/c) * norm (f x)" by auto
also have "… ≤ (1/c) * norm (real (nat ⌈f x⌉))" apply(rule mult_left_mono) using c x fpos apply auto
by (simp add: real_nat_ceiling_ge)
finally show "norm (g x) ≤ (1/c) * norm (real (nat ⌈f x⌉))" .
qed
qed
lemma eventually_nonneg_logplus: "c≥0 ⟹ eventually_nonneg sequentially (λn. c * log 2 (real (d + n)))"
unfolding eventually_nonneg_def eventually_sequentially apply(rule exI[where x=1])
unfolding log_def by auto
lemma log_2_asym': "(λx::nat. real (f x)) ∈ Θ(real) ⟹ (λn. log 2 (real (f n))) ∈ Θ(ln)"
apply(rule bigTheta_compose_linear[of _ "log 2"])
apply(rule stablebigO_ln)
apply(rule event_mono_ln)
unfolding log_def by (auto simp add: asymp_equiv_imp_bigtheta asymp_equiv_plus_const_left)
lemma log_2_asym: "(λn. log 2 (real (d + n))) ∈ Θ(ln)"
apply (rule log_2_asym')
by (auto simp add: asymp_equiv_imp_bigtheta asymp_equiv_plus_const_left)
lemma abcd_lnx:
assumes a: "a≥0" and b: "b≥1" and c: "c > 0" and d: "d ≥ 0" shows "(λn. a + b * real (nat ⌈c * log 2 (real (d + n))⌉)) ∈ Θ(λx. ln (real x))" (is "(λn. a + ?f n) ∈ Θ(?g)")
proof -
have "(λn. log 2 (real (d + n))) ∈ Θ(ln)" using log_2_asym by auto
then have log_c: "(%n. c * log 2 (real (d + n))) ∈ Θ(ln)" using c by auto
have ceil: "(λn. real (nat ⌈c * log 2 (real (d + n))⌉)) ∈ Θ(λx. ln (real x))"
apply(rule ceiling_Theta)
apply(rule eventually_nonneg_logplus) using c apply simp
using log_c by auto
then have ceil_b: "(λn. b * real (nat ⌈c * log 2 (real (d + n))⌉)) ∈ Θ(λx. ln (real x))" using b by auto
have plusa: "Θ(λx. a + ?f x) = Θ(?f)"
apply(rule landau_theta.plus_absorb1)
apply(rule landau_o.small.bigtheta_trans1'[OF _ ceil_b])
by auto
from ceil_b plusa show ?thesis
using bigtheta_sym by blast
qed
lemma log2_gt_zero: "x≥1 ⟹ log 2 x ≥ 0" unfolding log_def using ln_gt_zero by auto
section ‹Theta addition for any filter›
lemma
fixes f1 g1 f2 g2 :: "_ ⇒ real"
assumes "eventually_nonneg F f1" "eventually_nonneg F f2"
"eventually_nonneg F g1" "eventually_nonneg F g2"
"Θ[F](f1) = Θ[F](f2)" "Θ[F](g1) = Θ[F](g2)"
shows Theta_plus: "Θ[F](λx. f1 x + g1 x) = Θ[F](λx. f2 x + g2 x)"
proof (rule landau_theta.cong_bigtheta, rule)
from assms have f: "f1 ∈ O[F](f2)" and g: "g1 ∈ O[F](g2)" by simp_all
from f obtain cf where cf: "cf>0" and 1: "∀⇩F x in F. norm (f1 x) ≤ cf * norm (f2 x)" using landau_o.bigE by blast
from g obtain cg where cg: "cg>0" and 2: "∀⇩F x in F. norm (g1 x) ≤ cg * norm (g2 x)" using landau_o.bigE by blast
note B= 1 2 assms(2,4)[unfolded eventually_nonneg_def]
show "(λx. f1 x + g1 x) ∈ O[F](λx. f2 x + g2 x)"
apply(rule landau_o.bigI[where c="(max cf cg)"])
using cf cg apply simp
using B
proof eventually_elim
case (elim x)
have un: "norm (f1 x) ≤ (max cf cg) * norm (f2 x)" "norm (g1 x) ≤ (max cf cg) * norm (g2 x)"
by (meson elim(1,2) dual_order.trans max.cobounded1 max.cobounded2 mult_right_mono norm_ge_zero)+
have "norm (f1 x + g1 x) ≤ norm (f1 x) + norm (g1 x)" by (simp add: norm_triangle_ineq)
also have "… ≤ (max cf cg) * norm (f2 x) + (max cf cg) * norm (g2 x)" using un by linarith
also have "… = (max cf cg) * (norm (f2 x) + norm (g2 x))" by (simp add: distrib_left)
also have "… = (max cf cg) * norm (f2 x + g2 x)" using elim(3,4) by simp
finally show ?case .
qed
from assms have f: "f1 ∈ Ω[F](f2)" and g: "g1 ∈ Ω[F](g2)" by simp_all
from f obtain cf where cf: "cf>0" and 1: "∀⇩F x in F. norm (f1 x) ≥ cf * norm (f2 x)" using landau_omega.bigE by blast
from g obtain cg where cg: "cg>0" and 2: "∀⇩F x in F. norm (g1 x) ≥ cg * norm (g2 x)" using landau_omega.bigE by blast
note B=1 2 assms(1,3)[unfolded eventually_nonneg_def]
show "(λx. f1 x + g1 x) ∈ Ω[F](λx. f2 x + g2 x)"
apply(rule landau_omega.bigI[where c="(min cf cg)"])
using cf cg apply simp
using B
proof eventually_elim
case (elim x)
have un: "norm (f1 x) ≥ (min cf cg) * norm (f2 x)" "norm (g1 x) ≥ (min cf cg) * norm (g2 x)"
by (meson elim(1,2) min.cobounded2 min.cobounded1 mult_le_cancel_right norm_ge_zero not_le order_trans)+
have "min cf cg * norm (f2 x + g2 x) ≤ min cf cg * (norm (f2 x) + norm (g2 x))" apply(rule mult_left_mono)
using cf cg by auto
also have "… = (min cf cg) * norm (f2 x) + (min cf cg) * norm (g2 x)" by (simp add: distrib_left)
also have "… ≤ norm (f1 x) + norm (g1 x)" using un by linarith
also have "… ≤ norm (f1 x + g1 x)" using elim(3,4) by auto
finally show ?case .
qed
qed
lemma
fixes f1 g1 f2 g2 :: "_ ⇒ real"
assumes "eventually_nonneg F f1" "eventually_nonneg F f2"
"eventually_nonneg F g1" "eventually_nonneg F g2"
"Θ[F](f1) = Θ[F](f2)" "Θ[F](g1) = Θ[F](g2)"
shows Theta_plus': "Θ[F](f1 + g1) = Θ[F](f2 + g2)"
proof -
have 1: "(λx. f1 x + g1 x) = f1 + g1" by auto
have 2: "(λx. f2 x + g2 x) = f2 + g2" by auto
show ?thesis using 1 2 Theta_plus[OF assms] by auto
qed
section ‹Automation›
lemma landau_norms:
"real 1 = polylog 0 0 x"
"real x = polylog 1 0 x"
"ln x = polylog 0 1 x"
"real (x ^ a) = polylog a 0 x"
"(ln x) ^ b = polylog 0 b x"
"polylog a1 b1 x * polylog a2 b2 x = polylog (a1 + a2) (b1 + b2) x"
by (simp_all add: power_add polylog_def)
lemma plus_absorb1': "f ∈ o[F](g) ⟹ Θ[F](f + g) = Θ[F](g)"
unfolding plus_fun_def by (rule landau_theta.plus_absorb1)
lemma plus_absorb2': "g ∈ o[F](f) ⟹ Θ[F](f + g) = Θ[F](f)"
unfolding plus_fun_def by (rule landau_theta.plus_absorb2)
lemma plus_absorb_same': "Θ[F](f + f) = Θ[F](f)"
unfolding plus_fun_def by auto
lemma bigtheta_add:
assumes " eventually_nonneg F g1" " eventually_nonneg F g2"
"(λx. real (f1 x)) ∈ Θ[F](g1)" "(λx. real (f2 x)) ∈ Θ[F](g2)"
shows "(λx. real (f1 x + f2 x)) ∈ Θ[F](g1 + g2)"
proof -
have u: "g1 + g2 = (λx. g1 x + g2 x)" by auto
have "Θ[F](λx. real (f1 x) + real (f2 x)) = Θ[F](λx. g1 x + g2 x)"
apply(rule Theta_plus)
apply(rule event_nonneg_real)
apply fact
apply(rule event_nonneg_real)
apply fact
using assms landau_theta.cong_bigtheta by blast+
then show ?thesis by(simp add: u)
qed
lemma landau_norm_linear:
"polylog 1 0 = real" unfolding polylog_def by auto
lemma landau_norm_const:
"polylog 0 0 = (λx::nat. 1::real)" unfolding polylog_def by auto
lemma landau_norm_times:
"polylog a1 a2 * polylog b1 b2 = polylog (a1 + b1) (a2 + b2)"
unfolding times_fun_def by (subst landau_norms(6)) auto
lemma bigtheta_const:
"c > 0 ⟹ (λx. real c) ∈ Θ(polylog 0 0)"
unfolding polylog_def by simp
lemma bigtheta_linear:
"(λx. real x) ∈ Θ(polylog 1 0)"
unfolding polylog_def by simp
lemma bigtheta_mult:
"(λx. real (f1 x)) ∈ Θ[F](g1) ⟹ (λx. real (f2 x)) ∈ Θ[F](g2) ⟹
(λx. real (f1 x * f2 x)) ∈ Θ[F](g1 * g2)"
unfolding times_fun_def
apply (subst bigtheta_mult_eq_set_mult)
unfolding set_mult_def by auto
ML_file "landau_util.ML"
attribute_setup asym_bound = ‹setup_attrib LandauUtil.add_asym_bound›
ML_file "master_theorem_wrapper.ML"
method_setup master_theorem2 = ‹setup_master_theorem›
"automatically apply the Master theorem for recursive functions"
end