Theory HOL-Library.Landau_Symbols

(*
  File:   Landau_Symbols_Definition.thy
  Author: Manuel Eberl <manuel@pruvisto.org>

  Landau symbols for reasoning about the asymptotic growth of functions.
*)
section ‹Definition of Landau symbols›

theory Landau_Symbols
imports
  Complex_Main
begin

lemma eventually_subst':
  "eventually (λx. f x = g x) F ⟹ eventually (λx. P x (f x)) F = eventually (λx. P x (g x)) F"
  by (rule eventually_subst, erule eventually_rev_mp) simp


subsection ‹Definition of Landau symbols›

text ‹
  Our Landau symbols are sign-oblivious, i.e. any function always has the same growth
  as its absolute. This has the advantage of making some cancelling rules for sums nicer, but
  introduces some problems in other places. Nevertheless, we found this definition more convenient
  to work with.
›

definition bigo :: "'a filter ⇒ ('a ⇒ ('b :: real_normed_field)) ⇒ ('a ⇒ 'b) set"
    (‹(1O[_]'(_'))›)
  where "bigo F g = {f. (∃c>0. eventually (λx. norm (f x) ≤ c * norm (g x)) F)}"

definition smallo :: "'a filter ⇒ ('a ⇒ ('b :: real_normed_field)) ⇒ ('a ⇒ 'b) set"
    (‹(1o[_]'(_'))›)
  where "smallo F g = {f. (∀c>0. eventually (λx. norm (f x) ≤ c * norm (g x)) F)}"

definition bigomega :: "'a filter ⇒ ('a ⇒ ('b :: real_normed_field)) ⇒ ('a ⇒ 'b) set"
    (‹(1Ω[_]'(_'))›)
  where "bigomega F g = {f. (∃c>0. eventually (λx. norm (f x) ≥ c * norm (g x)) F)}"

definition smallomega :: "'a filter ⇒ ('a ⇒ ('b :: real_normed_field)) ⇒ ('a ⇒ 'b) set"
    (‹(1ω[_]'(_'))›)
  where "smallomega F g = {f. (∀c>0. eventually (λx. norm (f x) ≥ c * norm (g x)) F)}"

definition bigtheta :: "'a filter ⇒ ('a ⇒ ('b :: real_normed_field)) ⇒ ('a ⇒ 'b) set"
    (‹(1Θ[_]'(_'))›)
  where "bigtheta F g = bigo F g ∩ bigomega F g"

abbreviation bigo_at_top (‹(2O'(_'))›) where
  "O(g) ≡ bigo at_top g"

abbreviation smallo_at_top (‹(2o'(_'))›) where
  "o(g) ≡ smallo at_top g"

abbreviation bigomega_at_top (‹(2Ω'(_'))›) where
  "Ω(g) ≡ bigomega at_top g"

abbreviation smallomega_at_top (‹(2ω'(_'))›) where
  "ω(g) ≡ smallomega at_top g"

abbreviation bigtheta_at_top (‹(2Θ'(_'))›) where
  "Θ(g) ≡ bigtheta at_top g"


text ‹The following is a set of properties that all Landau symbols satisfy.›

named_theorems landau_divide_simps

locale landau_symbol =
  fixes L  :: "'a filter ⇒ ('a ⇒ ('b :: real_normed_field)) ⇒ ('a ⇒ 'b) set"
  and   L'  :: "'c filter ⇒ ('c ⇒ ('b :: real_normed_field)) ⇒ ('c ⇒ 'b) set"
  and   Lr  :: "'a filter ⇒ ('a ⇒ real) ⇒ ('a ⇒ real) set"
  assumes bot': "L bot f = UNIV"
  assumes filter_mono': "F1 ≤ F2 ⟹ L F2 f ⊆ L F1 f"
  assumes in_filtermap_iff:
    "f' ∈ L (filtermap h' F') g' ⟷ (λx. f' (h' x)) ∈ L' F' (λx. g' (h' x))"
  assumes filtercomap:
    "f' ∈ L F'' g' ⟹ (λx. f' (h' x)) ∈ L' (filtercomap h' F'') (λx. g' (h' x))"
  assumes sup: "f ∈ L F1 g ⟹ f ∈ L F2 g ⟹ f ∈ L (sup F1 F2) g"
  assumes in_cong: "eventually (λx. f x = g x) F ⟹ f ∈ L F (h) ⟷ g ∈ L F (h)"
  assumes cong: "eventually (λx. f x = g x) F ⟹ L F (f) = L F (g)"
  assumes cong_bigtheta: "f ∈ Θ[F](g) ⟹ L F (f) = L F (g)"
  assumes in_cong_bigtheta: "f ∈ Θ[F](g) ⟹ f ∈ L F (h) ⟷ g ∈ L F (h)"
  assumes cmult [simp]: "c ≠ 0 ⟹ L F (λx. c * f x) = L F (f)"
  assumes cmult_in_iff [simp]: "c ≠ 0 ⟹ (λx. c * f x) ∈ L F (g) ⟷ f ∈ L F (g)"
  assumes mult_left [simp]: "f ∈ L F (g) ⟹ (λx. h x * f x) ∈ L F (λx. h x * g x)"
  assumes inverse: "eventually (λx. f x ≠ 0) F ⟹ eventually (λx. g x ≠ 0) F ⟹
                        f ∈ L F (g) ⟹ (λx. inverse (g x)) ∈ L F (λx. inverse (f x))"
  assumes subsetI: "f ∈ L F (g) ⟹ L F (f) ⊆ L F (g)"
  assumes plus_subset1: "f ∈ o[F](g) ⟹ L F (g) ⊆ L F (λx. f x + g x)"
  assumes trans: "f ∈ L F (g) ⟹ g ∈ L F (h) ⟹ f ∈ L F (h)"
  assumes compose: "f ∈ L F (g) ⟹ filterlim h' F G ⟹ (λx. f (h' x)) ∈ L' G (λx. g (h' x))"
  assumes norm_iff [simp]: "(λx. norm (f x)) ∈ Lr F (λx. norm (g x)) ⟷ f ∈ L F (g)"
  assumes abs [simp]: "Lr Fr (λx. ¦fr x¦) = Lr Fr fr"
  assumes abs_in_iff [simp]: "(λx. ¦fr x¦) ∈ Lr Fr gr ⟷ fr ∈ Lr Fr gr"
begin

lemma bot [simp]: "f ∈ L bot g" by (simp add: bot')

lemma filter_mono: "F1 ≤ F2 ⟹ f ∈ L F2 g ⟹ f ∈ L F1 g"
  using filter_mono'[of F1 F2] by blast

lemma cong_ex:
  "eventually (λx. f1 x = f2 x) F ⟹ eventually (λx. g1 x = g2 x) F ⟹
     f1 ∈ L F (g1) ⟷ f2 ∈ L F (g2)"
  by (subst cong, assumption, subst in_cong, assumption, rule refl)

lemma cong_ex_bigtheta:
  "f1 ∈ Θ[F](f2) ⟹ g1 ∈ Θ[F](g2) ⟹ f1 ∈ L F (g1) ⟷ f2 ∈ L F (g2)"
  by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl)

