# Theory Landau_Real_Products

theory Landau_Real_Products
imports Function_Algebras Set_Algebras Landau_Symbols Group_Sort
```(*
File:   Landau_Real_Products.thy
Author: Manuel Eberl <eberlm@in.tum.de>

Mathematical background and reification for a decision procedure for Landau symbols of
products of powers of real functions (currently the identity and the natural logarithm)

TODO: more functions (exp?), more preprocessing (log)
*)
section ‹Decision procedure for real functions›

theory Landau_Real_Products
imports
Main
"HOL-Library.Function_Algebras"
"HOL-Library.Set_Algebras"
"HOL-Library.Landau_Symbols"
Group_Sort
begin

subsection ‹Eventual non-negativity/non-zeroness›

text ‹
For certain transformations of Landau symbols, it is required that the functions involved
are eventually non-negative of non-zero. In the following, we set up a system to guide the
simplifier to discharge these requirements during simplification at least in obvious cases.
›

definition "eventually_nonzero F f ⟷ eventually (λx. (f x :: _ :: real_normed_field) ≠ 0) F"
definition "eventually_nonneg F f ⟷ eventually (λx. (f x :: _ :: linordered_field) ≥ 0) F"

named_theorems eventually_nonzero_simps

lemmas [eventually_nonzero_simps] =
eventually_nonzero_def [symmetric] eventually_nonneg_def [symmetric]

lemma eventually_nonzeroD: "eventually_nonzero F f ⟹ eventually (λx. f x ≠ 0) F"

lemma eventually_nonzero_const [eventually_nonzero_simps]:
"eventually_nonzero F (λ_::_::linorder. c) ⟷ F = bot ∨ c ≠ 0"
unfolding eventually_nonzero_def by (auto simp add: eventually_False)

lemma eventually_nonzero_inverse [eventually_nonzero_simps]:
"eventually_nonzero F (λx. inverse (f x)) ⟷ eventually_nonzero F f"
unfolding eventually_nonzero_def by simp

lemma eventually_nonzero_mult [eventually_nonzero_simps]:
"eventually_nonzero F (λx. f x * g x) ⟷ eventually_nonzero F f ∧ eventually_nonzero F g"
unfolding eventually_nonzero_def by (simp_all add: eventually_conj_iff[symmetric])

lemma eventually_nonzero_pow [eventually_nonzero_simps]:
"eventually_nonzero F (λx::_::linorder. f x ^ n) ⟷ n = 0 ∨ eventually_nonzero F f"
by (induction n) (auto simp: eventually_nonzero_simps)

lemma eventually_nonzero_divide [eventually_nonzero_simps]:
"eventually_nonzero F (λx. f x / g x) ⟷ eventually_nonzero F f ∧ eventually_nonzero F g"
unfolding eventually_nonzero_def by (simp_all add: eventually_conj_iff[symmetric])

lemma eventually_nonzero_ident_at_top_linorder [eventually_nonzero_simps]:
"eventually_nonzero at_top (λx::'a::{real_normed_field,linordered_field}. x)"
unfolding eventually_nonzero_def by simp

lemma eventually_nonzero_ident_nhds [eventually_nonzero_simps]:
"eventually_nonzero (nhds a) (λx. x) ⟷ a ≠ 0"
using eventually_nhds_in_open[of "-{0}" a]
by (auto elim!: eventually_mono simp: eventually_nonzero_def open_Compl
dest: eventually_nhds_x_imp_x)

lemma eventually_nonzero_ident_at_within [eventually_nonzero_simps]:
"eventually_nonzero (at a within A) (λx. x)"
using eventually_nonzero_ident_nhds[of a]
by (cases "a = 0") (auto simp: eventually_nonzero_def eventually_at_filter elim!: eventually_mono)

lemma eventually_nonzero_ln_at_top [eventually_nonzero_simps]:
"eventually_nonzero at_top (λx::real. ln x)"
unfolding eventually_nonzero_def by (auto intro!: eventually_mono[OF eventually_gt_at_top[of 1]])

lemma eventually_nonzero_ln_const_at_top [eventually_nonzero_simps]:
"b > 0 ⟹ eventually_nonzero at_top (λx. ln (b * x :: real))"
unfolding eventually_nonzero_def
apply (rule eventually_mono [OF eventually_gt_at_top[of "max 1 (inverse b)"]])
by (metis exp_ln exp_minus exp_minus_inverse less_numeral_extra(3) ln_gt_zero max_less_iff_conj mult.commute mult_strict_right_mono)

lemma eventually_nonzero_ln_const'_at_top [eventually_nonzero_simps]:
"b > 0 ⟹ eventually_nonzero at_top (λx. ln (x * b :: real))"
using eventually_nonzero_ln_const_at_top[of b] by (simp add: mult.commute)

lemma eventually_nonzero_powr_at_top [eventually_nonzero_simps]:
"eventually_nonzero at_top (λx::real. f x powr p) ⟷ eventually_nonzero at_top f"
unfolding eventually_nonzero_def by simp

lemma eventually_nonneg_const [eventually_nonzero_simps]:
"eventually_nonneg F (λ_. c) ⟷ F = bot ∨ c ≥ 0"
unfolding eventually_nonneg_def by (auto simp: eventually_False)

lemma eventually_nonneg_inverse [eventually_nonzero_simps]:
"eventually_nonneg F (λx. inverse (f x)) ⟷ eventually_nonneg F f"
unfolding eventually_nonneg_def by (intro eventually_subst) (auto)

assumes "eventually_nonneg F f" "eventually_nonneg F g"
shows   "eventually_nonneg F (λx. f x + g x)"
using assms unfolding eventually_nonneg_def by eventually_elim simp

lemma eventually_nonneg_mult [eventually_nonzero_simps]:
assumes "eventually_nonneg F f" "eventually_nonneg F g"
shows   "eventually_nonneg F (λx. f x * g x)"
using assms unfolding eventually_nonneg_def by eventually_elim simp

lemma eventually_nonneg_mult' [eventually_nonzero_simps]:
assumes "eventually_nonneg F (λx. -f x)" "eventually_nonneg F (λx. - g x)"
shows   "eventually_nonneg F (λx. f x * g x)"
using assms unfolding eventually_nonneg_def by eventually_elim (auto intro: mult_nonpos_nonpos)

lemma eventually_nonneg_divide [eventually_nonzero_simps]:
assumes "eventually_nonneg F f" "eventually_nonneg F g"
shows   "eventually_nonneg F (λx. f x / g x)"
using assms unfolding eventually_nonneg_def by eventually_elim simp

lemma eventually_nonneg_divide' [eventually_nonzero_simps]:
assumes "eventually_nonneg F (λx. -f x)" "eventually_nonneg F (λx. - g x)"
shows   "eventually_nonneg F (λx. f x / g x)"
using assms unfolding eventually_nonneg_def by eventually_elim (auto intro: divide_nonpos_nonpos)

lemma eventually_nonneg_ident_at_top [eventually_nonzero_simps]:
"eventually_nonneg at_top (λx. x)" unfolding eventually_nonneg_def by (rule eventually_ge_at_top)

lemma eventually_nonneg_ident_nhds [eventually_nonzero_simps]:
fixes a :: "'a :: {linorder_topology, linordered_field}"
shows "a > 0 ⟹ eventually_nonneg (nhds a) (λx. x)" unfolding eventually_nonneg_def
using eventually_nhds_in_open[of "{0<..}" a]
by (auto simp: eventually_nonneg_def dest: eventually_nhds_x_imp_x elim!: eventually_mono)

lemma eventually_nonneg_ident_at_within [eventually_nonzero_simps]:
fixes a :: "'a :: {linorder_topology, linordered_field}"
shows "a > 0 ⟹ eventually_nonneg (at a within A) (λx. x)"
using eventually_nonneg_ident_nhds[of a]
by (auto simp: eventually_nonneg_def eventually_at_filter elim: eventually_mono)

lemma eventually_nonneg_pow [eventually_nonzero_simps]:
"eventually_nonneg F f ⟹ eventually_nonneg F (λx. f x ^ n)"
by (induction n) (auto simp: eventually_nonzero_simps)

lemma eventually_nonneg_powr [eventually_nonzero_simps]:
"eventually_nonneg F (λx. f x powr y :: real)" by (simp add: eventually_nonneg_def)

lemma eventually_nonneg_ln_at_top [eventually_nonzero_simps]:
"eventually_nonneg at_top (λx. ln x :: real)"
by (auto intro!: eventually_mono[OF eventually_gt_at_top[of "1::real"]]
simp: eventually_nonneg_def)

lemma eventually_nonneg_ln_const [eventually_nonzero_simps]:
"b > 0 ⟹ eventually_nonneg at_top (λx. ln (b*x) :: real)"
unfolding eventually_nonneg_def using eventually_ge_at_top[of "inverse b"]

lemma eventually_nonneg_ln_const' [eventually_nonzero_simps]:
"b > 0 ⟹ eventually_nonneg at_top (λx. ln (x*b) :: real)"
using eventually_nonneg_ln_const[of b] by (simp add: mult.commute)

lemma eventually_nonzero_bigtheta':
"f ∈ Θ[F](g) ⟹ eventually_nonzero F f ⟷ eventually_nonzero F g"
unfolding eventually_nonzero_def by (rule eventually_nonzero_bigtheta)

lemma eventually_nonneg_at_top:
assumes "filterlim f at_top F"
shows   "eventually_nonneg F f"
proof -
from assms have "eventually (λx. f x ≥ 0) F"
thus ?thesis unfolding eventually_nonneg_def by eventually_elim simp
qed

lemma eventually_nonzero_at_top:
assumes "filterlim (f :: 'a ⇒ 'b :: {linordered_field, real_normed_field}) at_top F"
shows   "eventually_nonzero F f"
proof -
from assms have "eventually (λx. f x ≥ 1) F"
thus ?thesis unfolding eventually_nonzero_def by eventually_elim auto
qed

lemma eventually_nonneg_at_top_ASSUMPTION [eventually_nonzero_simps]:
"ASSUMPTION (filterlim f at_top F) ⟹ eventually_nonneg F f"

lemma eventually_nonzero_at_top_ASSUMPTION [eventually_nonzero_simps]:
"ASSUMPTION (filterlim f (at_top :: 'a :: {linordered_field, real_normed_field} filter) F) ⟹
eventually_nonzero F f"
using eventually_nonzero_at_top[of f F] by (simp add: ASSUMPTION_def)

lemma filterlim_at_top_iff_smallomega:
fixes f :: "_ ⇒ real"
shows "filterlim f at_top F ⟷ f ∈ ω[F](λ_. 1) ∧ eventually_nonneg F f"
unfolding eventually_nonneg_def
proof safe
assume A: "filterlim f at_top F"
thus B: "eventually (λx. f x ≥ 0) F" by (simp add: eventually_nonzero_simps)
{
fix c
from A have "filterlim (λx. norm (f x)) at_top F"
by (intro filterlim_at_infinity_imp_norm_at_top filterlim_at_top_imp_at_infinity)
hence "eventually (λx. norm (f x) ≥ c) F" by (auto simp: filterlim_at_top)
}
thus "f ∈ ω[F](λ_. 1)" by (rule landau_omega.smallI)
next
assume A: "f ∈ ω[F](λ_. 1)" and B: "eventually (λx. f x ≥ 0) F"
{
fix c :: real assume "c > 0"
from landau_omega.smallD[OF A this] B
have "eventually (λx. f x ≥ c) F" by eventually_elim simp
}
thus "filterlim f at_top F"
by (subst filterlim_at_top_gt[of _ _ 0]) simp_all
qed

lemma smallomega_1_iff:
"eventually_nonneg F f ⟹ f ∈ ω[F](λ_. 1 :: real) ⟷ filterlim f at_top F"

lemma smallo_1_iff:
"eventually_nonneg F f ⟹ (λ_. 1 :: real) ∈ o[F](f) ⟷ filterlim f at_top F"

assumes "eventually_nonneg F f" "g ∈ o[F](f)"
shows   "eventually_nonneg F (λx. f x + g x :: real)"
using  landau_o.smallD[OF assms(2) zero_less_one] assms(1) unfolding eventually_nonneg_def
by eventually_elim simp_all

assumes "eventually_nonneg F g" "f ∈ o[F](g)"
shows   "eventually_nonneg F (λx. f x + g x :: real)"
using  landau_o.smallD[OF assms(2) zero_less_one] assms(1) unfolding eventually_nonneg_def
by eventually_elim simp_all

lemma eventually_nonneg_diff1 [eventually_nonzero_simps]:
assumes "eventually_nonneg F f" "g ∈ o[F](f)"
shows   "eventually_nonneg F (λx. f x - g x :: real)"
using  landau_o.smallD[OF assms(2) zero_less_one] assms(1) unfolding eventually_nonneg_def
by eventually_elim simp_all

lemma eventually_nonneg_diff2 [eventually_nonzero_simps]:
assumes "eventually_nonneg F (λx. - g x)" "f ∈ o[F](g)"
shows   "eventually_nonneg F (λx. f x - g x :: real)"
using  landau_o.smallD[OF assms(2) zero_less_one] assms(1) unfolding eventually_nonneg_def
by eventually_elim simp_all

subsection ‹Rewriting Landau symbols›

lemma bigtheta_mult_eq: "Θ[F](λx. f x * g x) = Θ[F](f) * Θ[F](g)"
proof (intro equalityI subsetI)
fix h assume "h ∈ Θ[F](f) * Θ[F](g)"
thus "h ∈ Θ[F](λx. f x * g x)"
by (elim set_times_elim, hypsubst, unfold func_times) (erule (1) landau_theta.mult)
next
fix h assume "h ∈ Θ[F](λx. f x * g x)"
then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
note c = this

define h1 h2
where "h1 x = (if g x = 0 then if f x = 0 then if h x = 0 then h x else 1 else f x else h x / g x)"
and "h2 x = (if g x = 0 then if f x = 0 then h x else h x / f x else g x)"
for x

have "h = h1 * h2" by (intro ext) (auto simp: h1_def h2_def field_simps)
moreover have "h1 ∈ Θ[F](f)"
proof (rule bigthetaI')
from c(3) show "min c2 1 > 0" by simp
from c(1) show "max c1 1 > 0" by simp
from c(2,4)
show "eventually (λx. min c2 1 * (norm (f x)) ≤ norm (h1 x) ∧
norm (h1 x) ≤ max c1 1 * (norm (f x))) F"
apply eventually_elim
proof (rule conjI)
fix x assume A: "(norm (h x)) ≤ c1 * norm (f x * g x)"
and B: "(norm (h x)) ≥ c2 * norm (f x * g x)"
have m: "min c2 1 * (norm (f x)) ≤ 1 * (norm (f x))" by (rule mult_right_mono) simp_all
have "min c2 1 * norm (f x * g x) ≤ c2 * norm (f x * g x)" by (intro mult_right_mono) simp_all
also note B
finally show "norm (h1 x) ≥ min c2 1 * (norm (f x))" using m A
by (cases "g x = 0") (simp_all add: h1_def norm_mult norm_divide field_simps)+

have m: "1 * (norm (f x)) ≤ max c1 1 * (norm (f x))" by (rule mult_right_mono) simp_all
note A
also have "c1 * norm (f x * g x) ≤ max c1 1 * norm (f x * g x)"
by (intro mult_right_mono) simp_all
finally show "norm (h1 x) ≤ max c1 1 * (norm (f x))" using m A
by (cases "g x = 0") (simp_all add: h1_def norm_mult norm_divide field_simps)+
qed
qed
moreover have "h2 ∈ Θ[F](g)"
proof (rule bigthetaI')
from c(3) show "min c2 1 > 0" by simp
from c(1) show "max c1 1 > 0" by simp
from c(2,4)
show "eventually (λx. min c2 1 * (norm (g x)) ≤ norm (h2 x) ∧
norm (h2 x) ≤ max c1 1 * (norm (g x))) F"
apply eventually_elim
proof (rule conjI)
fix x assume A: "(norm (h x)) ≤ c1 * norm (f x * g x)"
and B: "(norm (h x)) ≥ c2 * norm (f x * g x)"
have m: "min c2 1 * (norm (f x)) ≤ 1 * (norm (f x))" by (rule mult_right_mono) simp_all
have "min c2 1 * norm (f x * g x) ≤ c2 * norm (f x * g x)"
by (intro mult_right_mono) simp_all
also note B
finally show "norm (h2 x) ≥ min c2 1 * (norm (g x))" using m A B
by (cases "g x = 0") (auto simp: h2_def abs_mult field_simps)+

have m: "1 * (norm (g x)) ≤ max c1 1 * (norm (g x))" by (rule mult_right_mono) simp_all
note A
also have "c1 * norm (f x * g x) ≤ max c1 1 * norm (f x * g x)"
by (intro mult_right_mono) simp_all
finally show "norm (h2 x) ≤ max c1 1 * (norm (g x))" using m A
by (cases "g x = 0") (simp_all add: h2_def abs_mult field_simps)+
qed
qed
ultimately show "h ∈ Θ[F](f) * Θ[F](g)" by blast
qed

text ‹
Since the simplifier does not currently rewriting with relations other than equality,
but we want to rewrite terms like @{term "Θ(λx. log 2 x * x)"} to @{term "Θ(λx. ln x * x)"},
we need to bring the term into something that contains @{term "Θ(λx. log 2 x)"} and
@{term "Θ(λx. x)"}, which can then be rewritten individually.
For this, we introduce the following constants and rewrite rules. The rules are mainly used
by the simprocs, but may be useful for manual reasoning occasionally.
›

definition "set_mult A B = {λx. f x * g x |f g. f ∈ A ∧ g ∈ B}"
definition "set_inverse A = {λx. inverse (f x) |f. f ∈ A}"
definition "set_divide A B = {λx. f x / g x |f g. f ∈ A ∧ g ∈ B}"
definition "set_pow A n = {λx. f x ^ n |f. f ∈ A}"
definition "set_powr A y = {λx. f x powr y |f. f ∈ A}"

lemma bigtheta_mult_eq_set_mult:
shows "Θ[F](λx. f x * g x) = set_mult (Θ[F](f)) (Θ[F](g))"
unfolding bigtheta_mult_eq set_mult_def set_times_def func_times by blast

lemma bigtheta_inverse_eq_set_inverse:
shows "Θ[F](λx. inverse (f x)) = set_inverse (Θ[F](f))"
proof (intro equalityI subsetI)
fix g :: "'a ⇒ 'b" assume "g ∈ Θ[F](λx. inverse (f x))"
hence "(λx. inverse (g x)) ∈ Θ[F](λx. inverse (inverse (f x)))" by (subst bigtheta_inverse)
also have "(λx. inverse (inverse (f x))) = f" by (rule ext) simp
finally show "g ∈ set_inverse (Θ[F](f))" unfolding set_inverse_def by force
next
fix g :: "'a ⇒ 'b" assume "g ∈ set_inverse (Θ[F](f))"
then obtain g' where "g = (λx. inverse (g' x))" "g' ∈ Θ[F](f)" unfolding set_inverse_def by blast
hence "(λx. inverse (g' x)) ∈ Θ[F](λx. inverse (f x))" by (subst bigtheta_inverse)
also from ‹g = (λx. inverse (g' x))› have "(λx. inverse (g' x)) = g" by (intro ext) simp
finally show "g ∈ Θ[F](λx. inverse (f x))" .
qed

lemma set_divide_inverse:
"set_divide (A :: (_ ⇒ (_ :: division_ring)) set) B = set_mult A (set_inverse B)"
proof (intro equalityI subsetI)
fix f assume "f ∈ set_divide A B"
then obtain g h where "f = (λx. g x / h x)" "g ∈ A" "h ∈ B" unfolding set_divide_def by blast
hence "f = g * (λx. inverse (h x))" "(λx. inverse (h x)) ∈ set_inverse B"
unfolding set_inverse_def by (auto simp: divide_inverse)
with ‹g ∈ A› show "f ∈ set_mult A (set_inverse B)" unfolding set_mult_def by force
next
fix f assume "f ∈ set_mult A (set_inverse B)"
then obtain g h where "f = g * (λx. inverse (h x))" "g ∈ A" "h ∈ B"
unfolding set_times_def set_inverse_def set_mult_def by force
hence "f = (λx. g x / h x)" by (intro ext) (simp add: divide_inverse)
with ‹g ∈ A› ‹h ∈ B› show "f ∈ set_divide A B" unfolding set_divide_def by blast
qed

lemma bigtheta_divide_eq_set_divide:
shows "Θ[F](λx. f x / g x) = set_divide (Θ[F](f)) (Θ[F](g))"
by (simp only: set_divide_inverse divide_inverse bigtheta_mult_eq_set_mult
bigtheta_inverse_eq_set_inverse)

primrec bigtheta_pow where
"bigtheta_pow F A 0 = Θ[F](λ_. 1)"
| "bigtheta_pow F A (Suc n) = set_mult A (bigtheta_pow F A n)"

lemma bigtheta_pow_eq_set_pow: "Θ[F](λx. f x ^ n) = bigtheta_pow F (Θ[F](f)) n"
by (induction n) (simp_all add: bigtheta_mult_eq_set_mult)

definition bigtheta_powr where
"bigtheta_powr F A y = (if y = 0 then {f. ∃g∈A. eventually_nonneg F g ∧ f ∈ Θ[F](λx. g x powr y)}
else {f. ∃g∈A. eventually_nonneg F g ∧ (∀x. (norm (f x)) = g x powr y)})"

lemma bigtheta_powr_eq_set_powr:
assumes "eventually_nonneg F f"
shows   "Θ[F](λx. f x powr (y::real)) = bigtheta_powr F (Θ[F](f)) y"
proof (cases "y = 0")
assume [simp]: "y = 0"
show ?thesis
proof (intro equalityI subsetI)
fix h assume "h ∈ bigtheta_powr F Θ[F](f) y"
then obtain g where g: "g ∈ Θ[F](f)" "eventually_nonneg F g" "h ∈ Θ[F](λx. g x powr 0)"
unfolding bigtheta_powr_def by force
note this(3)
also have "(λx. g x powr 0) ∈ Θ[F](λx. ¦g x¦ powr 0)"
using assms unfolding eventually_nonneg_def
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
also from g(1) have "(λx. ¦g x¦ powr 0) ∈ Θ[F](λx. ¦f x¦ powr 0)"
by (rule bigtheta_powr)
also from g(2) have "(λx. f x powr 0) ∈ Θ[F](λx. ¦f x¦ powr 0)"
unfolding eventually_nonneg_def
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
finally show "h ∈ Θ[F](λx. f x powr y)" by simp
next
fix h assume "h ∈ Θ[F](λx. f x powr y)"
with assms have "∃g∈Θ[F](f). eventually_nonneg F g ∧ h ∈ Θ[F](λx. g x powr 0)"
by (intro bexI[of _ f] conjI) simp_all
thus "h ∈ bigtheta_powr F Θ[F](f) y" unfolding bigtheta_powr_def by simp
qed
next
assume y: "y ≠ 0"
show ?thesis
proof (intro equalityI subsetI)
fix h assume h: "h ∈ Θ[F](λx. f x powr y)"
let ?h' = "λx. ¦h x¦ powr inverse y"
from bigtheta_powr[OF h, of "inverse y"] y
have "?h' ∈ Θ[F](λx. f x powr 1)" by (simp add: powr_powr)
also have "(λx. f x powr 1) ∈ Θ[F](f)" using assms unfolding eventually_nonneg_def
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
finally have "?h' ∈ Θ[F](f)" .
with y have "∃g∈Θ[F](f). eventually_nonneg F g ∧ (∀x. (norm (h x)) = g x powr y)"
by (intro bexI[of _ ?h']) (simp_all add: powr_powr eventually_nonneg_def)
thus "h ∈ bigtheta_powr F Θ[F](f) y" using y unfolding bigtheta_powr_def by simp
next
fix h assume "h ∈ bigtheta_powr F (Θ[F](f)) y"
with y obtain g where A: "g ∈ Θ[F](f)" "⋀x. ¦h x¦ = g x powr y" "eventually_nonneg F g"
unfolding bigtheta_powr_def by force
from this(3) have "(λx. g x powr y) ∈ Θ[F](λx. ¦g x¦ powr y)" unfolding eventually_nonneg_def
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
also from A(1) have "(λx. ¦g x¦ powr y) ∈ Θ[F](λx. ¦f x¦ powr y)" by (rule bigtheta_powr)
also have "(λx. ¦f x¦ powr y) ∈ Θ[F](λx. f x powr y)" using assms unfolding eventually_nonneg_def
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
finally have "(λx. ¦h x¦) ∈ Θ[F](λx. f x powr y)" by (subst A(2))
thus "(λx. h x) ∈ Θ[F](λx. f x powr y)" by simp
qed
qed

lemmas bigtheta_factors_eq =
bigtheta_mult_eq_set_mult bigtheta_inverse_eq_set_inverse bigtheta_divide_eq_set_divide
bigtheta_pow_eq_set_pow bigtheta_powr_eq_set_powr

lemmas landau_bigtheta_congs = landau_symbols[THEN landau_symbol.cong_bigtheta]

lemma (in landau_symbol) meta_cong_bigtheta: "Θ[F](f) ≡ Θ[F](g) ⟹ L F (f) ≡ L F (g)"
using bigtheta_refl[of f] by (intro eq_reflection cong_bigtheta) blast

lemmas landau_bigtheta_meta_congs = landau_symbols[THEN landau_symbol.meta_cong_bigtheta]

subsection ‹Preliminary facts›

lemma real_powr_at_top:
assumes "(p::real) > 0"
shows   "filterlim (λx. x powr p) at_top at_top"
proof (subst filterlim_cong[OF refl refl])
show "LIM x at_top. exp (p * ln x) :> at_top"
by (rule filterlim_compose[OF exp_at_top filterlim_tendsto_pos_mult_at_top[OF tendsto_const]])
show "eventually (λx. x powr p = exp (p * ln x)) at_top"
using eventually_gt_at_top[of 0] by eventually_elim (simp add: powr_def)
qed

lemma tendsto_ln_over_powr:
assumes "(a::real) > 0"
shows   "((λx. ln x / x powr a) ⤏ 0) at_top"
proof (rule lhospital_at_top_at_top)
from assms show "LIM x at_top. x powr a :> at_top" by (rule real_powr_at_top)
show "eventually (λx. a * x powr (a - 1) ≠ 0) at_top"
using eventually_gt_at_top[of "0::real"] by eventually_elim (insert assms, simp)
show "eventually (λx::real. (ln has_real_derivative (inverse x)) (at x)) at_top"
using eventually_gt_at_top[of "0::real"] DERIV_ln by (elim eventually_mono) simp
show "eventually (λx. ((λx. x powr a) has_real_derivative a * x powr (a - 1)) (at x)) at_top"
using eventually_gt_at_top[of "0::real"]
by eventually_elim (auto intro!: derivative_eq_intros)
have "eventually (λx. inverse a * x powr -a = inverse x / (a*x powr (a-1))) at_top"
using eventually_gt_at_top[of "0::real"]
by (elim eventually_mono) (simp add: field_simps powr_diff powr_minus)
moreover from assms have "((λx. inverse a * x powr -a) ⤏ 0) at_top"
by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_ident) simp_all
ultimately show "((λx. inverse x / (a * x powr (a - 1))) ⤏ 0) at_top"
by (subst (asm) tendsto_cong) simp_all
qed

lemma tendsto_ln_powr_over_powr:
assumes "(a::real) > 0" "b > 0"
shows   "((λx. ln x powr a / x powr b) ⤏ 0) at_top"
proof-
have "eventually (λx. ln x powr a / x powr b = (ln x / x powr (b/a)) powr a) at_top"
using assms eventually_gt_at_top[of "1::real"]
by (elim eventually_mono) (simp add: powr_divide powr_powr)
moreover have "eventually (λx. 0 < ln x / x powr (b / a)) at_top"
using eventually_gt_at_top[of "1::real"] by (elim eventually_mono) simp
with assms have "((λx. (ln x / x powr (b/a)) powr a) ⤏ 0) at_top"
by (intro tendsto_zero_powrI tendsto_ln_over_powr) (simp_all add: eventually_mono)
ultimately show ?thesis by (subst tendsto_cong) simp_all
qed

lemma tendsto_ln_powr_over_powr':
assumes "b > 0"
shows   "((λx::real. ln x powr a / x powr b) ⤏ 0) at_top"
proof (cases "a ≤ 0")
assume a: "a ≤ 0"
show ?thesis
proof (rule tendsto_sandwich[of "λ_::real. 0"])
have "eventually (λx. ln x powr a ≤ 1) at_top" unfolding eventually_at_top_linorder
proof (intro allI exI impI)
fix x :: real assume x: "x ≥ exp 1"
have "0 < exp (1::real)" by simp
also have "… ≤ x" by fact
finally have "ln x ≥ ln (exp 1)" using x by (subst ln_le_cancel_iff) auto
hence "ln x powr a ≤ ln (exp 1) powr a" using a by (intro powr_mono2') simp_all
thus "ln x powr a ≤ 1" by simp
qed
thus "eventually (λx. ln x powr a / x powr b ≤ x powr -b) at_top"
by eventually_elim (insert a, simp add: field_simps powr_minus divide_right_mono)
qed (auto intro!: filterlim_ident tendsto_neg_powr assms)
qed (intro tendsto_ln_powr_over_powr, simp_all add: assms)

lemma tendsto_ln_over_ln:
assumes "(a::real) > 0" "c > 0"
shows   "((λx. ln (a*x) / ln (c*x)) ⤏ 1) at_top"
proof (rule lhospital_at_top_at_top)
show "LIM x at_top. ln (c*x) :> at_top"
by (intro filterlim_compose[OF ln_at_top] filterlim_tendsto_pos_mult_at_top[OF tendsto_const]
filterlim_ident assms(2))
show "eventually (λx. ((λx. ln (a*x)) has_real_derivative (inverse x)) (at x)) at_top"
using eventually_gt_at_top[of "inverse a"] assms
by (auto elim!: eventually_mono intro!: derivative_eq_intros simp: field_simps)
show "eventually (λx. ((λx. ln (c*x)) has_real_derivative (inverse x)) (at x)) at_top"
using eventually_gt_at_top[of "inverse c"] assms
by (auto elim!: eventually_mono intro!: derivative_eq_intros simp: field_simps)
show "((λx::real. inverse x / inverse x) ⤏ 1) at_top"
by (subst tendsto_cong[of _ "λ_. 1"]) simp_all
qed simp_all

lemma tendsto_ln_powr_over_ln_powr:
assumes "(a::real) > 0" "c > 0"
shows   "((λx. ln (a*x) powr d / ln (c*x) powr d) ⤏ 1) at_top"
proof-
have "eventually (λx. ln (a*x) powr d / ln (c*x) powr d = (ln (a*x) / ln (c*x)) powr d) at_top"
using assms eventually_gt_at_top[of "max (inverse a) (inverse c)"]
by (auto elim!: eventually_mono simp: powr_divide field_simps)
moreover have "((λx. (ln (a*x) / ln (c*x)) powr d) ⤏ 1) at_top" using assms
by (intro tendsto_eq_rhs[OF tendsto_powr[OF tendsto_ln_over_ln tendsto_const]]) simp_all
ultimately show ?thesis by (subst tendsto_cong)
qed

lemma tendsto_ln_powr_over_ln_powr':
"c > 0 ⟹ ((λx::real. ln x powr d / ln (c*x) powr d) ⤏ 1) at_top"
using tendsto_ln_powr_over_ln_powr[of 1 c d] by simp

lemma tendsto_ln_powr_over_ln_powr'':
"a > 0 ⟹ ((λx::real. ln (a*x) powr d / ln x powr d) ⤏ 1) at_top"
using tendsto_ln_powr_over_ln_powr[of _ 1] by simp

lemma bigtheta_const_ln_powr [simp]: "a > 0 ⟹ (λx::real. ln (a*x) powr d) ∈ Θ(λx. ln x powr d)"
by (intro bigthetaI_tendsto[of 1] tendsto_ln_powr_over_ln_powr'') simp

lemma bigtheta_const_ln_pow [simp]: "a > 0 ⟹ (λx::real. ln (a*x) ^ d) ∈ Θ(λx. ln x ^ d)"
proof-
assume a: "a > 0"
have "∀⇩F x in at_top. ln (a * x) ^ d = ln (a * x) powr real d"
using eventually_gt_at_top[of "1/a"]
by eventually_elim (insert a, subst powr_realpow, auto simp: field_simps)
hence "(λx::real. ln (a*x) ^ d) ∈ Θ(λx. ln (a*x) powr real d)"
by (rule bigthetaI_cong)
also from a have "(λx. ln (a*x) powr real d) ∈ Θ(λx. ln x powr real d)" by simp
also have "∀⇩F x in at_top. ln x powr real d = ln x ^ d"
using eventually_gt_at_top[of 1]
by eventually_elim (subst powr_realpow, auto simp: field_simps)
hence "(λx. ln x powr real d) ∈ Θ(λx. ln x ^ d)"
by (rule bigthetaI_cong)
finally show ?thesis .
qed

lemma bigtheta_const_ln [simp]: "a > 0 ⟹ (λx::real. ln (a*x)) ∈ Θ(λx. ln x)"
using tendsto_ln_over_ln[of a 1]  by (intro bigthetaI_tendsto[of 1]) simp_all

text ‹
If there are two functions @{term "f"} and @{term "g"} where any power of @{term "g"} is
asymptotically smaller than @{term "f"}, propositions like @{term "(λx. f x ^ p1 * g x ^ q1) ∈
O(λx. f x ^ p2 * g x ^ q2)"} can be decided just by looking at the exponents:
the proposition is true iff @{term "p1 < p2"} or @{term "p1 = p2 ∧ q1 ≤ q2"}.

The functions @{term "λx. x"}, @{term "λx. ln x"}, @{term "λx. ln (ln x)"}, \$\ldots\$
form a chain in which every function dominates all succeeding functions in the above sense,
allowing to decide propositions involving Landau symbols and functions that are products of
powers of functions from this chain by reducing the proposition to a statement involving only
logical connectives and comparisons on the exponents.

We will now give the mathematical background for this and implement reification to bring
functions from this class into a canonical form, allowing the decision procedure to be
implemented in a simproc.
›

subsection ‹Decision procedure›

definition "powr_closure f ≡ {λx. f x powr p :: real |p. True}"

lemma powr_closureI [simp]: "(λx. f x powr p) ∈ powr_closure f"
unfolding powr_closure_def by force

lemma powr_closureE:
assumes "g ∈ powr_closure f"
obtains p where "g = (λx. f x powr p)"
using assms unfolding powr_closure_def by force

locale landau_function_family =
fixes F :: "'a filter" and H :: "('a ⇒ real) set"
assumes F_nontrivial: "F ≠ bot"
assumes pos: "h ∈ H ⟹ eventually (λx. h x > 0) F"
assumes linear: "h1 ∈ H ⟹ h2 ∈ H ⟹ h1 ∈ o[F](h2) ∨ h2 ∈ o[F](h1) ∨ h1 ∈ Θ[F](h2)"
assumes mult: "h1 ∈ H ⟹ h2 ∈ H ⟹ (λx. h1 x * h2 x) ∈ H"
assumes inverse: "h ∈ H ⟹ (λx. inverse (h x)) ∈ H"
begin

lemma div: "h1 ∈ H ⟹ h2 ∈ H ⟹ (λx. h1 x / h2 x) ∈ H"
by (subst divide_inverse) (intro mult inverse)

lemma nonzero: "h ∈ H ⟹ eventually (λx. h x ≠ 0) F"
by (drule pos) (auto elim: eventually_mono)

lemma landau_cases:
assumes "h1 ∈ H" "h2 ∈ H"
obtains "h1 ∈ o[F](h2)" | "h2 ∈ o[F](h1)" | "h1 ∈ Θ[F](h2)"
using linear[OF assms] by blast

lemma small_big_antisym:
assumes "h1 ∈ H" "h2 ∈ H" "h1 ∈ o[F](h2)" "h2 ∈ O[F](h1)" shows False
proof-
from nonzero[OF assms(1)] nonzero[OF assms(2)] landau_o.small_big_asymmetric[OF assms(3,4)]
have "eventually (λ_::'a. False) F" by eventually_elim simp
thus False by (simp add: eventually_False F_nontrivial)
qed

lemma small_antisym:
assumes "h1 ∈ H" "h2 ∈ H" "h1 ∈ o[F](h2)" "h2 ∈ o[F](h1)" shows False
using assms by (blast intro: small_big_antisym landau_o.small_imp_big)

end

locale landau_function_family_pair =
G: landau_function_family F G + H: landau_function_family F H for F G H +
fixes g
assumes gs_dominate: "g1 ∈ G ⟹ g2 ∈ G ⟹ h1 ∈ H ⟹ h2 ∈ H ⟹ g1 ∈ o[F](g2) ⟹
(λx. g1 x * h1 x) ∈ o[F](λx. g2 x * h2 x)"
assumes g: "g ∈ G"
assumes g_dominates: "h ∈ H ⟹ h ∈ o[F](g)"
begin

sublocale GH: landau_function_family F "G * H"
proof (unfold_locales; (elim set_times_elim; hypsubst)?)
fix g h assume "g ∈ G" "h ∈ H"
from G.pos[OF this(1)] H.pos[OF this(2)] show "eventually (λx. (g*h) x > 0) F"
by eventually_elim simp
next
fix g h assume A: "g ∈ G" "h ∈ H"
have "(λx. inverse ((g * h) x)) = (λx. inverse (g x)) * (λx. inverse (h x))" by (rule ext) simp
also from A have "... ∈ G * H" by (intro G.inverse H.inverse set_times_intro)
finally show "(λx. inverse ((g * h) x)) ∈ G * H" .
next
fix g1 g2 h1 h2 assume A: "g1 ∈ G" "g2 ∈ G" "h1 ∈ H" "h2 ∈ H"
from gs_dominate[OF this] gs_dominate[OF this(2,1,4,3)]
G.linear[OF this(1,2)] H.linear[OF this(3,4)]
show "g1 * h1 ∈ o[F](g2 * h2) ∨ g2 * h2 ∈ o[F](g1 * h1) ∨ g1 * h1 ∈ Θ[F](g2 * h2)"
by (elim disjE) (force simp: func_times bigomega_iff_bigo intro: landau_theta.mult
landau_o.small.mult landau_o.small_big_mult landau_o.big_small_mult)+
have B: "(λx. (g1 * h1) x * (g2 * h2) x) = (g1 * g2) * (h1 * h2)"
by (rule ext) (simp add: func_times mult_ac)
from A show "(λx. (g1 * h1) x * (g2 * h2) x) ∈ G * H"
by (subst B, intro set_times_intro) (auto intro: G.mult H.mult simp: func_times)
qed (fact G.F_nontrivial)

lemma smallo_iff:
assumes "g1 ∈ G" "g2 ∈ G" "h1 ∈ H" "h2 ∈ H"
shows "(λx. g1 x * h1 x) ∈ o[F](λx. g2 x * h2 x) ⟷
g1 ∈ o[F](g2) ∨ (g1 ∈ Θ[F](g2) ∧ h1 ∈ o[F](h2))" (is "?P ⟷ ?Q")
proof (rule G.landau_cases[OF assms(1,2)])
assume "g1 ∈ o[F](g2)"
thus ?thesis by (auto intro!: gs_dominate assms)
next
assume A: "g1 ∈ Θ[F](g2)"
hence B: "g2 ∈ O[F](g1)" by (subst (asm) bigtheta_sym) (rule bigthetaD1)
hence "g1 ∉ o[F](g2)" using assms by (auto dest: G.small_big_antisym)
moreover from A have "o[F](λx. g2 x * h2 x) = o[F](λx. g1 x * h2 x)"
by (intro landau_o.small.cong_bigtheta landau_theta.mult_right, subst bigtheta_sym)
ultimately show ?thesis using G.nonzero[OF assms(1)] A
next
assume A: "g2 ∈ o[F](g1)"
from gs_dominate[OF assms(2,1,4,3) this] have B: "g2 * h2 ∈ o[F](g1 * h1)" by (simp add: func_times)
have "g1 ∉ o[F](g2)" "g1 ∉ Θ[F](g2)" using assms A
by (auto dest: G.small_antisym G.small_big_antisym simp: bigomega_iff_bigo)
moreover have "¬?P"
by (intro notI GH.small_antisym[OF _ _ B] set_times_intro) (simp_all add: func_times assms)
ultimately show ?thesis by blast
qed

lemma bigo_iff:
assumes "g1 ∈ G" "g2 ∈ G" "h1 ∈ H" "h2 ∈ H"
shows "(λx. g1 x * h1 x) ∈ O[F](λx. g2 x * h2 x) ⟷
g1 ∈ o[F](g2) ∨ (g1 ∈ Θ[F](g2) ∧ h1 ∈ O[F](h2))" (is "?P ⟷ ?Q")
proof (rule G.landau_cases[OF assms(1,2)])
assume "g1 ∈ o[F](g2)"
thus ?thesis by (auto intro!: gs_dominate assms landau_o.small_imp_big)
next
assume A: "g2 ∈ o[F](g1)"
hence "g1 ∉ O[F](g2)" using assms by (auto dest: G.small_big_antisym)
moreover from gs_dominate[OF assms(2,1,4,3) A] have "g2*h2 ∈ o[F](g1*h1)" by (simp add: func_times)
hence "g1*h1 ∉ O[F](g2*h2)" by (blast intro: GH.small_big_antisym assms)
ultimately show ?thesis using A assms
by (auto simp: func_times dest: landau_o.small_imp_big)
next
assume A: "g1 ∈ Θ[F](g2)"
hence "g1 ∉ o[F](g2)" unfolding bigtheta_def using assms
by (auto dest: G.small_big_antisym simp: bigomega_iff_bigo)
moreover have "O[F](λx. g2 x * h2 x) = O[F](λx. g1 x * h2 x)"
by (subst landau_o.big.cong_bigtheta[OF landau_theta.mult_right[OF A]]) (rule refl)
ultimately show ?thesis using A G.nonzero[OF assms(2)]
by (auto simp: landau_o.big.mult_cancel_left eventually_nonzero_bigtheta)
qed

lemma bigtheta_iff:
"g1 ∈ G ⟹ g2 ∈ G ⟹ h1 ∈ H ⟹ h2 ∈ H ⟹
(λx. g1 x * h1 x) ∈ Θ[F](λx. g2 x * h2 x) ⟷ g1 ∈ Θ[F](g2) ∧ h1 ∈ Θ[F](h2)"
by (auto simp: bigtheta_def bigo_iff bigomega_iff_bigo intro: landau_o.small_imp_big
dest: G.small_antisym G.small_big_antisym)

end

lemma landau_function_family_powr_closure:
assumes "F ≠ bot" "filterlim f at_top F"
shows   "landau_function_family F (powr_closure f)"
proof (unfold_locales; (elim powr_closureE; hypsubst)?)
from assms have "eventually (λx. f x ≥ 1) F" using filterlim_at_top by auto
hence A: "eventually (λx. f x ≠ 0) F" by eventually_elim simp
{
fix p q :: real
show "(λx. f x powr p) ∈ o[F](λx. f x powr q) ∨
(λx. f x powr q) ∈ o[F](λx. f x powr p) ∨
(λx. f x powr p) ∈ Θ[F](λx. f x powr q)"
by (cases p q rule: linorder_cases)
(force intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric]  assms A)+
}
fix p
show "eventually (λx. f x powr p > 0) F" using A by simp
qed (auto simp: powr_add[symmetric] powr_minus[symmetric] ‹F ≠ bot› intro: powr_closureI)

lemma landau_function_family_pair_trans:
assumes "landau_function_family_pair Ftr F G f"
assumes "landau_function_family_pair Ftr G H g"
shows   "landau_function_family_pair Ftr F (G*H) f"
proof-
interpret FG: landau_function_family_pair Ftr F G f by fact
interpret GH: landau_function_family_pair Ftr G H g by fact
show ?thesis
proof (unfold_locales; (elim set_times_elim)?; (clarify)?;
(unfold func_times mult.assoc[symmetric])?)
fix f1 f2 g1 g2 h1 h2
assume A: "f1 ∈ F" "f2 ∈ F" "g1 ∈ G" "g2 ∈ G" "h1 ∈ H" "h2 ∈ H" "f1 ∈ o[Ftr](f2)"

from A have "(λx. f1 x * g1 x * h1 x) ∈ o[Ftr](λx. f1 x * g1 x * g x)"
by (intro landau_o.small.mult_left GH.g_dominates)
also have "(λx. f1 x * g1 x * g x) = (λx. f1 x * (g1 x * g x))" by (simp only: mult.assoc)
also from A have "... ∈ o[Ftr](λx. f2 x * (g2 x / g x))"
by (intro FG.gs_dominate FG.H.mult FG.H.div GH.g)
also from A have "(λx. inverse (h2 x)) ∈ o[Ftr](g)" by (intro GH.g_dominates GH.H.inverse)
with GH.g A have "(λx. f2 x * (g2 x / g x)) ∈ o[Ftr](λx. f2 x * (g2 x * h2 x))"
by (auto simp: FG.H.nonzero GH.H.nonzero divide_inverse
intro!: landau_o.small.mult_left intro: landau_o.small.inverse_flip)
also have "... = o[Ftr](λx. f2 x * g2 x * h2 x)" by (simp only: mult.assoc)
finally show "(λx. f1 x * g1 x * h1 x) ∈ o[Ftr](λx. f2 x * g2 x * h2 x)" .
next
fix g1 h1 assume A: "g1 ∈ G" "h1 ∈ H"
hence "(λx. g1 x * h1 x) ∈ o[Ftr](λx. g1 x * g x)"
by (intro landau_o.small.mult_left GH.g_dominates)
also from A have "(λx. g1 x * g x) ∈ o[Ftr](f)" by (intro FG.g_dominates FG.H.mult GH.g)
finally show "(λx. g1 x * h1 x) ∈ o[Ftr](f)" .
qed

lemma landau_function_family_pair_trans_powr:
assumes "landau_function_family_pair F (powr_closure g) H (λx. g x powr 1)"
assumes "filterlim f at_top F"
assumes "⋀p. (λx. g x powr p) ∈ o[F](f)"
shows   "landau_function_family_pair F (powr_closure f) (powr_closure g * H) (λx. f x powr 1)"
proof (rule landau_function_family_pair_trans[OF _ assms(1)])
interpret GH: landau_function_family_pair F "powr_closure g" H "λx. g x powr 1" by fact
interpret F: landau_function_family F "powr_closure f"
by (rule landau_function_family_powr_closure) (rule GH.G.F_nontrivial, rule assms)
show "landau_function_family_pair F (powr_closure f) (powr_closure g) (λx. f x powr 1)"
proof (unfold_locales; (elim powr_closureE; hypsubst)?)
show "(λx. f x powr 1) ∈ powr_closure f" by (rule powr_closureI)
next
fix p ::real
note assms(3)[of p]
also from assms(2) have "eventually (λx. f x ≥ 1) F" by (force simp: filterlim_at_top)
hence "f ∈ Θ[F](λx. f x powr 1)" by (auto intro!: bigthetaI_cong elim!: eventually_mono)
finally show "(λx. g x powr p) ∈ o[F](λx. f x powr 1)" .
next
fix p p1 p2 p3 :: real
assume A: "(λx. f x powr p) ∈ o[F](λx. f x powr p1)"
have p: "p < p1"
proof (cases p p1 rule: linorder_cases)
assume "p > p1"
moreover from assms(2) have "eventually (λx. f x ≥ 1) F"
by (force simp: filterlim_at_top)
hence "eventually (λx. f x ≠ 0) F" by eventually_elim simp
ultimately have "(λx. f x powr p1) ∈ o[F](λx. f x powr p)" using assms
by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
from F.small_antisym[OF _ _ this A] show ?thesis by (auto simp: powr_closureI)
next
assume "p = p1"
hence "(λx. f x powr p1) ∈ O[F](λx. f x powr p)" by (intro bigthetaD1) simp
with F.small_big_antisym[OF _ _ A this] show ?thesis by (auto simp: powr_closureI)
qed

from assms(2) have f_pos: "eventually (λx. f x ≥ 1) F" by (force simp: filterlim_at_top)
from assms have "(λx. g x powr ((p2 - p3)/(p1 - p))) ∈ o[F](f)" by simp
from smallo_powr[OF this, of "p1 - p"] p
have "(λx. g x powr (p2 - p3)) ∈ o[F](λx. ¦f x¦ powr (p1 - p))" by (simp add: powr_powr)
hence "(λx. ¦f x¦ powr p * g x powr p2) ∈ o[F](λx. ¦f x¦ powr p1 * g x powr p3)" (is ?P)
using GH.G.nonzero[OF GH.g] F.nonzero[OF powr_closureI]
landau_o.small.divide_eq2 mult.commute)
also have "?P ⟷ (λx. f x powr p * g x powr p2) ∈ o[F](λx. f x powr p1 * g x powr p3)"
using f_pos by (intro landau_o.small.cong_ex) (auto elim!: eventually_mono)
finally show "(λx. f x powr p * g x powr p2) ∈ o[F](λx. f x powr p1 * g x powr p3)" .
qed
qed

definition dominates :: "'a filter ⇒ ('a ⇒ real) ⇒ ('a ⇒ real) ⇒ bool" where
"dominates F f g = (∀p. (λx. g x powr p) ∈ o[F](f))"

lemma dominates_trans:
assumes "eventually (λx. g x > 0) F"
assumes "dominates F f g" "dominates F g h"
shows   "dominates F f h"
unfolding dominates_def
proof
fix p :: real
from assms(3) have "(λx. h x powr p) ∈ o[F](g)" unfolding dominates_def by simp
also from assms(1) have "g ∈ Θ[F](λx. g x powr 1)"
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
also from assms(2) have "(λx. g x powr 1) ∈ o[F](f)" unfolding dominates_def by simp
finally show "(λx. h x powr p) ∈ o[F](f)" .
qed

fun landau_dominating_chain where
"landau_dominating_chain F (f # g # gs) ⟷
dominates F f g ∧ landau_dominating_chain F (g # gs)"
| "landau_dominating_chain F [f] ⟷ (λx. 1) ∈ o[F](f)"
| "landau_dominating_chain F [] ⟷ True"

primrec landau_dominating_chain' where
"landau_dominating_chain' F [] ⟷ True"
| "landau_dominating_chain' F (f # gs) ⟷
landau_function_family_pair F (powr_closure f) (prod_list (map powr_closure gs)) (λx. f x powr 1) ∧
landau_dominating_chain' F gs"

primrec nonneg_list where
"nonneg_list [] ⟷ True"
| "nonneg_list (x#xs) ⟷ x > 0 ∨ (x = 0 ∧ nonneg_list xs)"

primrec pos_list where
"pos_list [] ⟷ False"
| "pos_list (x#xs) ⟷ x > 0 ∨ (x = 0 ∧ pos_list xs)"

lemma dominating_chain_imp_dominating_chain':
"Ftr ≠ bot ⟹ (⋀g. g ∈ set gs ⟹ filterlim g at_top Ftr) ⟹
landau_dominating_chain Ftr gs ⟹ landau_dominating_chain' Ftr gs"
proof (induction gs rule: landau_dominating_chain.induct)
case (1 F f g gs)
from 1 show ?case
by (auto intro!: landau_function_family_pair_trans_powr simp add: dominates_def)
next
case (2 F f)
then interpret F: landau_function_family F "powr_closure f"
by (intro landau_function_family_powr_closure) simp_all
from 2 have "eventually (λx. f x ≥ 1) F" by (force simp: filterlim_at_top)
hence "o[F](λx. f x powr 1) = o[F](λx. f x)"
by (intro landau_o.small.cong) (auto elim!: eventually_mono)
with 2 have "landau_function_family_pair F (powr_closure f) {λ_. 1} (λx. f x powr 1)"
by unfold_locales (auto intro: powr_closureI)
thus ?case by (simp add: one_fun_def)
next
case 3
then show ?case by simp
qed

locale landau_function_family_chain =
fixes F :: "'b filter"
fixes gs :: "'a list"
fixes get_param :: "'a ⇒ real"
fixes get_fun :: "'a ⇒ ('b ⇒ real)"
assumes F_nontrivial: "F ≠ bot"
assumes gs_pos: "g ∈ set (map get_fun gs) ⟹ filterlim g at_top F"
assumes dominating_chain: "landau_dominating_chain F (map get_fun gs)"
begin

lemma dominating_chain': "landau_dominating_chain' F (map get_fun gs)"
by (intro dominating_chain_imp_dominating_chain' gs_pos dominating_chain F_nontrivial)

lemma gs_powr_0_eq_one:
"eventually (λx. (∏g←gs. get_fun g x powr 0) = 1) F"
using gs_pos
proof (induction gs)
case (Cons g gs)
from Cons have "eventually (λx. get_fun g x > 0) F" by (auto simp: filterlim_at_top_dense)
moreover from Cons have "eventually (λx. (∏g←gs. get_fun g x powr 0) = 1) F" by simp
ultimately show ?case by eventually_elim simp
qed simp_all

lemma listmap_gs_in_listmap:
"(λx. ∏g←fs. h g x powr p g) ∈ prod_list (map powr_closure (map h fs))"
proof-
have "(λx. ∏g←fs. h g x powr p g) = (∏g←fs. (λx. h g x powr p g))"
by (rule ext, induction fs) simp_all
also have "... ∈ prod_list (map powr_closure (map h fs))"
apply (induction fs)
apply (simp only: list.map prod_list.Cons, rule set_times_intro)
apply simp_all
done
finally show ?thesis .
qed

lemma smallo_iff:
"(λ_. 1) ∈ o[F](λx. ∏g←gs. get_fun g x powr get_param g) ⟷ pos_list (map get_param gs)"
proof-
have "((λ_. 1) ∈ o[F](λx. ∏g←gs. get_fun g x powr get_param g)) ⟷
((λx. ∏g←gs. get_fun g x powr 0) ∈ o[F](λx. ∏g←gs. get_fun g x powr get_param g))"
by (rule sym, intro landau_o.small.in_cong gs_powr_0_eq_one)
also from gs_pos dominating_chain' have "... ⟷ pos_list (map get_param gs)"
proof (induction gs)
case Nil
have "(λx::'b. 1::real) ∉ o[F](λx. 1)" using F_nontrivial
by (auto dest!: landau_o.small_big_asymmetric)
thus ?case by simp
next
case (Cons g gs)
then interpret G: landau_function_family_pair F "powr_closure (get_fun g)"
"prod_list (map powr_closure (map get_fun gs))" "λx. get_fun g x powr 1" by simp
from Cons show ?case using listmap_gs_in_listmap[of get_fun _ gs] F_nontrivial
by (simp_all add: G.smallo_iff listmap_gs_in_listmap powr_smallo_iff powr_bigtheta_iff
del: powr_zero_eq_one)
qed
finally show ?thesis .
qed

lemma bigo_iff:
"(λ_. 1) ∈ O[F](λx. ∏g←gs. get_fun g x powr get_param g) ⟷ nonneg_list (map get_param gs)"
proof-
have "((λ_. 1) ∈ O[F](λx. ∏g←gs. get_fun g x powr get_param g)) ⟷
((λx. ∏g←gs. get_fun g x powr 0) ∈ O[F](λx. ∏g←gs. get_fun g x powr get_param g))"
by (rule sym, intro landau_o.big.in_cong gs_powr_0_eq_one)
also from gs_pos dominating_chain' have "... ⟷ nonneg_list (map get_param gs)"
proof (induction gs)
case Nil
then show ?case by (simp add: func_one)
next
case (Cons g gs)
then interpret G: landau_function_family_pair F "powr_closure (get_fun g)"
"prod_list (map powr_closure (map get_fun gs))" "λx. get_fun g x powr 1" by simp
from Cons show ?case using listmap_gs_in_listmap[of get_fun _ gs] F_nontrivial
by (simp_all add: G.bigo_iff listmap_gs_in_listmap powr_smallo_iff powr_bigtheta_iff
del: powr_zero_eq_one)
qed
finally show ?thesis .
qed

lemma bigtheta_iff:
"(λ_. 1) ∈ Θ[F](λx. ∏g←gs. get_fun g x powr get_param g) ⟷ list_all ((=) 0) (map get_param gs)"
proof-
have "((λ_. 1) ∈ Θ[F](λx. ∏g←gs. get_fun g x powr get_param g)) ⟷
((λx. ∏g←gs. get_fun g x powr 0) ∈ Θ[F](λx. ∏g←gs. get_fun g x powr get_param g))"
by (rule sym, intro landau_theta.in_cong gs_powr_0_eq_one)
also from gs_pos dominating_chain' have "... ⟷ list_all ((=) 0) (map get_param gs)"
proof (induction gs)
case Nil
then show ?case by (simp add: func_one)
next
case (Cons g gs)
then interpret G: landau_function_family_pair F "powr_closure (get_fun g)"
"prod_list (map powr_closure (map get_fun gs))" "λx. get_fun g x powr 1" by simp
from Cons show ?case using listmap_gs_in_listmap[of get_fun _ gs] F_nontrivial
by (simp_all add: G.bigtheta_iff listmap_gs_in_listmap powr_smallo_iff powr_bigtheta_iff
del: powr_zero_eq_one)
qed
finally show ?thesis .
qed

end

lemma fun_chain_at_top_at_top:
assumes "filterlim (f :: ('a::order) ⇒ 'a) at_top at_top"
shows   "filterlim (f ^^ n) at_top at_top"
by (induction n) (auto intro: filterlim_ident filterlim_compose[OF assms])

lemma const_smallo_ln_chain: "(λ_. 1) ∈ o((ln::real⇒real)^^n)"
proof (intro smalloI_tendsto)
show "((λx::real. 1 / (ln^^n) x) ⤏ 0) at_top"
by (rule tendsto_divide_0 tendsto_const filterlim_at_top_imp_at_infinity
fun_chain_at_top_at_top ln_at_top)+
next
from fun_chain_at_top_at_top[OF ln_at_top, of n]
have "eventually (λx::real. (ln^^n) x > 0) at_top" by (simp add: filterlim_at_top_dense)
thus "eventually (λx::real. (ln^^n) x ≠ 0) at_top" by eventually_elim simp_all
qed

lemma ln_fun_in_smallo_fun:
assumes "filterlim f at_top at_top"
shows   "(λx. ln (f x) powr p :: real) ∈ o(f)"
proof (rule smalloI_tendsto)
have "((λx. ln x powr p / x powr 1) ⤏ 0) at_top" by (rule tendsto_ln_powr_over_powr') simp
moreover have "eventually (λx. ln x powr p / x powr 1 = ln x powr p / x) at_top"
using eventually_gt_at_top[of "0::real"] by eventually_elim simp
ultimately have "((λx. ln x powr p / x) ⤏ 0) at_top" by (subst (asm) tendsto_cong)
from this assms show "((λx. ln (f x) powr p / f x) ⤏ 0) at_top"
by (rule filterlim_compose)
from assms have "eventually (λx. f x ≥ 1) at_top" by (simp add: filterlim_at_top)
thus "eventually (λx. f x ≠ 0) at_top" by eventually_elim simp
qed

lemma ln_chain_dominates: "m > n ⟹ dominates at_top ((ln::real ⇒ real)^^n) (ln^^m)"
proof (erule less_Suc_induct)
fix n show "dominates at_top ((ln::real⇒real)^^n) (ln^^(Suc n))" unfolding dominates_def
by (force intro: ln_fun_in_smallo_fun fun_chain_at_top_at_top ln_at_top)
next
fix k m n
assume A: "dominates at_top ((ln::real ⇒ real)^^k) (ln^^m)"
"dominates at_top ((ln::real ⇒ real)^^m) (ln^^n)"
from fun_chain_at_top_at_top[OF ln_at_top, of m]
have "eventually (λx::real. (ln^^m) x > 0) at_top" by (simp add: filterlim_at_top_dense)
from this A show "dominates at_top ((ln::real ⇒ real)^^k) ((ln::real ⇒ real)^^n)"
by (rule dominates_trans)
qed

datatype primfun = LnChain nat

instantiation primfun :: linorder
begin

fun less_eq_primfun :: "primfun ⇒ primfun ⇒ bool" where
"LnChain x ≤ LnChain y ⟷ x ≤ y"

fun less_primfun :: "primfun ⇒ primfun ⇒ bool" where
"LnChain x < LnChain y ⟷ x < y"

instance
proof (standard, goal_cases)
case (1 x y) show ?case by (induction x y rule: less_eq_primfun.induct) auto
next
case (2 x) show ?case by (cases x) auto
next
case (3 x y z) thus ?case
by (induction x y rule: less_eq_primfun.induct, cases z) auto
next
case (4 x y) thus ?case by (induction x y rule: less_eq_primfun.induct) auto
next
case (5 x y) thus ?case by (induction x y rule: less_eq_primfun.induct) auto
qed

end

fun eval_primfun' :: "_ ⇒ _ ⇒ real" where
"eval_primfun' (LnChain n) = (λx. (ln^^n) x)"

fun eval_primfun :: "_ ⇒ _ ⇒ real" where
"eval_primfun (f, e) = (λx. eval_primfun' f x powr e)"

lemma eval_primfun_altdef: "eval_primfun f x = eval_primfun' (fst f) x powr snd f"
by (cases f) simp

fun merge_primfun where
"merge_primfun (x::primfun, a) (y, b) = (x, a + b)"

fun inverse_primfun where
"inverse_primfun (x::primfun, a) = (x, -a)"

fun powr_primfun where
"powr_primfun (x::primfun, a) e = (x, e*a)"

lemma primfun_cases:
assumes "(⋀n e. P (LnChain n, e))"
shows   "P x"
proof (cases x, hypsubst)
fix a b show "P (a, b)" by (cases a; hypsubst, rule assms)
qed

lemma eval_primfun'_at_top: "filterlim (eval_primfun' f) at_top at_top"
by (cases f) (auto intro!: fun_chain_at_top_at_top ln_at_top)

lemma primfun_dominates:
"f < g ⟹ dominates at_top (eval_primfun' f) (eval_primfun' g)"
by (elim less_primfun.elims; hypsubst) (simp_all add: ln_chain_dominates)

lemma eval_primfun_pos: "eventually (λx::real. eval_primfun f x > 0) at_top"
proof (cases f, hypsubst)
fix f e
from eval_primfun'_at_top have "eventually (λx. eval_primfun' f x > 0) at_top"
by (auto simp: filterlim_at_top_dense)
thus "eventually (λx::real. eval_primfun (f,e) x > 0) at_top" by eventually_elim simp
qed

lemma eventually_nonneg_primfun: "eventually_nonneg at_top (eval_primfun f)"
unfolding eventually_nonneg_def using eval_primfun_pos[of f] by eventually_elim simp

lemma eval_primfun_nonzero: "eventually (λx. eval_primfun f x ≠ 0) at_top"
using eval_primfun_pos[of f] by eventually_elim simp

lemma eval_merge_primfun:
"fst f = fst g ⟹
eval_primfun (merge_primfun f g) x = eval_primfun f x * eval_primfun g x"

lemma eval_inverse_primfun:
"eval_primfun (inverse_primfun f) x = inverse (eval_primfun f x)"
by (induction f rule: inverse_primfun.induct) (simp_all add: powr_minus)

lemma eval_powr_primfun:
"eval_primfun (powr_primfun f e) x = eval_primfun f x powr e"
by (induction f e rule: powr_primfun.induct) (simp_all add: powr_powr mult.commute)

definition eval_primfuns where
"eval_primfuns fs x = (∏f←fs. eval_primfun f x)"

lemma eval_primfuns_pos: "eventually (λx. eval_primfuns fs x > 0) at_top"
proof-
have prod_list_pos: "(⋀x::_::linordered_semidom. x ∈ set xs ⟹ x > 0) ⟹ prod_list xs > 0"
for xs :: "real list" by (induction xs) auto
have "eventually (λx. ∀f∈set fs. eval_primfun f x > 0) at_top"
by (intro eventually_ball_finite ballI eval_primfun_pos finite_set)
thus ?thesis unfolding eval_primfuns_def by eventually_elim (rule prod_list_pos, auto)
qed

lemma eval_primfuns_nonzero: "eventually (λx. eval_primfuns fs x ≠ 0) at_top"
using eval_primfuns_pos[of fs] by eventually_elim simp

subsection ‹Reification›

definition LANDAU_PROD' where
"LANDAU_PROD' L c f = L(λx. c * f x)"

definition LANDAU_PROD where
"LANDAU_PROD L c1 c2 fs ⟷ (λ_. c1) ∈ L(λx. c2 * eval_primfuns fs x)"

definition BIGTHETA_CONST' where "BIGTHETA_CONST' c = Θ(λx. c)"
definition BIGTHETA_CONST where "BIGTHETA_CONST c A = set_mult Θ(λ_. c) A"
definition BIGTHETA_FUN where "BIGTHETA_FUN f = Θ(f)"

lemma BIGTHETA_CONST'_tag: "Θ(λx. c) = BIGTHETA_CONST' c" using BIGTHETA_CONST'_def ..
lemma BIGTHETA_CONST_tag: "Θ(f) = BIGTHETA_CONST 1 Θ(f)"
lemma BIGTHETA_FUN_tag: "Θ(f) = BIGTHETA_FUN f"

lemma set_mult_is_times: "set_mult A B = A * B"
unfolding set_mult_def set_times_def func_times by blast

lemma set_powr_mult:
assumes "eventually_nonneg F f" and "eventually_nonneg F g"
shows   "Θ[F](λx. (f x * g x :: real) powr p) = set_mult (Θ[F](λx. f x powr p)) (Θ[F](λx. g x powr p))"
proof-
from assms have "eventually (λx. f x ≥ 0) F" "eventually (λx. g x ≥ 0) F"
hence "eventually (λx. (f x * g x :: real) powr p = f x powr p * g x powr p) F"
hence "Θ[F](λx. (f x * g x :: real) powr p) = Θ[F](λx. f x powr p * g x powr p)"
by (rule landau_theta.cong)
also have "... = set_mult (Θ[F](λx. f x powr p)) (Θ[F](λx. g x powr p))"
finally show ?thesis .
qed

lemma eventually_nonneg_bigtheta_pow_realpow:
"Θ(λx. eval_primfun f x ^ e) = Θ(λx. eval_primfun f x powr real e)"
using eval_primfun_pos[of f]
by (auto intro!: landau_theta.cong elim!: eventually_mono simp: powr_realpow)

lemma BIGTHETA_CONST_fold:
"BIGTHETA_CONST (c::real) (BIGTHETA_CONST d A) = BIGTHETA_CONST (c*d) A"
"bigtheta_pow at_top (BIGTHETA_CONST c Θ(eval_primfun pf)) k =
BIGTHETA_CONST (c ^ k) Θ(λx. eval_primfun pf x powr k)"
"set_inverse (BIGTHETA_CONST c Θ(f)) = BIGTHETA_CONST (inverse c) Θ(λx. inverse (f x))"
"set_mult (BIGTHETA_CONST c Θ(f)) (BIGTHETA_CONST d Θ(g)) =
BIGTHETA_CONST (c*d) Θ(λx. f x*g x)"
"BIGTHETA_CONST' (c::real) = BIGTHETA_CONST c Θ(λ_. 1)"
"BIGTHETA_FUN (f::real⇒real) = BIGTHETA_CONST 1 Θ(f)"
apply (simp add: BIGTHETA_CONST_def set_mult_is_times bigtheta_mult_eq_set_mult mult_ac)
apply (simp only: BIGTHETA_CONST_def bigtheta_mult_eq_set_mult[symmetric]
bigtheta_pow_eq_set_pow[symmetric] power_mult_distrib mult_ac)
by (simp_all add: BIGTHETA_CONST_def BIGTHETA_CONST'_def BIGTHETA_FUN_def
bigtheta_mult_eq_set_mult[symmetric] set_mult_is_times[symmetric]
bigtheta_pow_eq_set_pow[symmetric] bigtheta_inverse_eq_set_inverse[symmetric]
mult_ac power_mult_distrib)

lemma fold_fun_chain:
"g x = (g ^^ 1) x" "(g ^^ m) ((g ^^ n) x) = (g ^^ (m+n)) x"

lemma reify_ln_chain1:
"Θ(λx. (ln ^^ n) x) = Θ(eval_primfun (LnChain n, 1))"
proof (intro landau_theta.cong)
have "filterlim ((ln :: real ⇒ real) ^^ n) at_top at_top"
by (intro fun_chain_at_top_at_top ln_at_top)
hence "eventually (λx::real. (ln ^^ n) x > 0) at_top" using filterlim_at_top_dense by auto
thus "eventually (λx. (ln ^^ n) x = eval_primfun (LnChain n, 1) x) at_top"
by eventually_elim simp
qed

lemma reify_monom1:
"Θ(λx::real. x) = Θ(eval_primfun (LnChain 0, 1))"
proof (intro landau_theta.cong)
from eventually_gt_at_top[of "0::real"]
show "eventually (λx. x = eval_primfun (LnChain 0, 1) x) at_top"
by eventually_elim simp
qed

lemma reify_monom_pow:
"Θ(λx::real. x ^ e) = Θ(eval_primfun (LnChain 0, real e))"
proof-
have "Θ(eval_primfun (LnChain 0, real e)) = Θ(λx. x powr (real e))" by simp
also have "eventually (λx. x powr (real e) = x ^ e) at_top"
using eventually_gt_at_top[of 0] by eventually_elim (simp add: powr_realpow)
hence "Θ(λx. x powr (real e)) = Θ(λx. x ^ e)"
by (rule landau_theta.cong)
finally show ?thesis ..
qed

lemma reify_monom_powr:
"Θ(λx::real. x powr e) = Θ(eval_primfun (LnChain 0, e))"
by (rule landau_theta.cong) simp

lemmas reify_monom = reify_monom1 reify_monom_pow reify_monom_powr

lemma reify_ln_chain_pow:
"Θ(λx. (ln ^^ n) x ^ e) = Θ(eval_primfun (LnChain n, real e))"
proof-
have "Θ(eval_primfun (LnChain n, real e)) = Θ(λx. (ln ^^ n) x powr (real e))" by simp
also have "eventually (λx::real. (ln ^^ n) x > 0) at_top"
using fun_chain_at_top_at_top[OF ln_at_top] unfolding filterlim_at_top_dense by blast
hence "eventually (λx. (ln ^^ n) x powr (real e) = (ln ^^ n) x ^ e) at_top"
by eventually_elim (subst powr_realpow, auto)
hence "Θ(λx. (ln ^^ n) x powr (real e)) = Θ(λx. (ln ^^ n) x^e)"
by (rule landau_theta.cong)
finally show ?thesis ..
qed

lemma reify_ln_chain_powr:
"Θ(λx. (ln ^^ n) x powr e) = Θ(eval_primfun (LnChain n, e))"
by (intro landau_theta.cong) simp

lemmas reify_ln_chain = reify_ln_chain1 reify_ln_chain_pow reify_ln_chain_powr

lemma numeral_power_Suc: "numeral n ^ Suc a = numeral n * numeral n ^ a"
by (rule power.simps)

lemmas landau_product_preprocess =
one_add_one one_plus_numeral numeral_plus_one arith_simps numeral_power_Suc power_0
fold_fun_chain[where g = ln] reify_ln_chain reify_monom

lemma LANDAU_PROD'_fold:
"BIGTHETA_CONST e Θ(λ_. d) = BIGTHETA_CONST (e*d) Θ(eval_primfuns [])"
"LANDAU_PROD' c (λ_. 1) = LANDAU_PROD' c (eval_primfuns [])"
"eval_primfun f = eval_primfuns [f]"
"eval_primfuns fs x * eval_primfuns gs x = eval_primfuns (fs @ gs) x"
apply (simp only: BIGTHETA_CONST_def set_mult_is_times eval_primfuns_def[abs_def] bigtheta_mult_eq)

lemma inverse_prod_list_field:
"prod_list (map (λx. inverse (f x)) xs) = inverse (prod_list (map f xs :: _ :: field list))"
by (induction xs) simp_all

lemma landau_prod_meta_cong:
assumes "landau_symbol L L' Lr"
assumes "Θ(f) ≡ BIGTHETA_CONST c1 (Θ(eval_primfuns fs))"
assumes "Θ(g) ≡ BIGTHETA_CONST c2 (Θ(eval_primfuns gs))"
shows   "f ∈ L at_top (g) ≡ LANDAU_PROD (L at_top) c1 c2 (map inverse_primfun fs @ gs)"
proof-
interpret landau_symbol L L' Lr by fact
have "f ∈ L at_top (g) ⟷ (λx. c1 * eval_primfuns fs x) ∈ L at_top (λx. c2 * eval_primfuns gs x)"
using assms(2,3)[symmetric] unfolding BIGTHETA_CONST_def
by (intro cong_ex_bigtheta) (simp_all add: bigtheta_mult_eq_set_mult[symmetric])
also have "... ⟷ (λx. c1) ∈ L at_top (λx. c2 * eval_primfuns gs x / eval_primfuns fs x)"
finally show "f ∈ L at_top (g) ≡ LANDAU_PROD (L at_top) c1 c2 (map inverse_primfun fs @ gs)"
by (simp add: LANDAU_PROD_def eval_primfuns_def eval_inverse_primfun
divide_inverse o_def inverse_prod_list_field mult_ac)
qed

fun pos_primfun_list where
"pos_primfun_list [] ⟷ False"
| "pos_primfun_list ((_,x)#xs) ⟷ x > 0 ∨ (x = 0 ∧ pos_primfun_list xs)"

fun nonneg_primfun_list where
"nonneg_primfun_list [] ⟷ True"
| "nonneg_primfun_list ((_,x)#xs) ⟷ x > 0 ∨ (x = 0 ∧ nonneg_primfun_list xs)"

fun iszero_primfun_list where
"iszero_primfun_list [] ⟷ True"
| "iszero_primfun_list ((_,x)#xs) ⟷ x = 0 ∧ iszero_primfun_list xs"

definition "group_primfuns ≡ groupsort.group_sort fst merge_primfun"

lemma list_ConsCons_induct:
assumes "P []" "⋀x. P [x]" "⋀x y xs. P (y#xs) ⟹ P (x#y#xs)"
shows   "P xs"
proof (induction xs rule: length_induct)
case (1 xs)
show ?case
proof (cases xs)
case (Cons x xs')
note A = this
from assms 1 show ?thesis
proof (cases xs')
case (Cons y xs'')
with 1 A have "P (y#xs'')" by simp
with Cons A assms show ?thesis by simp
qed

lemma landau_function_family_chain_primfuns:
assumes "sorted (map fst fs)"
assumes "distinct (map fst fs)"
shows   "landau_function_family_chain at_top fs (eval_primfun' o fst)"
proof (standard, goal_cases)
case 3
from assms show ?case
proof (induction fs rule: list_ConsCons_induct)
case (2 g)
from eval_primfun'_at_top[of "fst g"]
have "eval_primfun' (fst g) ∈ ω(λ_. 1)"
by (intro smallomegaI_filterlim_at_infinity filterlim_at_top_imp_at_infinity) simp
thus ?case by (simp add: smallomega_iff_smallo)
next
case (3 f g gs)
thus ?case by (auto simp: primfun_dominates)
qed simp
qed (auto simp: eval_primfun'_at_top)

lemma (in monoid_mult) fold_plus_prod_list_rev:
"fold times xs = times (prod_list (rev xs))"
proof
fix x
have "fold times xs x = prod_list (rev xs @ [x])"
also have "… = prod_list (rev xs) * x"
by simp
finally show "fold times xs x = prod_list (rev xs) * x" .
qed

interpretation groupsort_primfun: groupsort fst merge_primfun eval_primfuns
proof (standard, goal_cases)
case (1 x y)
thus ?case by (induction x y rule: merge_primfun.induct) simp_all
next
case (2 fs gs)
show ?case
proof
fix x
have "eval_primfuns fs x = fold (*) (map (λf. eval_primfun f x) fs) 1"
unfolding eval_primfuns_def by (simp add: fold_plus_prod_list_rev)
also have "fold (*) (map (λf. eval_primfun f x) fs) = fold (*) (map (λf. eval_primfun f x) gs)"
using 2 by (intro fold_multiset_equiv ext) auto
also have "... 1 = eval_primfuns gs x"
unfolding eval_primfuns_def by (simp add: fold_plus_prod_list_rev)
finally show "eval_primfuns fs x = eval_primfuns gs x" .
qed
qed (auto simp: fun_eq_iff eval_merge_primfun eval_primfuns_def)

lemma nonneg_primfun_list_iff: "nonneg_primfun_list fs = nonneg_list (map snd fs)"
by (induction fs rule: nonneg_primfun_list.induct) simp_all

lemma pos_primfun_list_iff: "pos_primfun_list fs = pos_list (map snd fs)"
by (induction fs rule: pos_primfun_list.induct) simp_all

lemma iszero_primfun_list_iff: "iszero_primfun_list fs = list_all ((=) 0) (map snd fs)"
by (induction fs rule: iszero_primfun_list.induct) simp_all

lemma landau_primfuns_iff:
"((λ_. 1) ∈ O(eval_primfuns fs)) = nonneg_primfun_list (group_primfuns fs)" (is "?A")
"((λ_. 1) ∈ o(eval_primfuns fs)) = pos_primfun_list (group_primfuns fs)" (is "?B")
"((λ_. 1) ∈ Θ(eval_primfuns fs)) = iszero_primfun_list (group_primfuns fs)" (is "?C")
proof-
interpret landau_function_family_chain at_top "group_primfuns fs" snd "eval_primfun' o fst"
by (rule landau_function_family_chain_primfuns)
groupsort_primfun.distinct_group_sort)

have "(λ_. 1) ∈ O(eval_primfuns fs) ⟷ (λ_. 1) ∈ O(eval_primfuns (group_primfuns fs))"
also have "... ⟷ nonneg_list (map snd (group_primfuns fs))" using bigo_iff
finally show ?A by (simp add: nonneg_primfun_list_iff)

have "(λ_. 1) ∈ o(eval_primfuns fs) ⟷ (λ_. 1) ∈ o(eval_primfuns (group_primfuns fs))"
also have "... ⟷ pos_list (map snd (group_primfuns fs))" using smallo_iff
finally show ?B by (simp add: pos_primfun_list_iff)

have "(λ_. 1) ∈ Θ(eval_primfuns fs) ⟷ (λ_. 1) ∈ Θ(eval_primfuns (group_primfuns fs))"
also have "... ⟷ list_all ((=) 0) (map snd (group_primfuns fs))" using bigtheta_iff
finally show ?C by (simp add: iszero_primfun_list_iff)
qed

lemma LANDAU_PROD_bigo_iff:
"LANDAU_PROD (bigo at_top) c1 c2 fs ⟷ c1 = 0 ∨ (c2 ≠ 0 ∧ nonneg_primfun_list (group_primfuns fs))"
unfolding LANDAU_PROD_def
by (cases "c1 = 0", simp, cases "c2 = 0", simp) (simp_all add: landau_primfuns_iff)

lemma LANDAU_PROD_smallo_iff:
"LANDAU_PROD (smallo at_top) c1 c2 fs ⟷ c1 = 0 ∨ (c2 ≠ 0 ∧ pos_primfun_list (group_primfuns fs))"
unfolding LANDAU_PROD_def
by (cases "c1 = 0", simp, cases "c2 = 0", simp) (simp_all add: landau_primfuns_iff)

lemma LANDAU_PROD_bigtheta_iff:
"LANDAU_PROD (bigtheta at_top) c1 c2 fs ⟷ (c1 = 0 ∧ c2 = 0) ∨ (c1 ≠ 0 ∧ c2 ≠ 0 ∧
iszero_primfun_list (group_primfuns fs))"
proof-
have A: "⋀P x. (x = 0 ⟹ P) ⟹ (x ≠ 0 ⟹ P) ⟹ P" by blast
{
assume "eventually (λx. eval_primfuns fs x = 0) at_top"
with eval_primfuns_nonzero[of fs] have "eventually (λx::real. False) at_top"
by eventually_elim simp
hence False by simp
} note B = this
show ?thesis by (rule A[of c1, case_product A[of c2]])
(insert B, auto simp: LANDAU_PROD_def landau_primfuns_iff)
qed

lemmas LANDAU_PROD_iff = LANDAU_PROD_bigo_iff LANDAU_PROD_smallo_iff LANDAU_PROD_bigtheta_iff

lemmas landau_real_prod_simps [simp] =
groupsort_primfun.group_part_def
group_primfuns_def groupsort_primfun.group_sort.simps
groupsort_primfun.group_part_aux.simps pos_primfun_list.simps
nonneg_primfun_list.simps iszero_primfun_list.simps

end
```