Theory Asymptotics_2D
theory Asymptotics_2D
imports Akra_Bazzi.Akra_Bazzi_Method Asymptotics_1D
begin
abbreviation "O⇩2(λx. f x) ≡ O[at_top ×⇩F at_top](λx. f x)"
abbreviation "o⇩2(λx. f x) ≡ o[at_top ×⇩F at_top](λx. f x)"
abbreviation "Θ⇩2(λx. f x) ≡ Θ[at_top ×⇩F at_top](λx. f x)"
abbreviation "Ω⇩2(λx. f x) ≡ Ω[at_top ×⇩F at_top](λx. f x)"
section ‹Normal form in two variables›
definition polylog2 :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat × nat ⇒ real" where
"polylog2 a b c d = (λ(n,m). polylog a b n * polylog c d m)"
lemma event_nonneg_polylog2: "eventually_nonneg (at_top ×⇩F at_top) (polylog2 a b c d)"
apply (simp add: polylog2_def)
apply (simp only: eventually_nonneg_def case_prod_beta)
apply (simp add: eventually_prod_sequentially)
apply (rule exI[where x=1]) unfolding polylog_def by auto
section ‹Stability in two variables›
definition stablebigO2 :: "(nat × nat ⇒ real) ⇒ bool" where
"stablebigO2 f = (∀c>0. ∀d>0. (λ(x,y). f (c * x, d * y)) ∈ O⇩2(f))"
lemma stablebigO2I:
assumes "⋀c d. 0 < c ⟹ 0 < d ⟹ (λx. f (c * (fst x), d * (snd x))) ∈ O⇩2(f)"
shows "stablebigO2 f"
proof -
have u: "⋀c d. (λx. f (c * (fst x), d * (snd x))) = (λ(x,y). f (c * x, d * y))" by auto
show ?thesis using assms unfolding stablebigO2_def u by simp
qed
lemma stablebigO2_mult:
fixes f g :: "nat ⇒ real"
assumes "stablebigO f" and "stablebigO g"
shows "stablebigO2 (λ(n,m). f n * g m)"
proof -
from assms(1)[unfolded stablebigO_def] have f: "⋀c. c>0 ⟹ (λx. f (c * x)) ∈ O(f)" by auto
from assms(2)[unfolded stablebigO_def] have g: "⋀d. d>0 ⟹ (λx. g (d * x)) ∈ O(g)" by auto
show ?thesis unfolding stablebigO2_def
proof (safe)
fix c d :: nat assume "c>0" "d>0"
with f g have f: "(λx. f (c * x)) ∈ O(f)"
and g: "(λx. g (d * x)) ∈ O(g)" by auto
from f obtain fc fn where fc: "fc>0" and fO: "∀x≥fn. norm (f (c * x)) ≤ fc * norm (f x)" using bigOE by blast
from g obtain gc gn where gc: "gc>0" and gO: "∀x≥gn. norm (g (d * x)) ≤ gc * norm (g x)" using bigOE by blast
let ?N = "max fn gn"
show "(λ(x, y). f (c * x) * g (d * y)) ∈ O⇩2 (λ(n, m). f n * g m)"
apply(rule landau_o.bigI[where c="(fc*gc)"])
subgoal using fc gc by simp
unfolding eventually_prod_sequentially
apply(rule exI[where x="?N"])
proof safe
fix n m :: nat assume ev: "?N≤m" "?N≤n"
have "norm (f (c * n) * g (d * m)) = norm (f (c*n)) * norm (g (d*m))" by (metis norm_mult)
also have "… ≤ (fc * norm (f n)) * norm (g (d*m))" apply(rule mult_right_mono)
using fO ev by auto
also have "… ≤ (fc * norm (f n)) * (gc * norm (g m))" apply(rule mult_left_mono)
using gO ev fc by auto
also have "… = (fc*gc) * norm (f n * g m)" using fc gc
by (metis mult.commute mult.left_commute norm_mult)
finally show "norm (f (c * n) * g (d * m)) ≤ (fc*gc) * norm (f n * g m)" .
qed
qed
qed
lemma stablebigO2D':
assumes "stablebigO2 f" "d1>0" "d2>0"
obtains c where "c>0" "eventually (λx. norm (f (d1*(fst x), d2*(snd x))) ≤ c * norm (f x)) (at_top ×⇩F at_top)"
proof -
from assms have "(λ(x,y). f (d1 * x, d2*y)) ∈ O⇩2(f)" (is "?f : _")
unfolding stablebigO2_def by auto
then obtain c where c0: "c>0" and "∀⇩F x in sequentially ×⇩F sequentially. norm (case x of (x, y) ⇒ f (d1 * x, d2 * y)) ≤ c * norm (f x)"
using landau_o.bigE by blast
then have "eventually (λx. norm (f (d1*(fst x), d2*(snd x))) ≤ c * norm (f x)) (at_top×⇩Fat_top)"
using eventually_mono by fastforce
with c0 show ?thesis by (rule that)
qed
lemma stablebigO2D:
assumes "stablebigO2 f" "d1>0" "d2>0"
obtains c where "c>0" "eventually (λ(x,y). norm (f (d1*x, d2*y)) ≤ c * norm (f (x,y))) (at_top ×⇩F at_top)"
proof -
from assms have "(λ(x,y). f (d1 * x, d2*y)) ∈ O⇩2(f)" (is "?f : _")
unfolding stablebigO2_def by auto
then obtain c where c0: "c>0" and "∀⇩F x in sequentially ×⇩F sequentially. norm (case x of (x, y) ⇒ f (d1 * x, d2 * y)) ≤ c * norm (f x)"
using landau_o.bigE by blast
then have "eventually (λ(x,y). norm (f (d1*x, d2*y)) ≤ c * norm (f (x,y))) (at_top×⇩Fat_top)"
using eventually_mono by fastforce
with c0 show ?thesis by (rule that)
qed
lemma stablebigO2_plus:
fixes f g :: "(nat*nat) ⇒ real"
assumes f: "stablebigO2 f" and g: "stablebigO2 g" and
evf: "eventually_nonneg (at_top ×⇩F at_top) f" and
evg: "eventually_nonneg (at_top ×⇩F at_top) g"
shows "stablebigO2 (f + g)"
proof (rule stablebigO2I)
fix d1 d2 :: nat assume d: "d1>0" "d2>0"
from f d obtain cf where "cf>0" and f: "eventually (λx. norm (f (d1*(fst x), d2*(snd x))) ≤ cf * norm (f x)) (sequentially×⇩Fsequentially)"
using stablebigO2D' by blast
from g d obtain cg where "cg>0" and g: "eventually (λx. norm (g (d1*(fst x), d2*(snd x))) ≤ cg * norm (g x)) (sequentially×⇩Fsequentially)"
using stablebigO2D' by blast
have evf: "eventually (λx. f x ≥ 0) (at_top ×⇩F at_top)" using evf by (simp add: eventually_nonneg_def)
have evg: "eventually (λx. g x ≥ 0) (at_top ×⇩F at_top)" using evg by (simp add: eventually_nonneg_def)
let ?c = "max cf cg"
show "(λx. (f + g) (d1 * fst x, d2 * snd x)) ∈ O⇩2 (f + g)"
apply(rule bigoI[where c="max cf cg"]) using f g evf evg
proof (eventually_elim)
case (elim x)
then have nf: "norm (f x + g x) = norm (f x)+ norm (g x)" by auto
have "norm ((f+g)(d1*(fst x), d2*(snd x))) = norm(f (d1*(fst x), d2*(snd x))+g (d1*(fst x), d2*(snd x)))" by auto
also have "… ≤ norm(f (d1*(fst x), d2*(snd x))) + norm (g (d1*(fst x), d2*(snd x)))"
by (simp add: norm_triangle_ineq)
also have "… ≤ cf * norm (f x) + cg * norm (g x)" using elim(1,2) 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)" unfolding nf by auto
finally show ?case by simp
qed
qed
lemma stable_polylog2: "stablebigO2 (polylog2 a b c d)"
apply (simp add: polylog2_def)
apply (rule stablebigO2_mult)
apply (rule stable_polylog)
apply (rule stable_polylog)
done
section ‹Eventual monotonicity in two variables›
definition event_mono2 :: "((nat*nat) ⇒ real) ⇒ bool" where
"event_mono2 g1 = eventually (λ(x1,y1). ∀x2≥x1. ∀y2≥y1. norm (g1 (x1,y1)) ≤ norm (g1 (x2,y2))) (at_top ×⇩F at_top)"
lemma event_mono2_mult:
assumes f: "event_mono f" and g: "event_mono g"
shows "event_mono2 (λ(x,y). f x * g y)"
proof -
note B=eventually_prodI[OF f[unfolded event_mono_def] g[unfolded event_mono_def]]
{ fix x :: "nat * nat"
assume a: "(∀x2≥fst x. norm (f (fst x)) ≤ norm (f x2))"
assume b: "(∀x2≥snd x. norm (g (snd x)) ≤ norm (g x2))"
have "∀x2≥fst x. ∀y2≥snd x. norm (f (fst x) * g (snd x)) ≤ norm (f x2 * g y2)"
proof safe
fix x2 assume x2: "x2≥fst x"
fix y2 assume y2: "y2≥snd x"
have "norm (f (fst x) * g (snd x)) ≤ norm (f (fst x)) * norm (g (snd x))"
by (metis norm_mult order_refl)
also have "… ≤ norm (f x2) * norm (g (snd x))" apply(rule mult_right_mono)
using a x2 by auto
also have "… ≤ norm (f x2) * norm (g y2)" apply(rule mult_left_mono)
using b y2 by auto
also have "… = (norm (f x2 * g y2))" by (metis norm_mult)
finally show "norm (f (fst x) * g (snd x)) ≤ norm (f x2 * g y2)" .
qed
} note A = this
show ?thesis unfolding event_mono2_def
apply(rule eventually_mono[OF B _])
using A by auto
qed
lemma event_mono2_polylog2: "event_mono2 (polylog2 a b c d)"
apply (simp add: polylog2_def)
apply (rule event_mono2_mult)
apply (rule event_mono_polylog)
apply (rule event_mono_polylog)
done
lemma event_mono2_plus:
assumes f : "event_mono2 f" and g: "event_mono2 g" and
evf: "eventually_nonneg (at_top ×⇩F at_top) f" and
evg: "eventually_nonneg (at_top ×⇩F at_top) g"
shows "event_mono2 (f + g)"
proof -
have "eventually (λx. f x ≥ 0) (at_top ×⇩F at_top)" using evf by (simp add: eventually_nonneg_def)
then have evf: "eventually (λx. ∀x2 y2. x2≥fst x ∧ y2≥snd x ⟶ f (x2,y2) ≥ 0) (at_top ×⇩F at_top)"
unfolding eventually_prod_sequentially apply auto subgoal for N apply(rule exI[where x=N]) by auto done
have "eventually (λx. g x ≥ 0) (at_top ×⇩F at_top)" using evg by (simp add: eventually_nonneg_def)
then have evg: "eventually (λx. ∀x2 y2. x2≥fst x ∧ y2≥snd x ⟶ g (x2,y2) ≥ 0) (at_top ×⇩F at_top)"
unfolding eventually_prod_sequentially apply auto subgoal for N apply(rule exI[where x=N]) by auto done
note prem = evf f[unfolded event_mono2_def] g[unfolded event_mono2_def] evg
show ?thesis
unfolding event_mono2_def plus_fun_def
using prem
proof eventually_elim
case (elim x)
show "case x of (x1, y1) ⇒ ∀x2≥x1. ∀y2≥y1. norm (f (x1, y1) + g (x1, y1)) ≤ norm (f (x2, y2) + g (x2, y2))"
proof safe
fix x1 y1 x2 y2 assume x_eq: "x = (x1, y1)" and x2: "x1 ≤ x2" and y2: "y1 ≤ y2"
with elim(1,4) have e: "f (x2, y2) ≥ 0" "g (x2, y2) ≥ 0" by force+
have "norm (f (x1, y1) + g (x1, y1)) ≤ norm (f (x1, y1)) + norm (g (x1, y1))" by (simp add: norm_triangle_ineq)
also have "… ≤ norm (f (x2, y2)) + norm (g (x2, y2))" using elim(2,3) x_eq x2 y2 by fastforce
also have "… = norm (f (x2, y2) + g (x2, y2))" using e by simp
finally show "norm (f (x1, y1) + g (x1, y1)) ≤ norm (f (x2, y2) + g (x2, y2))" .
qed
qed
qed
section ‹Auxiliary lemmas›
lemma bigO2E:
fixes f :: "nat × nat ⇒ real"
assumes "f ∈ O⇩2(g)"
obtains c n where "c > 0" "⋀x. fst x≥n ⟹ snd x≥n ⟹ norm (f x) ≤ c * norm (g x)"
proof -
from assms obtain c where c1: "c>0" and
"∀⇩F x in (at_top×⇩Fat_top). norm (f x) ≤ c * norm (g x)" using landau_o.bigE by blast
then obtain n where f1: "⋀x. fst x≥n ⟹ snd x ≥n ⟹ norm (f x) ≤ c * norm (g x)"
unfolding eventually_prod_sequentially apply auto by blast
from c1 and f1 show ?thesis by (rule that)
qed
lemma bigOmega2E:
fixes f :: "(nat*nat) ⇒ real"
assumes "f ∈ Ω⇩2(g)"
obtains c n where "c > 0" "⋀x. fst x≥n ⟹ snd x≥n ⟹ norm (f x) ≥ c * norm (g x)"
proof -
from assms obtain c where c1: "c>0" and
"∀⇩F x in (at_top×⇩Fat_top). norm (f x) ≥ c * norm (g x)" using landau_omega.bigE by blast
then obtain n where f1: "⋀x. fst x≥n ⟹ snd x ≥n ⟹ norm (f x) ≥ c * norm (g x)"
unfolding eventually_prod_sequentially apply auto by blast
from c1 and f1 show ?thesis by (rule that)
qed
section ‹Composition in the two variable case›
lemma mult_bivariate_I:
fixes f :: "nat ⇒ nat"
assumes "f ∈ Θ(λn. n)"
shows "(λ(n,m). real (f (n*m))) ∈ Θ⇩2(λ(n,m). real (n * m))" (is "?f ∈ Θ[?F](?g)")
proof
from assms have O: "f ∈ O(λn. n)" and Om: "f∈Ω(λn. n)" by auto
from O obtain CO NO where "⋀x. x≥NO ⟹ norm (f x) ≤ CO * norm (x)"
using bigOE by blast
then have O': "⋀x y. x*y≥NO ⟹ real (f (x*y)) ≤ CO * (real x * real y)" by fastforce
show "?f ∈ O[?F](?g)"
apply(rule bigoI[where c=CO])
apply(simp only: eventually_prod_sequentially)
apply(rule exI[where x="NO+1"])
apply auto apply(rule O')
using nat_le_prod_with_le by auto
from Om obtain CO NO where c0: "CO > 0" and "⋀x. x≥NO ⟹ CO * norm x ≤ norm (f x)"
using bigOmegaE by blast
then have "⋀x y. x*y≥NO ⟹ CO * (real x * real y) ≤ real (f (x*y))" by fastforce
then have Om': "⋀x y. x*y≥NO ⟹ (real x * real y) ≤ real (f (x*y)) / CO"
using c0 by (simp add: le_divide_eq mult.commute pos_le_divide_eq)
show "?f ∈ Ω[?F](?g)"
apply(rule bigomegaI[where c="(1/CO)"])
apply(simp only: eventually_prod_sequentially)
apply(rule exI[where x="NO+1"])
apply auto apply (rule Om')
using nat_le_prod_with_le by auto
qed
lemma bigO2_compose_both:
fixes f1 :: "nat × nat ⇒ nat" and f2a g2a f2b g2b:: "nat ⇒ nat"
assumes "stablebigO2 g1"
and "f1 ∈ O⇩2(g1)"
and a: "f2a ∈ O(g2a)" "f2a ∈ ω(λn. 1)" "g2a ∈ ω(λn. 1)"
and b: "f2b ∈ O(g2b)" "f2b ∈ ω(λn. 1)" "g2b ∈ ω(λn. 1)"
and monog1: "eventually (λ(x1,y1). ∀x2≥x1. ∀y2≥y1. norm (g1 (x1,y1)) ≤ norm (g1 (x2,y2))) (at_top ×⇩F at_top)"
shows "(λ(x,y). f1 (f2a x, f2b y)) ∈ O⇩2((λ(x,y). g1 (g2a x, g2b y)))"
proof -
from assms(2) obtain c1 :: real and n1 :: nat where c1: "c1>0" and
f1: "⋀x. fst x≥n1 ⟹ snd x≥n1 ⟹ norm (f1 x) ≤ c1 * norm (g1 x)" using bigO2E by blast
from a obtain c2a n2a :: nat where c2a: "c2a>0" and
f2a: "⋀x. x≥n2a ⟹ f2a x ≤ c2a * g2a x" using bigOE_nat by blast
from b obtain c2b n2b :: nat where c2b: "c2b>0" and
f2b: "⋀x. x≥n2b ⟹ f2b x ≤ c2b * g2b x" using bigOE_nat by blast
from assms(1) have "(λ(x, y). g1 (c2a * x, c2b* y)) ∈ O⇩2 g1"
unfolding stablebigO2_def using c2a c2b by blast
from bigO2E[OF this] obtain c3 ::real and n3 :: nat where c3: "c3>0" and
f3: "⋀x. n3 ≤ fst x ⟹ n3 ≤ snd x ⟹ norm (case x of (x, y) ⇒ g1 (c2a * x, c2b * y)) ≤ c3 * norm (g1 x)" by blast
then have
f3: "⋀x y. n3 ≤ x ⟹ n3 ≤ y ⟹ norm (g1 (c2a * x, c2b * y)) ≤ c3 * norm (g1 (x,y))" by auto
from a fsmall obtain nf2a where nf2a: "∀x≥nf2a. n1 ≤ f2a x" by fast
from a fsmall obtain ng2a where ng2a: "∀x≥ng2a. n3 ≤ g2a x" by fast
from b fsmall obtain nf2b where nf2b: "∀x≥nf2b. n1 ≤ f2b x" by fast
from b fsmall obtain ng2b where ng2b: "∀x≥ng2b. n3 ≤ g2b x" by fast
from monog1 obtain nM where"∀y1≥nM. ∀x1≥nM. ∀x2≥x1. ∀y2≥y1. norm (g1 (x1, y1)) ≤ norm (g1 (x2, y2))"
unfolding eventually_prod_sequentially by blast
then have monog1: "⋀x1 y1 x2 y2. x1 ≥ nM ⟹ y1 ≥ nM ⟹ x2≥x1 ⟹ y2≥y1 ⟹ norm (g1 (x1, y1)) ≤ norm (g1 (x2, y2))"
by auto
from a fsmall obtain nf3a where nf3a: "∀x≥nf3a. nM ≤ f2a x" by fast
from b fsmall obtain nf3b where nf3b: "∀x≥nf3b. nM ≤ f2b x" by fast
let ?n = "max (max nf2a nf2b) (max (max ng2a ng2b) (max (max nf3a nf3b) (max nM (max n3 (max (max n2a n2b) n1)))))"
show ?thesis
apply (rule bigoI[where c="c1 * c3"])
unfolding eventually_prod_sequentially
apply (rule exI[where x="?n"])
proof safe
fix n m :: nat
assume n: "?n≤n"
have z1a: "n1 ≤ f2a n" using n nf2a by auto
have z3a: "n3 ≤ g2a n" using n ng2a by auto
assume m: "?n≤m"
have z1b: "n1 ≤ f2b m" using m nf2b by auto
have z3b: "n3 ≤ g2b m" using m ng2b by auto
have "norm (real (f1 (f2a n, f2b m))) ≤ c1 * norm (g1 (f2a n, f2b m))"
apply (rule f1) using z1a z1b m by auto
also { have " norm (g1 (f2a n, f2b m)) ≤ norm (g1 (c2a * g2a n, c2b * g2b m))"
apply (rule monog1) using f2a f2b nf3a nf3b n m by auto
also have "… ≤ c3 * norm (g1 (g2a n, g2b m))"
apply (rule f3) using z3a z3b by auto
finally have " c1 * norm (g1 (f2a n, f2b m)) ≤ c1 * (c3 * norm (g1 (g2a n, g2b m)))"
using c1 by auto }
finally have "norm (real (f1 (f2a n, f2b m))) ≤ (c1 * c3) * (norm (g1 (g2a n, g2b m)))" by auto
then show "norm (real (f1 (f2a n, f2b m))) ≤ c1 * c3 * norm (g1 (g2a n, g2b m))"
using of_nat_mono by fastforce
qed
qed
lemma bigOmega2_compose_both:
fixes f1 :: "nat × nat ⇒ nat" and f2a g2a f2b g2b :: "nat ⇒ nat"
assumes "stablebigO2 g1"
and "f1 ∈ Ω⇩2(g1)"
and a: "f2a ∈ Ω(g2a)" "f2a ∈ ω(λn. 1)" "g2a ∈ ω(λn. 1)"
and b: "f2b ∈ Ω(g2b)" "f2b ∈ ω(λn. 1)" "g2b ∈ ω(λn. 1)"
and monog1: "eventually (λ(x1,y1). ∀x2≥x1. ∀y2≥y1. norm (g1 (x1,y1)) ≤ norm (g1 (x2,y2))) (at_top ×⇩F at_top)"
shows "(λ(x,y). f1 (f2a x,f2b y)) ∈ Ω⇩2((λ(x,y). g1 (g2a x,g2b y)))"
proof -
from assms(2) obtain c1 and n1 :: nat where c1: "c1>0"
and f1: "⋀x. fst x≥n1 ⟹ snd x≥n1 ⟹ norm (f1 x) ≥ c1 * norm (g1 x)" using bigOmega2E by blast
then have f1: "⋀x. fst x≥n1 ⟹ snd x≥n1 ⟹ norm (g1 x) ≤norm (f1 x) / c1" using c1
by (simp add: mult.commute pos_le_divide_eq)
from a obtain c2a n2a :: nat where c2a: "c2a>0" and
f2a: "⋀x. x ≥ n2a ⟹ g2a x ≤ c2a * f2a x" using bigOmegaE_nat by blast
from b obtain c2b n2b :: nat where c2b: "c2b>0" and
f2b: "⋀x. x ≥ n2b ⟹ g2b x ≤ c2b * f2b x" using bigOmegaE_nat by blast
from assms(1) have "(λ(x, y). g1 (c2a * x,c2b * y)) ∈ O⇩2 g1"
unfolding stablebigO2_def using c2a c2b by blast
from bigO2E[OF this] obtain c3 ::real and n3 :: nat where c3: "c3>0" and
f3: "⋀x. n3 ≤ fst x ⟹ n3 ≤ snd x ⟹ norm (case x of (x, y) ⇒ g1 (c2a * x,c2b * y)) ≤ c3 * norm (g1 x)" by blast
then have
f3: "⋀x y. n3 ≤ x ⟹ n3 ≤ y ⟹ norm (g1 (c2a * x,c2b * y)) ≤ c3 * norm (g1 (x,y))" by auto
from monog1 obtain nM where"∀y1≥nM. ∀x1≥nM. ∀x2≥x1. ∀y2≥y1. norm (g1 (x1, y1)) ≤ norm (g1 (x2, y2))"
unfolding eventually_prod_sequentially by blast
then have monog1: "⋀x1 y1 x2 y2. x1 ≥ nM ⟹ y1 ≥ nM ⟹ x2≥x1 ⟹y2≥y1 ⟹ norm (g1 (x1, y1)) ≤ norm (g1 (x2, y2))"
by auto
from a fsmall obtain nf2a where nf2a: "∀x≥nf2a. n1 ≤ f2a x" by force
from a fsmall obtain ng2a where ng2a: "∀x≥ng2a. n3 ≤ f2a x" by force
from a fsmall obtain ng3a where ng3a: "∀x≥ng3a. nM ≤ g2a x" by fast
from b fsmall obtain nf2b where nf2b: "∀x≥nf2b. n1 ≤ f2b x" by force
from b fsmall obtain ng2b where ng2b: "∀x≥ng2b. n3 ≤ f2b x" by force
from b fsmall obtain ng3b where ng3b: "∀x≥ng3b. nM ≤ g2b x" by fast
let ?n = "max (max nf2a nf2b) (max (max ng2a ng2b) (max nM (max (max ng3a ng3b) (max n1 (max (max n2a n2b) n3)))))"
show ?thesis
apply (rule bigomegaI[where c="c3/c1"])
unfolding eventually_prod_sequentially
apply (rule exI[where x="?n"])
proof safe
fix n m :: nat
assume n: "?n≤n"
have z1a: "n1 ≤ f2a n" using n nf2a by auto
have z2a: "n2a ≤ n" using n by auto
have z3a: "n3 ≤ f2a n" using n ng2a by auto
have z4a: "nM ≤ g2a n" using ng3a n by auto
assume m: "?n≤m"
have z1b: "n1 ≤ f2b m" using m nf2b by auto
have z2b: "n2b ≤m " using m by auto
have z3b: "n3 ≤ f2b m" using m ng2b by auto
have z4b: "nM ≤ g2b m" using ng3b m by auto
have za: "g2a n ≤ c2a * f2a n" using f2a z2a by auto
have zb: "g2b m ≤ c2b * f2b m" using f2b z2b by auto
have "norm ( (g1 (g2a n,g2b m))) ≤ norm (g1 (c2a * f2a n,c2b * f2b m))"
apply (rule monog1) using n m za zb z4a z4b by auto
also have "… ≤ c3 * norm (g1 (f2a n, f2b m))" apply(rule f3) using z3a z3b by auto
also have "… ≤ c3 * (norm (f1 (f2a n, f2b m))/c1)" apply(rule mult_left_mono) apply(rule f1)
using c3 z1a z1b by auto
also have "… = (c3/c1) * norm (f1 (f2a n, f2b m))" by auto
finally show "norm (g1 (g2a n, g2b m)) ≤ c3 / c1 * norm (real (f1 (f2a n, f2b m)))" by auto
qed
qed
lemma bigTheta2_compose_both:
fixes f1 :: "nat × nat ⇒ nat" and f2a g2a f2b g2b :: "nat ⇒ nat"
assumes "stablebigO2 g1"
and "f1 ∈ Θ⇩2(g1)"
and a: "f2a ∈ Θ(g2a)" "f2a ∈ ω(λn. 1)"
and b: "f2b ∈ Θ(g2b)" "f2b ∈ ω(λn. 1)"
and monog1: "eventually (λ(x1,y1). ∀x2≥x1. ∀y2≥y1. norm (g1 (x1,y1)) ≤ norm (g1 (x2,y2))) (at_top ×⇩F at_top)"
shows "(λ(x,y). f1 (f2a x,f2b y)) ∈ Θ⇩2((λ(x,y). g1 (g2a x,g2b y)))"
proof -
from a have a': "g2a ∈ ω(λn. 1)"
using landau_omega.small.in_cong_bigtheta by blast
from b have b': "g2b ∈ ω(λn. 1)"
using landau_omega.small.in_cong_bigtheta by blast
have "(λ(x,y). f1 (f2a x,f2b y)) ∈ O⇩2((λ(x,y). g1 (g2a x,g2b y)))"
apply (rule bigO2_compose_both) using assms a' b' by auto
moreover have "(λ(x,y). f1 (f2a x, f2b y)) ∈ Ω⇩2((λ(x,y). g1 (g2a x, g2b y)))"
apply (rule bigOmega2_compose_both) using assms a' b' by auto
ultimately show ?thesis by auto
qed
lemma bigTheta2_compose_both_linear:
fixes f1 :: "nat × nat ⇒nat" and f2a f2b :: "nat ⇒ nat"
assumes "stablebigO2 g1" "event_mono2 g1"
and "f1 ∈ Θ⇩2(g1)"
and a: "f2a ∈ Θ(%n. n)" and b: "f2b ∈ Θ(%n. n)"
shows "(λ(x,y). f1 (f2a x,f2b y)) ∈ Θ⇩2(g1)"
proof -
from a have a': "f2a ∈ ω(λn. 1)"
by (metis (full_types) bigthetaD2 eventually_at_top_linorder eventually_nat_real
filterlim_at_top filterlim_at_top_iff_smallomega landau_flip(4) landau_trans(41))
from b have b': "f2b ∈ ω(λn. 1)"
by (metis (full_types) bigthetaD2 eventually_at_top_linorder eventually_nat_real
filterlim_at_top filterlim_at_top_iff_smallomega landau_flip(4) landau_trans(41))
have "(λ(x,y). f1 (f2a x,f2b y)) ∈ Θ⇩2((λ(x,y). g1 (x, y)))"
apply(rule bigTheta2_compose_both)
using assms a' b' unfolding event_mono2_def by auto
then show ?thesis by auto
qed
lemma bigTheta2_compose_both_linear':
fixes f1 :: "nat × nat ⇒ nat" and f2a f2b :: "nat ⇒ nat"
assumes "stablebigO2 g1" "event_mono2 g1" "f1 ∈ Θ⇩2(g1)" "f2a ∈ Θ(polylog 1 0)" "f2b ∈ Θ(polylog 1 0)"
shows "(λx. real (f1 (f2a (fst x), f2b (snd x)))) ∈ Θ⇩2(g1)"
proof -
have 1: "(λx. real (f1 (f2a (fst x), f2b (snd x)))) = (λ(x,y). (f1 (f2a x, f2b y)))" by auto
have 2: "(λ(x,y). (f1 (f2a x, f2b y))) ∈ Θ⇩2(g1)"
apply (rule bigTheta2_compose_both_linear)
using assms unfolding polylog_def by auto
then show ?thesis using 1 2 by auto
qed
section ‹Small O, big O domination on two variables›
lemma oO_o:
fixes f1 f2 g1 g2 :: "nat ⇒ real"
assumes "f1 ∈ o(g1)" "f2 ∈ O(g2)"
shows "(λ(n,m). f1 n * f2 m) ∈ o⇩2(λ(n,m). g1 n * g2 m)"
proof (rule landau_o.smallI)
fix c :: real assume c: "0 < c"
thm landau_o.smallD landau_o.smallI
from assms(2) obtain c2 where c2: "c2>0" and 2: "∀⇩F x in at_top. norm (f2 x) ≤ c2 * norm (g2 x)" using landau_o.bigE by blast
have 1: "∀⇩F x in at_top. norm (f1 x) ≤ (c/c2) * norm (g1 x)" apply(rule landau_o.smallD)
using assms(1) c2 c by auto
note B=eventually_prodI[OF 1 2]
show "∀⇩F x in sequentially ×⇩F sequentially. norm (case x of (n, m) ⇒ f1 n * f2 m) ≤ c * norm (case x of (n, m) ⇒ g1 n * g2 m)"
proof (rule eventually_mono[OF B _], safe, simp)
fix n m
assume 1: "¦f1 n¦ ≤ c * ¦g1 n¦ / c2" and 2: "¦f2 m¦ ≤ c2 * ¦g2 m¦"
have "¦f1 n * f2 m¦ = ¦f1 n¦ * ¦f2 m¦" using abs_mult by blast
also have "… ≤ (c*¦g1 n¦/c2) * ¦f2 m¦" apply(rule mult_right_mono) apply fact by simp
also have "… ≤ (c*¦g1 n¦/c2) * (c2* ¦g2 m¦)" apply(rule mult_left_mono) apply fact using c c2 by simp
also have "… = c * ¦g1 n * g2 m¦" using c2 by (simp add: abs_mult)
finally show "¦f1 n * f2 m¦ ≤ c * ¦g1 n * g2 m¦" .
qed
qed
lemma Oo_o:
fixes f1 f2 g1 g2 :: "nat ⇒ real"
assumes "f1 ∈ O(g1)" "f2 ∈ o(g2)"
shows "(λ(n,m). f1 n * f2 m) ∈ o⇩2(λ(n,m). g1 n * g2 m)"
proof (rule landau_o.smallI)
fix c :: real assume c: "0 < c"
thm landau_o.smallD landau_o.smallI
from assms(1) obtain c1 where c2: "c1>0" and 1: "∀⇩F x in at_top. norm (f1 x) ≤ c1 * norm (g1 x)" using landau_o.bigE by blast
have 2: "∀⇩F x in at_top. norm (f2 x) ≤ (c/c1) * norm (g2 x)" apply(rule landau_o.smallD)
using assms(2) c2 c by auto
note B=eventually_prodI[OF 1 2]
show "∀⇩F x in sequentially ×⇩F sequentially. norm (case x of (n, m) ⇒ f1 n * f2 m) ≤ c * norm (case x of (n, m) ⇒ g1 n * g2 m)"
proof (rule eventually_mono[OF B _], safe, simp)
fix n m
assume 2: "¦f2 m¦ ≤ c * ¦g2 m¦ / c1" and 1: "¦f1 n¦ ≤ c1 * ¦g1 n¦"
have "¦f1 n * f2 m¦ = ¦f1 n¦ * ¦f2 m¦" using abs_mult by blast
also have "… ≤ ¦f1 n¦ * (c * ¦g2 m¦ / c1)" apply(rule mult_left_mono) apply fact by simp
also have "… ≤ (c1 * ¦g1 n¦) * (c * ¦g2 m¦ / c1)" apply(rule mult_right_mono) apply fact using c c2 by simp
also have "… = c * ¦g1 n * g2 m¦" using c2 by (simp add: abs_mult)
finally show "¦f1 n * f2 m¦ ≤ c * ¦g1 n * g2 m¦" .
qed
qed
section "2D Theta bound for product of 1D Theta bounds"
lemma mult_Theta_bivariate:
fixes f1 f2 :: "nat ⇒ nat" and g1 g2 :: "nat ⇒ real"
assumes "f1 ∈ Θ(λn. g1 n)" "f2 ∈ Θ(λn. g2 n)"
shows "(λ(n, m). f1 n * f2 m) ∈ Θ⇩2(λ(n, m). g1 n * g2 m)"
proof
thm landau_o.bigE landau_omega.bigE
from assms have 1: "f1 : O(λn. g1 n)" and 2: "f2 ∈ O(λn. g2 n)" by auto
from 1 obtain cf where cf: "cf>0" and 1: "∀⇩F x in at_top. norm (f1 x) ≤ cf * norm (g1 x)" using landau_o.bigE by blast
from 2 obtain cg where cg: "cg>0" and 2: "∀⇩F x in at_top. norm (f2 x) ≤ cg * norm (g2 x)" using landau_o.bigE by blast
note B=eventually_prodI[OF 1 2]
show "(λ(n, m). f1 n * f2 m) ∈ O⇩2(λ(n, m). g1 n * g2 m)"
apply(rule landau_o.bigI[where c="cf*cg"])
using cf cg apply simp
proof (rule eventually_mono[OF B _], safe, simp)
fix n m
assume "real (f1 n) ≤ cf * ¦g1 n¦"
assume "real (f2 m) ≤ cg * ¦g2 m¦"
have "real (f1 n) * real (f2 m) ≤ (cf * ¦g1 n¦) * real (f2 m)"
apply(rule mult_right_mono) apply fact by simp
also have "… ≤ (cf * ¦g1 n¦) * (cg * ¦g2 m¦)"
apply(rule mult_left_mono) apply fact using cf by simp
also have "… = (cf*cg) * ¦g1 n * g2 m¦" by(simp add: abs_mult)
finally show "real (f1 n) * real (f2 m) ≤ cf * cg * ¦g1 n * g2 m¦" .
qed
from assms have 1: "f1 : Ω(λn. (g1 n))" and 2: "f2 ∈ Ω(λn. (g2 n))" by auto
from 1 obtain cf where cf: "cf>0" and 1: "∀⇩F x in at_top. norm (f1 x) ≥ cf * norm (g1 x)" using landau_omega.bigE by blast
from 2 obtain cg where cg: "cg>0" and 2: "∀⇩F x in at_top. norm (f2 x) ≥ cg * norm (g2 x)" using landau_omega.bigE by blast
note B=eventually_prodI[OF 1 2]
show "(λ(n, m). f1 n * f2 m) ∈ Ω⇩2(λ(n, m). g1 n * g2 m)"
apply(rule landau_omega.bigI[where c="cf*cg"])
using cf cg apply simp
proof (rule eventually_mono[OF B _], safe, simp)
fix n m
assume "real (f1 n) ≥ cf * ¦g1 n¦"
assume "real (f2 m) ≥ cg * ¦g2 m¦"
have "(cf*cg) * ¦g1 n * g2 m¦ = (cf * ¦g1 n¦) * (cg * ¦g2 m¦)" by(simp add: abs_mult)
also have "… ≤ (cf * ¦g1 n¦) * real (f2 m)"
apply (rule mult_left_mono) apply fact using cf by simp
also have "… ≤ real (f1 n) * real (f2 m)"
apply (rule mult_right_mono) apply fact by simp
finally show "real (f1 n) * real (f2 m) ≥ cf * cg * ¦g1 n * g2 m¦" .
qed
qed
section ‹Comparison between polylog2 functions›
definition "cas1 a1 b1 c1 d1 a2 b2 c2 d2 = (((a1<a2 ∨ a1=a2 ∧ b1<b2) ∧ (c1<c2 ∨ c1=c2 ∧ d1≤d2))
∨ ((a1<a2 ∨ a1=a2 ∧ b1≤b2) ∧ (c1<c2 ∨ c1=c2 ∧ d1<d2)))"
lemma polylog2_compare:
assumes "f1 ∈ Θ⇩2(polylog2 a1 b1 c1 d1)" "f2 ∈ Θ⇩2(polylog2 a2 b2 c2 d2)"
shows "cas1 a1 b1 c1 d1 a2 b2 c2 d2 ⟹ f1 ∈ o⇩2(f2)"
proof -
assume "cas1 a1 b1 c1 d1 a2 b2 c2 d2"
then have AoB: "((a1<a2 ∨ a1=a2 ∧ b1<b2) ∧ (c1<c2 ∨ c1=c2 ∧ d1≤d2))
∨ ((a1<a2 ∨ a1=a2 ∧ b1≤b2) ∧ (c1<c2 ∨ c1=c2 ∧ d1<d2)) " (is "?A ∨ ?B") unfolding cas1_def by auto
show "f1 ∈ o⇩2(f2)"
proof (cases "?A")
case True
then have o: "polylog a1 b1 ∈ o(polylog a2 b2)"
and O: "polylog c1 d1 ∈ O(polylog c2 d2)"
unfolding polylog_def apply auto
apply(cases "d1=d2") apply auto
apply(cases "d1=d2") by auto
have "polylog2 a1 b1 c1 d1 ∈ o⇩2(polylog2 a2 b2 c2 d2)" unfolding polylog2_def
by(rule oO_o[OF o O])
then show ?thesis using assms
using landau_o.small.cong_ex_bigtheta by blast
next
case False
with AoB have B: "?B" by simp
then have O: "polylog a1 b1 ∈ O(polylog a2 b2)"
and o: "polylog c1 d1 ∈ o(polylog c2 d2)"
unfolding polylog_def apply auto
apply(cases "b1=b2") apply auto
apply(cases "b1=b2") by auto
have "polylog2 a1 b1 c1 d1 ∈ o⇩2(polylog2 a2 b2 c2 d2)" unfolding polylog2_def
by(rule Oo_o[OF O o])
then show ?thesis using assms
using landau_o.small.cong_ex_bigtheta by blast
qed
qed
lemma polylog2_compare':
assumes "(a1<a2 ∨ a1=a2 ∧ b1<b2) ∧ (c1<c2 ∨ c1=c2 ∧ d1≤d2)"
shows "polylog2 a1 b1 c1 d1 ∈ o⇩2(polylog2 a2 b2 c2 d2)"
proof -
have 1: "cas1 a1 b1 c1 d1 a2 b2 c2 d2" using assms cas1_def by metis
have 2: "polylog2 a1 b1 c1 d1 ∈ Θ⇩2(polylog2 a1 b1 c1 d1)" by auto
have 3: "polylog2 a2 b2 c2 d2 ∈ Θ⇩2(polylog2 a2 b2 c2 d2)" by auto
show ?thesis using polylog2_compare(1)[OF 2 3 1] by simp
qed
lemma polylog2_compare2':
assumes "(a1<a2 ∨ a1=a2 ∧ b1≤b2) ∧ (c1<c2 ∨ c1=c2 ∧ d1<d2)"
shows "polylog2 a1 b1 c1 d1 ∈ o⇩2(polylog2 a2 b2 c2 d2)"
proof -
have 1: "cas1 a1 b1 c1 d1 a2 b2 c2 d2" using assms cas1_def by metis
have 2: "polylog2 a1 b1 c1 d1 ∈ Θ⇩2(polylog2 a1 b1 c1 d1)" by auto
have 3: "polylog2 a2 b2 c2 d2 ∈ Θ⇩2(polylog2 a2 b2 c2 d2)" by auto
show ?thesis using polylog2_compare(1)[OF 2 3 1] by simp
qed
section ‹Setup for automation›
lemma landau_norms2:
"polylog a1 b1 (fst x) = polylog2 a1 b1 0 0 x"
"polylog a2 b2 (snd x) = polylog2 0 0 a2 b2 x"
"polylog2 a1 b1 a2 b2 x * polylog2 a3 b3 a4 b4 x = polylog2 (a1 + a3) (b1 + b3) (a2 + a4) (b2 + b4) x"
apply (metis (no_types, lifting) Groups.add_ac(2) landau_norms(1) landau_norms(4) landau_norms(5)
landau_norms(6) polylog2_def polylog_def prod.collapse prod.simps(2))
apply (metis (no_types, lifting) Groups.add_ac(2) landau_norms(1) landau_norms(4) landau_norms(5)
landau_norms(6) polylog2_def polylog_def prod.collapse prod.simps(2))
by (smt landau_norms(6) polylog2_def semiring_normalization_rules(13) split_beta)
lemma landau_norms2':
"polylog2 a1 b1 a2 b2 * polylog2 a3 b3 a4 b4 = polylog2 (a1 + a3) (b1 + b3) (a2 + a4) (b2 + b4)"
using landau_norms2(3) by auto
lemma mult_Theta_bivariate':
assumes "(λx. real (f1 x)) ∈ Θ(polylog a b)"
"(λx. real (f2 x)) ∈ Θ(polylog c d)"
shows "(λx. real (f1 (fst x) * f2 (snd x))) ∈ Θ⇩2 (polylog2 a b c d)"
proof -
have 1: "(λx. real (case x of (n, m) ⇒ f1 n * f2 m)) ∈ Θ⇩2 (λx. case x of (n, m) ⇒ polylog a b n * polylog c d m)"
using mult_Theta_bivariate[of f1 "polylog a b" f2 "polylog c d"] assms by auto
then show ?thesis
unfolding polylog2_def by (simp add: case_prod_beta)
qed
lemma mult_Theta_bivariate1:
assumes "(λx. real (f1 x)) ∈ Θ(polylog a b)"
shows "(λx. real (f1 (fst x))) ∈ Θ⇩2 (polylog2 a b 0 0)"
proof -
have 1: "(λx. real (f1 (fst x))) = (λx. real (f1 (fst x) * 1))" by auto
with assms show ?thesis
apply (subst 1) apply (rule mult_Theta_bivariate')
apply auto
apply (subst of_nat_1 [symmetric]) apply (rule bigtheta_const) by auto
qed
lemma mult_Theta_bivariate2:
assumes "(λx. real (f2 x)) ∈ Θ(polylog a b)"
shows "(λx. real (f2 (snd x))) ∈ Θ⇩2 (polylog2 0 0 a b)"
proof -
have 1: "(λx. real (f2 (snd x))) = (λx. real (1 * f2 (snd x)))" by auto
with assms show ?thesis
apply (subst 1) apply (rule mult_Theta_bivariate')
apply auto
apply (subst of_nat_1 [symmetric]) apply (rule bigtheta_const) by auto
qed
lemma polylog_omega1:
"a ≠ 0 ∨ b ≠ 0 ⟹ polylog a b ∈ ω(λx. 1::real)" unfolding polylog_def by auto
ML_file "landau_util_2d.ML"
end