lemma bigtheta_trans1:
  "f ∈ L F (g) ⟹ g ∈ Θ[F](h) ⟹ f ∈ L F (h)"
  by (subst cong_bigtheta[symmetric])

lemma bigtheta_trans2:
  "f ∈ Θ[F](g) ⟹ g ∈ L F (h) ⟹ f ∈ L F (h)"
  by (subst in_cong_bigtheta)

lemma cmult' [simp]: "c ≠ 0 ⟹ L F (λx. f x * c) = L F (f)"
  by (subst mult.commute) (rule cmult)

lemma cmult_in_iff' [simp]: "c ≠ 0 ⟹ (λx. f x * c) ∈ L F (g) ⟷ f ∈ L F (g)"
  by (subst mult.commute) (rule cmult_in_iff)

lemma cdiv [simp]: "c ≠ 0 ⟹ L F (λx. f x / c) = L F (f)"
  using cmult'[of "inverse c" F f] by (simp add: field_simps)

lemma cdiv_in_iff' [simp]: "c ≠ 0 ⟹ (λx. f x / c) ∈ L F (g) ⟷ f ∈ L F (g)"
  using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps)

lemma uminus [simp]: "L F (λx. -g x) = L F (g)" using cmult[of "-1"] by simp

lemma uminus_in_iff [simp]: "(λx. -f x) ∈ L F (g) ⟷ f ∈ L F (g)"
  using cmult_in_iff[of "-1"] by simp

lemma const: "c ≠ 0 ⟹ L F (λ_. c) = L F (λ_. 1)"
  by (subst (2) cmult[symmetric]) simp_all

(* Simplifier loops without the NO_MATCH *)
lemma const' [simp]: "NO_MATCH 1 c ⟹ c ≠ 0 ⟹ L F (λ_. c) = L F (λ_. 1)"
  by (rule const)

lemma const_in_iff: "c ≠ 0 ⟹ (λ_. c) ∈ L F (f) ⟷ (λ_. 1) ∈ L F (f)"
  using cmult_in_iff'[of c "λ_. 1"] by simp

lemma const_in_iff' [simp]: "NO_MATCH 1 c ⟹ c ≠ 0 ⟹ (λ_. c) ∈ L F (f) ⟷ (λ_. 1) ∈ L F (f)"
  by (rule const_in_iff)

lemma plus_subset2: "g ∈ o[F](f) ⟹ L F (f) ⊆ L F (λx. f x + g x)"
  by (subst add.commute) (rule plus_subset1)

lemma mult_right [simp]: "f ∈ L F (g) ⟹ (λx. f x * h x) ∈ L F (λx. g x * h x)"
  using mult_left by (simp add: mult.commute)

lemma mult: "f1 ∈ L F (g1) ⟹ f2 ∈ L F (g2) ⟹ (λx. f1 x * f2 x) ∈ L F (λx. g1 x * g2 x)"
  by (rule trans, erule mult_left, erule mult_right)

lemma inverse_cancel:
  assumes "eventually (λx. f x ≠ 0) F"
  assumes "eventually (λx. g x ≠ 0) F"
  shows   "(λx. inverse (f x)) ∈ L F (λx. inverse (g x)) ⟷ g ∈ L F (f)"
proof
  assume "(λx. inverse (f x)) ∈ L F (λx. inverse (g x))"
  from inverse[OF _ _ this] assms show "g ∈ L F (f)" by simp
qed (intro inverse assms)

lemma divide_right:
  assumes "eventually (λx. h x ≠ 0) F"
  assumes "f ∈ L F (g)"
  shows   "(λx. f x / h x) ∈ L F (λx. g x / h x)"
  by (subst (1 2) divide_inverse) (intro mult_right inverse assms)

lemma divide_right_iff:
  assumes "eventually (λx. h x ≠ 0) F"
  shows   "(λx. f x / h x) ∈ L F (λx. g x / h x) ⟷ f ∈ L F (g)"
proof
  assume "(λx. f x / h x) ∈ L F (λx. g x / h x)"
  from mult_right[OF this, of h] assms show "f ∈ L F (g)"
    by (subst (asm) cong_ex[of _ f F _ g]) (auto elim!: eventually_mono)
qed (simp add: divide_right assms)

lemma divide_left:
  assumes "eventually (λx. f x ≠ 0) F"
  assumes "eventually (λx. g x ≠ 0) F"
  assumes "g ∈ L F(f)"
  shows   "(λx. h x / f x) ∈ L F (λx. h x / g x)"
  by (subst (1 2) divide_inverse) (intro mult_left inverse assms)

lemma divide_left_iff:
  assumes "eventually (λx. f x ≠ 0) F"
  assumes "eventually (λx. g x ≠ 0) F"
  assumes "eventually (λx. h x ≠ 0) F"
  shows   "(λx. h x / f x) ∈ L F (λx. h x / g x) ⟷ g ∈ L F (f)"
proof
  assume A: "(λx. h x / f x) ∈ L F (λx. h x / g x)"
  from assms have B: "eventually (λx. h x / f x / h x = inverse (f x)) F"
    by eventually_elim (simp add: divide_inverse)
  from assms have C: "eventually (λx. h x / g x / h x = inverse (g x)) F"
    by eventually_elim (simp add: divide_inverse)
  from divide_right[OF assms(3) A] assms show "g ∈ L F (f)"
    by (subst (asm) cong_ex[OF B C]) (simp add: inverse_cancel)
qed (simp add: divide_left assms)

lemma divide:
  assumes "eventually (λx. g1 x ≠ 0) F"
  assumes "eventually (λx. g2 x ≠ 0) F"
  assumes "f1 ∈ L F (f2)" "g2 ∈ L F (g1)"
  shows   "(λx. f1 x / g1 x) ∈ L F (λx. f2 x / g2 x)"
  by (subst (1 2) divide_inverse) (intro mult inverse assms)

lemma divide_eq1:
  assumes "eventually (λx. h x ≠ 0) F"
  shows   "f ∈ L F (λx. g x / h x) ⟷ (λx. f x * h x) ∈ L F (g)"
proof-
  have "f ∈ L F (λx. g x / h x) ⟷ (λx. f x * h x / h x) ∈ L F (λx. g x / h x)"
    using assms by (intro in_cong) (auto elim: eventually_mono)
  thus ?thesis by (simp only: divide_right_iff assms)
qed

lemma divide_eq2:
  assumes "eventually (λx. h x ≠ 0) F"
  shows   "(λx. f x / h x) ∈ L F (λx. g x) ⟷ f ∈ L F (λx. g x * h x)"
proof-
  have "L F (λx. g x) = L F (λx. g x * h x / h x)"
    using assms by (intro cong) (auto elim: eventually_mono)
  thus ?thesis by (simp only: divide_right_iff assms)
qed

lemma inverse_eq1:
  assumes "eventually (λx. g x ≠ 0) F"
  shows   "f ∈ L F (λx. inverse (g x)) ⟷ (λx. f x * g x) ∈ L F (λ_. 1)"
  using divide_eq1[of g F f "λ_. 1"] by (simp add: divide_inverse assms)

lemma inverse_eq2:
  assumes "eventually (λx. f x ≠ 0) F"
  shows   "(λx. inverse (f x)) ∈ L F (g) ⟷ (λx. 1) ∈ L F (λx. f x * g x)"
  using divide_eq2[of f F "λ_. 1" g] by (simp add: divide_inverse assms mult_ac)

lemma inverse_flip:
  assumes "eventually (λx. g x ≠ 0) F"
  assumes "eventually (λx. h x ≠ 0) F"
  assumes "(λx. inverse (g x)) ∈ L F (h)"
  shows   "(λx. inverse (h x)) ∈ L F (g)"
using assms by (simp add: divide_eq1 divide_eq2 inverse_eq_divide mult.commute)

lemma lift_trans:
  assumes "f ∈ L F (g)"
  assumes "(λx. t x (g x)) ∈ L F (h)"
  assumes "⋀f g. f ∈ L F (g) ⟹ (λx. t x (f x)) ∈ L F (λx. t x (g x))"
  shows   "(λx. t x (f x)) ∈ L F (h)"
  by (rule trans[OF assms(3)[OF assms(1)] assms(2)])

lemma lift_trans':
  assumes "f ∈ L F (λx. t x (g x))"
  assumes "g ∈ L F (h)"
  assumes "⋀g h. g ∈ L F (h) ⟹ (λx. t x (g x)) ∈ L F (λx. t x (h x))"
  shows   "f ∈ L F (λx. t x (h x))"
  by (rule trans[OF assms(1) assms(3)[OF assms(2)]])

lemma lift_trans_bigtheta:
  assumes "f ∈ L F (g)"
  assumes "(λx. t x (g x)) ∈ Θ[F](h)"
  assumes "⋀f g. f ∈ L F (g) ⟹ (λx. t x (f x)) ∈ L F (λx. t x (g x))"
  shows   "(λx. t x (f x)) ∈ L F (h)"
  using cong_bigtheta[OF assms(2)] assms(3)[OF assms(1)] by simp

lemma lift_trans_bigtheta':
  assumes "f ∈ L F (λx. t x (g x))"
  assumes "g ∈ Θ[F](h)"
  assumes "⋀g h. g ∈ Θ[F](h) ⟹ (λx. t x (g x)) ∈ Θ[F](λx. t x (h x))"
  shows   "f ∈ L F (λx. t x (h x))"
  using cong_bigtheta[OF assms(3)[OF assms(2)]] assms(1)  by simp

lemma (in landau_symbol) mult_in_1:
  assumes "f ∈ L F (λ_. 1)" "g ∈ L F (λ_. 1)"
  shows   "(λx. f x * g x) ∈ L F (λ_. 1)"
  using mult[OF assms] by simp

lemma (in landau_symbol) of_real_cancel:
  "(λx. of_real (f x)) ∈ L F (λx. of_real (g x)) ⟹ f ∈ Lr F g"
  by (subst (asm) norm_iff [symmetric], subst (asm) (1 2) norm_of_real) simp_all

lemma (in landau_symbol) of_real_iff:
  "(λx. of_real (f x)) ∈ L F (λx. of_real (g x)) ⟷ f ∈ Lr F g"
  by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all

lemmas [landau_divide_simps] =
  inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2

end


text ‹
  The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with
  $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.
  The following locale captures this fact.
›

locale landau_pair =
  fixes L l :: "'a filter ⇒ ('a ⇒ ('b :: real_normed_field)) ⇒ ('a ⇒ 'b) set"
  fixes L' l' :: "'c filter ⇒ ('c ⇒ ('b :: real_normed_field)) ⇒ ('c ⇒ 'b) set"
  fixes Lr lr :: "'a filter ⇒ ('a ⇒ real) ⇒ ('a ⇒ real) set"
  and   R :: "real ⇒ real ⇒ bool"
  assumes L_def: "L F g = {f. ∃c>0. eventually (λx. R (norm (f x)) (c * norm (g x))) F}"
  and     l_def: "l F g = {f. ∀c>0. eventually (λx. R (norm (f x)) (c * norm (g x))) F}"
  and     L'_def: "L' F' g' = {f. ∃c>0. eventually (λx. R (norm (f x)) (c * norm (g' x))) F'}"
  and     l'_def: "l' F' g' = {f. ∀c>0. eventually (λx. R (norm (f x)) (c * norm (g' x))) F'}"
  and     Lr_def: "Lr F'' g'' = {f. ∃c>0. eventually (λx. R (norm (f x)) (c * norm (g'' x))) F''}"
  and     lr_def: "lr F'' g'' = {f. ∀c>0. eventually (λx. R (norm (f x)) (c * norm (g'' x))) F''}"
  and     R:     "R = (≤) ∨ R = (≥)"

interpretation landau_o:
    landau_pair bigo smallo bigo smallo bigo smallo "(≤)"
  by unfold_locales (auto simp: bigo_def smallo_def intro!: ext)

interpretation landau_omega:
    landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(≥)"
  by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext)


context landau_pair
begin

lemmas R_E = disjE [OF R, case_names le ge]

lemma bigI:
  "c > 0 ⟹ eventually (λx. R (norm (f x)) (c * norm (g x))) F ⟹ f ∈ L F (g)"
  unfolding L_def by blast

lemma bigE:
  assumes "f ∈ L F (g)"
  obtains c where "c > 0" "eventually (λx. R (norm (f x)) (c * (norm (g x)))) F"
  using assms unfolding L_def by blast

lemma smallI:
  "(⋀c. c > 0 ⟹ eventually (λx. R (norm (f x)) (c * (norm (g x)))) F) ⟹ f ∈ l F (g)"
  unfolding l_def by blast

lemma smallD:
  "f ∈ l F (g) ⟹ c > 0 ⟹ eventually (λx. R (norm (f x)) (c * (norm (g x)))) F"
  unfolding l_def by blast

lemma bigE_nonneg_real:
  assumes "f ∈ Lr F (g)" "eventually (λx. f x ≥ 0) F"
  obtains c where "c > 0" "eventually (λx. R (f x) (c * ¦g x¦)) F"
proof-
  from assms(1) obtain c where c: "c > 0" "eventually (λx. R (norm (f x)) (c * norm (g x))) F"
    by (auto simp: Lr_def)
  from c(2) assms(2) have "eventually (λx. R (f x) (c * ¦g x¦)) F"
    by eventually_elim simp
  from c(1) and this show ?thesis by (rule that)
qed

lemma smallD_nonneg_real:
  assumes "f ∈ lr F (g)" "eventually (λx. f x ≥ 0) F" "c > 0"
  shows   "eventually (λx. R (f x) (c * ¦g x¦)) F"
  using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2)

lemma small_imp_big: "f ∈ l F (g) ⟹ f ∈ L F (g)"
  by (rule bigI[OF _ smallD, of 1]) simp_all

lemma small_subset_big: "l F (g) ⊆ L F (g)"
  using small_imp_big by blast

lemma R_refl [simp]: "R x x" using R by auto

lemma R_linear: "¬R x y ⟹ R y x"
  using R by auto

lemma R_trans [trans]: "R a b ⟹ R b c ⟹ R a c"
  using R by auto

lemma R_mult_left_mono: "R a b ⟹ c ≥ 0 ⟹ R (c*a) (c*b)"
  using R by (auto simp: mult_left_mono)

lemma R_mult_right_mono: "R a b ⟹ c ≥ 0 ⟹ R (a*c) (b*c)"
  using R by (auto simp: mult_right_mono)

lemma big_trans:
  assumes "f ∈ L F (g)" "g ∈ L F (h)"
  shows   "f ∈ L F (h)"
proof-
  from assms obtain c d where *: "0 < c" "0 < d"
    and **: "∀⇩F x in F. R (norm (f x)) (c * norm (g x))"
            "∀⇩F x in F. R (norm (g x)) (d * norm (h x))"
    by (elim bigE)
  from ** have "eventually (λx. R (norm (f x)) (c * d * (norm (h x)))) F"
  proof eventually_elim
    fix x assume "R (norm (f x)) (c * (norm (g x)))"
    also assume "R (norm (g x)) (d * (norm (h x)))"
    with ‹0 < c› have "R (c * (norm (g x))) (c * (d * (norm (h x))))"
      by (intro R_mult_left_mono) simp_all
    finally show "R (norm (f x)) (c * d * (norm (h x)))"
      by (simp add: algebra_simps)
  qed
  with * show ?thesis by (intro bigI[of "c*d"]) simp_all
qed

lemma big_small_trans:
  assumes "f ∈ L F (g)" "g ∈ l F (h)"
  shows   "f ∈ l F (h)"
proof (rule smallI)
  fix c :: real assume c: "c > 0"
  from assms(1) obtain d where d: "d > 0" and *: "∀⇩F x in F. R (norm (f x)) (d * norm (g x))"
    by (elim bigE)
  from assms(2) c d have "eventually (λx. R (norm (g x)) (c * inverse d * norm (h x))) F"
    by (intro smallD) simp_all
  with * show "eventually (λx. R (norm (f x)) (c * (norm (h x)))) F"
  proof eventually_elim
    case (elim x)
    show ?case
      by (use elim(1) in ‹rule R_trans›) (use elim(2) R d in ‹auto simp: field_simps›)
  qed
qed

lemma small_big_trans:
  assumes "f ∈ l F (g)" "g ∈ L F (h)"
  shows   "f ∈ l F (h)"
proof (rule smallI)
  fix c :: real assume c: "c > 0"
  from assms(2) obtain d where d: "d > 0" and *: "∀⇩F x in F. R (norm (g x)) (d * norm (h x))"
    by (elim bigE)
  from assms(1) c d have "eventually (λx. R (norm (f x)) (c * inverse d * norm (g x))) F"
    by (intro smallD) simp_all
  with * show "eventually (λx. R (norm (f x)) (c * norm (h x))) F"
    by eventually_elim (rotate_tac 2, erule R_trans, insert R c d, auto simp: field_simps)
qed

lemma small_trans:
  "f ∈ l F (g) ⟹ g ∈ l F (h) ⟹ f ∈ l F (h)"
  by (rule big_small_trans[OF small_imp_big])

lemma small_big_trans':
  "f ∈ l F (g) ⟹ g ∈ L F (h) ⟹ f ∈ L F (h)"
  by (rule small_imp_big[OF small_big_trans])

lemma big_small_trans':
  "f ∈ L F (g) ⟹ g ∈ l F (h) ⟹ f ∈ L F (h)"
  by (rule small_imp_big[OF big_small_trans])

lemma big_subsetI [intro]: "f ∈ L F (g) ⟹ L F (f) ⊆ L F (g)"
  by (intro subsetI) (drule (1) big_trans)

lemma small_subsetI [intro]: "f ∈ L F (g) ⟹ l F (f) ⊆ l F (g)"
  by (intro subsetI) (drule (1) small_big_trans)

lemma big_refl [simp]: "f ∈ L F (f)"
  by (rule bigI[of 1]) simp_all

lemma small_refl_iff: "f ∈ l F (f) ⟷ eventually (λx. f x = 0) F"
proof (rule iffI[OF _ smallI])
  assume f: "f ∈ l F f"
  have "(1/2::real) > 0" "(2::real) > 0" by simp_all
  from smallD[OF f this(1)] smallD[OF f this(2)]
    show "eventually (λx. f x = 0) F" by eventually_elim (insert R, auto)
next
  fix c :: real assume "c > 0" "eventually (λx. f x = 0) F"
  from this(2) show "eventually (λx. R (norm (f x)) (c * norm (f x))) F"
    by eventually_elim simp_all
qed

lemma big_small_asymmetric: "f ∈ L F (g) ⟹ g ∈ l F (f) ⟹ eventually (λx. f x = 0) F"
  by (drule (1) big_small_trans) (simp add: small_refl_iff)

lemma small_big_asymmetric: "f ∈ l F (g) ⟹ g ∈ L F (f) ⟹ eventually (λx. f x = 0) F"
  by (drule (1) small_big_trans) (simp add: small_refl_iff)

lemma small_asymmetric: "f ∈ l F (g) ⟹ g ∈ l F (f) ⟹ eventually (λx. f x = 0) F"
  by (drule (1) small_trans) (simp add: small_refl_iff)


lemma plus_aux:
  assumes "f ∈ o[F](g)"
  shows "g ∈ L F (λx. f x + g x)"
proof (rule R_E)
  assume R: "R = (≤)"
  have A: "1/2 > (0::real)" by simp
  have B: "1/2 * (norm (g x)) ≤ norm (f x + g x)"
    if "norm (f x) ≤ 1/2 * norm (g x)" for x
  proof -
    from that have "1/2 * (norm (g x)) ≤ (norm (g x)) - (norm (f x))"
      by simp
    also have "norm (g x) - norm (f x) ≤ norm (f x + g x)"
      by (subst add.commute) (rule norm_diff_ineq)
    finally show ?thesis by simp
  qed
  show "g ∈ L F (λx. f x + g x)"
    apply (rule bigI[of "2"])
     apply simp
    apply (use landau_o.smallD[OF assms A] in eventually_elim)
    apply (use B in ‹simp add: R algebra_simps›)
    done
next
  assume R: "R = (λx y. x ≥ y)"
  show "g ∈ L F (λx. f x + g x)"
  proof (rule bigI[of "1/2"])
    show "eventually (λx. R (norm (g x)) (1/2 * norm (f x + g x))) F"
      using landau_o.smallD[OF assms zero_less_one]
    proof eventually_elim
      case (elim x)
      have "norm (f x + g x) ≤ norm (f x) + norm (g x)"
        by (rule norm_triangle_ineq)
      also note elim
      finally show ?case by (simp add: R)
    qed
  qed simp_all
qed

end

lemma summable_comparison_test_bigo:
  fixes f :: "nat ⇒ real"
  assumes "summable (λn. norm (g n))" "f ∈ O(g)"
  shows   "summable f"
proof -
  from ‹f ∈ O(g)› obtain C where C: "eventually (λx. norm (f x) ≤ C * norm (g x)) at_top"
    by (auto elim: landau_o.bigE)
  thus ?thesis
    by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
qed

lemma bigomega_iff_bigo: "g ∈ Ω[F](f) ⟷ f ∈ O[F](g)"
proof
  assume "f ∈ O[F](g)"
  then obtain c where "0 < c" "∀⇩F x in F. norm (f x) ≤ c * norm (g x)"
    by (rule landau_o.bigE)
  then show "g ∈ Ω[F](f)"
    by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps)
next
  assume "g ∈ Ω[F](f)"
  then obtain c where "0 < c" "∀⇩F x in F. c * norm (f x) ≤ norm (g x)"
    by (rule landau_omega.bigE)
  then show "f ∈ O[F](g)"
    by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps)
qed

lemma smallomega_iff_smallo: "g ∈ ω[F](f) ⟷ f ∈ o[F](g)"
proof
  assume "f ∈ o[F](g)"
  from landau_o.smallD[OF this, of "inverse c" for c]
    show "g ∈ ω[F](f)" by (intro landau_omega.smallI) (simp_all add: field_simps)
next
  assume "g ∈ ω[F](f)"
  from landau_omega.smallD[OF this, of "inverse c" for c]
    show "f ∈ o[F](g)" by (intro landau_o.smallI) (simp_all add: field_simps)
qed


context landau_pair
begin

lemma big_mono:
  "eventually (λx. R (norm (f x)) (norm (g x))) F ⟹ f ∈ L F (g)"
  by (rule bigI[OF zero_less_one]) simp

lemma big_mult:
  assumes "f1 ∈ L F (g1)" "f2 ∈ L F (g2)"
  shows   "(λx. f1 x * f2 x) ∈ L F (λx. g1 x * g2 x)"
proof-
  from assms obtain c1 c2 where *: "c1 > 0" "c2 > 0"
    and **: "∀⇩F x in F. R (norm (f1 x)) (c1 * norm (g1 x))"
            "∀⇩F x in F. R (norm (f2 x)) (c2 * norm (g2 x))"
    by (elim bigE)
  from * have "c1 * c2 > 0" by simp
  moreover have "eventually (λx. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F"
    using **
  proof eventually_elim
    case (elim x)
    show ?case
    proof (cases rule: R_E)
      case le
      have "norm (f1 x) * norm (f2 x) ≤ (c1 * norm (g1 x)) * (c2 * norm (g2 x))"
        using elim le * by (intro mult_mono mult_nonneg_nonneg) auto
      with le show ?thesis by (simp add: le norm_mult mult_ac)
    next
      case ge
      have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) ≤ norm (f1 x) * norm (f2 x)"
        using elim ge * by (intro mult_mono mult_nonneg_nonneg) auto
      with ge show ?thesis by (simp_all add: norm_mult mult_ac)
    qed
  qed
  ultimately show ?thesis by (rule bigI)
qed

lemma small_big_mult:
  assumes "f1 ∈ l F (g1)" "f2 ∈ L F (g2)"
  shows   "(λx. f1 x * f2 x) ∈ l F (λx. g1 x * g2 x)"
proof (rule smallI)
  fix c1 :: real assume c1: "c1 > 0"
  from assms(2) obtain c2 where c2: "c2 > 0"
    and *: "∀⇩F x in F. R (norm (f2 x)) (c2 * norm (g2 x))" by (elim bigE)
  from assms(1) c1 c2 have "eventually (λx. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F"
    by (auto intro!: smallD)
  with * show "eventually (λx. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F"
  proof eventually_elim
    case (elim x)
    show ?case
    proof (cases rule: R_E)
      case le
      have "norm (f1 x) * norm (f2 x) ≤ (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
        using elim le c1 c2 by (intro mult_mono mult_nonneg_nonneg) auto
      with le c2 show ?thesis by (simp add: le norm_mult field_simps)
    next
      case ge
      have "norm (f1 x) * norm (f2 x) ≥ (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
        using elim ge c1 c2 by (intro mult_mono mult_nonneg_nonneg) auto
      with ge c2 show ?thesis by (simp add: ge norm_mult field_simps)
    qed
  qed
qed

lemma big_small_mult:
  "f1 ∈ L F (g1) ⟹ f2 ∈ l F (g2) ⟹ (λx. f1 x * f2 x) ∈ l F (λx. g1 x * g2 x)"
  by (subst (1 2) mult.commute) (rule small_big_mult)

lemma small_mult: "f1 ∈ l F (g1) ⟹ f2 ∈ l F (g2) ⟹ (λx. f1 x * f2 x) ∈ l F (λx. g1 x * g2 x)"
  by (rule small_big_mult, assumption, rule small_imp_big)

lemmas mult = big_mult small_big_mult big_small_mult small_mult

lemma big_power:
  assumes "f ∈ L F (g)"
  shows   "(λx. f x ^ m) ∈ L F (λx. g x ^ m)"
  using assms by (induction m) (auto intro: mult)

lemma (in landau_pair) small_power:
  assumes "f ∈ l F (g)" "m > 0"
  shows   "(λx. f x ^ m) ∈ l F (λx. g x ^ m)"
proof -
  have "(λx. f x * f x ^ (m - 1)) ∈ l F (λx. g x * g x ^ (m - 1))"
    by (intro small_big_mult assms big_power[OF small_imp_big])
  thus ?thesis
    using assms by (cases m) (simp_all add: mult_ac)
qed

lemma big_power_increasing:
  assumes "(λ_. 1) ∈ L F f" "m ≤ n"
  shows   "(λx. f x ^ m) ∈ L F (λx. f x ^ n)"
proof -
  have "(λx. f x ^ m * 1 ^ (n - m)) ∈ L F (λx. f x ^ m * f x ^ (n - m))"
    using assms by (intro mult big_power) auto
  also have "(λx. f x ^ m * f x ^ (n - m)) = (λx. f x ^ (m + (n - m)))"
    by (subst power_add [symmetric]) (rule refl)
  also have "m + (n - m) = n"
    using assms by simp
  finally show ?thesis by simp
qed

lemma small_power_increasing:
  assumes "(λ_. 1) ∈ l F f" "m < n"
  shows   "(λx. f x ^ m) ∈ l F (λx. f x ^ n)"
proof -
  note [trans] = small_big_trans
  have "(λx. f x ^ m * 1) ∈ l F (λx. f x ^ m * f x)"
    using assms by (intro big_small_mult) auto
  also have "(λx. f x ^ m * f x) = (λx. f x ^ Suc m)"
    by (simp add: mult_ac)
  also have "… ∈ L F (λx. f x ^ n)"
    using assms by (intro big_power_increasing[OF small_imp_big]) auto
  finally show ?thesis by simp
qed
  
sublocale big: landau_symbol L L' Lr
proof
  have L: "L = bigo ∨ L = bigomega"
    by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
  have A: "(λx. c * f x) ∈ L F f" if "c ≠ 0" for c :: 'b and F and f :: "'a ⇒ 'b"
    using that by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
  show "L F (λx. c * f x) = L F f" if "c ≠ 0" for c :: 'b and F and f :: "'a ⇒ 'b"
    using ‹c ≠ 0› and A[of c f] and A[of "inverse c" "λx. c * f x"]
    by (intro equalityI big_subsetI) (simp_all add: field_simps)
  show "((λx. c * f x) ∈ L F g) = (f ∈ L F g)" if "c ≠ 0"
    for c :: 'b and F and f g :: "'a ⇒ 'b"
  proof -
    from ‹c ≠ 0› and A[of c f] and A[of "inverse c" "λx. c * f x"]
    have "(λx. c * f x) ∈ L F f" "f ∈ L F (λx. c * f x)"
      by (simp_all add: field_simps)
    then show ?thesis by (intro iffI) (erule (1) big_trans)+
  qed
  show "(λx. inverse (g x)) ∈ L F (λx. inverse (f x))"
    if *: "f ∈ L F (g)" and **: "eventually (λx. f x ≠ 0) F" "eventually (λx. g x ≠ 0) F"
    for f g :: "'a ⇒ 'b" and F
  proof -
    from * obtain c where c: "c > 0" and ***: "∀⇩F x in F. R (norm (f x)) (c * norm (g x))"
      by (elim bigE)
    from ** *** have "eventually (λx. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
      by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide c)
    with c show ?thesis by (rule bigI)
  qed
  show "L F g ⊆ L F (λx. f x + g x)" if "f ∈ o[F](g)" for f g :: "'a ⇒ 'b" and F
    using plus_aux that by (blast intro!: big_subsetI)
  show "L F (f) = L F (g)" if "eventually (λx. f x = g x) F" for f g :: "'a ⇒ 'b" and F
    unfolding L_def by (subst eventually_subst'[OF that]) (rule refl)
  show "f ∈ L F (h) ⟷ g ∈ L F (h)" if "eventually (λx. f x = g x) F"
    for f g h :: "'a ⇒ 'b" and F
    unfolding L_def mem_Collect_eq
    by (subst (1) eventually_subst'[OF that]) (rule refl)
  show "L F f ⊆ L F g" if "f ∈ L F g" for f g :: "'a ⇒ 'b" and F
    using that by (rule big_subsetI)
  show "L F (f) = L F (g)" if "f ∈ Θ[F](g)" for f g :: "'a ⇒ 'b" and F
    using L that unfolding bigtheta_def
    by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)
  show "f ∈ L F (h) ⟷ g ∈ L F (h)" if "f ∈ Θ[F](g)" for f g h :: "'a ⇒ 'b" and F
    by (rule disjE[OF L])
      (use that in ‹auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans›)
  show "(λx. h x * f x) ∈ L F (λx. h x * g x)" if "f ∈ L F g" for f g h :: "'a ⇒ 'b" and F
    using that by (intro big_mult) simp
  show "f ∈ L F (h)" if "f ∈ L F g" "g ∈ L F h" for f g h :: "'a ⇒ 'b" and F
    using that by (rule big_trans)
  show "(λx. f (h x)) ∈ L' G (λx. g (h x))"
    if "f ∈ L F g" and "filterlim h F G"
    for f g :: "'a ⇒ 'b" and h :: "'c ⇒ 'a" and F G
    using that by (auto simp: L_def L'_def filterlim_iff)
  show "f ∈ L (sup F G) g" if "f ∈ L F g" "f ∈ L G g"
    for f g :: "'a ⇒ 'b" and F G :: "'a filter"
  proof -
    from that [THEN bigE] obtain c1 c2
      where *: "c1 > 0" "c2 > 0"
        and **: "∀⇩F x in F. R (norm (f x)) (c1 * norm (g x))"
                "∀⇩F x in G. R (norm (f x)) (c2 * norm (g x))" .
    define c where "c = (if R c1 c2 then c2 else c1)"
    from * have c: "R c1 c" "R c2 c" "c > 0"
      by (auto simp: c_def dest: R_linear)
    with ** have "eventually (λx. R (norm (f x)) (c * norm (g x))) F"
                 "eventually (λx. R (norm (f x)) (c * norm (g x))) G"
      by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+
    with c show "f ∈ L (sup F G) g"
      by (auto simp: L_def eventually_sup)
  qed
  show "((λx. f (h x)) ∈ L' (filtercomap h F) (λx. g (h x)))" if "(f ∈ L F g)"
    for f g :: "'a ⇒ 'b" and h :: "'c ⇒ 'a" and F G :: "'a filter"
    using that unfolding L_def L'_def by auto
qed (auto simp: L_def Lr_def eventually_filtermap L'_def
          intro: filter_leD exI[of _ "1::real"])

sublocale small: landau_symbol l l' lr
proof
  have A: "(λx. c * f x) ∈ L F f" if "c ≠ 0" for c :: 'b and f :: "'a ⇒ 'b" and F
    using that by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
  show "l F (λx. c * f x) = l F f" if "c ≠ 0" for c :: 'b and f :: "'a ⇒ 'b" and F
    using that and A[of c f] and A[of "inverse c" "λx. c * f x"]
    by (intro equalityI small_subsetI) (simp_all add: field_simps)
  show "((λx. c * f x) ∈ l F g) = (f ∈ l F g)" if "c ≠ 0" for c :: 'b and f g :: "'a ⇒ 'b" and F
  proof -
    from that and A[of c f] and A[of "inverse c" "λx. c * f x"]
    have "(λx. c * f x) ∈ L F f" "f ∈ L F (λx. c * f x)"
      by (simp_all add: field_simps)
    then show ?thesis
      by (intro iffI) (erule (1) big_small_trans)+
  qed
  show "l F g ⊆ l F (λx. f x + g x)" if "f ∈ o[F](g)" for f g :: "'a ⇒ 'b" and F
    using plus_aux that by (blast intro!: small_subsetI)
  show "(λx. inverse (g x)) ∈ l F (λx. inverse (f x))"
    if A: "f ∈ l F (g)" and B: "eventually (λx. f x ≠ 0) F" "eventually (λx. g x ≠ 0) F"
    for f g :: "'a ⇒ 'b" and F
  proof (rule smallI)
    fix c :: real assume c: "c > 0"
    from B smallD[OF A c]
    show "eventually (λx. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
      by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)
  qed
  show "l F (f) = l F (g)" if "eventually (λx. f x = g x) F" for f g :: "'a ⇒ 'b" and F
    unfolding l_def by (subst eventually_subst'[OF that]) (rule refl)
  show "f ∈ l F (h) ⟷ g ∈ l F (h)" if "eventually (λx. f x = g x) F" for f g h :: "'a ⇒ 'b" and F
    unfolding l_def mem_Collect_eq by (subst (1) eventually_subst'[OF that]) (rule refl)
  show "l F f ⊆ l F g" if "f ∈ l F g" for f g :: "'a ⇒ 'b" and F
    using that by (intro small_subsetI small_imp_big)
  show "l F (f) = l F (g)" if "f ∈ Θ[F](g)" for f g :: "'a ⇒ 'b" and F
  proof -
    have L: "L = bigo ∨ L = bigomega"
      by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
    with that show ?thesis unfolding bigtheta_def
      by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)
  qed
  show "f ∈ l F (h) ⟷ g ∈ l F (h)" if "f ∈ Θ[F](g)" for f g h :: "'a ⇒ 'b" and F
  proof -
    have l: "l = smallo ∨ l = smallomega"
      by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)
    show ?thesis
      by (rule disjE[OF l])
        (use that in ‹auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo
          intro: landau_o.big_small_trans landau_o.small_big_trans›)
  qed
  show "(λx. h x * f x) ∈ l F (λx. h x * g x)" if "f ∈ l F g" for f g h :: "'a ⇒ 'b" and F
    using that by (intro big_small_mult) simp
  show "f ∈ l F (h)" if "f ∈ l F g" "g ∈ l F h" for f g h :: "'a ⇒ 'b" and F
    using that by (rule small_trans)
  show "(λx. f (h x)) ∈ l' G (λx. g (h x))" if "f ∈ l F g" and "filterlim h F G"
    for f g :: "'a ⇒ 'b" and h :: "'c ⇒ 'a" and F G
    using that by (auto simp: l_def l'_def filterlim_iff)
  show "((λx. f (h x)) ∈ l' (filtercomap h F) (λx. g (h x)))" if "f ∈ l F g"
    for f g :: "'a ⇒ 'b" and h :: "'c ⇒ 'a" and F G :: "'a filter"
    using that unfolding l_def l'_def by auto
qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)


text ‹These rules allow chaining of Landau symbol propositions in Isar with "also".›

lemma big_mult_1:    "f ∈ L F (g) ⟹ (λ_. 1) ∈ L F (h) ⟹ f ∈ L F (λx. g x * h x)"
  and big_mult_1':   "(λ_. 1) ∈ L F (g) ⟹ f ∈ L F (h) ⟹ f ∈ L F (λx. g x * h x)"
  and small_mult_1:  "f ∈ l F (g) ⟹ (λ_. 1) ∈ L F (h) ⟹ f ∈ l F (λx. g x * h x)"
  and small_mult_1': "(λ_. 1) ∈ L F (g) ⟹ f ∈ l F (h) ⟹ f ∈ l F (λx. g x * h x)"
  and small_mult_1'':  "f ∈ L F (g) ⟹ (λ_. 1) ∈ l F (h) ⟹ f ∈ l F (λx. g x * h x)"
  and small_mult_1''': "(λ_. 1) ∈ l F (g) ⟹ f ∈ L F (h) ⟹ f ∈ l F (λx. g x * h x)"
  by (drule (1) big.mult big_small_mult small_big_mult, simp)+

lemma big_1_mult:    "f ∈ L F (g) ⟹ h ∈ L F (λ_. 1) ⟹ (λx. f x * h x) ∈ L F (g)"
  and big_1_mult':   "h ∈ L F (λ_. 1) ⟹ f ∈ L F (g) ⟹ (λx. f x * h x) ∈ L F (g)"
  and small_1_mult:  "f ∈ l F (g) ⟹ h ∈ L F (λ_. 1) ⟹ (λx. f x * h x) ∈ l F (g)"
  and small_1_mult': "h ∈ L F (λ_. 1) ⟹ f ∈ l F (g) ⟹ (λx. f x * h x) ∈ l F (g)"
  and small_1_mult'':  "f ∈ L F (g) ⟹ h ∈ l F (λ_. 1) ⟹ (λx. f x * h x) ∈ l F (g)"
  and small_1_mult''': "h ∈ l F (λ_. 1) ⟹ f ∈ L F (g) ⟹ (λx. f x * h x) ∈ l F (g)"
  by (drule (1) big.mult big_small_mult small_big_mult, simp)+

lemmas mult_1_trans =
  big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''
  big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''

lemma big_equal_iff_bigtheta: "L F (f) = L F (g) ⟷ f ∈ Θ[F](g)"
proof
  have L: "L = bigo ∨ L = bigomega"
    by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)
  fix f g :: "'a ⇒ 'b" assume "L F (f) = L F (g)"
  with big_refl[of f F] big_refl[of g F] have "f ∈ L F (g)" "g ∈ L F (f)" by simp_all
  thus "f ∈ Θ[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
qed (rule big.cong_bigtheta)

lemma big_prod:
  assumes "⋀x. x ∈ A ⟹ f x ∈ L F (g x)"
  shows   "(λy. ∏x∈A. f x y) ∈ L F (λy. ∏x∈A. g x y)"
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)

lemma big_prod_in_1:
  assumes "⋀x. x ∈ A ⟹ f x ∈ L F (λ_. 1)"
  shows   "(λy. ∏x∈A. f x y) ∈ L F (λ_. 1)"
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)

end


context landau_symbol
begin

lemma plus_absorb1:
  assumes "f ∈ o[F](g)"
  shows   "L F (λx. f x + g x) = L F (g)"
proof (intro equalityI)
  from plus_subset1 and assms show "L F g ⊆ L F (λx. f x + g x)" .
  from landau_o.small.plus_subset1[OF assms] and assms have "(λx. -f x) ∈ o[F](λx. f x + g x)"
    by (auto simp: landau_o.small.uminus_in_iff)
  from plus_subset1[OF this] show "L F (λx. f x + g x) ⊆ L F (g)" by simp
qed

lemma plus_absorb2: "g ∈ o[F](f) ⟹ L F (λx. f x + g x) = L F (f)"
  using plus_absorb1[of g F f] by (simp add: add.commute)

lemma diff_absorb1: "f ∈ o[F](g) ⟹ L F (λx. f x - g x) = L F (g)"
  by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)

lemma diff_absorb2: "g ∈ o[F](f) ⟹ L F (λx. f x - g x) = L F (f)"
  by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)

lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2

end


lemma bigthetaI [intro]: "f ∈ O[F](g) ⟹ f ∈ Ω[F](g) ⟹ f ∈ Θ[F](g)"
  unfolding bigtheta_def bigomega_def by blast

lemma bigthetaD1 [dest]: "f ∈ Θ[F](g) ⟹ f ∈ O[F](g)"
  and bigthetaD2 [dest]: "f ∈ Θ[F](g) ⟹ f ∈ Ω[F](g)"
  unfolding bigtheta_def bigo_def bigomega_def by blast+

lemma bigtheta_refl [simp]: "f ∈ Θ[F](f)"
  unfolding bigtheta_def by simp

lemma bigtheta_sym: "f ∈ Θ[F](g) ⟷ g ∈ Θ[F](f)"
  unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)

lemmas landau_flip =
  bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]
  bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym


interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta
proof
  fix f g :: "'a ⇒ 'b" and F
  assume "f ∈ o[F](g)"
  hence "O[F](g) ⊆ O[F](λx. f x + g x)" "Ω[F](g) ⊆ Ω[F](λx. f x + g x)"
    by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+
  thus "Θ[F](g) ⊆ Θ[F](λx. f x + g x)" unfolding bigtheta_def by blast
next
  fix f g :: "'a ⇒ 'b" and F
  assume "f ∈ Θ[F](g)"
  thus A: "Θ[F](f) = Θ[F](g)"
    apply (subst (1 2) bigtheta_def)
    apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+
    apply (rule refl)
    done
  thus "Θ[F](f) ⊆ Θ[F](g)" by simp
  fix h :: "'a ⇒ 'b"
  show "f ∈ Θ[F](h) ⟷ g ∈ Θ[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)
next
  fix f g h :: "'a ⇒ 'b" and F
  assume "f ∈ Θ[F](g)" "g ∈ Θ[F](h)"
  thus "f ∈ Θ[F](h)" unfolding bigtheta_def
    by (blast intro: landau_o.big.trans landau_omega.big.trans)
next
  fix f :: "'a ⇒ 'b" and F1 F2 :: "'a filter"
  assume "F1 ≤ F2"
  thus "Θ[F2](f) ⊆ Θ[F1](f)"
    by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)
qed (auto simp: bigtheta_def landau_o.big.norm_iff
                landau_o.big.cmult landau_omega.big.cmult
                landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff
                landau_o.big.in_cong landau_omega.big.in_cong
                landau_o.big.mult landau_omega.big.mult
                landau_o.big.inverse landau_omega.big.inverse
                landau_o.big.compose landau_omega.big.compose
                landau_o.big.bot' landau_omega.big.bot'
                landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff
                landau_o.big.sup landau_omega.big.sup
                landau_o.big.filtercomap landau_omega.big.filtercomap
          dest: landau_o.big.cong landau_omega.big.cong)

lemmas landau_symbols =
  landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms
  landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms
  landau_theta.landau_symbol_axioms

lemma bigoI [intro]:
  assumes "eventually (λx. (norm (f x)) ≤ c * (norm (g x))) F"
  shows   "f ∈ O[F](g)"
proof (rule landau_o.bigI)
  show "max 1 c > 0" by simp
  have "c * (norm (g x)) ≤ max 1 c * (norm (g x))" for x
    by (simp add: mult_right_mono)
  with assms show "eventually (λx. (norm (f x)) ≤ max 1 c * (norm (g x))) F"
    by (auto elim!: eventually_mono dest: order.trans)
qed

lemma smallomegaD [dest]:
  assumes "f ∈ ω[F](g)"
  shows   "eventually (λx. (norm (f x)) ≥ c * (norm (g x))) F"
proof (cases "c > 0")
  case False
  show ?thesis
    by (intro always_eventually allI, rule order.trans[of _ 0])
       (insert False, auto intro!: mult_nonpos_nonneg)
qed (blast dest: landau_omega.smallD[OF assms, of c])


lemma bigthetaI':
  assumes "c1 > 0" "c2 > 0"
  assumes "eventually (λx. c1 * (norm (g x)) ≤ (norm (f x)) ∧ (norm (f x)) ≤ c2 * (norm (g x))) F"
  shows   "f ∈ Θ[F](g)"
apply (rule bigthetaI)
apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)
apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)
done

lemma bigthetaI_cong: "eventually (λx. f x = g x) F ⟹ f ∈ Θ[F](g)"
  by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)

lemma (in landau_symbol) ev_eq_trans1:
  "f ∈ L F (λx. g x (h x)) ⟹ eventually (λx. h x = h' x) F ⟹ f ∈ L F (λx. g x (h' x))"
  by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)

lemma (in landau_symbol) ev_eq_trans2:
  "eventually (λx. f x = f' x) F ⟹ (λx. g x (f' x)) ∈ L F (h) ⟹ (λx. g x (f x)) ∈ L F (h)"
  by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)

declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]
declare landau_o.bigE landau_omega.bigE [elim]
declare landau_o.smallD

lemma (in landau_symbol) bigtheta_trans1':
  "f ∈ L F (g) ⟹ h ∈ Θ[F](g) ⟹ f ∈ L F (h)"
  by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)

lemma (in landau_symbol) bigtheta_trans2':
  "g ∈ Θ[F](f) ⟹ g ∈ L F (h) ⟹ f ∈ L F (h)"
  by (rule bigtheta_trans2, subst bigtheta_sym)

lemma bigo_bigomega_trans:      "f ∈ O[F](g) ⟹ h ∈ Ω[F](g) ⟹ f ∈ O[F](h)"
  and bigo_smallomega_trans:    "f ∈ O[F](g) ⟹ h ∈ ω[F](g) ⟹ f ∈ o[F](h)"
  and smallo_bigomega_trans:    "f ∈ o[F](g) ⟹ h ∈ Ω[F](g) ⟹ f ∈ o[F](h)"
  and smallo_smallomega_trans:  "f ∈ o[F](g) ⟹ h ∈ ω[F](g) ⟹ f ∈ o[F](h)"
  and bigomega_bigo_trans:      "f ∈ Ω[F](g) ⟹ h ∈ O[F](g) ⟹ f ∈ Ω[F](h)"
  and bigomega_smallo_trans:    "f ∈ Ω[F](g) ⟹ h ∈ o[F](g) ⟹ f ∈ ω[F](h)"
  and smallomega_bigo_trans:    "f ∈ ω[F](g) ⟹ h ∈ O[F](g) ⟹ f ∈ ω[F](h)"
  and smallomega_smallo_trans:  "f ∈ ω[F](g) ⟹ h ∈ o[F](g) ⟹ f ∈ ω[F](h)"
  by (unfold bigomega_iff_bigo smallomega_iff_smallo)
     (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans
                landau_o.big_trans landau_o.small_trans)+

lemmas landau_trans_lift [trans] =
  landau_symbols[THEN landau_symbol.lift_trans]
  landau_symbols[THEN landau_symbol.lift_trans']
  landau_symbols[THEN landau_symbol.lift_trans_bigtheta]
  landau_symbols[THEN landau_symbol.lift_trans_bigtheta']

lemmas landau_mult_1_trans [trans] =
  landau_o.mult_1_trans landau_omega.mult_1_trans

lemmas landau_trans [trans] =
  landau_symbols[THEN landau_symbol.bigtheta_trans1]
  landau_symbols[THEN landau_symbol.bigtheta_trans2]
  landau_symbols[THEN landau_symbol.bigtheta_trans1']
  landau_symbols[THEN landau_symbol.bigtheta_trans2']
  landau_symbols[THEN landau_symbol.ev_eq_trans1]
  landau_symbols[THEN landau_symbol.ev_eq_trans2]

  landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans
  landau_omega.big_trans landau_omega.small_trans
    landau_omega.small_big_trans landau_omega.big_small_trans

  bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans
  bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans

lemma bigtheta_inverse [simp]:
  shows "(λx. inverse (f x)) ∈ Θ[F](λx. inverse (g x)) ⟷ f ∈ Θ[F](g)"
proof -
  have "(λx. inverse (f x)) ∈ O[F](λx. inverse (g x))"
    if A: "f ∈ Θ[F](g)"
    for f g :: "'a ⇒ 'b" and F
  proof -
    from A obtain c1 c2 :: real where *: "c1 > 0" "c2 > 0"
      and **: "∀⇩F x in F. norm (f x) ≤ c1 * norm (g x)"
              "∀⇩F x in F. c2 * norm (g x) ≤ norm (f x)"
      unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
    from ‹c2 > 0› have c2: "inverse c2 > 0" by simp
    from ** have "eventually (λx. norm (inverse (f x))